# HG changeset patch
# User wenzelm
# Date 1702057878 -3600
# Node ID 601aa36071ba70c80e7c148ae1cbf1fa1c3b9041
# Parent  35ead2206eb1a9b40aa90b9e21c9e5d9f2325446
clarified signature;

diff -r 35ead2206eb1 -r 601aa36071ba src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 08 18:40:31 2023 +0100
+++ b/src/Pure/thm.ML	Fri Dec 08 18:51:18 2023 +0100
@@ -1280,7 +1280,7 @@
     (case prop of
       Const ("Pure.imp", _) $ A $ B =>
         if A aconv propA then
-          Thm (deriv_rule2 (curry Proofterm.%%, curry ZAppP) der derA,
+          Thm (deriv_rule2 (curry Proofterm.%%, curry ZAppp) der derA,
            {cert = join_certificate2 (thAB, thA),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
diff -r 35ead2206eb1 -r 601aa36071ba src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Fri Dec 08 18:40:31 2023 +0100
+++ b/src/Pure/zterm.ML	Fri Dec 08 18:51:18 2023 +0100
@@ -135,14 +135,14 @@
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
-  | ZConstP of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
-  | ZBoundP of int
+  | ZConstp of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
+  | ZBoundp of int
   | ZHyp of zterm
   | ZAbst of string * ztyp * zproof
-  | ZAbsP of string * zterm * zproof
+  | ZAbsp of string * zterm * zproof
   | ZAppt of zproof * zterm
-  | ZAppP of zproof * zproof
-  | ZClassP of ztyp * class;       (*OFCLASS proof from sorts algebra*)
+  | ZAppp of zproof * zproof
+  | ZClassp of ztyp * class;       (*OFCLASS proof from sorts algebra*)
 
 
 
@@ -158,6 +158,10 @@
   val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
   val ztyp_ord: ztyp * ztyp -> order
   val aconv_zterm: zterm * zterm -> bool
+  val ZAbsts: (string * ztyp) list -> zproof -> zproof
+  val ZAbsps: zterm list -> zproof -> zproof
+  val ZAppts: zproof * zterm list -> zproof
+  val ZAppps: zproof * zproof list -> zproof
   val incr_bv_same: int -> int -> zterm Same.operation
   val incr_bv: int -> int -> zterm -> zterm
   val incr_boundvars: int -> zterm -> zterm
@@ -220,11 +224,11 @@
 
 (* derived operations *)
 
-val mk_ZAbst = fold_rev (fn (x, T) => fn prf => ZAbst (x, T, prf));
-val mk_ZAbsP = fold_rev (fn t => fn prf => ZAbsP ("H", t, prf));
+val ZAbsts = fold_rev (fn (x, T) => fn prf => ZAbst (x, T, prf));
+val ZAbsps = fold_rev (fn t => fn prf => ZAbsp ("H", t, prf));
 
-val mk_ZAppt = Library.foldl ZAppt;
-val mk_ZAppP = Library.foldl ZAppP;
+val ZAppts = Library.foldl ZAppt;
+val ZAppps = Library.foldl ZAppp;
 
 
 (* substitution of bound variables *)
@@ -326,20 +330,20 @@
 fun map_proof_same typ term =
   let
     fun proof ZDummy = raise Same.SAME
-      | proof (ZConstP (a, A, instT, inst)) =
+      | proof (ZConstp (a, A, instT, inst)) =
           let val (instT', inst') = map_insts_same typ term (instT, inst)
-          in ZConstP (a, A, instT', inst') end
-      | proof (ZBoundP _) = raise Same.SAME
+          in ZConstp (a, A, instT', inst') end
+      | proof (ZBoundp _) = raise Same.SAME
       | proof (ZHyp h) = ZHyp (term h)
       | proof (ZAbst (a, T, p)) =
           (ZAbst (a, typ T, Same.commit proof p) handle Same.SAME => ZAbst (a, T, proof p))
-      | proof (ZAbsP (a, t, p)) =
-          (ZAbsP (a, term t, Same.commit proof p) handle Same.SAME => ZAbsP (a, t, proof p))
+      | proof (ZAbsp (a, t, p)) =
+          (ZAbsp (a, term t, Same.commit proof p) handle Same.SAME => ZAbsp (a, t, proof p))
       | proof (ZAppt (p, t)) =
           (ZAppt (proof p, Same.commit term t) handle Same.SAME => ZAppt (p, term t))
-      | proof (ZAppP (p, q)) =
-          (ZAppP (proof p, Same.commit proof q) handle Same.SAME => ZAppP (p, proof q))
-      | proof (ZClassP (T, c)) = ZClassP (typ T, c);
+      | proof (ZAppp (p, q)) =
+          (ZAppp (proof p, Same.commit proof q) handle Same.SAME => ZAppp (p, proof q))
+      | proof (ZClassp (T, c)) = ZClassp (typ T, c);
   in proof end;
 
 fun map_proof_types_same typ =
@@ -504,15 +508,15 @@
         (case a of
           ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, a) tab
         | _ => tab)));
-  in ZConstP (a, t, instT, inst) end;
+  in ZConstp (a, t, instT, inst) end;
 
 fun map_const_proof (f, g) prf =
   (case prf of
-    ZConstP (a, A, instT, inst) =>
+    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
+      in ZConstp (a, A, instT', inst') end
   | _ => prf);
 
 
@@ -528,20 +532,20 @@
   ZHyp (zterm_of thy A);
 
 fun trivial_proof thy A =
-  ZAbsP ("H", zterm_of thy A, ZBoundP 0);
+  ZAbsp ("H", zterm_of thy A, ZBoundp 0);
 
 fun implies_intr_proof thy A prf =
   let
     val h = zterm_of thy A;
-    fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else raise Same.SAME
+    fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundp i else raise Same.SAME
       | proof i (ZAbst (x, T, p)) = ZAbst (x, T, proof i p)
-      | proof i (ZAbsP (x, t, p)) = ZAbsP (x, t, proof (i + 1) p)
+      | proof i (ZAbsp (x, t, p)) = ZAbsp (x, t, proof (i + 1) p)
       | proof i (ZAppt (p, t)) = ZAppt (proof i p, t)
-      | proof i (ZAppP (p, q)) =
-          (ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME =>
-            ZAppP (p, proof i q))
+      | proof i (ZAppp (p, q)) =
+          (ZAppp (proof i p, Same.commit (proof i) q) handle Same.SAME =>
+            ZAppp (p, proof i q))
       | proof _ _ = raise Same.SAME;
-  in ZAbsP ("H", h, Same.commit (proof 0) prf) end;
+  in ZAbsp ("H", h, Same.commit (proof 0) prf) end;
 
 fun forall_intr_proof thy T (a, x) prf =
   let
@@ -560,22 +564,22 @@
         | _ => raise Same.SAME);
 
     fun proof i (ZAbst (x, T, prf)) = ZAbst (x, T, proof (i + 1) prf)
-      | proof i (ZAbsP (x, t, prf)) =
-          (ZAbsP (x, term i t, Same.commit (proof i) prf) handle Same.SAME =>
-            ZAbsP (x, t, proof i prf))
+      | proof i (ZAbsp (x, t, prf)) =
+          (ZAbsp (x, term i t, Same.commit (proof i) prf) handle Same.SAME =>
+            ZAbsp (x, t, proof i prf))
       | proof i (ZAppt (p, t)) =
           (ZAppt (proof i p, Same.commit (term i) t) handle Same.SAME =>
             ZAppt (p, term i t))
-      | proof i (ZAppP (p, q)) =
-          (ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME =>
-            ZAppP (p, proof i q))
+      | proof i (ZAppp (p, q)) =
+          (ZAppp (proof i p, Same.commit (proof i) q) handle Same.SAME =>
+            ZAppp (p, proof i q))
       | proof _ _ = raise Same.SAME;
 
   in ZAbst (a, Z, Same.commit (proof 0) prf) end;
 
 fun forall_elim_proof thy t p = ZAppt (p, zterm_of thy t);
 
-fun of_class_proof (T, c) = ZClassP (ztyp_of T, c);
+fun of_class_proof (T, c) = ZClassp (ztyp_of T, c);
 
 
 (* equality *)
@@ -598,7 +602,7 @@
 in
 
 val is_reflexive_proof =
-  fn ZConstP (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false;
+  fn ZConstp (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false;
 
 fun reflexive_proof thy T t =
   let
@@ -616,7 +620,7 @@
       val x = zterm t;
       val y = zterm u;
       val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
-    in ZAppP (ax, prf) end;
+    in ZAppp (ax, prf) end;
 
 fun transitive_proof thy T t u v prf1 prf2 =
   if is_reflexive_proof prf1 then prf2
@@ -629,7 +633,7 @@
       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;
-    in ZAppP (ZAppP (ax, prf1), prf2) end;
+    in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun equal_intr_proof thy t u prf1 prf2 =
   let
@@ -637,7 +641,7 @@
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
-  in ZAppP (ZAppP (ax, prf1), prf2) end;
+  in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun equal_elim_proof thy t u prf1 prf2 =
   let
@@ -645,7 +649,7 @@
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
-  in ZAppP (ZAppP (ax, prf1), prf2) end;
+  in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun abstract_rule_proof thy T U x t u prf =
   let
@@ -657,7 +661,7 @@
     val ax =
       map_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;
+  in ZAppp (ax, forall_intr_proof thy T x prf) end;
 
 fun combination_proof thy T U f g t u prf1 prf2 =
   let
@@ -671,7 +675,7 @@
     val ax =
       map_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;
+  in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 end;
 
@@ -741,10 +745,10 @@
     val i = length asms;
     val j = length Bs;
   in
-    mk_ZAbsP (map zterm Bs @ [zterm Bi']) (mk_ZAppP (prf, map ZBoundP
-      (j downto 1) @ [mk_ZAbst (map (apsnd ztyp) params) (mk_ZAbsP (map zterm asms)
-        (mk_ZAppP (mk_ZAppt (ZBoundP i, map ZBound ((length params - 1) downto 0)),
-          map ZBoundP (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
+    ZAbsps (map zterm Bs @ [zterm Bi']) (ZAppps (prf, map ZBoundp
+      (j downto 1) @ [ZAbsts (map (apsnd ztyp) params) (ZAbsps (map zterm asms)
+        (ZAppps (ZAppts (ZBoundp i, map ZBound ((length params - 1) downto 0)),
+          map ZBoundp (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   end;
 
 fun permute_prems_proof thy prems' j k prf =
@@ -752,8 +756,8 @@
     val {zterm, ...} = zterm_cache thy;
     val n = length prems';
   in
-    mk_ZAbsP (map zterm prems')
-      (mk_ZAppP (prf, map ZBoundP ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+    ZAbsps (map zterm prems')
+      (ZAppps (prf, map ZBoundp ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
   end;
 
 
@@ -761,9 +765,9 @@
 
 fun mk_asm_prf C i m =
   let
-    fun imp _ i 0 = ZBoundP i
-      | imp (ZApp (ZApp (ZConst0 "Pure.imp", A), B)) i m = ZAbsP ("H", A, imp B (i + 1) (m - 1))
-      | imp _ i _ = ZBoundP i;
+    fun imp _ i 0 = ZBoundp i
+      | imp (ZApp (ZApp (ZConst0 "Pure.imp", A), B)) i m = ZAbsp ("H", A, imp B (i + 1) (m - 1))
+      | imp _ i _ = ZBoundp i;
     fun all (ZApp (ZConst1 ("Pure.all", _), ZAbs (a, T, t))) = ZAbst (a, T, all t)
       | all t = imp t (~ i) m
   in all C end;
@@ -773,8 +777,8 @@
     val cache as {zterm, ...} = norm_cache thy;
     val normt = zterm #> Same.commit (norm_term_same cache envir);
   in
-    mk_ZAbsP (map normt Bs)
-      (mk_ZAppP (prf, map ZBoundP (length Bs - 1 downto 0) @ [mk_asm_prf (normt Bi) n ~1]))
+    ZAbsps (map normt Bs)
+      (ZAppps (prf, map ZBoundp (length Bs - 1 downto 0) @ [mk_asm_prf (normt Bi) n ~1]))
     |> Same.commit (norm_proof_same cache envir)
   end;