author | clasohm |
Wed, 14 Dec 1994 11:41:49 +0100 | |
changeset 782 | 200a16083201 |
parent 760 | f0200e91b272 |
child 803 | 4c8333ab3eae |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/quniv |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
For quniv.thy. A small universe for lazy recursive types |
|
7 |
*) |
|
8 |
||
9 |
open QUniv; |
|
10 |
||
11 |
(** Introduction and elimination rules avoid tiresome folding/unfolding **) |
|
12 |
||
13 |
goalw QUniv.thy [quniv_def] |
|
14 |
"!!X A. X <= univ(eclose(A)) ==> X : quniv(A)"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
15 |
by (etac PowI 1); |
760 | 16 |
qed "qunivI"; |
0 | 17 |
|
18 |
goalw QUniv.thy [quniv_def] |
|
19 |
"!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
20 |
by (etac PowD 1); |
760 | 21 |
qed "qunivD"; |
0 | 22 |
|
23 |
goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)"; |
|
24 |
by (etac (eclose_mono RS univ_mono RS Pow_mono) 1); |
|
760 | 25 |
qed "quniv_mono"; |
0 | 26 |
|
27 |
(*** Closure properties ***) |
|
28 |
||
29 |
goalw QUniv.thy [quniv_def] "univ(eclose(A)) <= quniv(A)"; |
|
30 |
by (rtac (Transset_iff_Pow RS iffD1) 1); |
|
31 |
by (rtac (Transset_eclose RS Transset_univ) 1); |
|
760 | 32 |
qed "univ_eclose_subset_quniv"; |
0 | 33 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
34 |
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*) |
0 | 35 |
goal QUniv.thy "univ(A) <= quniv(A)"; |
36 |
by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1); |
|
37 |
by (rtac univ_eclose_subset_quniv 1); |
|
760 | 38 |
qed "univ_subset_quniv"; |
0 | 39 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
40 |
bind_thm ("univ_into_quniv", (univ_subset_quniv RS subsetD)); |
0 | 41 |
|
42 |
goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)"; |
|
43 |
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1); |
|
760 | 44 |
qed "Pow_univ_subset_quniv"; |
0 | 45 |
|
46 |
val univ_subset_into_quniv = standard |
|
47 |
(PowI RS (Pow_univ_subset_quniv RS subsetD)); |
|
48 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
49 |
bind_thm ("zero_in_quniv", (zero_in_univ RS univ_into_quniv)); |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
50 |
bind_thm ("one_in_quniv", (one_in_univ RS univ_into_quniv)); |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
51 |
bind_thm ("two_in_quniv", (two_in_univ RS univ_into_quniv)); |
0 | 52 |
|
53 |
val A_subset_quniv = standard |
|
54 |
([A_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
55 |
||
56 |
val A_into_quniv = A_subset_quniv RS subsetD; |
|
57 |
||
58 |
(*** univ(A) closure for Quine-inspired pairs and injections ***) |
|
59 |
||
60 |
(*Quine ordered pairs*) |
|
61 |
goalw QUniv.thy [QPair_def] |
|
62 |
"!!A a. [| a <= univ(A); b <= univ(A) |] ==> <a;b> <= univ(A)"; |
|
63 |
by (REPEAT (ares_tac [sum_subset_univ] 1)); |
|
760 | 64 |
qed "QPair_subset_univ"; |
0 | 65 |
|
66 |
(** Quine disjoint sum **) |
|
67 |
||
68 |
goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)"; |
|
69 |
by (etac (empty_subsetI RS QPair_subset_univ) 1); |
|
760 | 70 |
qed "QInl_subset_univ"; |
0 | 71 |
|
72 |
val naturals_subset_nat = |
|
73 |
rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset) |
|
74 |
RS bspec; |
|
75 |
||
76 |
val naturals_subset_univ = |
|
77 |
[naturals_subset_nat, nat_subset_univ] MRS subset_trans; |
|
78 |
||
79 |
goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)"; |
|
80 |
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1); |
|
760 | 81 |
qed "QInr_subset_univ"; |
0 | 82 |
|
83 |
(*** Closure for Quine-inspired products and sums ***) |
|
84 |
||
85 |
(*Quine ordered pairs*) |
|
86 |
goalw QUniv.thy [quniv_def,QPair_def] |
|
87 |
"!!A a. [| a: quniv(A); b: quniv(A) |] ==> <a;b> : quniv(A)"; |
|
88 |
by (REPEAT (dtac PowD 1)); |
|
89 |
by (REPEAT (ares_tac [PowI, sum_subset_univ] 1)); |
|
760 | 90 |
qed "QPair_in_quniv"; |
0 | 91 |
|
92 |
goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)"; |
|
93 |
by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1 |
|
94 |
ORELSE eresolve_tac [QSigmaE, ssubst] 1)); |
|
760 | 95 |
qed "QSigma_quniv"; |
0 | 96 |
|
97 |
val QSigma_subset_quniv = standard |
|
98 |
(QSigma_mono RS (QSigma_quniv RSN (2,subset_trans))); |
|
99 |
||
100 |
(*The opposite inclusion*) |
|
101 |
goalw QUniv.thy [quniv_def,QPair_def] |
|
102 |
"!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"; |
|
129 | 103 |
by (etac ([Transset_eclose RS Transset_univ, PowD] MRS |
104 |
Transset_includes_summands RS conjE) 1); |
|
0 | 105 |
by (REPEAT (ares_tac [conjI,PowI] 1)); |
760 | 106 |
qed "quniv_QPair_D"; |
0 | 107 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
108 |
bind_thm ("quniv_QPair_E", (quniv_QPair_D RS conjE)); |
0 | 109 |
|
110 |
goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"; |
|
111 |
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1 |
|
112 |
ORELSE etac conjE 1)); |
|
760 | 113 |
qed "quniv_QPair_iff"; |
0 | 114 |
|
115 |
||
116 |
(** Quine disjoint sum **) |
|
117 |
||
118 |
goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)"; |
|
119 |
by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1)); |
|
760 | 120 |
qed "QInl_in_quniv"; |
0 | 121 |
|
122 |
goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)"; |
|
123 |
by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1)); |
|
760 | 124 |
qed "QInr_in_quniv"; |
0 | 125 |
|
126 |
goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)"; |
|
127 |
by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1 |
|
128 |
ORELSE eresolve_tac [qsumE, ssubst] 1)); |
|
760 | 129 |
qed "qsum_quniv"; |
0 | 130 |
|
131 |
val qsum_subset_quniv = standard |
|
132 |
(qsum_mono RS (qsum_quniv RSN (2,subset_trans))); |
|
133 |
||
134 |
(*** The natural numbers ***) |
|
135 |
||
136 |
val nat_subset_quniv = standard |
|
137 |
([nat_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
138 |
||
139 |
(* n:nat ==> n:quniv(A) *) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
140 |
bind_thm ("nat_into_quniv", (nat_subset_quniv RS subsetD)); |
0 | 141 |
|
142 |
val bool_subset_quniv = standard |
|
143 |
([bool_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
144 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
145 |
bind_thm ("bool_into_quniv", (bool_subset_quniv RS subsetD)); |
0 | 146 |
|
147 |
||
148 |
(**** Properties of Vfrom analogous to the "take-lemma" ****) |
|
149 |
||
150 |
(*** Intersecting a*b with Vfrom... ***) |
|
151 |
||
152 |
(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*) |
|
153 |
goal Univ.thy |
|
154 |
"!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
|
155 |
\ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
156 |
by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
157 |
by (assume_tac 1); |
0 | 158 |
by (fast_tac ZF_cs 1); |
760 | 159 |
qed "doubleton_in_Vfrom_D"; |
0 | 160 |
|
161 |
(*This weaker version says a, b exist at the same level*) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
162 |
bind_thm ("Vfrom_doubleton_D", (Transset_Vfrom RS Transset_doubleton_D)); |
0 | 163 |
|
164 |
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i) |
|
165 |
implies a, b : Vfrom(X,i), which is useless for induction. |
|
166 |
Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i))) |
|
167 |
implies a, b : Vfrom(X,i), leaving the succ(i) case untreated. |
|
168 |
The combination gives a reduction by precisely one level, which is |
|
169 |
most convenient for proofs. |
|
170 |
**) |
|
171 |
||
172 |
goalw Univ.thy [Pair_def] |
|
173 |
"!!X. [| <a,b> : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
|
174 |
\ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
|
175 |
by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1); |
|
760 | 176 |
qed "Pair_in_Vfrom_D"; |
0 | 177 |
|
178 |
goal Univ.thy |
|
179 |
"!!X. Transset(X) ==> \ |
|
180 |
\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"; |
|
181 |
by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1); |
|
760 | 182 |
qed "product_Int_Vfrom_subset"; |
0 | 183 |
|
184 |
(*** Intersecting <a;b> with Vfrom... ***) |
|
185 |
||
186 |
goalw QUniv.thy [QPair_def,sum_def] |
|
187 |
"!!X. Transset(X) ==> \ |
|
188 |
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
189 |
by (rtac (Int_Un_distrib RS ssubst) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
190 |
by (rtac Un_mono 1); |
0 | 191 |
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, |
192 |
[Int_lower1, subset_refl] MRS Sigma_mono] 1)); |
|
760 | 193 |
qed "QPair_Int_Vfrom_succ_subset"; |
0 | 194 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
195 |
(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****) |
0 | 196 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
197 |
(*Rule for level i -- preserving the level, not decreasing it*) |
0 | 198 |
|
199 |
goalw QUniv.thy [QPair_def] |
|
200 |
"!!X. Transset(X) ==> \ |
|
201 |
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
202 |
by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); |
760 | 203 |
qed "QPair_Int_Vfrom_subset"; |
0 | 204 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
205 |
(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*) |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
206 |
val QPair_Int_Vset_subset_trans = standard |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
207 |
([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); |
0 | 208 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
209 |
goal QUniv.thy |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
210 |
"!!i. [| Ord(i) \ |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
211 |
\ |] ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"; |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
212 |
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
213 |
(*0 case*) |
0 | 214 |
by (rtac (Vfrom_0 RS ssubst) 1); |
215 |
by (fast_tac ZF_cs 1); |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
216 |
(*succ(j) case*) |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
217 |
by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
218 |
by (rtac (succI1 RS UN_upper) 1); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
219 |
(*Limit(i) case*) |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
220 |
by (asm_simp_tac (ZF_ss addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl, |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
221 |
UN_mono, QPair_Int_Vset_subset_trans]) 1); |
760 | 222 |
qed "QPair_Int_Vset_subset_UN"; |