Quelle Sketch_and_Explore.thy

Sprache: Isabelle

(*   Title:   HOL/ex/Sketch_and_Explore.thy
     Author:  Florian Haftmann, TU Muenchen
*)

chapter ‹Experimental commands 🪙‹sketch› and 🪙‹explore››

theory Sketch_and_Explore
  imports Main ― ‹TODO: generalize existing sledgehammer functions to Pure›
  keywords "sketch" "explore" "sketch_subgoals" :: diag
begin

ML ‹
split_clause t =
let
val (fixes, horn) = funpow_yield (length (Term.strip_all_vars t)) Logic.dest_all_global t;
val assms = Logic.strip_imp_prems horn;
val concl = Logic.strip_imp_concl horn;
in (fixes, assms, concl) end;

print_typ ctxt T =
T
|> Syntax.string_of_typ ctxt
|> ATP_Util.maybe_quote ctxt;

print_term ctxt t =
t
|> singleton (Syntax.uncheck_terms ctxt)
|> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
|> Syntax.unparse_term ctxt
|> Pretty.pure_string_of
|> Sledgehammer_Util.simplify_spaces
|> ATP_Util.maybe_quote ctxt;

eigen_context_for_statement (params, assms, concl) ctxt =
let
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
val ctxt' = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
handle ERROR _ =>
ctxt |> Variable.set_body true |> Proof_Context.add_fixes fixes |> snd
in ((params, assms, concl), ctxt') end;

print_isar_skeleton ctxt indent keyword stmt =
let
val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
val prefix = Symbol.spaces indent;
val prefix_sep = "\n" ^ prefix ^ " and ";
val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
val if_s = if null assms then NONE
else SOME (prefix ^ " if " ^ space_implode prefix_sep
(map (print_term ctxt') assms));
val for_s = if null fixes then NONE
else SOME (prefix ^ " for " ^ space_implode prefix_sep
(map (fn (v, T) => v ^ " :: " ^ print_typ ctxt T) fixes));
val s = cat_lines ([show_s] @ map_filter I [if_s, for_s] @
[prefix ^ " " ^ (if is_none if_s then "" else "using that ") ^ "sorry"]);
in
s
end;

print_skeleton ctxt indent keyword stmt =
let
val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
val prefix = Symbol.spaces indent;
val prefix_sep = "\n" ^ prefix ^ " and ";
val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
val assumes_s = if null assms then NONE
else SOME (prefix ^ "assume " ^ space_implode prefix_sep
(map (print_term ctxt') assms));
val fixes_s = if null fixes then NONE
else SOME (prefix ^ "fix " ^ space_implode prefix_sep
(map (fn (v, T) => v ^ " :: " ^ print_typ ctxt T) fixes));
val s = cat_lines (map_filter I [fixes_s, assumes_s] @ [show_s] @ [prefix ^ " sorry"]);
in
s
end;

print_sketch ctxt method_text clauses =
"proof" ^ method_text :: separate "next" (map (print_skeleton ctxt 2 "show") clauses) @ ["qed"];

print_exploration ctxt method_text [clause] =
["proof -", print_isar_skeleton ctxt 2 "have" clause,
" then show ?thesis", " by" ^ method_text, "qed"]
| print_exploration ctxt method_text (clause :: clauses) =
"proof -" :: print_isar_skeleton ctxt 2 "have" clause
:: map (print_isar_skeleton ctxt 2 "moreover have") clauses
@ [" ultimately show ?thesis", " by" ^ method_text, "qed"];

print_subgoal apply_line_opt (is_prems, is_for, is_sh) ctxt indent stmt =
let
val ((fixes, _, _), ctxt') = eigen_context_for_statement stmt ctxt;
val prefix = Symbol.spaces indent;
val fixes_s =
if not is_for orelse null fixes then NONE
else SOME ("for " ^ implode_space
(map (fn (v, _) => Thy_Header.print_name' ctxt' v) fixes));
val premises_s = if is_prems then SOME "premises prems" else NONE;
val sh_s = if is_sh then SOME "sledgehammer" else NONE;
val subgoal_s = map_filter I [SOME "subgoal", premises_s, fixes_s]
|> implode_space;
val using_s = if is_prems then SOME "using prems" else NONE;
val s = cat_lines (
[subgoal_s]
@ map_filter (Option.map (fn s => prefix ^ s)) [using_s, apply_line_opt, sh_s]
@ [prefix ^ "sorry"]);
in
s
end;

coalesce_method_txt [] = ""
| coalesce_method_txt [s] = s
| coalesce_method_txt (s1 :: s2 :: ss) =
if s1 = "(" orelse s1 = "["
orelse s2 = ")" orelse s2 = "]" orelse s2= ":"
then s1 ^ coalesce_method_txt (s2 :: ss)
else s1 ^ " " ^ coalesce_method_txt (s2 :: ss);

print_subgoals options apply_line_opt ctxt _ clauses =
separate "" (map (print_subgoal apply_line_opt options ctxt 2) clauses) @ ["done"];

print_proof_text_from_state print (some_method_ref : ((Method.text * Position.range) * Token.T list) option) state =
let
val state' = state
|> Proof.proof (Option.map fst some_method_ref)
|> Seq.the_result ""

val { context = ctxt, facts = _, goal } = Proof.goal state';

val ctxt_print = fold (fn opt => Config.put opt false)
[show_markup, Printer.show_type_emphasis, show_types, show_sorts, show_consts] ctxt

val method_text = case some_method_ref of
NONE => ""
| SOME (_, toks) => " " ^ coalesce_method_txt (map Token.unparse toks);
― ‹TODO proper printing required›
val goal_props = Logic.strip_imp_prems (Thm.prop_of goal);
val clauses = map split_clause goal_props;
val lines = if null clauses then
if is_none some_method_ref then [" .."]
else [" by" ^ method_text]
else print ctxt_print method_text clauses;
in Output.information (Active.sendback_markup_command (cat_lines lines)) end;

sketch = print_proof_text_from_state print_sketch;

explore method_ref = print_proof_text_from_state print_exploration (SOME method_ref);

subgoals options method_ref =
let
val apply_line_opt = case method_ref of
NONE => NONE
| SOME (_, toks) => SOME ("apply " ^ coalesce_method_txt (map Token.unparse toks))
val succeed_method_ref = SOME ((Method.succeed_text, Position.no_range), [])
in
print_proof_text_from_state (print_subgoals options apply_line_opt) succeed_method_ref
end;

sketch_cmd some_method_text =
Toplevel.keep_proof (fn state => sketch some_method_text (Toplevel.proof_of state));

explore_cmd method_text =
Toplevel.keep_proof (fn state => explore method_text (Toplevel.proof_of state));

subgoals_cmd (modes, method_ref) =
let
val is_prems = not (member (op =) modes "noprems")
val is_for = not (member (op =) modes "nofor")
val is_sh = member (op =) modes "sh"
in
Toplevel.keep_proof (fn state =>
subgoals (is_prems, is_for, is_sh) method_ref (Toplevel.proof_of state))
end;

_ =
Outer_Syntax.command 🍋‹sketch›
"print sketch of Isar proof text after method application"
(Scan.option (Scan.trace Method.parse) >> sketch_cmd);

_ =
Outer_Syntax.command 🍋‹explore›
"explore proof obligations after method application as Isar proof text"
(Scan.trace Method.parse >> explore_cmd);

opt_modes =
Scan.optional (🍋‹(› |-- Parse.!!! (Scan.repeat1 Parse.name --| 🍋‹)›)) [];

_ =
Outer_Syntax.command 🍋‹sketch_subgoals›
"sketch proof obligations as subgoals, applying a method and/or sledgehammer to each"
(opt_modes -- Scan.option (Scan.trace Method.parse) >> subgoals_cmd);
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.