--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Nov 12 09:06:44 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:31:15 2020 +0200
@@ -241,7 +241,7 @@
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
@@ -268,8 +268,10 @@
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
@@ -327,7 +329,7 @@
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
@@ -358,9 +360,10 @@
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
@@ -423,7 +426,7 @@
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 =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Nov 12 09:06:44 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 21 17:31:15 2020 +0200
@@ -64,9 +64,9 @@
| 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))
@@ -160,11 +160,12 @@
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)
@@ -272,8 +273,11 @@
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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu Nov 12 09:06:44 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Wed Oct 21 17:31:15 2020 +0200
@@ -74,7 +74,7 @@
| _ => 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),
@@ -83,13 +83,14 @@
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 *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Nov 12 09:06:44 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Wed Oct 21 17:31:15 2020 +0200
@@ -77,8 +77,8 @@
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
@@ -109,7 +109,7 @@
|> 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
@@ -120,9 +120,9 @@
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
@@ -244,7 +244,7 @@
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)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Nov 12 09:06:44 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Oct 21 17:31:15 2020 +0200
@@ -16,7 +16,11 @@
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
@@ -68,7 +72,11 @@
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
@@ -94,7 +102,7 @@
(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
@@ -114,7 +122,8 @@
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))
@@ -146,8 +155,10 @@
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
@@ -159,8 +170,13 @@
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
@@ -181,10 +197,11 @@
(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
@@ -209,11 +226,12 @@
(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
@@ -240,17 +258,18 @@
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)
@@ -364,10 +383,10 @@
#> 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