# HG changeset patch
# User wenzelm
# Date 1701727967 -3600
# Node ID e475d6ac8eb1c7d06b0c8bcbd964c4db1977d34f
# Parent  486a32079c60061d47be85d7892cd60ed68f0eb6# Parent  89d4a8f52738eddf6a8c9fae0a499fd67aed982e
merged

diff -r 486a32079c60 -r e475d6ac8eb1 src/Pure/cterm_items.ML
--- a/src/Pure/cterm_items.ML	Sat Dec 02 20:49:50 2023 +0000
+++ b/src/Pure/cterm_items.ML	Mon Dec 04 23:12:47 2023 +0100
@@ -33,7 +33,7 @@
 structure Term_Items = Term_Items
 (
   type key = cterm;
-  val ord = Thm.fast_term_ord
+  val ord = Thm.fast_term_ord;
 );
 open Term_Items;
 
diff -r 486a32079c60 -r e475d6ac8eb1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Dec 02 20:49:50 2023 +0000
+++ b/src/Pure/proofterm.ML	Mon Dec 04 23:12:47 2023 +0100
@@ -132,7 +132,6 @@
   val assumption_proof: term list -> term -> int -> proof -> proof
   val bicompose_proof: bool -> term list -> term list -> term option -> term list ->
     int -> int -> proof -> proof -> proof
-  val equality_axms: (string * term) list
   val reflexive_axm: proof
   val symmetric_axm: proof
   val transitive_axm: proof
@@ -1286,34 +1285,14 @@
 
 (** axioms for equality **)
 
-val aT = TFree ("'a", []);
-val bT = TFree ("'b", []);
-val x = Free ("x", aT);
-val y = Free ("y", aT);
-val z = Free ("z", aT);
-val A = Free ("A", propT);
-val B = Free ("B", propT);
-val f = Free ("f", aT --> bT);
-val g = Free ("g", aT --> bT);
-
-val equality_axms =
- [("reflexive", Logic.mk_equals (x, x)),
-  ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
-  ("transitive",
-    Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
-  ("equal_intr",
-    Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
-  ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
-  ("abstract_rule",
-    Logic.mk_implies
-      (Logic.all x (Logic.mk_equals (f $ x, g $ x)),
-        Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
-  ("combination", Logic.list_implies
-    ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
+local val thy = Sign.local_path (Context.the_global_context ()) in
 
 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
   equal_elim_axm, abstract_rule_axm, combination_axm] =
-    map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
+    map (fn (b, t) => PAxm (Sign.full_name thy b, Logic.varify_global t, NONE))
+      Theory.equality_axioms;
+
+end;
 
 val reflexive_proof = reflexive_axm % NONE;
 
@@ -1347,27 +1326,23 @@
 
 fun combination_proof f g t u prf1 prf2 =
   let
-    val f = Envir.beta_norm f;
-    val g = Envir.beta_norm g;
-    val prf =
-      if check_comb prf1 then
-        combination_axm % NONE % NONE
-      else
-        (case prf1 of
-          PAxm ("Pure.reflexive", _, _) % _ =>
-            combination_axm %> remove_types f % NONE
-        | _ => combination_axm %> remove_types f %> remove_types g)
-  in
-    prf %
-      (case head_of f of
+    val f' = Envir.beta_norm f;
+    val g' = Envir.beta_norm g;
+    val ax =
+      if check_comb prf1 then combination_axm % NONE % NONE
+      else if is_reflexive_proof prf1 then combination_axm %> remove_types f' % NONE
+      else combination_axm %> remove_types f' %> remove_types g'
+    val t' =
+      (case head_of f' of
         Abs _ => SOME (remove_types t)
       | Var _ => SOME (remove_types t)
-      | _ => NONE) %
-      (case head_of g of
+      | _ => NONE);
+    val u' =
+      (case head_of g' of
         Abs _ => SOME (remove_types u)
       | Var _ => SOME (remove_types u)
-      | _ => NONE) %% prf1 %% prf2
-  end;
+      | _ => NONE);
+  in ax % t' % u' %% prf1 %% prf2 end;
 
 
 
diff -r 486a32079c60 -r e475d6ac8eb1 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Dec 02 20:49:50 2023 +0000
+++ b/src/Pure/pure_thy.ML	Mon Dec 04 23:12:47 2023 +0100
@@ -235,7 +235,6 @@
       \ (CONST Pure.term :: 'a itself \<Rightarrow> prop) (CONST Pure.type :: 'a itself)"),
     (Binding.make ("conjunction_def", \<^here>),
       prop "(A &&& B) \<equiv> (\<And>C::prop. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)")] #> snd
-  #> fold (fn (a, prop) =>
-      snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms);
+  #> fold (#2 oo Thm.add_axiom_global) Theory.equality_axioms);
 
 end;
diff -r 486a32079c60 -r e475d6ac8eb1 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Sat Dec 02 20:49:50 2023 +0000
+++ b/src/Pure/term_items.ML	Mon Dec 04 23:12:47 2023 +0100
@@ -25,6 +25,8 @@
   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
+  val update: key * 'a -> 'a table -> 'a table
+  val remove: key -> 'a table -> 'a table
   val add: key * 'a -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table
   val make1: key * 'a -> 'a table
@@ -70,6 +72,9 @@
 fun lookup (Table tab) = Table.lookup tab;
 fun defined (Table tab) = Table.defined tab;
 
+fun update e (Table tab) = Table (Table.update e tab);
+fun remove x (Table tab) = Table (Table.delete_safe x tab);
+
 fun add entry (Table tab) = Table (Table.default entry tab);
 fun make es = build (fold add es);
 fun make1 e = build (add e);
@@ -178,7 +183,7 @@
 structure Term_Items = Term_Items
 (
   type key = indexname * typ;
-  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
+  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord);
 );
 open Term_Items;
 
@@ -199,7 +204,7 @@
 structure Term_Items = Term_Items
 (
   type key = string;
-  val ord = fast_string_ord
+  val ord = fast_string_ord;
 );
 open Term_Items;
 
diff -r 486a32079c60 -r e475d6ac8eb1 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Dec 02 20:49:50 2023 +0000
+++ b/src/Pure/theory.ML	Mon Dec 04 23:12:47 2023 +0100
@@ -38,6 +38,7 @@
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   val check_overloading: Proof.context -> bool -> string * typ -> unit
+  val equality_axioms: (binding * term) list
 end
 
 structure Theory: THEORY =
@@ -357,4 +358,39 @@
 
 end;
 
+
+(** axioms for equality **)
+
+local
+
+val aT = TFree ("'a", []);
+val bT = TFree ("'b", []);
+val x = Free ("x", aT);
+val y = Free ("y", aT);
+val z = Free ("z", aT);
+val A = Free ("A", propT);
+val B = Free ("B", propT);
+val f = Free ("f", aT --> bT);
+val g = Free ("g", aT --> bT);
+
+in
+
+val equality_axioms =
+ [(Binding.make ("reflexive", \<^here>), Logic.mk_equals (x, x)),
+  (Binding.make ("symmetric", \<^here>),
+    Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
+  (Binding.make ("transitive", \<^here>),
+    Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
+  (Binding.make ("equal_intr", \<^here>),
+    Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
+  (Binding.make ("equal_elim", \<^here>), Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
+  (Binding.make ("abstract_rule", \<^here>),
+    Logic.mk_implies
+      (Logic.all x (Logic.mk_equals (f $ x, g $ x)),
+        Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+  (Binding.make ("combination", \<^here>), Logic.list_implies
+    ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
+
 end;
+
+end;
diff -r 486a32079c60 -r e475d6ac8eb1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 02 20:49:50 2023 +0000
+++ b/src/Pure/thm.ML	Mon Dec 04 23:12:47 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) T (a, x) 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]));
 
 
@@ -1341,16 +1370,18 @@
 (*Reflexivity
   t \<equiv> t
 *)
-fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
-   {cert = cert,
-    tags = [],
-    maxidx = maxidx,
-    constraints = [],
-    shyps = sorts,
-    hyps = [],
-    tpairs = [],
-    prop = Logic.mk_equals (t, t)});
+fun reflexive (Cterm {cert, t, T, maxidx, sorts}) =
+  let fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t in
+    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf),
+     {cert = cert,
+      tags = [],
+      maxidx = maxidx,
+      constraints = [],
+      shyps = sorts,
+      hyps = [],
+      tpairs = [],
+      prop = Logic.mk_equals (t, t)})
+  end;
 
 (*Symmetry
   t \<equiv> u
@@ -1359,16 +1390,18 @@
 *)
 fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
   (case prop of
-    (eq as Const ("Pure.eq", _)) $ t $ u =>
-      Thm (deriv_rule1 (Proofterm.symmetric_proof, ZTerm.todo_proof) der,
-       {cert = cert,
-        tags = [],
-        maxidx = maxidx,
-        constraints = constraints,
-        shyps = shyps,
-        hyps = hyps,
-        tpairs = tpairs,
-        prop = eq $ u $ t})
+    (eq as Const ("Pure.eq", Type ("fun", [T, _]))) $ t $ u =>
+      let fun zprf prf = ZTerm.symmetric_proof (Context.certificate_theory cert) T t u prf in
+        Thm (deriv_rule1 (Proofterm.symmetric_proof, zprf) der,
+         {cert = cert,
+          tags = [],
+          maxidx = maxidx,
+          constraints = constraints,
+          shyps = shyps,
+          hyps = hyps,
+          tpairs = tpairs,
+          prop = eq $ u $ t})
+      end
     | _ => raise THM ("symmetric", 0, [th]));
 
 (*Transitivity
@@ -1385,33 +1418,41 @@
     fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
   in
     case (prop1, prop2) of
-      ((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
+      ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
         if not (u aconv u') then err "middle term"
         else
-          Thm (deriv_rule2 (Proofterm.transitive_proof U u, K ZTerm.todo_proof) der1 der2,
-           {cert = join_certificate2 (th1, th2),
-            tags = [],
-            maxidx = Int.max (maxidx1, maxidx2),
-            constraints = union_constraints constraints1 constraints2,
-            shyps = Sorts.union shyps1 shyps2,
-            hyps = union_hyps hyps1 hyps2,
-            tpairs = union_tpairs tpairs1 tpairs2,
-            prop = eq $ t1 $ t2})
-     | _ =>  err "premises"
+          let
+            val cert = join_certificate2 (th1, th2);
+            fun zprf prf1 prf2 =
+              ZTerm.transitive_proof (Context.certificate_theory cert) T t1 u t2 prf1 prf2;
+          in
+            Thm (deriv_rule2 (Proofterm.transitive_proof T u, zprf) der1 der2,
+             {cert = cert,
+              tags = [],
+              maxidx = Int.max (maxidx1, maxidx2),
+              constraints = union_constraints constraints1 constraints2,
+              shyps = Sorts.union shyps1 shyps2,
+              hyps = union_hyps hyps1 hyps2,
+              tpairs = union_tpairs tpairs1 tpairs2,
+              prop = eq $ t1 $ t2})
+          end
+     | _ => err "premises"
   end;
 
 (*Beta-conversion
   (\<lambda>x. t) u \<equiv> t[u/x]
   fully beta-reduces the term if full = true
 *)
-fun beta_conversion full (Cterm {cert, t, T = _, maxidx, sorts}) =
-  let val t' =
-    if full then Envir.beta_norm t
-    else
-      (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
-      | _ => raise THM ("beta_conversion: not a redex", 0, []));
+fun beta_conversion full (Cterm {cert, t, T, maxidx, sorts}) =
+  let
+    val t' =
+      if full then Envir.beta_norm t
+      else
+        (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
+        | _ => raise THM ("beta_conversion: not a redex", 0, []));
+    fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t;
   in
-    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
+    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -1422,27 +1463,31 @@
       prop = Logic.mk_equals (t, t')})
   end;
 
-fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
-   {cert = cert,
-    tags = [],
-    maxidx = maxidx,
-    constraints = [],
-    shyps = sorts,
-    hyps = [],
-    tpairs = [],
-    prop = Logic.mk_equals (t, Envir.eta_contract t)});
+fun eta_conversion (Cterm {cert, t, T, maxidx, sorts}) =
+  let fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t in
+    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf),
+     {cert = cert,
+      tags = [],
+      maxidx = maxidx,
+      constraints = [],
+      shyps = sorts,
+      hyps = [],
+      tpairs = [],
+      prop = Logic.mk_equals (t, Envir.eta_contract t)})
+  end;
 
-fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
-  Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
-   {cert = cert,
-    tags = [],
-    maxidx = maxidx,
-    constraints = [],
-    shyps = sorts,
-    hyps = [],
-    tpairs = [],
-    prop = Logic.mk_equals (t, Envir.eta_long [] t)});
+fun eta_long_conversion (Cterm {cert, t, T, maxidx, sorts}) =
+  let fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t in
+    Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf),
+     {cert = cert,
+      tags = [],
+      maxidx = maxidx,
+      constraints = [],
+      shyps = sorts,
+      hyps = [],
+      tpairs = [],
+      prop = Logic.mk_equals (t, Envir.eta_long [] t)})
+  end;
 
 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   The bound variable will be named "a" (since x will be something like x320)
@@ -1454,22 +1499,30 @@
     (Cterm {t = x, T, sorts, ...})
     (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) =
   let
-    val (t, u) = Logic.dest_equals prop
-      handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
+    val (U, t, u) =
+      (case prop of
+        Const ("Pure.eq", Type ("fun", [U, _])) $ t $ u => (U, t, u)
+      | _ => raise THM ("abstract_rule: premise not an equality", 0, [th]));
     fun check_result a ts =
       if occs x ts tpairs then
         raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th])
       else
-        Thm (deriv_rule1 (Proofterm.abstract_rule_proof (b, x), ZTerm.todo_proof) der,
-         {cert = cert,
-          tags = [],
-          maxidx = maxidx,
-          constraints = constraints,
-          shyps = Sorts.union sorts shyps,
-          hyps = hyps,
-          tpairs = tpairs,
-          prop = Logic.mk_equals
-            (Abs (b, T, abstract_over (x, t)), Abs (b, T, abstract_over (x, u)))});
+        let
+          val f = Abs (b, T, abstract_over (x, t));
+          val g = Abs (b, T, abstract_over (x, u));
+          fun zprf prf =
+            ZTerm.abstract_rule_proof (Context.certificate_theory cert) T U (b, x) f g prf;
+        in
+          Thm (deriv_rule1 (Proofterm.abstract_rule_proof (b, x), zprf) der,
+           {cert = cert,
+            tags = [],
+            maxidx = maxidx,
+            constraints = constraints,
+            shyps = Sorts.union sorts shyps,
+            hyps = hyps,
+            tpairs = tpairs,
+            prop = Logic.mk_equals (f, g)})
+        end;
   in
     (case x of
       Free (a, _) => check_result a hyps
@@ -1488,27 +1541,31 @@
         hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1
     and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
         hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2;
-    fun chktypes fT tT =
-      (case fT of
-        Type ("fun", [T1, _]) =>
-          if T1 <> tT then
-            raise THM ("combination: types", 0, [th1, th2])
-          else ()
-      | _ => raise THM ("combination: not function type", 0, [th1, th2]));
   in
     (case (prop1, prop2) of
       (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
        Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
-        (chktypes fT tT;
-          Thm (deriv_rule2 (Proofterm.combination_proof f g t u, K ZTerm.todo_proof) der1 der2,
-           {cert = join_certificate2 (th1, th2),
+        let
+          val U =
+            (case fT of
+              Type ("fun", [T1, U]) =>
+                if T1 = tT then U
+                else raise THM ("combination: types", 0, [th1, th2])
+            | _ => raise THM ("combination: not function type", 0, [th1, th2]));
+          val cert = join_certificate2 (th1, th2);
+          fun zprf prf1 prf2 =
+            ZTerm.combination_proof (Context.certificate_theory cert) fT U f g t u prf1 prf2;
+        in
+          Thm (deriv_rule2 (Proofterm.combination_proof f g t u, zprf) der1 der2,
+           {cert = cert,
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
             constraints = union_constraints constraints1 constraints2,
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,
-            prop = Logic.mk_equals (f $ t, g $ u)}))
+            prop = Logic.mk_equals (f $ t, g $ u)})
+        end
      | _ => raise THM ("combination: premises", 0, [th1, th2]))
   end;
 
@@ -1528,15 +1585,21 @@
     (case (prop1, prop2) of
       (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
         if A aconv A' andalso B aconv B' then
-          Thm (deriv_rule2 (Proofterm.equal_intr_proof A B, K ZTerm.todo_proof) der1 der2,
-           {cert = join_certificate2 (th1, th2),
-            tags = [],
-            maxidx = Int.max (maxidx1, maxidx2),
-            constraints = union_constraints constraints1 constraints2,
-            shyps = Sorts.union shyps1 shyps2,
-            hyps = union_hyps hyps1 hyps2,
-            tpairs = union_tpairs tpairs1 tpairs2,
-            prop = Logic.mk_equals (A, B)})
+          let
+            val cert = join_certificate2 (th1, th2);
+            fun zprf prf1 prf2 =
+              ZTerm.equal_intr_proof (Context.certificate_theory cert) A B prf1 prf2;
+          in
+            Thm (deriv_rule2 (Proofterm.equal_intr_proof A B, zprf) der1 der2,
+             {cert = cert,
+              tags = [],
+              maxidx = Int.max (maxidx1, maxidx2),
+              constraints = union_constraints constraints1 constraints2,
+              shyps = Sorts.union shyps1 shyps2,
+              hyps = union_hyps hyps1 hyps2,
+              tpairs = union_tpairs tpairs1 tpairs2,
+              prop = Logic.mk_equals (A, B)})
+          end
         else err "not equal"
     | _ =>  err "premises")
   end;
@@ -1557,15 +1620,21 @@
     (case prop1 of
       Const ("Pure.eq", _) $ A $ B =>
         if prop2 aconv A then
-          Thm (deriv_rule2 (Proofterm.equal_elim_proof A B, K ZTerm.todo_proof) der1 der2,
-           {cert = join_certificate2 (th1, th2),
-            tags = [],
-            maxidx = Int.max (maxidx1, maxidx2),
-            constraints = union_constraints constraints1 constraints2,
-            shyps = Sorts.union shyps1 shyps2,
-            hyps = union_hyps hyps1 hyps2,
-            tpairs = union_tpairs tpairs1 tpairs2,
-            prop = B})
+          let
+            val cert = join_certificate2 (th1, th2);
+            fun zprf prf1 prf2 =
+              ZTerm.equal_elim_proof (Context.certificate_theory cert) A B prf1 prf2;
+          in
+            Thm (deriv_rule2 (Proofterm.equal_elim_proof A B, zprf) der1 der2,
+             {cert = cert,
+              tags = [],
+              maxidx = Int.max (maxidx1, maxidx2),
+              constraints = union_constraints constraints1 constraints2,
+              shyps = Sorts.union shyps1 shyps2,
+              hyps = union_hyps hyps1 hyps2,
+              tpairs = union_tpairs tpairs1 tpairs2,
+              prop = B})
+          end
         else err "not equal"
      | _ =>  err "major premise")
   end;
@@ -1784,15 +1853,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 486a32079c60 -r e475d6ac8eb1 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Dec 02 20:49:50 2023 +0000
+++ b/src/Pure/zterm.ML	Mon Dec 04 23:12:47 2023 +0100
@@ -4,11 +4,12 @@
 Tight representation of types / terms / proof terms, notably for proof recording.
 *)
 
-(* global datatypes *)
+(*** global ***)
+
+(* types and terms *)
 
 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 +18,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*)
@@ -27,54 +27,42 @@
   | ZApp of zterm * zterm
   | ZClass of ztyp * class         (*OFCLASS proposition*)
 
-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
-  | ZAbsP of string * zterm * zproof
-  | ZAppt of zproof * zterm
-  | ZAppP of zproof * zproof
-  | ZClassP of ztyp * class        (*OFCLASS proof from sorts algebra*)
-  | ZOracle of serial * zterm * ztyp list
+structure ZTerm =
+struct
+
+(* 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;
 
 
-signature ZTERM =
-sig
-  datatype ztyp = datatype ztyp
-  datatype zterm = datatype zterm
-  datatype zproof = datatype zproof
-  val ztyp_ord: ztyp * ztyp -> order
-  val zaconv: 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 dummy_proof: 'a -> zproof
-  val todo_proof: 'a -> zproof
-end;
-
-structure ZTerm: ZTERM =
-struct
-
-datatype ztyp = datatype ztyp;
-datatype zterm = datatype zterm;
-datatype zproof = datatype zproof;
-
-
-(* orderings *)
+(* ordering *)
 
 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 +73,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
@@ -102,27 +88,127 @@
 
 end;
 
+end;
 
-(* alpha conversion *)
+
+(* term items *)
+
+structure ZTVars:
+sig
+  include TERM_ITEMS
+  val add_tvarsT: ztyp -> set -> set
+  val add_tvars: zterm -> set -> set
+end =
+struct
+  open TVars;
+  val add_tvarsT = ZTerm.fold_tvars add_set;
+  val add_tvars = ZTerm.fold_types add_tvarsT;
+end;
+
+structure ZVars:
+sig
+  include TERM_ITEMS
+  val add_vars: zterm -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+  type key = indexname * ztyp;
+  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord ZTerm.ztyp_ord);
+);
+open Term_Items;
+
+val add_vars = ZTerm.fold_aterms (fn ZVar v => add_set v | _ => I);
+
+end;
+
+
+(* proofs *)
+
+datatype zproof =
+    ZDummy                         (*dummy proof*)
+  | ZBoundP of int
+  | ZHyp of zterm
+  | ZAbst of string * ztyp * zproof
+  | ZAbsP of string * zterm * zproof
+  | ZAppt of zproof * zterm
+  | ZAppP of zproof * zproof
+  | ZClassP of ztyp * class        (*OFCLASS proof from sorts algebra*)
+  | ZAxiom of {name: string, oracle: bool} * zterm * (ztyp ZTVars.table * zterm ZVars.table);
+
 
-fun zaconv (tm1, tm2) =
+
+(*** local ***)
+
+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
+  val ztyp_ord: ztyp * ztyp -> order
+  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 -> typ -> string * term -> zproof -> zproof
+  val forall_elim_proof: theory -> term -> zproof -> zproof
+  val reflexive_proof: theory -> typ -> term -> zproof
+  val symmetric_proof: theory -> typ -> term -> term -> zproof -> zproof
+  val transitive_proof: theory -> typ -> term -> term -> term -> zproof -> zproof -> zproof
+  val equal_intr_proof: theory -> term -> term -> zproof -> zproof -> zproof
+  val equal_elim_proof: theory -> term -> term -> zproof -> zproof -> zproof
+  val abstract_rule_proof: theory -> typ -> typ -> string * term -> term -> term -> zproof -> zproof
+  val combination_proof: theory -> typ -> typ -> term -> term -> term -> term ->
+    zproof -> zproof -> zproof
+end;
+
+structure ZTerm: ZTERM =
+struct
+
+datatype ztyp = datatype ztyp;
+datatype zterm = datatype zterm;
+datatype zproof = datatype zproof;
+
+open ZTerm;
+
+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);
 
 
+(* instantiation *)
+
+fun init_instT t = ZTVars.build (ZTVars.add_tvars t) |> ZTVars.map (fn v => fn _ => ZTVar v);
+fun init_inst t = ZVars.build (ZVars.add_vars t) |> ZVars.map (fn v => fn _ => ZVar v);
+fun init_insts t = (init_instT t, init_inst t);
+
+
 (* 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 +220,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 +240,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 +251,159 @@
       | 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;
 
+
+(* basic logic *)
+
+fun axiom_proof thy a A =
+  let
+    val t = global_zterm_of thy A;
+    val insts = init_insts t;
+  in ZAxiom (a, t, insts) 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 T (a, x) prf =
+  let
+    val Z = ztyp_of T;
+    val z = global_zterm_of thy x;
+
+    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 abs_proof i (ZAbst (x, T, prf)) = ZAbst (x, T, abs_proof (i + 1) prf)
+      | abs_proof i (ZAbsP (x, t, prf)) = ZAbsP (x, abs_term i t, abs_proof i prf)
+      | abs_proof i (ZAppt (p, t)) = ZAppt (abs_proof i p, abs_term i t)
+      | abs_proof i (ZAppP (p, q)) = ZAppP (abs_proof i p, abs_proof i q)
+      | abs_proof _ p = p;
+
+  in ZAbst (a, Z, abs_proof 0 prf) end;
+
+fun forall_elim_proof thy t p = ZAppt (p, global_zterm_of thy t);
+
+
+(* equality *)
+
+local
+
+val thy0 =
+  Context.the_global_context ()
+  |> Sign.add_types_global [(Binding.name "fun", 2, NoSyn), (Binding.name "prop", 0, NoSyn)]
+  |> Sign.local_path
+  |> Sign.add_consts
+   [(Binding.name "all", (Term.aT [] --> propT) --> propT, NoSyn),
+    (Binding.name "imp", propT --> propT --> propT, NoSyn),
+    (Binding.name "eq", Term.aT [] --> Term.aT [] --> propT, NoSyn)];
+
+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 {name = Sign.full_name thy0 b, oracle = false} t);
+
+fun inst_axiom (f, g) (ZAxiom (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 ZAxiom (a, A, (instT', inst')) end;
+
+in
+
+val is_reflexive_proof =
+  fn ZAxiom ({name = "Pure.reflexive", oracle = false}, _, _) => true | _ => false;
+
+fun reflexive_proof thy T t =
+  let
+    val A = ztyp_of T;
+    val x = global_zterm_of thy t;
+  in inst_axiom (fn "'a" => A, fn "x" => x) reflexive_axiom end;
+
+fun symmetric_proof thy T t u prf =
+  if is_reflexive_proof prf then prf
+  else
+    let
+      val A = ztyp_of T;
+      val x = global_zterm_of thy t;
+      val y = global_zterm_of thy u;
+      val ax = inst_axiom (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 =
+  if is_reflexive_proof prf1 then prf2
+  else if is_reflexive_proof prf2 then prf1
+  else
+    let
+      val A = ztyp_of T;
+      val x = global_zterm_of thy t;
+      val y = global_zterm_of thy u;
+      val z = global_zterm_of thy v;
+      val ax = inst_axiom (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 =
+  let
+    val A = global_zterm_of thy t;
+    val B = global_zterm_of thy u;
+    val ax = inst_axiom (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 =
+  let
+    val A = global_zterm_of thy t;
+    val B = global_zterm_of thy u;
+    val ax = inst_axiom (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 =
+  let
+    val A = ztyp_of T;
+    val B = ztyp_of U;
+    val f = global_zterm_of thy t;
+    val g = global_zterm_of thy u;
+    val ax = inst_axiom (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g) abstract_rule_axiom;
+  in ZAppP (ax, forall_intr_proof thy T x prf) end;
+
+fun combination_proof thy T U f g t u prf1 prf2 =
+  let
+    val A = ztyp_of T;
+    val B = ztyp_of U;
+    val f' = global_zterm_of thy f;
+    val g' = global_zterm_of thy g;
+    val x = global_zterm_of thy t;
+    val y = global_zterm_of thy u;
+    val ax =
+      inst_axiom (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y)
+        combination_axiom;
+  in ZAppP (ZAppP (ax, prf1), prf2) end;
+
 end;
+
+end;