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,480 +1,483 @@ (* 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 ((l, t), rule) ctxt = let val (skos, meths) = (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) else if is_arith_rule rule then ([], arith_methods) else ([], rewrite_methods)) ||> massage_methods in (Prove ([], skos, l, t, [], ([], []), meths, ""), 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 (_, _, _, _, subs, (ls, _), _, _)) = member (op =) ls l orelse exists (is_referenced_in_proof l) subs - and is_referenced_in_proof l (Proof (_, _, steps)) = + and is_referenced_in_proof l (Proof {steps, ...}) = exists (is_referenced_in_step l) steps fun insert_lemma_in_step lem (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, 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') subs in if length (filter I refs) = 1 then let val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs in [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)] end 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 (fix, assms, steps)) = - Proof (fix, assms, insert_lemma_in_steps lem steps) + and insert_lemma_in_proof lem (Proof {fixes, assumptions, steps}) = + let val steps' = insert_lemma_in_steps lem steps in + Proof {fixes = fixes, assumptions = assumptions, steps = steps'} + end 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 (if outer then [Show] else [], [], no_label, concl_t, [], sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) 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 sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") 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 (skos, [], rev accum) + 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 ([], skos, l, t, [], deps, meths, "")) 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 (maybe_show outer c, [], l, t, map isar_case (filter_out (null o snd) cases), sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") in isar_steps outer (SOME l) (step :: accum) infs end - and isar_proof outer fix assms lems infs = - Proof (fix, assms, - fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs)) + 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 (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => + Proof {steps = [Prove (_, _, _, _, _, (_, gfs), 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_compress.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML @@ -1,292 +1,296 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Author: Steffen Juilf Smolka, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Compression of Isar proofs by merging steps. Only proof steps using the same proof method are merged. *) signature SLEDGEHAMMER_ISAR_COMPRESS = sig type isar_proof = Sledgehammer_Isar_Proof.isar_proof type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data val compress_isar_proof : Proof.context -> real -> Time.time -> isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof end; structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS = struct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay fun collect_successors steps lbls = let fun collect_steps _ (accum as ([], _)) = accum | collect_steps [] accum = accum | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum) and collect_step (step as Prove (_, _, l, _, subproofs, _, _, _)) x = (case collect_subproofs subproofs x of (accum as ([], _)) => accum | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum) | collect_step _ accum = accum and collect_subproofs [] accum = accum | collect_subproofs (proof :: subproofs) accum = (case collect_steps (steps_of_isar_proof proof) accum of accum as ([], _) => accum | accum => collect_subproofs subproofs accum) in rev (snd (collect_steps steps (lbls, []))) end fun update_steps updates steps = let fun update_steps [] updates = ([], updates) | update_steps steps [] = (steps, []) | update_steps (step :: steps) updates = update_step step (update_steps steps updates) and update_step step (steps, []) = (step :: steps, []) | update_step (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) (steps, updates as Prove (qs', xs', l', t', subproofs', facts', meths', comment') :: updates') = (if l = l' then update_subproofs subproofs' updates' |>> (fn subproofs'' => Prove (qs', xs', l', t', subproofs'', facts', meths', comment')) else update_subproofs subproofs updates |>> (fn subproofs' => Prove (qs, xs, l, t, subproofs', facts, meths, comment))) |>> (fn step => step :: steps) | update_step step (steps, updates) = (step :: steps, updates) and update_subproofs [] updates = ([], updates) | update_subproofs steps [] = (steps, []) | update_subproofs (proof :: subproofs) updates = update_proof proof (update_subproofs subproofs updates) and update_proof proof (proofs, []) = (proof :: proofs, []) - | update_proof (Proof (xs, assms, steps)) (proofs, updates) = + | update_proof (Proof {fixes, assumptions, steps}) (proofs, updates) = let val (steps', updates') = update_steps steps updates in - (Proof (xs, assms, steps') :: proofs, updates') + (Proof {fixes = fixes, assumptions = assumptions, steps = steps'} :: proofs, updates') end in fst (update_steps steps (rev updates)) end fun merge_methods preplay_data (l1, meths1) (l2, meths2) = let fun is_hopeful l meth = let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in not (Lazy.is_finished outcome) orelse (case Lazy.force outcome of Played _ => true | Play_Timed_Out _ => true | _ => false) end val (hopeful, hopeless) = meths2 @ subtract (op =) meths2 meths1 |> List.partition (is_hopeful l1 andf is_hopeful l2) in (hopeful @ hopeless, hopeless) end fun merge_steps preplay_data (Prove ([], xs1, l1, _, subproofs1, (lfs1, gfs1), meths1, comment1)) (Prove (qs2, xs2, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) = let val (meths, hopeless) = merge_methods preplay_data (l1, meths1) (l2, meths2) val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) val gfs = union (op =) gfs1 gfs2 in (Prove (qs2, inter (op =) (Term.add_frees t []) (xs1 @ xs2), l2, t, subproofs1 @ subproofs2, sort_facts (lfs, gfs), meths, comment1 ^ comment2), hopeless) end val merge_slack_time = seconds 0.01 val merge_slack_factor = 1.5 fun adjust_merge_timeout max time = let val timeout = time_mult merge_slack_factor (merge_slack_time + time) in if max < timeout then max else timeout end val compress_degree = 2 (* Precondition: The proof must be labeled canonically. *) fun compress_isar_proof ctxt compress preplay_timeout preplay_data proof = if compress <= 1.0 then proof else let val (compress_further, decrement_step_count) = let val number_of_steps = add_isar_steps (steps_of_isar_proof proof) 0 val target_number_of_steps = Real.ceil (Real.fromInt number_of_steps / compress) val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps) in (fn () => !delta > 0, fn () => delta := !delta - 1) end val (get_successors, replace_successor) = let fun add_refs (Prove (_, _, l, _, _, (lfs, _), _, _)) = fold (fn key => Canonical_Label_Tab.cons_list (key, l)) lfs | add_refs _ = I val tab = Canonical_Label_Tab.empty |> fold_isar_steps add_refs (steps_of_isar_proof proof) (* "rev" should have the same effect as "sort canonical_label_ord" *) |> Canonical_Label_Tab.map (K rev) |> Unsynchronized.ref fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab) fun replace_successor old new dest = get_successors dest |> Ord_List.remove canonical_label_ord old |> Ord_List.union canonical_label_ord new |> set_successors dest in (get_successors, replace_successor) end fun reference_time l = (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of Played time => time | _ => preplay_timeout) (* elimination of trivial, one-step subproofs *) fun elim_one_subproof time (step as Prove (qs, xs, l, t, _, (lfs, gfs), meths, comment)) subs nontriv_subs = if null subs orelse not (compress_further ()) then Prove (qs, xs, l, t, List.revAppend (nontriv_subs, subs), (lfs, gfs), meths, comment) else (case subs of - (sub as Proof (_, assms, [Prove (_, _, l', _, [], (lfs', gfs'), meths', _)])) :: subs => + (sub as Proof {assumptions, + steps = [Prove (_, _, l', _, [], (lfs', gfs'), meths', _)], ...}) :: subs => let (* merge steps *) val subs'' = subs @ nontriv_subs - val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs') + val lfs'' = union (op =) lfs (subtract (op =) (map fst assumptions) lfs') val gfs'' = union (op =) gfs' gfs val (meths'' as _ :: _, hopeless) = merge_methods (!preplay_data) (l', meths') (l, meths) val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment) (* check if the modified step can be preplayed fast enough *) val timeout = adjust_merge_timeout preplay_timeout (time + reference_time l') in (case preplay_isar_step ctxt [] timeout hopeless step'' of meths_outcomes as (_, Played time'') :: _ => (* "l'" successfully eliminated *) (decrement_step_count (); set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes; map (replace_successor l' [l]) lfs'; elim_one_subproof time'' step'' subs nontriv_subs) | _ => elim_one_subproof time step subs (sub :: nontriv_subs)) end | sub :: subs => elim_one_subproof time step subs (sub :: nontriv_subs)) fun elim_subproofs (step as Prove (_, _, l, _, subproofs, _, _, _)) = if exists (null o tl o steps_of_isar_proof) subproofs then elim_one_subproof (reference_time l) step subproofs [] else step | elim_subproofs step = step fun compress_top_level steps = let val cand_key = apfst (length o get_successors) val cand_ord = prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key fun pop_next_candidate [] = (NONE, []) | pop_next_candidate (cands as (cand :: cands')) = fold (fn x => fn y => if is_less (cand_ord (x, y)) then x else y) cands' cand |> (fn best => (SOME best, remove (op =) best cands)) fun try_eliminate i l labels steps = let val (steps_before, (cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps_after) = chop i steps val succs = collect_successors steps_after labels val (succs', hopelesses) = split_list (map (merge_steps (!preplay_data) cand) succs) in (case try (map ((fn Played time => time) o forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of NONE => steps | SOME times0 => let val n = length labels val total_time = Library.foldl (op +) (reference_time l, times0) val timeout = adjust_merge_timeout preplay_timeout (Time.fromReal (Time.toReal total_time / Real.fromInt n)) val meths_outcomess = @{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs' in (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of NONE => steps | SOME times => (* "l" successfully eliminated *) (decrement_step_count (); @{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times succs' meths_outcomess; map (replace_successor l labels) lfs; steps_before @ update_steps succs' steps_after)) end) end fun compression_loop candidates steps = if not (compress_further ()) then steps else (case pop_next_candidate candidates of (NONE, _) => steps (* no more candidates for elimination *) | (SOME (l, (num_xs, _)), candidates') => (case find_index (curry (op =) (SOME l) o label_of_isar_step) steps of ~1 => steps | i => let val successors = get_successors l val num_successors = length successors in (* Careful with "obtain", so we don't "obtain" twice the same variable after a merge. *) if num_successors > (if num_xs > 0 then 1 else compress_degree) then steps else steps |> not (null successors) ? try_eliminate i l successors |> compression_loop candidates' end)) fun add_cand (Prove (_, xs, l, t, _, _, _, _)) = cons (l, (length xs, size_of_term t)) | add_cand _ = I (* the very last step is not a candidate *) val candidates = fold add_cand (fst (split_last steps)) [] in compression_loop candidates steps end (* Proofs are compressed bottom-up, beginning with the innermost subproofs. On the innermost proof level, the proof steps have no subproofs. In the best case, these steps can be merged into just one step, resulting in a trivial subproof. Going one level up, trivial subproofs can be eliminated. In the best case, this once again leads to a proof whose proof steps do not have subproofs. Applying this approach recursively will result in a flat proof in the best cast. *) - fun compress_proof (proof as (Proof (xs, assms, steps))) = - if compress_further () then Proof (xs, assms, compress_steps steps) else proof + fun compress_proof (proof as (Proof {fixes, assumptions, steps})) = + if compress_further () then + Proof {fixes = fixes, assumptions = assumptions, steps = compress_steps steps} + else + proof and compress_steps steps = (* bottom-up: compress innermost proofs first *) steps |> map (fn step => step |> compress_further () ? compress_sub_levels) |> compress_further () ? compress_top_level and compress_sub_levels (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = (* compress subproofs *) Prove (qs, xs, l, t, map compress_proof subproofs, facts, meths, comment) (* eliminate trivial subproofs *) |> compress_further () ? elim_subproofs | compress_sub_levels step = step in compress_proof proof end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML @@ -1,122 +1,123 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Author: Steffen Juilf Smolka, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Minimize dependencies (used facts) of Isar proof steps. *) signature SLEDGEHAMMER_ISAR_MINIMIZE = sig type isar_step = Sledgehammer_Isar_Proof.isar_step type isar_proof = Sledgehammer_Isar_Proof.isar_proof type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step val minimized_isar_step : Proof.context -> thm list -> Time.time -> isar_step -> Time.time * isar_step val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step val postprocess_isar_proof_remove_show_stuttering : isar_proof -> isar_proof val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof end; structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE = struct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, meths, comment)) = Prove (qs, xs, l, t, subproofs, facts, meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @, comment) | keep_fastest_method_of_isar_step _ step = step val slack = seconds 0.025 fun minimized_isar_step ctxt chained time (Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) = let fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment) fun minimize_half _ min_facts [] time = (min_facts, time) | minimize_half mk_step min_facts (fact :: facts) time = (case preplay_isar_step_for_method ctxt chained (time + slack) meth (mk_step (min_facts @ facts)) of Played time' => minimize_half mk_step min_facts facts time' | _ => minimize_half mk_step (fact :: min_facts) facts time) val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time val (min_gfs, time'') = minimize_half (mk_step_lfs_gfs min_lfs) [] gfs0 time' in (time'', mk_step_lfs_gfs min_lfs min_gfs) end fun minimize_isar_step_dependencies ctxt preplay_data (step as Prove (_, _, l, _, _, _, meth :: meths, _)) = (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of Played time => let fun old_data_for_method meth' = (meth', peek_at_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth')) val (time', step') = minimized_isar_step ctxt [] time step in set_preplay_outcomes_of_isar_step ctxt time' preplay_data step' ((meth, Played time') :: (if step' = step then map old_data_for_method meths else [])); step' end | _ => step (* don't touch steps that time out or fail *)) | minimize_isar_step_dependencies _ _ step = step -fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) = +fun postprocess_isar_proof_remove_show_stuttering (Proof {fixes, assumptions, steps}) = let fun process_steps [] = [] | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1), Prove ([Show], [], l2, t2, _, _, _, comment2)]) = if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] else steps | process_steps (step :: steps) = step :: process_steps steps in - Proof (fix, assms, process_steps steps) + Proof {fixes = fixes, assumptions = assumptions, steps = process_steps steps} end fun postprocess_isar_proof_remove_unreferenced_steps postproc_step = let - fun process_proof (Proof (fix, assms, steps)) = - process_steps steps ||> (fn steps => Proof (fix, assms, steps)) + fun process_proof (Proof {fixes, assumptions, steps}) = + process_steps steps + ||> (fn steps' => Proof {fixes = fixes, assumptions = assumptions, steps = steps'}) and process_steps [] = ([], []) | process_steps steps = (* the last step is always implicitly referenced *) let val (steps, (used, concl)) = split_last steps ||> process_used_step in fold_rev process_step steps (used, [concl]) end and process_step step (used, accu) = (case label_of_isar_step step of NONE => (used, step :: accu) | SOME l => if Ord_List.member label_ord used l then process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu) else (used, accu)) and process_used_step step = process_used_step_subproofs (postproc_step step) and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) = let val (used, subproofs) = map process_proof subproofs |> split_list |>> Ord_List.unions label_ord |>> fold (Ord_List.insert label_ord) lfs in (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)) end in snd o process_proof end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML @@ -1,251 +1,251 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Author: Steffen Juilf Smolka, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Preplaying of Isar proofs. *) signature SLEDGEHAMMER_ISAR_PREPLAY = sig type play_outcome = Sledgehammer_Proof_Methods.play_outcome type proof_method = Sledgehammer_Proof_Methods.proof_method type isar_step = Sledgehammer_Isar_Proof.isar_step type isar_proof = Sledgehammer_Isar_Proof.isar_proof type label = Sledgehammer_Isar_Proof.label val trace : bool Config.T type isar_preplay_data val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context val preplay_isar_step_for_method : Proof.context -> thm list -> Time.time -> proof_method -> isar_step -> play_outcome val preplay_isar_step : Proof.context -> thm list -> Time.time -> proof_method list -> isar_step -> (proof_method * play_outcome) list val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time -> isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method -> play_outcome Lazy.lazy val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome end; structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY = struct open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof val trace = Attrib.setup_config_bool \<^binding>\sledgehammer_preplay_trace\ (K false) fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime fun par_list_map_filter_with_timeout _ _ _ _ [] = [] | par_list_map_filter_with_timeout get_time min_timeout timeout0 f xs = let val next_timeout = Unsynchronized.ref timeout0 fun apply_f x = let val timeout = !next_timeout in if timeout <= min_timeout then NONE else let val y = f timeout x in (case get_time y of SOME time => next_timeout := time_min (time, !next_timeout) | _ => ()); SOME y end end in chop_groups (Multithreading.max_threads ()) xs |> map (map_filter I o Par_List.map apply_f) |> flat end fun enrich_context_with_local_facts proof ctxt = let val thy = Proof_Context.theory_of ctxt fun enrich_with_fact l t = Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t]) val enrich_with_assms = fold (uncurry enrich_with_fact) - fun enrich_with_proof (Proof (_, assms, isar_steps)) = - enrich_with_assms assms #> fold enrich_with_step isar_steps + fun enrich_with_proof (Proof {assumptions, steps = isar_steps, ...}) = + enrich_with_assms assumptions #> fold enrich_with_step isar_steps and enrich_with_step (Prove (_, _, l, t, subproofs, _, _, _)) = enrich_with_fact l t #> fold enrich_with_proof subproofs | enrich_with_step _ = I in enrich_with_proof proof ctxt end fun preplay_trace ctxt assmsp concl outcome = let val ctxt = ctxt |> Config.put show_markup true val assms = op @ assmsp val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]") val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms) val concl = Syntax.pretty_term ctxt concl in tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) end fun take_time timeout tac arg = let val timing = Timing.start () in (Timeout.apply timeout tac arg; Played (#cpu (Timing.result timing))) handle Timeout.TIMEOUT _ => Play_Timed_Out timeout end fun resolve_fact_names ctxt names = (names |>> map string_of_label |> apply2 (maps (thms_of_name ctxt))) handle ERROR msg => error ("preplay error: " ^ msg) -fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = +fun thm_of_proof ctxt (Proof {fixes, assumptions, steps}) = let val thy = Proof_Context.theory_of ctxt val concl = (case try List.last steps of SOME (Prove (_, [], _, t, _, _, _, _)) => t | _ => raise Fail "preplay error: malformed subproof") val var_idx = maxidx_of_term concl + 1 fun var_of_free (x, T) = Var ((x, var_idx), T) - val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees + val subst = map (`var_of_free #> swap #> apfst Free) fixes in - Logic.list_implies (assms |> map snd, concl) + Logic.list_implies (assumptions |> map snd, concl) |> subst_free subst |> Skip_Proof.make_thm thy end (* may throw exceptions *) fun raw_preplay_step_for_method ctxt chained timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) = let val goal = (case xs of [] => t | _ => (* proof obligation: !!thesis. (!!x1...xn. t ==> thesis) ==> thesis (cf. "~~/src/Pure/Isar/obtain.ML") *) let val frees = map Free xs val thesis = Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT)) val thesis_prop = HOLogic.mk_Trueprop thesis (* !!x1...xn. t ==> thesis *) val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop)) in (* !!thesis. (!!x1...xn. t ==> thesis) ==> thesis *) Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) end) val assmsp = resolve_fact_names ctxt facts |>> append (map (thm_of_proof ctxt) subproofs) |>> append chained fun prove () = Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => HEADGOAL (tac_of_proof_method ctxt assmsp meth)) handle ERROR msg => error ("Preplay error: " ^ msg) val play_outcome = take_time timeout prove () in if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else (); play_outcome end fun preplay_isar_step_for_method ctxt chained timeout meth = try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed val min_preplay_timeout = seconds 0.002 fun preplay_isar_step ctxt chained timeout0 hopeless step = let fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step) fun get_time (_, Played time) = SOME time | get_time _ = NONE val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless in par_list_map_filter_with_timeout get_time min_preplay_timeout timeout0 preplay meths |> sort (play_outcome_ord o apply2 snd) end type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table fun time_of_play (Played time) = time | time_of_play (Play_Timed_Out time) = time fun add_preplay_outcomes Play_Failed _ = Play_Failed | add_preplay_outcomes _ Play_Failed = Play_Failed | add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2) | add_preplay_outcomes play1 play2 = Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2))) fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = let fun lazy_preplay meth = Lazy.lazy (fn () => preplay_isar_step_for_method ctxt [] timeout meth step) val meths_outcomes = meths_outcomes0 |> map (apsnd Lazy.value) |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths in preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes []) (!preplay_data) end | set_preplay_outcomes_of_isar_step _ _ _ _ _ = () fun get_best_method_outcome force = tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *) #> map (apsnd force) #> sort (play_outcome_ord o apply2 snd) #> hd fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l = let val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l) in if forall (not o Lazy.is_finished o snd) meths_outcomes then (case Lazy.force outcome1 of outcome as Played _ => outcome | _ => snd (get_best_method_outcome Lazy.force meths_outcomes)) else let val outcome = snd (get_best_method_outcome peek_at_outcome meths_outcomes) in if outcome = Play_Timed_Out Time.zeroTime then snd (get_best_method_outcome Lazy.force meths_outcomes) else outcome end end fun preplay_outcome_of_isar_step_for_method preplay_data l = AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l)) #> the_default (Lazy.value (Play_Timed_Out Time.zeroTime)) fun fastest_method_of_isar_step preplay_data = the o Canonical_Label_Tab.lookup preplay_data #> get_best_method_outcome Lazy.force #> fst fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths, _)) = Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths)) | forced_outcome_of_step _ _ = Played Time.zeroTime -fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) = +fun preplay_outcome_of_isar_proof preplay_data (Proof {steps, ...}) = fold_isar_steps (add_preplay_outcomes o forced_outcome_of_step preplay_data) steps (Played Time.zeroTime) 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,379 +1,398 @@ (* 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 (string * typ) list * (label * term) list * isar_step list + Proof of { + fixes : (string * typ) list, + assumptions: (label * term) list, + steps : isar_step list + } and isar_step = Let of term * term | Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * facts * proof_method list * 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 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 (string * typ) list * (label * term) list * isar_step list + Proof of { + fixes : (string * typ) list, + assumptions: (label * term) list, + steps : isar_step list + } and isar_step = Let of term * term | Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * facts * proof_method list * 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 steps_of_isar_proof (Proof {steps, ...}) = steps fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l | label_of_isar_step _ = NONE fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs | subproofs_of_isar_step _ = [] fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts | facts_of_isar_step _ = ([], []) fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths | 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 (fix, assms, steps)) = Proof (fix, assms, map map_step steps) + fun map_proof (Proof {fixes, assumptions, steps}) = + Proof {fixes = fixes, assumptions = assumptions, steps = map map_step steps} and map_step (step as Let _) = f step | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, 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 (qs, xs, l, t, subs, facts, meths, _)) = Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths) | 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 (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) = let val (qs', lfs) = chain_qs_lfs lbl lfs in Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, 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 (fix, assms, steps)) = - Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps) +and chain_isar_proof (Proof {fixes, assumptions, steps}) = + let val steps' = chain_isar_steps (try (List.last #> fst) assumptions) steps in + Proof {fixes = fixes, assumptions = assumptions, steps = steps'} + end 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 (qs, xs, l, t, subs, facts, meths, comment)) = Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment) | kill_step step = step - and kill_proof (Proof (fix, assms, steps)) = - Proof (fix, map (apfst kill_label) assms, map kill_step steps) + 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 (qs, fix, l, t, subs, (lfs, gfs), meths, 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 subs ||>> next_label l in (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum') end | relabel_step step accum = (step, accum) - and relabel_proof (Proof (fix, assms, steps)) = - fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms + 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 (assms, steps) => Proof (fix, assms, 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 (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) (accum as (_, subst)) = let val lfs' = maps (the_list o AList.lookup (op =) subst) lfs val (l', accum' as (_, subst')) = next_label depth have_prefix l accum val subs' = map (relabel_proof subst' (depth + 1)) subs in (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum') end | relabel_step _ step accum = (step, accum) - and relabel_proof subst depth (Proof (fix, assms, steps)) = + 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)) assms + |> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assumptions ||>> fold_map (relabel_step depth) steps - |> (fn ((assms, steps), _) => Proof (fix, assms, 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 (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt = let val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt val t' = subst_atomic subst' t val subs' = map (rationalize_proof false subst_ctxt') subs in (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt') end - and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof (fix, assms, steps)) = + and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof {fixes, assumptions, steps}) = let - val (fix', subst_ctxt' as (subst', _)) = + val (fixes', subst_ctxt' as (subst', _)) = if outer then (* last call: eliminate any remaining skolem names (from SMT proofs) *) - (fix, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fix, ctxt)) + (fixes, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fixes, ctxt)) else - rename_obtains fix subst_ctxt + 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 (fix', map (apsnd (subst_atomic subst')) assms, - fst (fold_map rationalize_step steps subst_ctxt')) + 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 (t1, t2)) = add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n" | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) = add_step_pre ind qs subs #> (case xs of [] => add_str (of_have qs (length subs) ^ " ") | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str (" where\n" ^ of_indent (ind + 1))) #> add_str (of_label l) #> add_term (if is_thesis ctxt t then HOLogic.mk_Trueprop (Var thesis_var) else t) #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^ (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n") and add_steps ind = fold (add_step ind) - and of_proof ind ctxt (Proof (xs, assms, steps)) = + and of_proof ind ctxt (Proof {fixes, assumptions, steps}) = ("", ctxt) - |> add_fix ind xs - |> fold (add_assm ind) assms + |> 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;