--- a/src/Pure/thm.ML Sat Dec 02 20:21:56 2023 +0100
+++ b/src/Pure/thm.ML Mon Dec 04 10:53:32 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) (a, x) T 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]));
@@ -1784,15 +1813,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:21:56 2023 +0100
+++ b/src/Pure/zterm.ML Mon Dec 04 10:53:32 2023 +0100
@@ -7,8 +7,7 @@
(* global datatypes *)
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 +16,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*)
@@ -29,7 +27,6 @@
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
@@ -37,22 +34,40 @@
| ZAppt of zproof * zterm
| ZAppP of zproof * zproof
| ZClassP of ztyp * class (*OFCLASS proof from sorts algebra*)
- | ZOracle of serial * zterm * ztyp list
+ | 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 zaconv: zterm * zterm -> bool
+ 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 =
@@ -63,18 +78,51 @@
datatype zproof = datatype zproof;
+(* 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;
+
+
+(* 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 *)
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 +133,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
@@ -105,24 +151,24 @@
(* alpha conversion *)
-fun zaconv (tm1, tm2) =
+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);
(* 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 +180,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 +200,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 +211,60 @@
| 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;
+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;
+
+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 (a, x) T prf =
+ let
+ 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
+ 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 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;
+
+ in ZAbst (a, Z, abd_proof 0 prf) end;
+
+fun forall_elim_proof thy t p = ZAppt (p, global_zterm_of thy t);
+
end;