# HG changeset patch
# User wenzelm
# Date 1703022992 -3600
# Node ID 3b03af5125dede3fbb4ac2548142edd35cabf8c4
# Parent  8db60cadad86f5c2a5c447d63c58ee75c4d07445
use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;

diff -r 8db60cadad86 -r 3b03af5125de src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Tue Dec 19 20:02:17 2023 +0100
+++ b/src/Pure/global_theory.ML	Tue Dec 19 22:56:32 2023 +0100
@@ -245,7 +245,13 @@
 
 (* store theorems and proofs *)
 
-fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
+fun register_proofs thms thy =
+  let
+    val (thms', thy') =
+      if Proofterm.zproof_enabled (Proofterm.get_proofs_level ())
+      then fold_map Thm.store_zproof thms thy
+      else (thms, thy);
+  in (thms', Thm.register_proofs (Lazy.value thms') thy') end;
 
 fun bind_name thy b = (Sign.full_name thy b, Binding.default_pos_of b);
 
diff -r 8db60cadad86 -r 3b03af5125de src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 19 20:02:17 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 19 22:56:32 2023 +0100
@@ -173,6 +173,8 @@
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
+  val get_zproof: theory -> serial -> {prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} option
+  val store_zproof: thm -> theory -> thm * theory
   val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
@@ -943,23 +945,30 @@
 structure Data = Theory_Data
 (
   type T =
+    {prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} Inttab.table *  (*stored thms: zproof*)
     unit Name_Space.table *  (*oracles: authentic derivation names*)
     classes;  (*type classes within the logic*)
 
-  val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes);
-  fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T =
-    (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2));
+  val empty : T = (Inttab.empty, Name_Space.empty_table Markup.oracleN, empty_classes);
+  fun merge ((zproofs1, oracles1, sorts1), (zproofs2, oracles2, sorts2)) : T =
+   (Inttab.merge (K true) (zproofs1, zproofs2),
+    Name_Space.merge_tables (oracles1, oracles2),
+    merge_classes (sorts1, sorts2));
 );
 
-val get_oracles = #1 o Data.get;
-val map_oracles = Data.map o apfst;
+val get_zproofs = #1 o Data.get;
+fun map_zproofs f = Data.map (fn (a, b, c) => (f a, b, c));
 
-val get_classes = (fn (_, Classes args) => args) o Data.get;
+val get_oracles = #2 o Data.get;
+fun map_oracles f = Data.map (fn (a, b, c) => (a, f b, c));
+
+val get_classes = (fn (_, _, Classes args) => args) o Data.get;
 val get_classrels = #classrels o get_classes;
 val get_arities = #arities o get_classes;
 
 fun map_classes f =
-  (Data.map o apsnd) (fn Classes {classrels, arities} => make_classes (f (classrels, arities)));
+  Data.map (fn (a, b, Classes {classrels, arities}) =>
+    (a, b, make_classes (f (classrels, arities))));
 fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities));
 fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities));
 
@@ -1997,6 +2006,24 @@
   end;
 
 
+(* stored thms: zproof *)
+
+val get_zproof = Inttab.lookup o get_zproofs;
+
+fun store_zproof thm thy =
+  let
+    val Thm (Deriv {promises, body = PBody body}, args as {hyps, prop, ...}) = thm;
+    val {oracles, thms, zboxes, zproof, proof} = body;
+    val _ = null promises orelse
+      raise THM ("store_zproof: theorem may not use promises", 0, [thm]);
+
+    val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy hyps prop zproof;
+    val thy' = thy
+      |> map_zproofs (Inttab.update (i, {prop = zprop, zboxes = zboxes, zproof = zprf}));
+    val der' = make_deriv promises oracles thms [] zproof' proof;
+  in (Thm (der', args), thy') end;
+
+
 
 (*** Inference rules for tactics ***)
 
diff -r 8db60cadad86 -r 3b03af5125de src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 19 20:02:17 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 19 22:56:32 2023 +0100
@@ -197,7 +197,8 @@
 datatype zproof_name =
     ZAxiom of string
   | ZOracle of string
-  | ZBox of serial;
+  | ZBox of serial
+  | ZThm of serial;
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
@@ -264,8 +265,8 @@
   type zboxes = zbox Ord_List.T
   val union_zboxes: zboxes -> zboxes -> zboxes
   val unions_zboxes: zboxes list -> zboxes
-  val box_proof: theory -> term list -> term -> zproof -> zbox * zproof
   val add_box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof
+  val thm_proof: theory -> term list -> term -> zproof -> zbox * zproof
   val axiom_proof:  theory -> string -> term -> zproof
   val oracle_proof:  theory -> string -> term -> zproof
   val assume_proof: theory -> term -> zproof
@@ -785,9 +786,7 @@
       | proof _ _ = raise Same.SAME;
   in ZAbsps hyps (Same.commit (proof 0) prf) end;
 
-in
-
-fun box_proof thy hyps concl prf =
+fun box_proof zproof_name thy hyps concl prf =
   let
     val {zterm, ...} = zterm_cache thy;
     val hyps' = map zterm hyps;
@@ -798,11 +797,15 @@
 
     val i = serial ();
     val zbox: zbox = (i, (prop', prf'));
-    val zbox_prf = ZAppts (ZConstp (zproof_const (ZBox i) prop'), hyps');
+    val zbox_prf = ZAppts (ZConstp (zproof_const (zproof_name i) prop'), hyps');
   in (zbox, zbox_prf) end;
 
+in
+
+val thm_proof = box_proof ZThm;
+
 fun add_box_proof thy hyps concl (zboxes, prf) =
-  let val (zbox, zbox_prf) = box_proof thy hyps concl prf
+  let val (zbox, zbox_prf) = box_proof ZBox thy hyps concl prf
   in (add_zboxes zbox zboxes, zbox_prf) end;
 
 end;