--- a/src/Pure/thm.ML Mon Dec 04 22:39:57 2023 +0100
+++ b/src/Pure/thm.ML Mon Dec 04 23:07:06 2023 +0100
@@ -1316,7 +1316,7 @@
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;
+ fun zprf p = ZTerm.forall_intr_proof (Context.certificate_theory cert) T (a, x) p;
in
Thm (deriv_rule1 (prf, zprf) der,
{cert = cert,
@@ -1370,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
@@ -1388,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
@@ -1414,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,
@@ -1451,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)
@@ -1483,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
@@ -1517,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;
@@ -1557,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;
@@ -1586,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;
--- a/src/Pure/zterm.ML Mon Dec 04 22:39:57 2023 +0100
+++ b/src/Pure/zterm.ML Mon Dec 04 23:07:06 2023 +0100
@@ -4,7 +4,9 @@
Tight representation of types / terms / proof terms, notably for proof recording.
*)
-(* global datatypes *)
+(*** global ***)
+
+(* types and terms *)
datatype ztyp =
ZTVar of indexname * sort (*free: index ~1*)
@@ -25,59 +27,9 @@
| ZApp of zterm * zterm
| ZClass of ztyp * class (*OFCLASS proposition*)
-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 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 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 =
+structure ZTerm =
struct
-datatype ztyp = datatype ztyp;
-datatype zterm = datatype zterm;
-datatype zproof = datatype zproof;
-
-
(* fold *)
fun fold_tvars f (ZTVar v) = f v
@@ -100,19 +52,7 @@
| 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 *)
+(* ordering *)
local
@@ -148,8 +88,101 @@
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);
+
+
+
+(*** 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
@@ -159,6 +192,13 @@
| (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 (a, S)) = ZTVar ((a, ~1), S)
@@ -221,11 +261,14 @@
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 Ts = make_tvars t;
- in ZAxiom (a, t, map ZTVar Ts) end;
+ val insts = init_insts t;
+ in ZAxiom (a, t, insts) end;
fun assume_proof thy A =
ZHyp (global_zterm_of thy A);
@@ -244,10 +287,10 @@
| abs_hyp _ p = p;
in ZAbsP ("H", h, abs_hyp 0 prf) end;
-fun forall_intr_proof thy (a, x) T prf =
+fun forall_intr_proof thy T (a, x) prf =
let
+ val Z = ztyp_of T;
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
@@ -257,14 +300,110 @@
| 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;
+ 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, abd_proof 0 prf) end;
+ 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;