# HG changeset patch
# User wenzelm
# Date 1701543477 -3600
# Node ID 686b7b14d041bab75617275ac1f0c40c310ed8e4
# Parent  5109e4b2a292be871128aa34f7ec4c15d1ad6c51
clarified proof_body: cover zboxes from zproof;

diff -r 5109e4b2a292 -r 686b7b14d041 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Dec 02 19:57:57 2023 +0100
@@ -184,6 +184,7 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
+        zboxes = Proofterm.empty_zboxes,
         proof = (prf, ZDummy)};
   in Proofterm.thm_body body end;
 
diff -r 5109e4b2a292 -r 686b7b14d041 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/proofterm.ML	Sat Dec 02 19:57:57 2023 +0100
@@ -13,6 +13,7 @@
       prop: term, types: typ list option}
   type thm_body
   type thm_node
+  type zboxes = (zterm * zproof future) Inttab.table
   datatype proof =
      MinProof
    | PBound of int
@@ -28,6 +29,7 @@
   and proof_body = PBody of
     {oracles: ((string * Position.T) * term option) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
+     zboxes: zboxes,
      proof: proof * zproof}
   type proofs = proof * zproof
   type oracle = (string * Position.T) * term option
@@ -60,6 +62,8 @@
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
   val union_thms: thm Ord_List.T -> thm Ord_List.T -> thm Ord_List.T
   val unions_thms: thm Ord_List.T list -> thm Ord_List.T
+  val empty_zboxes: zboxes
+  val union_zboxes: zboxes -> zboxes -> zboxes
   val no_proof: proofs
   val no_proof_body: proofs -> proof_body
   val no_thm_names: proof -> proof
@@ -213,6 +217,8 @@
   {serial: serial, pos: Position.T list, theory_name: string, name: string,
     prop: term, types: typ list option};
 
+type zboxes = (zterm * zproof future) Inttab.table;
+
 datatype proof =
    MinProof
  | PBound of int
@@ -228,6 +234,7 @@
 and proof_body = PBody of
   {oracles: ((string * Position.T) * term option) Ord_List.T,
    thms: (serial * thm_node) Ord_List.T,
+   zboxes: zboxes,
    proof: proof * zproof}
 and thm_body =
   Thm_Body of {open_proof: proof -> proof, body: proof_body future}
@@ -252,8 +259,8 @@
 val zproof_of = snd o proofs_of;
 val join_proof = Future.join #> proof_of;
 
-fun map_proofs_of f (PBody {oracles, thms, proof}) =
-  PBody {oracles = oracles, thms = thms, proof = f proof};
+fun map_proofs_of f (PBody {oracles, thms, zboxes, proof}) =
+  PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = f proof};
 
 fun thm_header serial pos theory_name name prop types : thm_header =
   {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
@@ -335,8 +342,11 @@
 val union_thms = Ord_List.union thm_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
+val empty_zboxes: zboxes = Inttab.empty;
+val union_zboxes = curry (Inttab.merge (fn (_: (zterm * zproof future), _) => true));
+
 val no_proof = (MinProof, ZDummy);
-fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
+fun no_proof_body proof = PBody {oracles = [], thms = [], zboxes = empty_zboxes, proof = proof};
 val no_thm_body = thm_body (no_proof_body no_proof);
 
 fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
@@ -391,7 +401,7 @@
       pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
         (map Position.properties_of pos,
           (prop, (types, map_proofs_of (apfst open_proof) (Future.join body)))))]
-and proof_body consts (PBody {oracles, thms, proof = (prf, _)}) =
+and proof_body consts (PBody {oracles, thms, zboxes = _, proof = (prf, _)}) =
   triple (list (pair (pair string (properties o Position.properties_of))
       (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
 and thm consts (a, thm_node) =
@@ -459,7 +469,7 @@
     val (a, b, c) =
       triple (list (pair (pair string (Position.of_properties o properties))
         (option (term consts)))) (list (thm consts)) (proof consts) x;
-  in PBody {oracles = a, thms = b, proof = (c, ZDummy)} end
+  in PBody {oracles = a, thms = b, zboxes = empty_zboxes, proof = (c, ZDummy)} end
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
@@ -2012,14 +2022,17 @@
 fun fulfill_norm_proof thy ps body0 =
   let
     val _ = consolidate_bodies (map #2 ps @ [body0]);
-    val PBody {oracles = oracles0, thms = thms0, proof = (proof0, zproof)} = body0;
+    val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (proof0, zproof)} = body0;
     val oracles =
       unions_oracles
         (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
     val thms =
       unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
+    val zboxes = fold (fn (_, PBody {zboxes, ...}) => union_zboxes zboxes) ps zboxes0;
     val proof = rew_proof thy proof0;
-  in PBody {oracles = oracles, thms = thms, proof = (proof, zproof)} end;
+  in
+    PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = (proof, zproof)}
+  end;
 
 fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
   let
@@ -2227,12 +2240,11 @@
 
     val (ucontext, prop1) = Logic.unconstrainT shyps prop;
 
-    val PBody {oracles = oracles0, thms = thms0, proof = (prf, zprf)} = body;
+    val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf, zprf)} = body;
     val proofs = ! proofs;
     val prf' = if proof_enabled proofs then fold_rev implies_intr_proof hyps prf else MinProof;
     val zprf' = if zproof_enabled proofs then ZTerm.todo_proof zprf else ZDummy;
-
-    val body0 = Future.value (PBody {oracles = oracles0, thms = thms0, proof = (prf', zprf')});
+    val body0 = PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf', zprf')};
 
     fun new_prf () =
       let
@@ -2240,7 +2252,7 @@
         val unconstrainT =
           unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
         val postproc = map_proofs_of (apfst (unconstrainT #> named ? rew_proof thy));
-      in (i, fulfill_proof_future thy promises postproc body0) end;
+      in (i, fulfill_proof_future thy promises postproc (Future.value body0)) end;
 
     val (i, body') =
       (*somewhat non-deterministic proof boxes!*)
diff -r 5109e4b2a292 -r 686b7b14d041 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 02 19:57:57 2023 +0100
@@ -744,10 +744,11 @@
 
 (** derivations and promised proofs **)
 
-fun make_deriv promises oracles thms proof =
-  Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
+fun make_deriv promises oracles thms zboxes proof =
+  Deriv {promises = promises,
+    body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = proof}};
 
-val empty_deriv = make_deriv [] [] [] Proofterm.no_proof;
+val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes Proofterm.no_proof;
 
 
 (* inference rules *)
@@ -758,14 +759,16 @@
   error ("Illegal level of detail for proof objects: " ^ string_of_int i);
 
 fun deriv_rule2 (f, g)
-    (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = proof1}})
-    (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = proof2}}) =
+    (Deriv {promises = ps1, body = body1}) (Deriv {promises = ps2, body = body2}) =
   let
     val ps = Ord_List.union promise_ord ps1 ps2;
+
+    val PBody {oracles = oracles1, thms = thms1, zboxes = zboxes1, proof = (prf1, zprf1)} = body1;
+    val PBody {oracles = oracles2, thms = thms2, zboxes = zboxes2, proof = (prf2, zprf2)} = body2;
+
     val oracles = Proofterm.union_oracles oracles1 oracles2;
     val thms = Proofterm.union_thms thms1 thms2;
-    val (prf1, zprf1) = proof1;
-    val (prf2, zprf2) = proof2;
+    val zboxes = Proofterm.union_zboxes zboxes1 zboxes2;
     val proof =
       (case ! Proofterm.proofs of
         0 => Proofterm.no_proof
@@ -775,22 +778,22 @@
       | 5 => (MinProof, g zprf1 zprf2)
       | 6 => (f prf1 prf2, g zprf1 zprf2)
       | i => bad_proofs i);
-  in make_deriv ps oracles thms proof end;
+  in make_deriv ps oracles thms zboxes proof end;
 
 fun deriv_rule1 (f, g) = deriv_rule2 (K f, K g) empty_deriv;
 
 fun deriv_rule0 (f, g) =
   let val proofs = ! Proofterm.proofs in
     if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
-      deriv_rule1 (I, I) (make_deriv [] [] []
+      deriv_rule1 (I, I) (make_deriv [] [] [] Proofterm.empty_zboxes
        (if Proofterm.proof_enabled proofs then f () else MinProof,
         if Proofterm.zproof_enabled proofs then g () else ZDummy))
     else empty_deriv
   end;
 
 fun deriv_rule_unconditional (f, g)
-    (Deriv {promises, body = PBody {oracles, thms, proof = (prf, zprf)}}) =
-  make_deriv promises oracles thms (f prf, g zprf);
+    (Deriv {promises, body = PBody {oracles, thms, zboxes, proof = (prf, zprf)}}) =
+  make_deriv promises oracles thms zboxes (f prf, g zprf);
 
 
 (* fulfilled proofs *)
@@ -850,7 +853,7 @@
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] Proofterm.no_proof,
+    Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes Proofterm.no_proof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -990,20 +993,24 @@
 
 local
 
-fun union_digest (oracles1, thms1) (oracles2, thms2) =
-  (Proofterm.union_oracles oracles1 oracles2, Proofterm.union_thms thms1 thms2);
+val empty_digest = ([], [], Proofterm.empty_zboxes);
 
-fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
-  (oracles, thms);
+fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) =
+ (Proofterm.union_oracles oracles1 oracles2,
+  Proofterm.union_thms thms1 thms2,
+  Proofterm.union_zboxes zboxes1 zboxes2);
+
+fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, zboxes, ...}, ...}, _)) =
+  (oracles, thms, zboxes);
 
 fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
   Sorts.of_sort_derivation (Sign.classes_of thy)
    {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 =>
-      if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
+      if c1 = c2 then empty_digest else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
     type_constructor = fn (a, _) => fn dom => fn c =>
       let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c))
       in (fold o fold) (union_digest o #1) dom arity_digest end,
-    type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
+    type_variable = fn T => map (pair empty_digest) (Type.sort_of_atyp T)}
    (typ, sort);
 
 in
@@ -1024,10 +1031,10 @@
             raise THEORY ("solve_constraints: bad theories for theorem\n" ^
               Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys);
 
-        val Deriv {promises, body = PBody {oracles, thms, proof}} = der;
-        val (oracles', thms') = (oracles, thms)
+        val Deriv {promises, body = PBody {oracles, thms, zboxes, proof}} = der;
+        val (oracles', thms', zboxes') = (oracles, thms, zboxes)
           |> fold (fold union_digest o constraint_digest) constraints;
-        val body' = PBody {oracles = oracles', thms = thms', proof = proof};
+        val body' = PBody {oracles = oracles', thms = thms', zboxes = zboxes', proof = proof};
       in
         Thm (Deriv {promises = promises, body = body'},
           {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
@@ -1132,7 +1139,7 @@
         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
           name_pos shyps hyps prop ps body;
       val zprf = ZTerm.todo_proof (Proofterm.zproof_of body);
-      val der' = make_deriv [] [] [pthm] (prf, zprf);
+      val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
     in Thm (der', args) end);
 
 fun close_derivation pos =
@@ -1168,7 +1175,7 @@
               | 6 => (make_oracle (), (Proofterm.oracle_proof name prop, ZTerm.todo_proof ()))
               | i => bad_proofs i);
           in
-            Thm (make_deriv [] [oracle] [] proof,
+            Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes proof,
              {cert = Context.join_certificate (Context.Certificate thy', cert2),
               tags = [],
               maxidx = maxidx,
@@ -1832,7 +1839,7 @@
         Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
           shyps prop ps body;
       val zprf = ZTerm.todo_proof body;
-      val der' = make_deriv [] [] [pthm] (prf, zprf);
+      val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
       val prop' = Proofterm.thm_node_prop (#2 pthm);
     in
       Thm (der',
diff -r 5109e4b2a292 -r 686b7b14d041 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/zterm.ML	Sat Dec 02 19:57:57 2023 +0100
@@ -38,11 +38,6 @@
   | ZAppP of zproof * zproof
   | ZClassP of ztyp * class        (*OFCLASS proof from sorts algebra*)
   | ZOracle of serial * zterm * ztyp list
-and zproof_body = ZPBody of
-  {boxes: (zterm * zproof future) Inttab.table,
-   consts: serial Ord_List.T,
-   oracles: ((string * Position.T) * zterm option) Ord_List.T,
-   proof: zproof}
 
 
 signature ZTERM =