--- 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;