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