# HG changeset patch
# User wenzelm
# Date 1701683612 -3600
# Node ID cf29db6c95e1c0a79670ad5680659d26b82065e9
# Parent  0c7de2ae814b7518fc42f572ad9c9f48cd657b2d
more zterm operations;
more zproofs;

diff -r 0c7de2ae814b -r cf29db6c95e1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 02 20:21:56 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 04 10:53:32 2023 +0100
@@ -872,7 +872,10 @@
   (case Name_Space.lookup (Theory.axiom_table thy) name of
     SOME prop =>
       let
-        val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop, ZTerm.todo_proof);
+        val der =
+          deriv_rule0
+           (fn () => Proofterm.axm_proof name prop,
+            fn () => ZTerm.axiom_proof thy {name = name, oracle = false} prop);
         val cert = Context.Certificate thy;
         val maxidx = maxidx_of_term prop;
         val shyps = Sorts.insert_term prop [];
@@ -1163,20 +1166,23 @@
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else
           let
+            val cert = Context.join_certificate (Context.Certificate thy', cert2);
             fun no_oracle () = ((name, Position.none), NONE);
             fun make_oracle () = ((name, Position.thread_data ()), SOME prop);
+            fun zproof () =
+              ZTerm.axiom_proof (Context.certificate_theory cert) {name = name, oracle = true} prop;
             val (oracle, proof) =
               (case ! Proofterm.proofs of
                 0 => (no_oracle (), Proofterm.no_proof)
               | 1 => (make_oracle (), Proofterm.no_proof)
-              | 2 => (make_oracle (), (Proofterm.oracle_proof name prop, ZDummy))
-              | 4 => (no_oracle (), (MinProof, ZTerm.todo_proof ()))
-              | 5 => (make_oracle (), (MinProof, ZTerm.todo_proof ()))
-              | 6 => (make_oracle (), (Proofterm.oracle_proof name prop, ZTerm.todo_proof ()))
+              | 2 => (make_oracle (), (Proofterm.oracle_proof name prop, zproof ()))
+              | 4 => (no_oracle (), (MinProof, zproof ()))
+              | 5 => (make_oracle (), (MinProof, zproof ()))
+              | 6 => (make_oracle (), (Proofterm.oracle_proof name prop, zproof ()))
               | i => bad_proofs i);
           in
             Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes proof,
-             {cert = Context.join_certificate (Context.Certificate thy', cert2),
+             {cert = cert,
               tags = [],
               maxidx = maxidx,
               constraints = [],
@@ -1212,15 +1218,21 @@
       raise THM ("assume: prop", 0, [])
     else if maxidx <> ~1 then
       raise THM ("assume: variables", maxidx, [])
-    else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop, ZTerm.todo_proof),
-     {cert = cert,
-      tags = [],
-      maxidx = ~1,
-      constraints = [],
-      shyps = sorts,
-      hyps = [prop],
-      tpairs = [],
-      prop = prop})
+    else
+      let
+        fun prf () = Proofterm.Hyp prop;
+        fun zprf () = ZTerm.assume_proof (Context.certificate_theory cert) prop;
+      in
+        Thm (deriv_rule0 (prf, zprf),
+         {cert = cert,
+          tags = [],
+          maxidx = ~1,
+          constraints = [],
+          shyps = sorts,
+          hyps = [prop],
+          tpairs = [],
+          prop = prop})
+      end
   end;
 
 (*Implication introduction
@@ -1236,15 +1248,21 @@
   if T <> propT then
     raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   else
-    Thm (deriv_rule1 (Proofterm.implies_intr_proof A, ZTerm.todo_proof) der,
-     {cert = join_certificate1 (ct, th),
-      tags = [],
-      maxidx = Int.max (maxidx1, maxidx2),
-      constraints = constraints,
-      shyps = Sorts.union sorts shyps,
-      hyps = remove_hyps A hyps,
-      tpairs = tpairs,
-      prop = Logic.mk_implies (A, prop)});
+    let
+      val cert = join_certificate1 (ct, th);
+      val prf = Proofterm.implies_intr_proof A;
+      fun zprf b = ZTerm.implies_intr_proof (Context.certificate_theory cert) A b;
+    in
+      Thm (deriv_rule1 (prf, zprf) der,
+       {cert = cert,
+        tags = [],
+        maxidx = Int.max (maxidx1, maxidx2),
+        constraints = constraints,
+        shyps = Sorts.union sorts shyps,
+        hyps = remove_hyps A hyps,
+        tpairs = tpairs,
+        prop = Logic.mk_implies (A, prop)})
+    end;
 
 
 (*Implication elimination
@@ -1263,7 +1281,7 @@
     (case prop of
       Const ("Pure.imp", _) $ A $ B =>
         if A aconv propA then
-          Thm (deriv_rule2 (curry Proofterm.%%, K ZTerm.todo_proof) der derA,
+          Thm (deriv_rule2 (curry Proofterm.%%, curry ZAppP) der derA,
            {cert = join_certificate2 (thAB, thA),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1295,15 +1313,21 @@
       if occs x ts tpairs then
         raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
       else
-        Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE, ZTerm.todo_proof) der,
-         {cert = join_certificate1 (ct, th),
-          tags = [],
-          maxidx = Int.max (maxidx1, maxidx2),
-          constraints = constraints,
-          shyps = Sorts.union sorts shyps,
-          hyps = hyps,
-          tpairs = tpairs,
-          prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
+        let
+          val cert = join_certificate1 (ct, th);
+          val prf = Proofterm.forall_intr_proof (a, x) NONE;
+          fun zprf p = ZTerm.forall_intr_proof (Context.certificate_theory cert) (a, x) T p;
+        in
+          Thm (deriv_rule1 (prf, zprf) der,
+           {cert = cert,
+            tags = [],
+            maxidx = Int.max (maxidx1, maxidx2),
+            constraints = constraints,
+            shyps = Sorts.union sorts shyps,
+            hyps = hyps,
+            tpairs = tpairs,
+            prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))})
+        end;
   in
     (case x of
       Free (a, _) => check_result a hyps
@@ -1324,15 +1348,20 @@
       if T <> qary then
         raise THM ("forall_elim: type mismatch", 0, [th])
       else
-        Thm (deriv_rule1 (Proofterm.% o rpair (SOME t), ZTerm.todo_proof) der,
-         {cert = join_certificate1 (ct, th),
-          tags = [],
-          maxidx = Int.max (maxidx1, maxidx2),
-          constraints = constraints,
-          shyps = Sorts.union sorts shyps,
-          hyps = hyps,
-          tpairs = tpairs,
-          prop = Term.betapply (A, t)})
+        let
+          val cert = join_certificate1 (ct, th);
+          fun zprf p = ZTerm.forall_elim_proof (Context.certificate_theory cert) t p;
+        in
+          Thm (deriv_rule1 (Proofterm.% o rpair (SOME t), zprf) der,
+           {cert = cert,
+            tags = [],
+            maxidx = Int.max (maxidx1, maxidx2),
+            constraints = constraints,
+            shyps = Sorts.union sorts shyps,
+            hyps = hyps,
+            tpairs = tpairs,
+            prop = Term.betapply (A, t)})
+        end
   | _ => raise THM ("forall_elim: not quantified", 0, [th]));
 
 
@@ -1784,15 +1813,17 @@
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
-    Thm (deriv_rule0 (fn () => Proofterm.trivial_proof, ZTerm.todo_proof),
-     {cert = cert,
-      tags = [],
-      maxidx = maxidx,
-      constraints = [],
-      shyps = sorts,
-      hyps = [],
-      tpairs = [],
-      prop = Logic.mk_implies (A, A)});
+    let fun zprf () = ZTerm.trivial_proof (Context.certificate_theory cert) A in
+      Thm (deriv_rule0 (fn () => Proofterm.trivial_proof, zprf),
+       {cert = cert,
+        tags = [],
+        maxidx = maxidx,
+        constraints = [],
+        shyps = sorts,
+        hyps = [],
+        tpairs = [],
+        prop = Logic.mk_implies (A, A)})
+    end;
 
 (*Axiom-scheme reflecting signature contents
         T :: c
diff -r 0c7de2ae814b -r cf29db6c95e1 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Dec 02 20:21:56 2023 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 04 10:53:32 2023 +0100
@@ -7,8 +7,7 @@
 (* global datatypes *)
 
 datatype ztyp =
-    ZTFree of string * sort
-  | ZTVar of indexname * sort
+    ZTVar of indexname * sort      (*free: index ~1*)
   | ZFun of ztyp * ztyp
   | ZProp
   | ZItself of ztyp
@@ -17,8 +16,7 @@
   | ZType of string * ztyp list    (*type constructor: >= 2 arguments*)
 
 datatype zterm =
-    ZFree of string * ztyp
-  | ZVar of indexname * ztyp
+    ZVar of indexname * ztyp       (*free: index ~1*)
   | ZBound of int
   | ZConst0 of string              (*monomorphic constant*)
   | ZConst1 of string * ztyp       (*polymorphic constant: 1 type argument*)
@@ -29,7 +27,6 @@
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
-  | ZConstP of serial * ztyp list  (*proof constant: local box, global axiom or thm*)
   | ZBoundP of int
   | ZHyp of zterm
   | ZAbst of string * ztyp * zproof
@@ -37,22 +34,40 @@
   | ZAppt of zproof * zterm
   | ZAppP of zproof * zproof
   | ZClassP of ztyp * class        (*OFCLASS proof from sorts algebra*)
-  | ZOracle of serial * zterm * ztyp list
+  | ZAxiom of {name: string, oracle: bool} * zterm * ztyp list;
 
+signature ZTVARS =
+sig
+  include TERM_ITEMS
+  val add_tvarsT: ztyp -> set -> set
+  val add_tvars: zterm -> set -> set
+end
 
 signature ZTERM =
 sig
   datatype ztyp = datatype ztyp
   datatype zterm = datatype zterm
   datatype zproof = datatype zproof
+  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
+  structure ZTVars: ZTVARS
   val ztyp_ord: ztyp * ztyp -> order
-  val zaconv: zterm * zterm -> bool
+  val aconv_zterm: zterm * zterm -> bool
   val ztyp_of: typ -> ztyp
   val typ_of: ztyp -> typ
   val zterm_of: Consts.T -> term -> zterm
   val term_of: Consts.T -> zterm -> term
+  val global_zterm_of: theory -> term -> zterm
+  val global_term_of: theory -> zterm -> term
   val dummy_proof: 'a -> zproof
   val todo_proof: 'a -> zproof
+  val axiom_proof:  theory -> {name: string, oracle: bool} -> term -> zproof
+  val assume_proof: theory -> term -> zproof
+  val trivial_proof: theory -> term -> zproof
+  val implies_intr_proof: theory -> term -> zproof -> zproof
+  val forall_intr_proof: theory -> string * term -> typ -> zproof -> zproof
+  val forall_elim_proof: theory -> term -> zproof -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -63,18 +78,51 @@
 datatype zproof = datatype zproof;
 
 
+(* fold *)
+
+fun fold_tvars f (ZTVar v) = f v
+  | fold_tvars f (ZFun (T, U)) = fold_tvars f T #> fold_tvars f U
+  | fold_tvars f (ZItself T) = fold_tvars f T
+  | fold_tvars f (ZType1 (_, T)) = fold_tvars f T
+  | fold_tvars f (ZType (_, Ts)) = fold (fold_tvars f) Ts
+  | fold_tvars _ _ = I;
+
+fun fold_aterms f (ZApp (t, u)) = fold_aterms f t #> fold_aterms f u
+  | fold_aterms f (ZAbs (_, _, t)) = fold_aterms f t
+  | fold_aterms f a = f a;
+
+fun fold_types f (ZVar (_, T)) = f T
+  | fold_types f (ZConst1 (_, T)) = f T
+  | fold_types f (ZConst (_, As)) = fold f As
+  | fold_types f (ZAbs (_, T, b)) = f T #> fold_types f b
+  | fold_types f (ZApp (t, u)) = fold_types f t #> fold_types f u
+  | fold_types f (ZClass (T, _)) = f T
+  | fold_types _ _ = I;
+
+
+(* term items *)
+
+structure ZTVars: ZTVARS =
+struct
+  open TVars;
+  val add_tvarsT = fold_tvars add_set;
+  val add_tvars = fold_types add_tvarsT;
+end;
+
+val make_tvars = ZTVars.list_set o ZTVars.build o ZTVars.add_tvars;
+
+
 (* orderings *)
 
 local
 
-fun cons_nr (ZTFree _) = 0
-  | cons_nr (ZTVar _) = 1
-  | cons_nr (ZFun _) = 2
-  | cons_nr ZProp = 3
-  | cons_nr (ZItself _) = 4
-  | cons_nr (ZType0 _) = 5
-  | cons_nr (ZType1 _) = 6
-  | cons_nr (ZType _) = 7;
+fun cons_nr (ZTVar _) = 0
+  | cons_nr (ZFun _) = 1
+  | cons_nr ZProp = 2
+  | cons_nr (ZItself _) = 3
+  | cons_nr (ZType0 _) = 4
+  | cons_nr (ZType1 _) = 5
+  | cons_nr (ZType _) = 6;
 
 val fast_indexname_ord = Term_Ord.fast_indexname_ord;
 val sort_ord = Term_Ord.sort_ord;
@@ -85,10 +133,8 @@
   if pointer_eq TU then EQUAL
   else
     (case TU of
-      (ZTFree (a, A), ZTFree (b, B)) =>
-        (case fast_string_ord (a, b) of EQUAL => sort_ord (A, B) | ord => ord)
-    | (ZTVar (a, A), ZTVar (b, B)) =>
-        (case fast_indexname_ord (a, b) of EQUAL => Term_Ord.sort_ord (A, B) | ord => ord)
+      (ZTVar (a, A), ZTVar (b, B)) =>
+        (case fast_indexname_ord (a, b) of EQUAL => sort_ord (A, B) | ord => ord)
     | (ZFun (T, T'), ZFun (U, U')) =>
         (case ztyp_ord (T, U) of EQUAL => ztyp_ord (T', U') | ord => ord)
     | (ZProp, ZProp) => EQUAL
@@ -105,24 +151,24 @@
 
 (* alpha conversion *)
 
-fun zaconv (tm1, tm2) =
+fun aconv_zterm (tm1, tm2) =
   pointer_eq (tm1, tm2) orelse
     (case (tm1, tm2) of
-      (ZApp (t1, u1), ZApp (t2, u2)) => zaconv (t1, t2) andalso zaconv (u1, u2)
-    | (ZAbs (_, T1, t1), ZAbs (_, T2, t2)) => zaconv (t1, t2) andalso T1 = T2
+      (ZApp (t1, u1), ZApp (t2, u2)) => aconv_zterm (t1, t2) andalso aconv_zterm (u1, u2)
+    | (ZAbs (_, T1, t1), ZAbs (_, T2, t2)) => aconv_zterm (t1, t2) andalso T1 = T2
     | (a1, a2) => a1 = a2);
 
 
 (* convert ztyp / zterm vs. regular typ / term *)
 
-fun ztyp_of (TFree v) = ZTFree v
+fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)
   | ztyp_of (TVar v) = ZTVar v
   | ztyp_of (Type ("fun", [T, U])) = ZFun (ztyp_of T, ztyp_of U)
   | ztyp_of (Type (c, [])) = if c = "prop" then ZProp else ZType0 c
   | ztyp_of (Type (c, [T])) = if c = "itself" then ZItself (ztyp_of T) else ZType1 (c, ztyp_of T)
   | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
 
-fun typ_of (ZTFree v) = TFree v
+fun typ_of (ZTVar ((a, ~1), S)) = TFree (a, S)
   | typ_of (ZTVar v) = TVar v
   | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
   | typ_of ZProp = propT
@@ -134,7 +180,7 @@
 fun zterm_of consts =
   let
     val typargs = Consts.typargs consts;
-    fun zterm (Free (x, T)) = ZFree (x, ztyp_of T)
+    fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp_of T)
       | zterm (Var (xi, T)) = ZVar (xi, ztyp_of T)
       | zterm (Bound i) = ZBound i
       | zterm (Const (c, T)) =
@@ -154,7 +200,7 @@
   let
     val instance = Consts.instance consts;
     fun const (c, Ts) = Const (c, instance (c, Ts));
-    fun term (ZFree (x, T)) = Free (x, typ_of T)
+    fun term (ZVar ((x, ~1), T)) = Free (x, typ_of T)
       | term (ZVar (xi, T)) = Var (xi, typ_of T)
       | term (ZBound i) = Bound i
       | term (ZConst0 c) = const (c, [])
@@ -165,10 +211,60 @@
       | term (ZClass (T, c)) = Logic.mk_of_class (typ_of T, c);
   in term end;
 
+val global_zterm_of = zterm_of o Sign.consts_of;
+val global_term_of = term_of o Sign.consts_of;
 
-(* proofs *)
+
+
+(** proof construction **)
 
 fun dummy_proof _ = ZDummy;
 val todo_proof = dummy_proof;
 
+fun axiom_proof thy a A =
+  let
+    val t = global_zterm_of thy A;
+    val Ts = make_tvars t;
+  in ZAxiom (a, t, map ZTVar Ts) end;
+
+fun assume_proof thy A =
+  ZHyp (global_zterm_of thy A);
+
+fun trivial_proof thy A =
+  ZAbsP ("H", global_zterm_of thy A, ZBoundP 0);
+
+fun implies_intr_proof thy A prf =
+  let
+    val h = global_zterm_of thy A;
+    fun abs_hyp i (p as ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else p
+      | abs_hyp i (ZAbst (x, T, p)) = ZAbst (x, T, abs_hyp i p)
+      | abs_hyp i (ZAbsP (x, t, p)) = ZAbsP (x, t, abs_hyp (i + 1) p)
+      | abs_hyp i (ZAppt (p, t)) = ZAppt (abs_hyp i p, t)
+      | abs_hyp i (ZAppP (p, q)) = ZAppP (abs_hyp i p, abs_hyp i q)
+      | abs_hyp _ p = p;
+  in ZAbsP ("H", h, abs_hyp 0 prf) end;
+
+fun forall_intr_proof thy (a, x) T prf =
+  let
+    val z = global_zterm_of thy x;
+    val Z = ztyp_of T;
+
+    fun abs_term i b =
+      if aconv_zterm (b, z) then ZBound i
+      else
+        (case b of
+          ZAbs (x, T, t) => ZAbs (x, T, abs_term (i + 1) t)
+        | ZApp (t, u) => ZApp (abs_term i t, abs_term i u)
+        | _ => b);
+
+    fun abd_proof i (ZAbst (x, T, prf)) = ZAbst (x, T, abd_proof (i + 1) prf)
+      | abd_proof i (ZAbsP (x, t, prf)) = ZAbsP (x, abs_term i t, abd_proof i prf)
+      | abd_proof i (ZAppt (p, t)) = ZAppt (abd_proof i p, abs_term i t)
+      | abd_proof i (ZAppP (p, q)) = ZAppP (abd_proof i p, abd_proof i q)
+      | abd_proof _ p = p;
+
+  in ZAbst (a, Z, abd_proof 0 prf) end;
+
+fun forall_elim_proof thy t p = ZAppt (p, global_zterm_of thy t);
+
 end;