# HG changeset patch # User smolkas # Date 1361186162 -3600 # Node ID 06689dbfe072e47741c6b9a2e7cf7725b81c4f38 # Parent e8c9755fd14e32dc48c230316a997abdd3e55ded simplified byline, isar_qualifier diff -r e8c9755fd14e -r 06689dbfe072 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Feb 18 11:33:43 2013 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Feb 18 12:16:02 2013 +0100 @@ -11,6 +11,7 @@ keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl begin + ML_file "Tools/Sledgehammer/async_manager.ML" ML_file "Tools/Sledgehammer/sledgehammer_util.ML" ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" diff -r e8c9755fd14e -r 06689dbfe072 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Feb 18 11:33:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Feb 18 12:16:02 2013 +0100 @@ -34,7 +34,6 @@ fun get i v = Vector.sub (v, i) fun replace x i v = Vector.update (v, i, x) fun update f i v = replace (get i v |> f) i v -fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList fun v_fold_index f v s = Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd @@ -69,7 +68,7 @@ val metis_fail = fn () => !metis_fail end - (* compress proof on top level - do not compress case splits *) + (* compress proof on top level - do not compress subproofs *) fun compress_top_level on_top_level ctxt proof = let (* proof vector *) @@ -87,13 +86,13 @@ val lookup_indices = map_filter (Label_Table.lookup label_index_table) (* proof references *) - fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs - | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs - | refs (Prove (_, _, _, Case_Split cases)) = maps (maps refs) cases - | refs (Prove (_, _, _, Subblock proof)) = maps refs proof + fun refs (Obtain (_, _, _, _, By_Metis (subproofs, (lfs, _)))) = + maps (maps refs) subproofs @ lookup_indices lfs + | refs (Prove (_, _, _, By_Metis (subproofs, (lfs, _)))) = + maps (maps refs) subproofs @ lookup_indices lfs | refs _ = [] val refed_by_vect = - Vector.tabulate (n, (fn _ => [])) + Vector.tabulate (n, K []) |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof |> Vector.map rev (* after rev, indices are sorted in ascending order *) @@ -113,11 +112,10 @@ (* cache metis preplay times in lazy time vector *) val metis_time = - v_map_index + Vector.map (if not preplay then K (zero_preplay_time) #> Lazy.value else - apsnd the (* step *) - #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *) + the #> try_metis debug type_enc lam_trans ctxt preplay_timeout #> handle_metis_fail #> Lazy.lazy) @@ -129,18 +127,20 @@ zero_preplay_time lazy_time_vector (* Merging *) - fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 = + fun merge (Prove (_, label1, _, By_Metis (subproofs1, (lfs1, gfs1)))) + step2 = let - val (step_constructor, lfs2, gfs2) = + val (step_constructor, (subproofs2, (lfs2, gfs2))) = (case step2 of - (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) => - (fn by => Prove (qs2, label2, t, by), lfs2, gfs2) - | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) => - (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2) + Prove (qs2, label2, t, By_Metis x) => + (fn by => Prove (qs2, label2, t, by), x) + | Obtain (qs2, xs, label2, t, By_Metis x) => + (fn by => Obtain (qs2, xs, label2, t, by), x) | _ => error "sledgehammer_compress: unmergeable Isar steps" ) val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 val gfs = union (op =) gfs1 gfs2 - in step_constructor (By_Metis (lfs, gfs)) end + val subproofs = subproofs1 @ subproofs2 + in step_constructor (By_Metis (subproofs, (lfs, gfs))) end | merge _ _ = error "sledgehammer_compress: unmergeable Isar steps" fun try_merge metis_time (s1, i) (s2, j) = @@ -156,8 +156,8 @@ val s12 = merge s1 s2 val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) in - case try_metis_quietly debug type_enc lam_trans ctxt timeout - (NONE, s12) () of + case try_metis_quietly debug type_enc lam_trans + ctxt timeout s12 () of (true, _) => (NONE, metis_time) | exact_time => (SOME s12, metis_time @@ -218,28 +218,25 @@ | enrich_with_step _ = I val rich_ctxt = fold enrich_with_step proof ctxt - (* compress subproofs (case_splits and subblocks) and top-levl *) + (* compress subproofs and top-levl proof *) val ((proof, top_level_time), lower_level_time) = - proof |> do_subproof rich_ctxt + proof |> do_subproofs rich_ctxt |>> compress_top_level on_top_level rich_ctxt in (proof, add_preplay_time lower_level_time top_level_time) end - and do_subproof ctxt proof = + and do_subproofs ctxt proof = let - fun compress_each_and_collect_time compress candidates = - let fun f_m cand time = compress cand ||> add_preplay_time time - in fold_map f_m candidates zero_preplay_time end - val compress_subproof = + fun compress_each_and_collect_time compress subproofs = + let fun f_m proof time = compress proof ||> add_preplay_time time + in fold_map f_m subproofs zero_preplay_time end + val compress_subproofs = compress_each_and_collect_time (do_proof false ctxt) - fun compress (Prove (qs, l, t, Case_Split cases)) = - let val (cases, time) = compress_subproof cases - in (Prove (qs, l, t, Case_Split cases), time) end - | compress (Prove (qs, l, t, Subblock proof)) = - let val ([proof], time) = compress_subproof [proof] - in (Prove (qs, l, t, Subblock proof), time) end - | compress step = (step, zero_preplay_time) + fun compress (Prove (qs, l, t, By_Metis(subproofs, facts))) = + let val (subproofs, time) = compress_subproofs subproofs + in (Prove (qs, l, t, By_Metis(subproofs, facts)), time) end + | compress atomic_step = (atomic_step, zero_preplay_time) in compress_each_and_collect_time compress proof end diff -r e8c9755fd14e -r 06689dbfe072 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Feb 18 11:33:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Feb 18 12:16:02 2013 +0100 @@ -14,9 +14,9 @@ val add_preplay_time : preplay_time -> preplay_time -> preplay_time val string_of_preplay_time : preplay_time -> string val try_metis : bool -> string -> string -> Proof.context -> - Time.time -> (isar_step option * isar_step) -> unit -> preplay_time + Time.time -> isar_step -> unit -> preplay_time val try_metis_quietly : bool -> string -> string -> Proof.context -> - Time.time -> (isar_step option * isar_step) -> unit -> preplay_time + Time.time -> isar_step -> unit -> preplay_time end structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = @@ -55,13 +55,30 @@ |> op @ |> maps (thms_of_name ctxt) -exception ZEROTIME -fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) = +(* *) +fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) +fun fact_of_subproof ctxt proof = let - val (t, byline, obtain) = + val (fixed_frees, assms, concl) = split_proof proof + val var_idx = maxidx_of_term concl + 1 + fun var_of_free (x, T) = Var((x, var_idx), T) + val substitutions = + map (`var_of_free #> swap #> apfst Free) fixed_frees + val assms = assms |> map snd + in + Logic.list_implies(assms, concl) + |> subst_free substitutions + |> thm_of_term ctxt + end + +exception ZEROTIME +fun try_metis debug type_enc lam_trans ctxt timeout step = + let + val (t, subproofs, fact_names, obtain) = (case step of - Prove (_, _, t, byline) => (t, byline, false) - | Obtain (_, xs, _, t, byline) => + Prove (_, _, t, By_Metis (subproofs, fact_names)) => + (t, subproofs, fact_names, false) + | Obtain (_, xs, _, t, By_Metis (subproofs, fact_names)) => (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis (see ~~/src/Pure/Isar/obtain.ML) *) let @@ -77,39 +94,12 @@ val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop)) in - (prop, byline, true) + (prop, subproofs, fact_names, true) end | _ => raise ZEROTIME) - val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) val facts = - (case byline of - By_Metis fact_names => resolve_fact_names ctxt fact_names - | Case_Split cases => - (case the succedent of - Assume (_, t) => make_thm t - | Obtain (_, _, _, t, _) => make_thm t - | Prove (_, _, t, _) => make_thm t - | _ => error "preplay error: unexpected succedent of case split") - :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) - | _ => error "preplay error: malformed case split") - #> make_thm) cases - | Subblock proof => - let - val (steps, last_step) = split_last proof - val concl = - (case last_step of - Prove (_, _, t, _) => t - | _ => error "preplay error: unexpected conclusion of subblock") - (* TODO: assuming Fix may only occur at the beginning of a subblock, - this can be optimized *) - val fixed_frees = fold (fn Fix xs => append xs | _ => I) steps [] - val var_idx = maxidx_of_term concl + 1 - fun var_of_free (x, T) = Var((x, var_idx), T) - val substitutions = - map (`var_of_free #> swap #> apfst Free) fixed_frees - in - concl |> subst_free substitutions |> make_thm |> single - end) + map (fact_of_subproof ctxt) subproofs @ + resolve_fact_names ctxt fact_names val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |> obtain ? Config.put Metis_Tactic.new_skolem true val goal = diff -r e8c9755fd14e -r 06689dbfe072 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Feb 18 11:33:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Feb 18 12:16:02 2013 +0100 @@ -9,9 +9,11 @@ signature SLEDGEHAMMER_PROOF = sig type label = string * int + val no_label : label type facts = label list * string list + val no_facts : facts - datatype isar_qualifier = Show | Then | Ultimately + datatype isar_qualifier = Show | Then datatype isar_step = Fix of (string * typ) list | @@ -21,22 +23,26 @@ isar_qualifier list * (string * typ) list * label * term * byline | Prove of isar_qualifier list * label * term * byline and byline = - By_Metis of facts | - Case_Split of isar_step list list | - Subblock of isar_step list + By_Metis of isar_step list list * facts val string_for_label : label -> string val metis_steps_top_level : isar_step list -> int val metis_steps_total : isar_step list -> int + val term_of_assm : isar_step -> term + val term_of_prove : isar_step -> term + val split_proof : + isar_step list -> (string * typ) list * (label * term) list * term end structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = struct type label = string * int +val no_label = ("", ~1) type facts = label list * string list +val no_facts = ([],[]) -datatype isar_qualifier = Show | Then | Ultimately +datatype isar_qualifier = Show | Then datatype isar_step = Fix of (string * typ) list | @@ -45,9 +51,7 @@ Obtain of isar_qualifier list * (string * typ) list * label * term * byline | Prove of isar_qualifier list * label * term * byline and byline = - By_Metis of facts | - Case_Split of isar_step list list | - Subblock of isar_step list + By_Metis of isar_step list list * facts fun string_for_label (s, num) = s ^ string_of_int num @@ -55,12 +59,33 @@ fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) proof 0 fun metis_steps_total proof = - fold (fn Obtain _ => Integer.add 1 - | Prove (_, _, _, By_Metis _) => Integer.add 1 - | Prove (_, _, _, Case_Split cases) => - Integer.add (fold (Integer.add o metis_steps_total) cases 1) - | Prove (_, _, _, Subblock subproof) => - Integer.add (metis_steps_total subproof + 1) - | _ => I) proof 0 + let + fun add_substeps subproofs i = + Integer.add (fold Integer.add (map metis_steps_total subproofs) i) + in + fold + (fn Obtain (_, _, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1 + | Prove (_, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1 + | _ => I) + proof 0 + end + +fun term_of_assm (Assume (_, t)) = t + | term_of_assm _ = error "sledgehammer proof: unexpected constructor" +fun term_of_prove (Prove (_, _, t, _)) = t + | term_of_prove _ = error "sledgehammer proof: unexpected constructor" + +fun split_proof proof = + let + fun split_step step (fixes, assms, _) = + (case step of + Fix xs => (xs@fixes, assms, step) + | Assume a => (fixes, a::assms, step) + | _ => (fixes, assms, step)) + val (fixes, assms, concl) = + fold split_step proof ([], [], Let (Term.dummy, Term.dummy)) (* FIXME: hack *) + in + (rev fixes, rev assms, term_of_prove concl) + end end diff -r e8c9755fd14e -r 06689dbfe072 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Feb 18 11:33:43 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Feb 18 12:16:02 2013 +0100 @@ -456,23 +456,29 @@ map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) val indent_size = 2 -val no_label = ("", ~1) fun string_for_proof ctxt type_enc lam_trans i n = let + fun maybe_show qs = if member (op =) qs Show then "show" else "have" fun of_indent ind = replicate_string (ind * indent_size) " " fun of_free (s, T) = maybe_quote s ^ " :: " ^ maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T)) val of_frees = space_implode " and " o map of_free + fun maybe_moreover ind qs nr_subproofs = + if member (op =) qs Then andalso nr_subproofs > 0 + then of_indent ind ^ "moreover\n" + else "" fun of_label l = if l = no_label then "" else string_for_label l ^ ": " - fun of_have qs = - (if member (op =) qs Ultimately then "ultimately " else "") ^ - (if member (op =) qs Then then - if member (op =) qs Show then "thus" else "hence" - else - if member (op =) qs Show then "show" else "have") + fun of_have qs nr_subproofs = + if (member (op =) qs Then andalso nr_subproofs>0) orelse (nr_subproofs>1) + then "ultimately " ^ maybe_show qs + else + (if member (op =) qs Then orelse nr_subproofs>0 then + if member (op =) qs Show then "thus" else "hence" + else + maybe_show qs) fun of_obtain qs xs = (if member (op =) qs Then then "then " else "") ^ "obtain " ^ of_frees xs ^ " where" @@ -492,21 +498,19 @@ of_indent ind ^ "let " ^ of_term t1 ^ " = " ^ of_term t2 ^ "\n" | of_step ind (Assume (l, t)) = of_indent ind ^ "assume " ^ of_label l ^ of_term t ^ "\n" - | of_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = + | of_step ind (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) = (* FIXME *) + maybe_moreover ind qs (length subproofs) ^ + of_subproofs ind subproofs ^ of_indent ind ^ of_obtain qs xs ^ " " ^ of_label l ^ of_term t ^ (* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding Vampire). *) of_metis ind "using [[metis_new_skolem]] " facts ^ "\n" - | of_step ind (Prove (qs, l, t, By_Metis facts)) = - of_prove ind qs l t facts - | of_step ind (Prove (qs, l, t, Case_Split proofs)) = - implode (map (prefix (of_indent ind ^ "moreover\n") o of_block ind) - proofs) ^ - of_prove ind qs l t ([], []) - | of_step ind (Prove (qs, l, t, Subblock proof)) = - of_block ind proof ^ of_prove ind qs l t ([], []) + | of_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) = + maybe_moreover ind qs (length subproofs) ^ + of_subproofs ind subproofs ^ + of_prove ind qs (length subproofs) l t facts and of_steps prefix suffix ind steps = let val s = implode (map (of_step ind) steps) in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ @@ -515,39 +519,39 @@ suffix ^ "\n" end and of_block ind proof = of_steps "{ " " }" (ind + 1) proof - and of_prove ind qs l t facts = - of_indent ind ^ of_have qs ^ " " ^ of_label l ^ of_term t ^ + and of_subproofs ind subproofs = + subproofs + |> map (of_block ind) + |> space_implode (of_indent ind ^ "moreover\n") + and of_prove ind qs nr_subproofs l t facts = + of_indent ind ^ of_have qs nr_subproofs ^ " " ^ of_label l ^ of_term t ^ of_metis ind "" facts ^ "\n" (* One-step proofs are pointless; better use the Metis one-liner directly. *) - and of_proof [Prove (_, _, _, By_Metis _)] = "" + and of_proof [Prove (_, _, _, By_Metis ([], _))] = "" | of_proof proof = (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ of_indent 0 ^ "proof -\n" ^ of_steps "" "" 1 proof ^ of_indent 0 ^ (if n <> 1 then "next" else "qed") in of_proof end -fun used_labels_of_step (Obtain (_, _, _, _, By_Metis (ls, _))) = ls - | used_labels_of_step (Prove (_, _, _, by)) = - (case by of - By_Metis (ls, _) => ls - | Case_Split proofs => fold (union (op =) o used_labels_of) proofs [] - | Subblock proof => used_labels_of proof) - | used_labels_of_step _ = [] -and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] +fun add_labels_of_step (Obtain (_, _, _, _, By_Metis (subproofs, (ls, _)))) = + union (op =) (add_labels_of_proofs subproofs ls) + | add_labels_of_step (Prove (_, _, _, By_Metis (subproofs, (ls, _)))) = + union (op =) (add_labels_of_proofs subproofs ls) + | add_labels_of_step _ = I +and add_labels_of_proof proof = fold add_labels_of_step proof +and add_labels_of_proofs proofs = fold add_labels_of_proof proofs fun kill_useless_labels_in_proof proof = let - val used_ls = used_labels_of proof + val used_ls = add_labels_of_proof proof [] fun do_label l = if member (op =) used_ls l then l else no_label fun do_step (Assume (l, t)) = Assume (do_label l, t) - | do_step (Obtain (qs, xs, l, t, by)) = Obtain (qs, xs, do_label l, t, by) - | do_step (Prove (qs, l, t, by)) = - Prove (qs, do_label l, t, - case by of - Case_Split proofs => Case_Split (map do_proof proofs) - | Subblock proof => Subblock (do_proof proof) - | _ => by) + | do_step (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) = + Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts)) + | do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) = + Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts)) | do_step step = step and do_proof proof = map do_step proof in do_proof proof end @@ -565,12 +569,9 @@ end fun do_facts subst = apfst (maps (the_list o AList.lookup (op =) subst)) - fun do_byline subst depth nexts by = - case by of - By_Metis facts => By_Metis (do_facts subst facts) - | Case_Split proofs => - Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs) - | Subblock proof => Subblock (do_proof subst depth nexts proof) + fun do_byline subst depth nexts (By_Metis (subproofs, facts)) = + By_Metis + (map (do_proof subst (depth + 1) (1, 1)) subproofs, do_facts subst facts) and do_proof _ _ _ [] = [] | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) = if l = no_label then @@ -608,27 +609,27 @@ | label_of (Obtain (_, _, l, _, _)) = SOME l | label_of (Prove (_, l, _, _)) = SOME l | label_of _ = NONE - fun chain_step (SOME l0) - (step as Obtain (qs, xs, l, t, By_Metis (lfs, gfs))) = - if member (op =) lfs l0 then - Obtain (Then :: qs, xs, l, t, By_Metis (lfs |> remove (op =) l0, gfs)) - else - step - | chain_step (SOME l0) - (step as Prove (qs, l, t, By_Metis (lfs, gfs))) = - if member (op =) lfs l0 then - Prove (Then :: qs, l, t, By_Metis (lfs |> remove (op =) l0, gfs)) - else - step - | chain_step _ (Prove (qs, l, t, Case_Split proofs)) = - Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs)) - | chain_step _ (Prove (qs, l, t, Subblock proof)) = - Prove (qs, l, t, Subblock (chain_proof NONE proof)) + fun do_qs_lfs NONE lfs = ([], lfs) + | do_qs_lfs (SOME l0) lfs = + if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) + else ([], lfs) + fun chain_step lbl (Obtain (qs, xs, l, t, + By_Metis (subproofs, (lfs, gfs)))) = + let val (qs', lfs) = do_qs_lfs lbl lfs in + Obtain (qs' @ qs, xs, l, t, + By_Metis (chain_proofs subproofs, (lfs, gfs))) + end + | chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) = + let val (qs', lfs) = do_qs_lfs lbl lfs in + Prove (qs' @ qs, l, t, + By_Metis (chain_proofs subproofs, (lfs, gfs))) + end | chain_step _ step = step and chain_proof _ [] = [] | chain_proof (prev as SOME _) (i :: is) = chain_step prev i :: chain_proof (label_of i) is | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is + and chain_proofs proofs = map (chain_proof NONE) proofs in chain_proof NONE end type isar_params = @@ -721,16 +722,16 @@ | _ => fold (curry s_disj) lits @{term False} end |> HOLogic.mk_Trueprop |> close_form - fun isar_proof_of_direct_proof outer accum [] = + fun isar_proof_of_direct_proof outer predecessor accum [] = rev accum |> outer ? (append assms #> not (null params) ? cons (Fix params)) - | isar_proof_of_direct_proof outer accum (inf :: infs) = + | isar_proof_of_direct_proof outer predecessor accum (inf :: infs) = let fun maybe_show outer c = (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show - fun do_rest step = - isar_proof_of_direct_proof outer (step :: accum) infs + fun do_rest lbl step = + isar_proof_of_direct_proof outer lbl (step :: accum) infs val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev @@ -741,8 +742,9 @@ val l = label_of_clause c val t = prop_of_clause c val by = - By_Metis (fold (add_fact_from_dependencies fact_names) gamma - ([], [])) + By_Metis ([], + (fold (add_fact_from_dependencies fact_names) + gamma no_facts)) fun prove outer = Prove (maybe_show outer c [], l, t, by) in if is_clause_tainted c then @@ -751,33 +753,35 @@ if is_clause_skolemize_rule g andalso is_clause_tainted g then let - val proof = + val subproof = Fix (skolems_of (prop_of_clause g)) :: rev accum in - isar_proof_of_direct_proof outer - [Prove (maybe_show outer c [Then], + isar_proof_of_direct_proof outer l + [Prove (maybe_show outer c [], label_of_clause c, prop_of_clause c, - Subblock proof)] [] + By_Metis ([subproof], no_facts))] [] end else - do_rest (prove outer) - | _ => do_rest (prove outer) + do_rest l (prove outer) + | _ => do_rest l (prove outer) else if is_clause_skolemize_rule c then - do_rest (Obtain ([], skolems_of t, l, t, by)) + do_rest l (Obtain ([], skolems_of t, l, t, by)) else - do_rest (prove outer) + do_rest l (prove outer) end | Cases cases => let fun do_case (c, infs) = Assume (label_of_clause c, prop_of_clause c) :: - isar_proof_of_direct_proof false [] infs + isar_proof_of_direct_proof false no_label [] infs val c = succedent_of_cases cases + val l = label_of_clause c in - do_rest (Prove (maybe_show outer c [Ultimately], - label_of_clause c, prop_of_clause c, - Case_Split (map do_case cases))) + do_rest l + (Prove (maybe_show outer c [], + l, prop_of_clause c, + By_Metis (map do_case cases, ([predecessor], [])))) end end val cleanup_labels_in_proof = @@ -787,7 +791,7 @@ val (isar_proof, (preplay_fail, preplay_time)) = refute_graph |> redirect_graph axioms tainted bot - |> isar_proof_of_direct_proof true [] + |> isar_proof_of_direct_proof true no_label [] |> (if not preplay andalso isar_compress <= 1.0 then rpair (false, (true, seconds 0.0)) else