# HG changeset patch
# User wenzelm
# Date 1702571625 -3600
# Node ID bf2e724ff57e9b1ad29daf53fee2ba1afb5186af
# Parent  64c655e8e8bf59134ffef155fbc92b8331efa47d
clarified signature;
clarified modules;

diff -r 64c655e8e8bf -r bf2e724ff57e src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Thu Dec 14 17:33:45 2023 +0100
@@ -184,7 +184,7 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
-        zboxes = Proofterm.empty_zboxes,
+        zboxes = ZTerm.empty_zboxes,
         zproof = ZDummy,
         proof = prf};
   in Proofterm.thm_body body end;
diff -r 64c655e8e8bf -r bf2e724ff57e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 14 17:33:45 2023 +0100
@@ -13,7 +13,6 @@
       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
@@ -29,7 +28,7 @@
   and proof_body = PBody of
     {oracles: ((string * Position.T) * term option) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
-     zboxes: zboxes,
+     zboxes: ZTerm.zboxes,
      zproof: zproof,
      proof: proof}
   type oracle = (string * Position.T) * term option
@@ -61,8 +60,6 @@
   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_body: zproof -> proof -> proof_body
   val no_thm_names: proof -> proof
   val no_thm_proofs: proof -> proof
@@ -217,8 +214,6 @@
   {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
@@ -234,7 +229,7 @@
 and proof_body = PBody of
   {oracles: ((string * Position.T) * term option) Ord_List.T,
    thms: (serial * thm_node) Ord_List.T,
-   zboxes: zboxes,
+   zboxes: ZTerm.zboxes,
    zproof: zproof,
    proof: proof}
 and thm_body =
@@ -343,11 +338,8 @@
 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));
-
 fun no_proof_body zproof proof =
-  PBody {oracles = [], thms = [], zboxes = empty_zboxes, zproof = zproof, proof = proof};
+  PBody {oracles = [], thms = [], zboxes = ZTerm.empty_zboxes, zproof = zproof, proof = proof};
 val no_thm_body = thm_body (no_proof_body ZDummy MinProof);
 
 fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
@@ -471,7 +463,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, zboxes = empty_zboxes, zproof = ZDummy, proof = c} end
+  in PBody {oracles = a, thms = b, zboxes = ZTerm.empty_zboxes, zproof = ZDummy, proof = c} end
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
@@ -1990,7 +1982,7 @@
         (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 zboxes = fold (fn (_, PBody {zboxes, ...}) => ZTerm.union_zboxes zboxes) ps zboxes0;
     val proof = rew_proof thy proof0;
   in
     PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}
@@ -2260,7 +2252,7 @@
     val zproof = ZTerm.todo_proof ();
 
     val proof_body =
-      PBody {oracles = [], thms = [thm], zboxes = empty_zboxes, zproof = zproof, proof = proof};
+      PBody {oracles = [], thms = [thm], zboxes = ZTerm.empty_zboxes, zproof = zproof, proof = proof};
   in (thm, proof_body) end;
 
 in
diff -r 64c655e8e8bf -r bf2e724ff57e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/thm.ML	Thu Dec 14 17:33:45 2023 +0100
@@ -750,7 +750,7 @@
   make_deriv0 promises
     (PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});
 
-val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes ZDummy MinProof;
+val empty_deriv = make_deriv [] [] [] ZTerm.empty_zboxes ZDummy MinProof;
 
 
 (* inference rules *)
@@ -768,7 +768,7 @@
 
     val oracles' = Proofterm.union_oracles oracles1 oracles2;
     val thms' = Proofterm.union_thms thms1 thms2;
-    val zboxes' = Proofterm.union_zboxes zboxes1 zboxes2;
+    val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2;
 
     val proofs = Proofterm.get_proofs_level ();
     val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZDummy;
@@ -780,7 +780,7 @@
 fun deriv_rule0 zproof proof =
   let val proofs = Proofterm.get_proofs_level () in
     if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
-      deriv_rule1 I I (make_deriv [] [] [] Proofterm.empty_zboxes
+      deriv_rule1 I I (make_deriv [] [] [] ZTerm.empty_zboxes
        (if Proofterm.zproof_enabled proofs then zproof () else ZDummy)
        (if Proofterm.proof_enabled proofs then proof () else MinProof))
     else empty_deriv
@@ -844,7 +844,7 @@
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes ZDummy MinProof,
+    Thm (make_deriv [(i, future)] [] [] ZTerm.empty_zboxes ZDummy MinProof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -985,12 +985,12 @@
 
 local
 
-val empty_digest = ([], [], Proofterm.empty_zboxes);
+val empty_digest = ([], [], ZTerm.empty_zboxes);
 
 fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) =
  (Proofterm.union_oracles oracles1 oracles2,
   Proofterm.union_thms thms1 thms2,
-  Proofterm.union_zboxes zboxes1 zboxes2);
+  ZTerm.union_zboxes zboxes1 zboxes2);
 
 fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, zboxes, ...}, ...}, _)) =
   (oracles, thms, zboxes);
@@ -1171,7 +1171,7 @@
               then ZTerm.oracle_proof (Context.certificate_theory cert) name prop
               else ZDummy;
           in
-            Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes zproof proof,
+            Thm (make_deriv [] [oracle] [] ZTerm.empty_zboxes zproof proof,
              {cert = cert,
               tags = [],
               maxidx = maxidx,
diff -r 64c655e8e8bf -r bf2e724ff57e src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Dec 14 12:21:09 2023 +0100
+++ b/src/Pure/zterm.ML	Thu Dec 14 17:33:45 2023 +0100
@@ -153,6 +153,10 @@
   datatype ztyp = datatype ztyp
   datatype zterm = datatype zterm
   datatype zproof = datatype zproof
+  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
@@ -525,38 +529,44 @@
 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 *)
 
-fun const_proof thy a A =
+type zproof_const = zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table;
+
+fun zproof_const a A : zproof_const =
   let
-    val t = zterm_of thy A;
     val instT =
-      ZTVars.build (t |> (fold_types o fold_tvars) (fn v => fn tab =>
+      ZTVars.build (A |> (fold_types o fold_tvars) (fn v => fn tab =>
         if ZTVars.defined tab v then tab else ZTVars.update (v, ZTVar v) tab));
     val inst =
-      ZVars.build (t |> fold_aterms (fn a => fn tab =>
-        (case a of
-          ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, a) tab
+      ZVars.build (A |> fold_aterms (fn t => fn tab =>
+        (case t of
+          ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, t) tab
         | _ => tab)));
-  in ZConstp (a, t, instT, inst) end;
+  in (a, A, instT, inst) end;
 
-fun map_const_proof (f, g) prf =
-  (case prf of
-    ZConstp (a, A, instT, inst) =>
-      let
-        val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT;
-        val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst;
-      in ZConstp (a, A, instT', inst') end
-  | _ => prf);
+fun make_const_proof (f, g) ((a, A, instT, inst): zproof_const) =
+  let
+    val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT;
+    val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst;
+  in ZConstp (a, A, instT', inst') end;
 
 
 (* basic logic *)
 
-fun axiom_proof thy name =
-  const_proof thy (ZAxiom name);
+fun axiom_proof thy name A =
+  ZConstp (zproof_const (ZAxiom name) (zterm_of thy A));
 
-fun oracle_proof thy name =
-  const_proof thy (ZOracle name);
+fun oracle_proof thy name A =
+  ZConstp (zproof_const (ZOracle name) (zterm_of thy A));
 
 fun assume_proof thy A =
   ZHyp (zterm_of thy A);
@@ -627,7 +637,8 @@
 
 val [reflexive_axiom, symmetric_axiom, transitive_axiom, equal_intr_axiom, equal_elim_axiom,
   abstract_rule_axiom, combination_axiom] =
-    Theory.equality_axioms |> map (fn (b, t) => axiom_proof thy0 (Sign.full_name thy0 b) t);
+    Theory.equality_axioms |> map (fn (b, t) =>
+      let val ZConstp c = axiom_proof thy0 (Sign.full_name thy0 b) t in c end);
 
 in
 
@@ -639,7 +650,7 @@
     val {ztyp, zterm} = zterm_cache thy;
     val A = ztyp T;
     val x = zterm t;
-  in map_const_proof (fn "'a" => A, fn "x" => x) reflexive_axiom end;
+  in make_const_proof (fn "'a" => A, fn "x" => x) reflexive_axiom end;
 
 fun symmetric_proof thy T t u prf =
   if is_reflexive_proof prf then prf
@@ -649,7 +660,7 @@
       val A = ztyp T;
       val x = zterm t;
       val y = zterm u;
-      val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
+      val ax = make_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
     in ZAppp (ax, prf) end;
 
 fun transitive_proof thy T t u v prf1 prf2 =
@@ -662,7 +673,7 @@
       val x = zterm t;
       val y = zterm u;
       val z = zterm v;
-      val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom;
+      val ax = make_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom;
     in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun equal_intr_proof thy t u prf1 prf2 =
@@ -670,7 +681,7 @@
     val {zterm, ...} = zterm_cache thy;
     val A = zterm t;
     val B = zterm u;
-    val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
+    val ax = make_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
   in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun equal_elim_proof thy t u prf1 prf2 =
@@ -678,7 +689,7 @@
     val {zterm, ...} = zterm_cache thy;
     val A = zterm t;
     val B = zterm u;
-    val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
+    val ax = make_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
   in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun abstract_rule_proof thy T U x t u prf =
@@ -689,7 +700,7 @@
     val f = zterm t;
     val g = zterm u;
     val ax =
-      map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g)
+      make_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g)
         abstract_rule_axiom;
   in ZAppp (ax, forall_intr_proof thy T x prf) end;
 
@@ -703,7 +714,7 @@
     val x = zterm t;
     val y = zterm u;
     val ax =
-      map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y)
+      make_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y)
         combination_axiom;
   in ZAppp (ZAppp (ax, prf1), prf2) end;