diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML @@ -1,522 +1,522 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen Isar proof reconstruction from ATP proofs. *) signature SLEDGEHAMMER_ISAR = sig type atp_step_name = ATP_Proof.atp_step_name type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature type one_line_params = Sledgehammer_Proof_Methods.one_line_params val trace : bool Config.T type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int -> one_line_params -> string end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Compress open Sledgehammer_Isar_Minimize structure String_Redirect = ATP_Proof_Redirect( type key = atp_step_name val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') val string_of = fst) open String_Redirect val trace = Attrib.setup_config_bool \<^binding>\sledgehammer_isar_trace\ (K false) val e_definition_rule = "definition" val e_skolemize_rule = "skolemize" val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" val satallax_skolemize_rule = "tab_ex" val vampire_skolemisation_rule = "skolemisation" val veriT_la_generic_rule = "la_generic" val veriT_simp_arith_rule = "simp_arith" val veriT_skolemize_rules = Verit_Proof.skolemization_steps val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") val zipperposition_cnf_rule = "cnf" val skolemize_rules = [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, zipperposition_cnf_rule] @ veriT_skolemize_rules fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix val is_skolemize_rule = member (op =) skolemize_rules fun is_arith_rule rule = String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse rule = veriT_la_generic_rule fun raw_label_of_num num = (num, 0) fun label_of_clause [(num, _)] = raw_label_of_num num | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) fun add_global_fact ss = apsnd (union (op =) ss) fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names)) fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) if role = Conjecture orelse role = Negated_Conjecture then line :: lines else if t aconv \<^prop>\True\ then map (replace_dependencies_in_line (name, [])) lines else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines else if role = Axiom then lines (* axioms (facts) need no proof lines *) else map (replace_dependencies_in_line (name, [])) lines | add_line_pass1 line lines = line :: lines fun add_lines_pass2 res [] = rev res | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = let fun normalize role = role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) val norm_t = normalize role t val is_duplicate = exists (fn (prev_name, prev_role, prev_t, _, _) => (prev_role = Hypothesis andalso prev_t aconv t) orelse (member (op =) deps prev_name andalso Term.aconv_untyped (normalize prev_role prev_t, norm_t))) res fun looks_boring () = t aconv \<^prop>\False\ orelse length deps < 2 fun is_skolemizing_line (_, _, _, rule', deps') = is_skolemize_rule rule' andalso member (op =) deps' name fun is_before_skolemize_rule () = exists is_skolemizing_line lines in if is_duplicate orelse (role = Plain andalso not (is_skolemize_rule rule) andalso not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) else add_lines_pass2 (line :: res) lines end type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method] val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods val systematic_methods = basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods val skolem_methods = Moura_Method :: systematic_methods fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = let val _ = if debug then writeln "Constructing Isar proof..." else () fun generate_proof_text () = let val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = isar_params () in if null atp_proof0 then one_line_proof_text ctxt 0 one_line_params else let val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods fun massage_methods (meths as meth :: _) = if not try0 then [meth] else if smt_proofs then SMT_Method SMT_Default :: meths else meths val (params, _, concl_t) = strip_subgoal goal subgoal ctxt 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 val do_preplay = preplay_timeout <> Time.zeroTime val compress = (case compress of NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 | SOME n => n) fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev fun get_role keep_role ((num, _), role, t, rule, _) = if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE val trace = Config.get ctxt trace val string_of_atp_steps = let val to_string = ATP_Proof.string_of_atp_step (Syntax.string_of_term ctxt) I in enclose "[\n" "\n]" o cat_lines o map (enclose " " "," o to_string) end val atp_proof = atp_proof0 |> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps) |> (fn x => fold_rev add_line_pass1 x []) |> add_lines_pass2 [] |> trace ? tap (tracing o prefix "atp_proof = " o string_of_atp_steps) val conjs = map_filter (fn (name, role, _, _, _) => if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) atp_proof val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof fun add_lemma ((label, goal), rule) ctxt = let val (skos, proof_methods) = (if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods) else if is_arith_rule rule then ([], arith_methods) else ([], rewrite_methods)) ||> massage_methods val prove = Prove { qualifiers = [], obtains = skos, label = label, goal = goal, subproofs = [], facts = ([], []), proof_methods = proof_methods, comment = ""} in (prove, ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) end val (lems, _) = fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt val bot = #1 (List.last atp_proof) val refute_graph = atp_proof |> map (fn (name, _, _, _, from) => (from, name)) |> make_refute_graph bot |> fold (Atom_Graph.default_node o rpair ()) conjs val axioms = axioms_of_refute_graph refute_graph conjs val tainted = tainted_atoms_of_refute_graph refute_graph conjs val is_clause_tainted = exists (member (op =) tainted) val steps = Symtab.empty |> fold (fn (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then HOLogic.dest_Trueprop #> role <> Conjecture ? s_not #> fold exists_of (map Var (Term.add_vars t [])) #> HOLogic.mk_Trueprop else I)))) atp_proof fun is_referenced_in_step _ (Let _) = false | is_referenced_in_step l (Prove {subproofs, facts = (ls, _), ...}) = member (op =) ls l orelse exists (is_referenced_in_proof l) subproofs and is_referenced_in_proof l (Proof {steps, ...}) = exists (is_referenced_in_step l) steps fun insert_lemma_in_step lem (step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs), proof_methods, comment}) = let val l' = the (label_of_isar_step lem) in if member (op =) ls l' then [lem, step] else let val refs = map (is_referenced_in_proof l') subproofs in if length (filter I refs) = 1 then [Prove { qualifiers = qualifiers, obtains = obtains, label = label, goal = goal, subproofs = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subproofs, facts = (ls, gs), proof_methods = proof_methods, comment = comment}] else [lem, step] end end and insert_lemma_in_steps lem [] = [lem] | insert_lemma_in_steps lem (step :: steps) = if is_referenced_in_step (the (label_of_isar_step lem)) step then insert_lemma_in_step lem step @ steps else step :: insert_lemma_in_steps lem steps and insert_lemma_in_proof lem (proof as Proof {steps, ...}) = - isar_proof_with_steps proof (insert_lemma_in_steps lem steps) + isar_proof_with_steps proof (insert_lemma_in_steps lem steps) val rule_of_clause_id = fst o the o Symtab.lookup steps o fst val finish_off = close_form #> rename_bound_vars fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off | prop_of_clause names = let val lits = map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) in (case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) => s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) | _ => fold (curry s_disj) lits \<^term>\False\) end |> HOLogic.mk_Trueprop |> finish_off fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] fun isar_steps outer predecessor accum [] = accum |> (if tainted = [] then (* e.g., trivial, empty proof by Z3 *) cons (Prove { qualifiers = if outer then [Show] else [], obtains = [], label = no_label, goal = concl_t, subproofs = [], facts = sort_facts (the_list predecessor, []), proof_methods = massage_methods systematic_methods', comment = ""}) else I) |> rev | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = let val l = label_of_clause c val t = prop_of_clause c val rule = rule_of_clause_id id val skolem = is_skolemize_rule rule val deps = ([], []) |> fold add_fact_of_dependency gamma |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] |> sort_facts val meths = (if skolem then skolem_methods else if is_arith_rule rule then arith_methods else systematic_methods') |> massage_methods fun prove subproofs facts = Prove { qualifiers = maybe_show outer c, obtains = [], label = l, goal = t, subproofs = subproofs, facts = facts, proof_methods = meths, comment = ""} fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs in if is_clause_tainted c then (case gamma of [g] => if skolem andalso is_clause_tainted g then let val skos = skolems_of ctxt (prop_of_clause g) val subproof = Proof {fixes = skos, assumptions = [], steps = rev accum} in isar_steps outer (SOME l) [prove [subproof] ([], [])] infs end else steps_of_rest (prove [] deps) | _ => steps_of_rest (prove [] deps)) else steps_of_rest (if skolem then (case skolems_of ctxt t of [] => prove [] deps | skos => Prove { qualifiers = [], obtains = skos, label = l, goal = t, subproofs = [], facts = deps, proof_methods = meths, comment = ""}) else prove [] deps) end | isar_steps outer predecessor accum (Cases cases :: infs) = let fun isar_case (c, subinfs) = isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs val c = succedent_of_cases cases val l = label_of_clause c val t = prop_of_clause c val step = Prove { qualifiers = maybe_show outer c, obtains = [], label = l, goal = t, subproofs = map isar_case (filter_out (null o snd) cases), facts = sort_facts (the_list predecessor, []), proof_methods = massage_methods systematic_methods', comment = ""} in isar_steps outer (SOME l) (step :: accum) infs end and isar_proof outer fixes assumptions lems infs = let val steps = fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs) in Proof {fixes = fixes, assumptions = assumptions, steps = steps} end val canonical_isar_proof = refute_graph |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) |> redirect_graph axioms tainted bot |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) |> isar_proof true params assms lems |> postprocess_isar_proof_remove_show_stuttering |> postprocess_isar_proof_remove_unreferenced_steps I |> relabel_isar_proof_canonically val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty val _ = fold_isar_steps (fn meth => K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) (steps_of_isar_proof canonical_isar_proof) () fun str_of_preplay_outcome outcome = if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" fun str_of_meth l meth = string_of_proof_method [] meth ^ " " ^ str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) fun comment_of l = map (str_of_meth l) #> commas fun trace_isar_proof label proof = if trace then tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof ctxt subgoal subgoal_count (comment_isar_proof comment_of proof) ^ "\n") else () fun comment_of l (meth :: _) = (case (verbose, Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of (false, Played _) => "" | (_, outcome) => string_of_play_outcome outcome) val (play_outcome, isar_proof) = canonical_isar_proof |> tap (trace_isar_proof "Original") |> compress_isar_proof ctxt compress preplay_timeout preplay_data |> tap (trace_isar_proof "Compressed") |> postprocess_isar_proof_remove_unreferenced_steps (keep_fastest_method_of_isar_step (!preplay_data) #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") |> `(preplay_outcome_of_isar_proof (!preplay_data)) ||> (comment_isar_proof comment_of #> chain_isar_proof #> kill_useless_labels_in_isar_proof #> relabel_isar_proof_nicely #> rationalize_obtains_in_isar_proofs ctxt) in (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of (0, 1) => one_line_proof_text ctxt 0 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then (case isar_proof of Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}], ...} => let val used_facts' = map_filter (fn s => if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained) used_facts then NONE else SOME (s, (Global, General))) gfs in ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) end) else one_line_params) ^ (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") | (_, num_steps) => let val msg = (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ (if do_preplay then [string_of_play_outcome play_outcome] else []) in one_line_proof_text ctxt 0 one_line_params ^ "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ Active.sendback_markup_command (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) end) end end in if debug then generate_proof_text () else (case try generate_proof_text () of SOME s => s | NONE => one_line_proof_text ctxt 0 one_line_params ^ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) end fun isar_proof_would_be_a_good_idea (_, play) = (case play of Played _ => false | Play_Timed_Out time => time > Time.zeroTime | Play_Failed => true) fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained (one_line_params as ((_, preplay), _, _, _)) = (if isar_proofs = SOME true orelse (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params else one_line_proof_text ctxt num_chained) one_line_params end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML @@ -1,484 +1,484 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen Basic data structures for representing and basic methods for dealing with Isar proof texts. *) signature SLEDGEHAMMER_ISAR_PROOF = sig type proof_method = Sledgehammer_Proof_Methods.proof_method type label = string * int type facts = label list * string list (* local and global facts *) datatype isar_qualifier = Show | Then datatype isar_proof = Proof of { fixes : (string * typ) list, assumptions: (label * term) list, steps : isar_step list } and isar_step = Let of { lhs : term, rhs : term } | Prove of { qualifiers : isar_qualifier list, obtains : (string * typ) list, label : label, goal : term, subproofs : isar_proof list, facts : facts, proof_methods : proof_method list, comment : string } val no_label : label val label_ord : label ord val string_of_label : label -> string val sort_facts : facts -> facts val steps_of_isar_proof : isar_proof -> isar_step list val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof val label_of_isar_step : isar_step -> label option val facts_of_isar_step : isar_step -> facts val proof_methods_of_isar_step : isar_step -> proof_method list val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof val add_isar_steps : isar_step list -> int -> int structure Canonical_Label_Tab : TABLE val canonical_label_ord : label ord val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof val chain_isar_proof : isar_proof -> isar_proof val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof val relabel_isar_proof_canonically : isar_proof -> isar_proof val relabel_isar_proof_nicely : isar_proof -> isar_proof val rationalize_obtains_in_isar_proofs : Proof.context -> isar_proof -> isar_proof val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string end; structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Annotate type label = string * int type facts = label list * string list (* local and global facts *) datatype isar_qualifier = Show | Then datatype isar_proof = Proof of { fixes : (string * typ) list, assumptions: (label * term) list, steps : isar_step list } and isar_step = Let of { lhs : term, rhs : term } | Prove of { qualifiers : isar_qualifier list, obtains : (string * typ) list, label : label, goal : term, subproofs : isar_proof list, facts : facts, proof_methods : proof_method list, comment : string } val no_label = ("", ~1) (* cf. "label_ord" below *) val assume_prefix = "a" val have_prefix = "f" fun label_ord ((s1, i1), (s2, i2)) = (case int_ord (apply2 String.size (s1, s2)) of EQUAL => (case string_ord (s1, s2) of EQUAL => int_ord (i1, i2) | ord => ord (* "assume" before "have" *)) | ord => ord) fun string_of_label (s, num) = s ^ string_of_int num (* Put the nearest local label first, since it's the most likely to be replaced by a "hence". (Some preplaying proof methods, e.g. "blast", react poorly to fact reorderings.) *) fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs) fun steps_of_isar_proof (Proof {steps, ...}) = steps fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps = Proof {fixes = fixes, assumptions = assumptions, steps = steps} fun label_of_isar_step (Prove {label, ...}) = SOME label | label_of_isar_step _ = NONE fun subproofs_of_isar_step (Prove {subproofs, ...}) = subproofs | subproofs_of_isar_step _ = [] fun facts_of_isar_step (Prove {facts, ...}) = facts | facts_of_isar_step _ = ([], []) fun proof_methods_of_isar_step (Prove {proof_methods, ...}) = proof_methods | proof_methods_of_isar_step _ = [] fun fold_isar_step f step = fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step and fold_isar_steps f = fold (fold_isar_step f) fun map_isar_steps f = let fun map_proof (proof as Proof {steps, ...}) = isar_proof_with_steps proof (map map_step steps) and map_step (step as Let _) = f step | map_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, comment}) = f (Prove { qualifiers = qualifiers, obtains = obtains, label = label, goal = goal, subproofs = map map_proof subproofs, facts = facts, proof_methods = proof_methods, comment = comment}) in map_proof end val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) (* canonical proof labels: 1, 2, 3, ... in post traversal order *) fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2) structure Canonical_Label_Tab = Table( type key = label val ord = canonical_label_ord) fun comment_isar_step comment_of (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, ...}) = Prove { qualifiers = qualifiers, obtains = obtains, label = label, goal = goal, subproofs = subproofs, facts = facts, proof_methods = proof_methods, comment = comment_of label proof_methods} | comment_isar_step _ step = step fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of) fun chain_qs_lfs NONE lfs = ([], lfs) | chain_qs_lfs (SOME l0) lfs = if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs) fun chain_isar_step lbl (Prove {qualifiers, obtains, label, goal, subproofs, facts = (lfs, gfs), proof_methods, comment}) = let val (qs', lfs) = chain_qs_lfs lbl lfs in Prove { qualifiers = qs' @ qualifiers, obtains = obtains, label = label, goal = goal, subproofs = map chain_isar_proof subproofs, facts = (lfs, gfs), proof_methods = proof_methods, comment = comment} end | chain_isar_step _ step = step and chain_isar_steps _ [] = [] | chain_isar_steps prev (i :: is) = chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is and chain_isar_proof (proof as Proof {assumptions, steps, ...}) = - isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps) + isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps) fun kill_useless_labels_in_isar_proof proof = let val used_ls = fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) [] fun kill_label l = if member (op =) used_ls l then l else no_label fun kill_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, comment}) = Prove { qualifiers = qualifiers, obtains = obtains, label = kill_label label, goal = goal, subproofs = map kill_proof subproofs, facts = facts, proof_methods = proof_methods, comment = comment} | kill_step step = step and kill_proof (Proof {fixes, assumptions, steps}) = let val assumptions' = map (apfst kill_label) assumptions val steps' = map kill_step steps in Proof {fixes = fixes, assumptions = assumptions', steps = steps'} end in kill_proof proof end fun relabel_isar_proof_canonically proof = let fun next_label l (next, subst) = let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end fun relabel_step (Prove {qualifiers, obtains, label, goal, subproofs, facts = (lfs, gfs), proof_methods, comment}) (accum as (_, subst)) = let val lfs' = maps (the_list o AList.lookup (op =) subst) lfs val ((subs', l'), accum') = accum |> fold_map relabel_proof subproofs ||>> next_label label val prove = Prove { qualifiers = qualifiers, obtains = obtains, label = l', goal = goal, subproofs = subs', facts = (lfs', gfs), proof_methods = proof_methods, comment = comment} in (prove, accum') end | relabel_step step accum = (step, accum) and relabel_proof (Proof {fixes, assumptions, steps}) = fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assumptions ##>> fold_map relabel_step steps #>> (fn (assumptions', steps') => Proof {fixes = fixes, assumptions = assumptions', steps = steps'}) in fst (relabel_proof proof (0, [])) end val relabel_isar_proof_nicely = let fun next_label depth prefix l (accum as (next, subst)) = if l = no_label then (l, accum) else let val l' = (replicate_string (depth + 1) prefix, next) in (l', (next + 1, (l, l') :: subst)) end fun relabel_step depth (Prove {qualifiers, obtains, label, goal, subproofs, facts = (lfs, gfs), proof_methods, comment}) (accum as (_, subst)) = let val (l', accum' as (_, subst')) = next_label depth have_prefix label accum val prove = Prove { qualifiers = qualifiers, obtains = obtains, label = l', goal = goal, subproofs = map (relabel_proof subst' (depth + 1)) subproofs, facts = (maps (the_list o AList.lookup (op =) subst) lfs, gfs), proof_methods = proof_methods, comment = comment} in (prove, accum') end | relabel_step _ step accum = (step, accum) and relabel_proof subst depth (Proof {fixes, assumptions, steps}) = (1, subst) |> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assumptions ||>> fold_map (relabel_step depth) steps |> (fn ((assumptions', steps'), _) => Proof {fixes = fixes, assumptions = assumptions', steps = steps'}) in relabel_proof [] 0 end fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s fun rationalize_obtains_in_isar_proofs ctxt = let fun rename_obtains xs (subst, ctxt) = let val Ts = map snd xs val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt val ys = map2 pair new_names Ts in (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt')) end fun rationalize_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods, comment}) subst_ctxt = let val (obtains', subst_ctxt' as (subst', _)) = rename_obtains obtains subst_ctxt val prove = Prove { qualifiers = qualifiers, obtains = obtains', label = label, goal = subst_atomic subst' goal, subproofs = map (rationalize_proof false subst_ctxt') subproofs, facts = facts, proof_methods = proof_methods, comment = comment} in (prove, subst_ctxt') end and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof {fixes, assumptions, steps}) = let val (fixes', subst_ctxt' as (subst', _)) = if outer then (* last call: eliminate any remaining skolem names (from SMT proofs) *) (fixes, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fixes, ctxt)) else rename_obtains fixes subst_ctxt val assumptions' = map (apsnd (subst_atomic subst')) assumptions val steps' = fst (fold_map rationalize_step steps subst_ctxt') in Proof { fixes = fixes', assumptions = assumptions', steps = steps'} end in rationalize_proof true ([], ctxt) end val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT) fun is_thesis ctxt t = (case Vartab.lookup (Variable.binds_of ctxt) (fst thesis_var) of SOME (_, t') => HOLogic.mk_Trueprop t' aconv t | NONE => false) val indent_size = 2 fun string_of_isar_proof ctxt0 i n proof = let val keywords = Thy_Header.get_keywords' ctxt0 (* Make sure only type constraints inserted by the type annotation code are printed. *) val ctxt = ctxt0 |> Config.put show_markup false |> Config.put Printer.show_type_emphasis false |> Config.put show_types false |> Config.put show_sorts false |> Config.put show_consts false fun add_str s' = apfst (suffix s') fun of_indent ind = replicate_string (ind * indent_size) " " fun of_moreover ind = of_indent ind ^ "moreover\n" fun of_label l = if l = no_label then "" else string_of_label l ^ ": " fun of_obtain qs nr = (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " else if nr = 1 orelse member (op =) qs Then then "then " else "") ^ "obtain" fun of_show_have qs = if member (op =) qs Show then "show" else "have" fun of_thus_hence qs = if member (op =) qs Show then "then show" else "then have" fun of_have qs nr = if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs else of_show_have qs fun add_term term (s, ctxt) = (s ^ (term |> singleton (Syntax.uncheck_terms ctxt) |> annotate_types_in_term ctxt |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |> simplify_spaces |> maybe_quote keywords), ctxt |> perhaps (try (Proof_Context.augment term))) fun using_facts [] [] = "" | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss)) (* Local facts are always passed via "using", which affects "meson" and "metis". This is arguably stylistically superior, because it emphasises the structure of the proof. It is also more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "then" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) fun of_method ls ss meth = let val direct = is_proof_method_direct meth in using_facts ls (if direct then [] else ss) ^ "by " ^ string_of_proof_method (if direct then ss else []) meth end fun of_free (s, T) = maybe_quote keywords s ^ " :: " ^ maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T)) fun add_frees xs (s, ctxt) = (s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs)) fun add_fix _ [] = I | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n" fun add_assm ind (l, t) = add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n" fun of_subproof ind ctxt proof = let val ind = ind + 1 val s = of_proof ind ctxt proof val prefix = "{ " val suffix = " }" in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^ suffix ^ "\n" end and of_subproofs _ _ _ [] = "" | of_subproofs ind ctxt qs subs = (if member (op =) qs Then then of_moreover ind else "") ^ space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs) and add_step_pre ind qs subs (s, ctxt) = (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt) and add_step ind (Let {lhs = t1, rhs = t2}) = add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n" | add_step ind (Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, ss), proof_methods = meth :: _, comment}) = let val num_subproofs = length subproofs in add_step_pre ind qualifiers subproofs #> (case obtains of [] => add_str (of_have qualifiers num_subproofs ^ " ") | _ => add_str (of_obtain qualifiers num_subproofs ^ " ") #> add_frees obtains #> add_str (" where\n" ^ of_indent (ind + 1))) #> add_str (of_label label) #> add_term (if is_thesis ctxt goal then HOLogic.mk_Trueprop (Var thesis_var) else goal) #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^ (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n") end and add_steps ind = fold (add_step ind) and of_proof ind ctxt (Proof {fixes, assumptions, steps}) = ("", ctxt) |> add_fix ind fixes |> fold (add_assm ind) assumptions |> add_steps ind steps |> fst in (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ of_indent 0 ^ (if n = 1 then "qed" else "next") end end;