# HG changeset patch
# User desharna
# Date 1603294275 -7200
# Node ID b69a3a7655f2a0832efbd2ef0e2ee3855ec0af6f
# Parent  de581f98a3a1efa54f561b1343887b4493853356
Tuned isar_proof datatype

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