# HG changeset patch
# User wenzelm
# Date 1702656959 -3600
# Node ID 3c194f50beefa6235ebc18b6b15d8ef1cb1f4829
# Parent  07b93dee105f70d3cdec41bcac17de7ff2251596
more zproofs;

diff -r 07b93dee105f -r 3c194f50beef src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Dec 14 20:43:10 2023 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 15 17:15:59 2023 +0100
@@ -2196,10 +2196,13 @@
 
     val {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof0, proof = proof0} = body;
     val proofs = get_proofs_level ();
-    val zproof' = if zproof_enabled proofs then ZTerm.todo_proof zproof0 else ZDummy;
-    val proof' = if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0 else MinProof;
-    val body0 =
-      PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof', proof = proof'};
+    val (zboxes', zproof') =
+      if zproof_enabled proofs then ZTerm.box_proof thy hyps concl (zboxes0, zproof0)
+      else (ZTerm.empty_zboxes, ZDummy);
+    val proof' =
+      if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0
+      else MinProof;
+    val body1 = {oracles = oracles0, thms = thms0, zboxes = zboxes', zproof = zproof', proof = proof'};
 
     fun new_prf () =
       let
@@ -2207,7 +2210,7 @@
         val unconstrainT =
           unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
         val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
-      in (i, fulfill_proof_future thy promises postproc (Future.value body0)) end;
+      in (i, fulfill_proof_future thy promises postproc (Future.value (PBody body1))) end;
 
     val (i, body') =
       (*somewhat non-deterministic proof boxes!*)
@@ -2249,10 +2252,12 @@
       else
         proof_combP (proof_combt' (head, args),
           map PClass (#outer_constraints ucontext) @ map Hyp hyps);
-    val zproof = ZTerm.todo_proof ();
+    val (zboxes2, zproof2) =
+      if unconstrain then (ZTerm.empty_zboxes, ZTerm.todo_proof ())
+      else (#zboxes body1, #zproof body1);
 
     val proof_body =
-      PBody {oracles = [], thms = [thm], zboxes = ZTerm.empty_zboxes, zproof = zproof, proof = proof};
+      PBody {oracles = [], thms = [thm], zboxes = zboxes2, zproof = zproof2, proof = proof};
   in (thm, proof_body) end;
 
 in
diff -r 07b93dee105f -r 3c194f50beef src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Dec 14 20:43:10 2023 +0100
+++ b/src/Pure/zterm.ML	Fri Dec 15 17:15:59 2023 +0100
@@ -219,10 +219,8 @@
   datatype ztyp = datatype ztyp
   datatype zterm = datatype zterm
   datatype zproof = datatype zproof
+  exception ZTERM of string * ztyp list * zterm list * zproof list
   type zproof_const = zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
-  type zboxes = (zterm * zproof future) Inttab.table
-  val empty_zboxes: zboxes
-  val union_zboxes: zboxes -> zboxes -> zboxes
   val fold_tvars: (indexname * sort -> 'a -> 'a) -> ztyp -> 'a -> 'a
   val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a
   val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
@@ -251,6 +249,10 @@
   val norm_proof: theory -> Envir.env -> zproof -> zproof
   val dummy_proof: 'a -> zproof
   val todo_proof: 'a -> zproof
+  type zboxes = (zterm * zproof future) Inttab.table
+  val empty_zboxes: zboxes
+  val union_zboxes: zboxes -> zboxes -> zboxes
+  val box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof
   val axiom_proof:  theory -> string -> term -> zproof
   val oracle_proof:  theory -> string -> term -> zproof
   val assume_proof: theory -> term -> zproof
@@ -289,6 +291,8 @@
 datatype zterm = datatype zterm;
 datatype zproof = datatype zproof;
 
+exception ZTERM of string * ztyp list * zterm list * zproof list;
+
 open ZTerm;
 
 
@@ -589,14 +593,6 @@
 val todo_proof = dummy_proof;
 
 
-(* boxes *)
-
-type zboxes = (zterm * zproof future) Inttab.table;
-
-val empty_zboxes: zboxes = Inttab.empty;
-val union_zboxes: zboxes -> zboxes -> zboxes = curry (Inttab.merge (K true));
-
-
 (* constants *)
 
 type zproof_const = zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table;
@@ -620,6 +616,56 @@
   in ZConstp (a, A, instT', inst') end;
 
 
+(* closed proof boxes *)
+
+type zboxes = (zterm * zproof future) Inttab.table;
+
+val empty_zboxes: zboxes = Inttab.empty;
+val union_zboxes: zboxes -> zboxes -> zboxes = curry (Inttab.merge (K true));
+fun add_zboxes entry : zboxes -> zboxes = Inttab.update_new entry;
+
+local
+
+fun close_prop hyps concl =
+  fold_rev (fn A => fn B => ZApp (ZApp (ZConst0 "Pure.imp", A), B)) hyps concl;
+
+fun close_proof hyps prf =
+  let
+    val m = length hyps - 1;
+    val bounds = ZTerms.build (hyps |> fold_index (fn (i, h) => ZTerms.update (h, m - i)));
+
+    fun proof lev (ZHyp t) =
+          (case ZTerms.lookup bounds t of
+            SOME i => ZBoundp (lev + i)
+          | NONE => raise ZTERM ("Unbound proof hypothesis", [], [t], []))
+      | proof lev (ZAbst (x, T, p)) = ZAbst (x, T, proof lev p)
+      | proof lev (ZAbsp (x, t, p)) = ZAbsp (x, t, proof (lev + 1) p)
+      | proof lev (ZAppt (p, t)) = ZAppt (proof lev p, t)
+      | proof lev (ZAppp (p, q)) =
+          (ZAppp (proof lev p, Same.commit (proof lev) q) handle Same.SAME =>
+            ZAppp (p, proof lev q))
+      | proof _ _ = raise Same.SAME;
+  in ZAbsps hyps (Same.commit (proof 0) prf) end;
+
+in
+
+fun box_proof thy hyps concl (zboxes: zboxes, prf) =
+  let
+    val {zterm, ...} = zterm_cache thy;
+    val hyps' = map zterm hyps;
+    val concl' = zterm concl;
+
+    val prop' = close_prop hyps' concl';
+    val prf' = close_proof hyps' prf;
+
+    val i = serial ();
+    val zboxes' = add_zboxes (i, (prop', Future.value prf')) zboxes;
+    val prf'' = ZAppts (ZConstp (zproof_const (ZBox i) prop'), hyps');
+  in (zboxes', prf'') end;
+
+end;
+
+
 (* basic logic *)
 
 fun axiom_proof thy name A =