--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:31:15 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Oct 21 17:46:51 2020 +0200
@@ -268,10 +268,8 @@
insert_lemma_in_step lem step @ steps
else
step :: 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
+ and insert_lemma_in_proof lem (proof as Proof {steps, ...}) =
+ isar_proof_with_steps proof (insert_lemma_in_steps lem steps)
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 21 17:31:15 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Oct 21 17:46:51 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 {fixes, assumptions, steps}) (proofs, updates) =
+ | update_proof (proof as Proof {steps, ...}) (proofs, updates) =
let val (steps', updates') = update_steps steps updates in
- (Proof {fixes = fixes, assumptions = assumptions, steps = steps'} :: proofs, updates')
+ (isar_proof_with_steps proof steps' :: proofs, updates')
end
in
fst (update_steps steps (rev updates))
@@ -273,9 +273,9 @@
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 {fixes, assumptions, steps})) =
+ fun compress_proof (proof as (Proof {steps, ...})) =
if compress_further () then
- Proof {fixes = fixes, assumptions = assumptions, steps = compress_steps steps}
+ isar_proof_with_steps proof (compress_steps steps)
else
proof
and compress_steps steps =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Wed Oct 21 17:31:15 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Wed Oct 21 17:46:51 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 {fixes, assumptions, steps}) =
+fun postprocess_isar_proof_remove_show_stuttering (proof as Proof {steps, ...}) =
let
fun process_steps [] = []
| process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1),
@@ -83,14 +83,13 @@
else steps
| process_steps (step :: steps) = step :: process_steps steps
in
- Proof {fixes = fixes, assumptions = assumptions, steps = process_steps steps}
+ isar_proof_with_steps proof (process_steps steps)
end
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
let
- fun process_proof (Proof {fixes, assumptions, steps}) =
- process_steps steps
- ||> (fn steps' => Proof {fixes = fixes, assumptions = assumptions, steps = steps'})
+ fun process_proof (proof as Proof {steps, ...}) =
+ process_steps steps ||> isar_proof_with_steps proof
and process_steps [] = ([], [])
| process_steps steps =
(* the last step is always implicitly referenced *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Oct 21 17:31:15 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Oct 21 17:46:51 2020 +0200
@@ -33,6 +33,7 @@
val sort_facts : facts -> facts
val steps_of_isar_proof : isar_proof -> isar_step list
+ val isar_proof_with_steps : isar_proof -> isar_step list -> isar_proof
val label_of_isar_step : isar_step -> label option
val facts_of_isar_step : isar_step -> facts
val proof_methods_of_isar_step : isar_step -> proof_method list
@@ -103,6 +104,8 @@
fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs)
fun steps_of_isar_proof (Proof {steps, ...}) = steps
+fun isar_proof_with_steps (Proof {fixes, assumptions, ...}) steps =
+ Proof {fixes = fixes, assumptions = assumptions, steps = steps}
fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
| label_of_isar_step _ = NONE
@@ -122,8 +125,7 @@
fun map_isar_steps f =
let
- fun map_proof (Proof {fixes, assumptions, steps}) =
- Proof {fixes = fixes, assumptions = assumptions, steps = map map_step steps}
+ fun map_proof (proof as Proof {steps, ...}) = isar_proof_with_steps proof (map map_step steps)
and map_step (step as Let _) = f step
| map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
@@ -155,10 +157,8 @@
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 {fixes, assumptions, steps}) =
- let val steps' = chain_isar_steps (try (List.last #> fst) assumptions) steps in
- Proof {fixes = fixes, assumptions = assumptions, steps = steps'}
- end
+and chain_isar_proof (proof as Proof {assumptions, steps, ...}) =
+ isar_proof_with_steps proof (chain_isar_steps (try (List.last #> fst) assumptions) steps)
fun kill_useless_labels_in_isar_proof proof =
let