--- 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"
--- 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
--- 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 =
--- 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
--- 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