# HG changeset patch
# User desharna
# Date 1603295211 -7200
# Node ID e728d3a3d383604e64e6cb1910ba97f4ee79d581
# Parent  b69a3a7655f2a0832efbd2ef0e2ee3855ec0af6f
Tuned isar_proofs constructions

diff -r b69a3a7655f2 -r e728d3a3d383 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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
 
diff -r b69a3a7655f2 -r e728d3a3d383 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- 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 =
diff -r b69a3a7655f2 -r e728d3a3d383 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- 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 *)
diff -r b69a3a7655f2 -r e728d3a3d383 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- 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