author | lcp |
Thu, 07 Oct 1993 10:48:16 +0100 | |
changeset 37 | cebe01deba80 |
parent 27 | 0e152fe9571e |
child 187 | 8729bfdcb638 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/univ |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
The cumulative hierarchy and a small universe for recursive types |
|
7 |
*) |
|
8 |
||
9 |
open Univ; |
|
10 |
||
11 |
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*) |
|
12 |
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))"; |
|
13 |
by (rtac (Vfrom_def RS def_transrec RS ssubst) 1); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
14 |
by (simp_tac ZF_ss 1); |
0 | 15 |
val Vfrom = result(); |
16 |
||
17 |
(** Monotonicity **) |
|
18 |
||
19 |
goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"; |
|
20 |
by (eps_ind_tac "i" 1); |
|
21 |
by (rtac (impI RS allI) 1); |
|
22 |
by (rtac (Vfrom RS ssubst) 1); |
|
23 |
by (rtac (Vfrom RS ssubst) 1); |
|
24 |
by (etac Un_mono 1); |
|
25 |
by (rtac UN_mono 1); |
|
26 |
by (assume_tac 1); |
|
27 |
by (rtac Pow_mono 1); |
|
28 |
by (etac (bspec RS spec RS mp) 1); |
|
29 |
by (assume_tac 1); |
|
30 |
by (rtac subset_refl 1); |
|
31 |
val Vfrom_mono_lemma = result(); |
|
32 |
||
33 |
(* [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x) *) |
|
34 |
val Vfrom_mono = standard (Vfrom_mono_lemma RS spec RS mp); |
|
35 |
||
36 |
||
37 |
(** A fundamental equality: Vfrom does not require ordinals! **) |
|
38 |
||
39 |
goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))"; |
|
40 |
by (eps_ind_tac "x" 1); |
|
41 |
by (rtac (Vfrom RS ssubst) 1); |
|
42 |
by (rtac (Vfrom RS ssubst) 1); |
|
27 | 43 |
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); |
0 | 44 |
val Vfrom_rank_subset1 = result(); |
45 |
||
46 |
goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)"; |
|
47 |
by (eps_ind_tac "x" 1); |
|
48 |
by (rtac (Vfrom RS ssubst) 1); |
|
49 |
by (rtac (Vfrom RS ssubst) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
50 |
by (rtac (subset_refl RS Un_mono) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
51 |
by (rtac UN_least 1); |
27 | 52 |
(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*) |
53 |
by (etac (rank RS equalityD1 RS subsetD RS UN_E) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
54 |
by (rtac subset_trans 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
55 |
by (etac UN_upper 2); |
27 | 56 |
by (rtac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1); |
57 |
by (etac (ltI RS le_imp_subset) 1); |
|
58 |
by (rtac (Ord_rank RS Ord_succ) 1); |
|
0 | 59 |
by (etac bspec 1); |
60 |
by (assume_tac 1); |
|
61 |
val Vfrom_rank_subset2 = result(); |
|
62 |
||
63 |
goal Univ.thy "Vfrom(A,rank(x)) = Vfrom(A,x)"; |
|
64 |
by (rtac equalityI 1); |
|
65 |
by (rtac Vfrom_rank_subset2 1); |
|
66 |
by (rtac Vfrom_rank_subset1 1); |
|
67 |
val Vfrom_rank_eq = result(); |
|
68 |
||
69 |
||
70 |
(*** Basic closure properties ***) |
|
71 |
||
72 |
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)"; |
|
73 |
by (rtac (Vfrom RS ssubst) 1); |
|
74 |
by (fast_tac ZF_cs 1); |
|
75 |
val zero_in_Vfrom = result(); |
|
76 |
||
77 |
goal Univ.thy "i <= Vfrom(A,i)"; |
|
78 |
by (eps_ind_tac "i" 1); |
|
79 |
by (rtac (Vfrom RS ssubst) 1); |
|
80 |
by (fast_tac ZF_cs 1); |
|
81 |
val i_subset_Vfrom = result(); |
|
82 |
||
83 |
goal Univ.thy "A <= Vfrom(A,i)"; |
|
84 |
by (rtac (Vfrom RS ssubst) 1); |
|
85 |
by (rtac Un_upper1 1); |
|
86 |
val A_subset_Vfrom = result(); |
|
87 |
||
88 |
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"; |
|
89 |
by (rtac (Vfrom RS ssubst) 1); |
|
90 |
by (fast_tac ZF_cs 1); |
|
91 |
val subset_mem_Vfrom = result(); |
|
92 |
||
93 |
(** Finite sets and ordered pairs **) |
|
94 |
||
95 |
goal Univ.thy "!!a. a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"; |
|
96 |
by (rtac subset_mem_Vfrom 1); |
|
97 |
by (safe_tac ZF_cs); |
|
98 |
val singleton_in_Vfrom = result(); |
|
99 |
||
100 |
goal Univ.thy |
|
101 |
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"; |
|
102 |
by (rtac subset_mem_Vfrom 1); |
|
103 |
by (safe_tac ZF_cs); |
|
104 |
val doubleton_in_Vfrom = result(); |
|
105 |
||
106 |
goalw Univ.thy [Pair_def] |
|
107 |
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i) |] ==> \ |
|
108 |
\ <a,b> : Vfrom(A,succ(succ(i)))"; |
|
109 |
by (REPEAT (ares_tac [doubleton_in_Vfrom] 1)); |
|
110 |
val Pair_in_Vfrom = result(); |
|
111 |
||
112 |
val [prem] = goal Univ.thy |
|
113 |
"a<=Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"; |
|
114 |
by (REPEAT (resolve_tac [subset_mem_Vfrom, succ_subsetI] 1)); |
|
115 |
by (rtac (Vfrom_mono RSN (2,subset_trans)) 2); |
|
116 |
by (REPEAT (resolve_tac [prem, subset_refl, subset_succI] 1)); |
|
117 |
val succ_in_Vfrom = result(); |
|
118 |
||
119 |
(*** 0, successor and limit equations fof Vfrom ***) |
|
120 |
||
121 |
goal Univ.thy "Vfrom(A,0) = A"; |
|
122 |
by (rtac (Vfrom RS ssubst) 1); |
|
123 |
by (fast_tac eq_cs 1); |
|
124 |
val Vfrom_0 = result(); |
|
125 |
||
126 |
goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; |
|
127 |
by (rtac (Vfrom RS trans) 1); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
128 |
by (rtac (succI1 RS RepFunI RS Union_upper RSN |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
129 |
(2, equalityI RS subst_context)) 1); |
0 | 130 |
by (rtac UN_least 1); |
131 |
by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1); |
|
27 | 132 |
by (etac (ltI RS le_imp_subset) 1); |
133 |
by (etac Ord_succ 1); |
|
0 | 134 |
val Vfrom_succ_lemma = result(); |
135 |
||
136 |
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"; |
|
137 |
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1); |
|
138 |
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1); |
|
139 |
by (rtac (rank_succ RS ssubst) 1); |
|
140 |
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1); |
|
141 |
val Vfrom_succ = result(); |
|
142 |
||
143 |
(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces |
|
144 |
the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *) |
|
145 |
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))"; |
|
146 |
by (rtac (Vfrom RS ssubst) 1); |
|
147 |
by (rtac equalityI 1); |
|
148 |
(*first inclusion*) |
|
149 |
by (rtac Un_least 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
150 |
by (rtac (A_subset_Vfrom RS subset_trans) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
151 |
by (rtac (prem RS UN_upper) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
152 |
by (rtac UN_least 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
153 |
by (etac UnionE 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
154 |
by (rtac subset_trans 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
155 |
by (etac UN_upper 2); |
0 | 156 |
by (rtac (Vfrom RS ssubst) 1); |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
157 |
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1); |
0 | 158 |
(*opposite inclusion*) |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
159 |
by (rtac UN_least 1); |
0 | 160 |
by (rtac (Vfrom RS ssubst) 1); |
161 |
by (fast_tac ZF_cs 1); |
|
162 |
val Vfrom_Union = result(); |
|
163 |
||
164 |
(*** Limit ordinals -- general properties ***) |
|
165 |
||
166 |
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i"; |
|
27 | 167 |
by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1); |
0 | 168 |
val Limit_Union_eq = result(); |
169 |
||
170 |
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)"; |
|
171 |
by (etac conjunct1 1); |
|
172 |
val Limit_is_Ord = result(); |
|
173 |
||
27 | 174 |
goalw Univ.thy [Limit_def] "!!i. Limit(i) ==> 0 < i"; |
175 |
by (etac (conjunct2 RS conjunct1) 1); |
|
0 | 176 |
val Limit_has_0 = result(); |
177 |
||
27 | 178 |
goalw Univ.thy [Limit_def] "!!i. [| Limit(i); j<i |] ==> succ(j) < i"; |
0 | 179 |
by (fast_tac ZF_cs 1); |
180 |
val Limit_has_succ = result(); |
|
181 |
||
182 |
goalw Univ.thy [Limit_def] "Limit(nat)"; |
|
27 | 183 |
by (safe_tac (ZF_cs addSIs (ltI::nat_typechecks))); |
184 |
by (etac ltD 1); |
|
0 | 185 |
val Limit_nat = result(); |
186 |
||
187 |
goalw Univ.thy [Limit_def] |
|
37 | 188 |
"!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)"; |
0 | 189 |
by (safe_tac subset_cs); |
27 | 190 |
by (rtac (not_le_iff_lt RS iffD1) 2); |
191 |
by (fast_tac (lt_cs addEs [lt_anti_sym]) 4); |
|
192 |
by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1)); |
|
0 | 193 |
val non_succ_LimitI = result(); |
194 |
||
195 |
goal Univ.thy "!!i. Ord(i) ==> i=0 | (EX j. i=succ(j)) | Limit(i)"; |
|
27 | 196 |
by (fast_tac (ZF_cs addSIs [non_succ_LimitI, Ord_0_lt]) 1); |
0 | 197 |
val Ord_cases_lemma = result(); |
198 |
||
199 |
val major::prems = goal Univ.thy |
|
200 |
"[| Ord(i); \ |
|
201 |
\ i=0 ==> P; \ |
|
202 |
\ !!j. i=succ(j) ==> P; \ |
|
203 |
\ Limit(i) ==> P \ |
|
204 |
\ |] ==> P"; |
|
205 |
by (cut_facts_tac [major RS Ord_cases_lemma] 1); |
|
206 |
by (REPEAT (eresolve_tac (prems@[disjE, exE]) 1)); |
|
207 |
val Ord_cases = result(); |
|
208 |
||
209 |
||
210 |
(*** Vfrom applied to Limit ordinals ***) |
|
211 |
||
212 |
(*NB. limit ordinals are non-empty; |
|
213 |
Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *) |
|
214 |
val [limiti] = goal Univ.thy |
|
215 |
"Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"; |
|
27 | 216 |
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1); |
0 | 217 |
by (rtac (limiti RS Limit_Union_eq RS ssubst) 1); |
218 |
by (rtac refl 1); |
|
219 |
val Limit_Vfrom_eq = result(); |
|
220 |
||
27 | 221 |
goal Univ.thy "!!a. [| a: Vfrom(A,j); Limit(i); j<i |] ==> a : Vfrom(A,i)"; |
222 |
by (rtac (Limit_Vfrom_eq RS equalityD2 RS subsetD) 1); |
|
223 |
by (REPEAT (ares_tac [ltD RS UN_I] 1)); |
|
224 |
val Limit_VfromI = result(); |
|
225 |
||
226 |
val prems = goal Univ.thy |
|
227 |
"[| a: Vfrom(A,i); Limit(i); \ |
|
228 |
\ !!x. [| x<i; a: Vfrom(A,x) |] ==> R \ |
|
229 |
\ |] ==> R"; |
|
230 |
by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1); |
|
231 |
by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1)); |
|
232 |
val Limit_VfromE = result(); |
|
0 | 233 |
|
234 |
val [major,limiti] = goal Univ.thy |
|
235 |
"[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)"; |
|
27 | 236 |
by (rtac ([major,limiti] MRS Limit_VfromE) 1); |
237 |
by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
0 | 238 |
by (etac (limiti RS Limit_has_succ) 1); |
239 |
val singleton_in_Vfrom_limit = result(); |
|
240 |
||
241 |
val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD) |
|
242 |
and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD); |
|
243 |
||
244 |
(*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*) |
|
245 |
val [aprem,bprem,limiti] = goal Univ.thy |
|
246 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \ |
|
247 |
\ {a,b} : Vfrom(A,i)"; |
|
27 | 248 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
249 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
250 |
by (rtac ([doubleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
251 |
by (etac Vfrom_UnI1 1); |
|
252 |
by (etac Vfrom_UnI2 1); |
|
253 |
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); |
|
0 | 254 |
val doubleton_in_Vfrom_limit = result(); |
255 |
||
256 |
val [aprem,bprem,limiti] = goal Univ.thy |
|
257 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \ |
|
258 |
\ <a,b> : Vfrom(A,i)"; |
|
259 |
(*Infer that a, b occur at ordinals x,xa < i.*) |
|
27 | 260 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
261 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
262 |
by (rtac ([Pair_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
0 | 263 |
(*Infer that succ(succ(x Un xa)) < i *) |
27 | 264 |
by (etac Vfrom_UnI1 1); |
265 |
by (etac Vfrom_UnI2 1); |
|
266 |
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); |
|
0 | 267 |
val Pair_in_Vfrom_limit = result(); |
268 |
||
269 |
||
270 |
(*** Properties assuming Transset(A) ***) |
|
271 |
||
272 |
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))"; |
|
273 |
by (eps_ind_tac "i" 1); |
|
274 |
by (rtac (Vfrom RS ssubst) 1); |
|
275 |
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un, |
|
276 |
Transset_Pow]) 1); |
|
277 |
val Transset_Vfrom = result(); |
|
278 |
||
279 |
goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; |
|
280 |
by (rtac (Vfrom_succ RS trans) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
281 |
by (rtac (Un_upper2 RSN (2,equalityI)) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
282 |
by (rtac (subset_refl RSN (2,Un_least)) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
283 |
by (rtac (A_subset_Vfrom RS subset_trans) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
284 |
by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); |
0 | 285 |
val Transset_Vfrom_succ = result(); |
286 |
||
287 |
goalw Ord.thy [Pair_def,Transset_def] |
|
288 |
"!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C"; |
|
289 |
by (fast_tac ZF_cs 1); |
|
290 |
val Transset_Pair_subset = result(); |
|
291 |
||
292 |
goal Univ.thy |
|
293 |
"!!a b.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ |
|
294 |
\ <a,b> : Vfrom(A,i)"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
295 |
by (etac (Transset_Pair_subset RS conjE) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
296 |
by (etac Transset_Vfrom 1); |
0 | 297 |
by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1)); |
298 |
val Transset_Pair_subset_Vfrom_limit = result(); |
|
299 |
||
300 |
||
301 |
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i) |
|
302 |
is a model of simple type theory provided A is a transitive set |
|
303 |
and i is a limit ordinal |
|
304 |
***) |
|
305 |
||
306 |
(*There are three nearly identical proofs below -- needs a general theorem |
|
307 |
for proving ...a...b : Vfrom(A,i) where i is a limit ordinal*) |
|
308 |
||
309 |
(** products **) |
|
310 |
||
311 |
goal Univ.thy |
|
312 |
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i); Transset(A) |] ==> \ |
|
313 |
\ a*b : Vfrom(A, succ(succ(succ(i))))"; |
|
314 |
by (dtac Transset_Vfrom 1); |
|
315 |
by (rtac subset_mem_Vfrom 1); |
|
316 |
by (rewtac Transset_def); |
|
317 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
|
318 |
val prod_in_Vfrom = result(); |
|
319 |
||
320 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
321 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
322 |
\ a*b : Vfrom(A,i)"; |
|
323 |
(*Infer that a, b occur at ordinals x,xa < i.*) |
|
27 | 324 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
325 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
326 |
by (rtac ([prod_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
327 |
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 1); |
|
328 |
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 1); |
|
0 | 329 |
(*Infer that succ(succ(succ(x Un xa))) < i *) |
27 | 330 |
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt, transset] 1)); |
0 | 331 |
val prod_in_Vfrom_limit = result(); |
332 |
||
333 |
(** Disjoint sums, aka Quine ordered pairs **) |
|
334 |
||
335 |
goalw Univ.thy [sum_def] |
|
336 |
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i); Transset(A); 1:i |] ==> \ |
|
337 |
\ a+b : Vfrom(A, succ(succ(succ(i))))"; |
|
338 |
by (dtac Transset_Vfrom 1); |
|
339 |
by (rtac subset_mem_Vfrom 1); |
|
340 |
by (rewtac Transset_def); |
|
341 |
by (fast_tac (ZF_cs addIs [zero_in_Vfrom, Pair_in_Vfrom, |
|
342 |
i_subset_Vfrom RS subsetD]) 1); |
|
343 |
val sum_in_Vfrom = result(); |
|
344 |
||
345 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
346 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
347 |
\ a+b : Vfrom(A,i)"; |
|
348 |
(*Infer that a, b occur at ordinals x,xa < i.*) |
|
27 | 349 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
350 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
351 |
by (rtac ([sum_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
352 |
by (rtac (succI1 RS UnI1) 4); |
|
353 |
(*Infer that succ(succ(succ(succ(1) Un (x Un xa)))) < i *) |
|
354 |
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 1); |
|
355 |
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 1); |
|
356 |
by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt, |
|
357 |
transset] 1)); |
|
0 | 358 |
val sum_in_Vfrom_limit = result(); |
359 |
||
360 |
(** function space! **) |
|
361 |
||
362 |
goalw Univ.thy [Pi_def] |
|
363 |
"!!A. [| a: Vfrom(A,i); b: Vfrom(A,i); Transset(A) |] ==> \ |
|
364 |
\ a->b : Vfrom(A, succ(succ(succ(succ(i)))))"; |
|
365 |
by (dtac Transset_Vfrom 1); |
|
366 |
by (rtac subset_mem_Vfrom 1); |
|
367 |
by (rtac (Collect_subset RS subset_trans) 1); |
|
368 |
by (rtac (Vfrom RS ssubst) 1); |
|
369 |
by (rtac (subset_trans RS subset_trans) 1); |
|
370 |
by (rtac Un_upper2 3); |
|
371 |
by (rtac (succI1 RS UN_upper) 2); |
|
372 |
by (rtac Pow_mono 1); |
|
373 |
by (rewtac Transset_def); |
|
374 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom]) 1); |
|
375 |
val fun_in_Vfrom = result(); |
|
376 |
||
377 |
val [aprem,bprem,limiti,transset] = goal Univ.thy |
|
378 |
"[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ |
|
379 |
\ a->b : Vfrom(A,i)"; |
|
380 |
(*Infer that a, b occur at ordinals x,xa < i.*) |
|
27 | 381 |
by (rtac ([aprem,limiti] MRS Limit_VfromE) 1); |
382 |
by (rtac ([bprem,limiti] MRS Limit_VfromE) 1); |
|
383 |
by (rtac ([fun_in_Vfrom, limiti] MRS Limit_VfromI) 1); |
|
0 | 384 |
(*Infer that succ(succ(succ(x Un xa))) < i *) |
27 | 385 |
by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 1); |
386 |
by (etac (Vfrom_UnI2 RS Vfrom_UnI2) 1); |
|
387 |
by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt, transset] 1)); |
|
0 | 388 |
val fun_in_Vfrom_limit = result(); |
389 |
||
390 |
||
391 |
(*** The set Vset(i) ***) |
|
392 |
||
393 |
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))"; |
|
394 |
by (rtac (Vfrom RS ssubst) 1); |
|
395 |
by (fast_tac eq_cs 1); |
|
396 |
val Vset = result(); |
|
397 |
||
398 |
val Vset_succ = Transset_0 RS Transset_Vfrom_succ; |
|
399 |
||
400 |
val Transset_Vset = Transset_0 RS Transset_Vfrom; |
|
401 |
||
402 |
(** Characterisation of the elements of Vset(i) **) |
|
403 |
||
27 | 404 |
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i"; |
0 | 405 |
by (rtac (ordi RS trans_induct) 1); |
406 |
by (rtac (Vset RS ssubst) 1); |
|
407 |
by (safe_tac ZF_cs); |
|
408 |
by (rtac (rank RS ssubst) 1); |
|
27 | 409 |
by (rtac UN_succ_least_lt 1); |
410 |
by (fast_tac ZF_cs 2); |
|
411 |
by (REPEAT (ares_tac [ltI] 1)); |
|
0 | 412 |
val Vset_rank_imp1 = result(); |
413 |
||
27 | 414 |
(* [| Ord(i); x : Vset(i) |] ==> rank(x) < i *) |
415 |
val VsetD = standard (Vset_rank_imp1 RS spec RS mp); |
|
0 | 416 |
|
417 |
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"; |
|
418 |
by (rtac (ordi RS trans_induct) 1); |
|
419 |
by (rtac allI 1); |
|
420 |
by (rtac (Vset RS ssubst) 1); |
|
27 | 421 |
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1); |
0 | 422 |
val Vset_rank_imp2 = result(); |
423 |
||
27 | 424 |
goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)"; |
425 |
by (etac ltE 1); |
|
426 |
by (etac (Vset_rank_imp2 RS spec RS mp) 1); |
|
427 |
by (assume_tac 1); |
|
428 |
val VsetI = result(); |
|
0 | 429 |
|
27 | 430 |
goal Univ.thy "!!i. Ord(i) ==> b : Vset(i) <-> rank(b) < i"; |
0 | 431 |
by (rtac iffI 1); |
27 | 432 |
by (REPEAT (eresolve_tac [asm_rl, VsetD, VsetI] 1)); |
0 | 433 |
val Vset_Ord_rank_iff = result(); |
434 |
||
27 | 435 |
goal Univ.thy "b : Vset(a) <-> rank(b) < rank(a)"; |
0 | 436 |
by (rtac (Vfrom_rank_eq RS subst) 1); |
437 |
by (rtac (Ord_rank RS Vset_Ord_rank_iff) 1); |
|
438 |
val Vset_rank_iff = result(); |
|
439 |
||
440 |
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i"; |
|
441 |
by (rtac (rank RS ssubst) 1); |
|
442 |
by (rtac equalityI 1); |
|
443 |
by (safe_tac ZF_cs); |
|
444 |
by (EVERY' [wtac UN_I, |
|
445 |
etac (i_subset_Vfrom RS subsetD), |
|
446 |
etac (Ord_in_Ord RS rank_of_Ord RS ssubst), |
|
447 |
assume_tac, |
|
448 |
rtac succI1] 3); |
|
27 | 449 |
by (REPEAT (eresolve_tac [asm_rl, VsetD RS ltD, Ord_trans] 1)); |
0 | 450 |
val rank_Vset = result(); |
451 |
||
452 |
(** Lemmas for reasoning about sets in terms of their elements' ranks **) |
|
453 |
||
454 |
goal Univ.thy "a <= Vset(rank(a))"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
455 |
by (rtac subsetI 1); |
27 | 456 |
by (etac (rank_lt RS VsetI) 1); |
0 | 457 |
val arg_subset_Vset_rank = result(); |
458 |
||
459 |
val [iprem] = goal Univ.thy |
|
460 |
"[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"; |
|
27 | 461 |
by (rtac ([subset_refl, arg_subset_Vset_rank] MRS |
462 |
Int_greatest RS subset_trans) 1); |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
463 |
by (rtac (Ord_rank RS iprem) 1); |
0 | 464 |
val Int_Vset_subset = result(); |
465 |
||
466 |
(** Set up an environment for simplification **) |
|
467 |
||
468 |
val rank_rls = [rank_Inl, rank_Inr, rank_pair1, rank_pair2]; |
|
27 | 469 |
val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [lt_trans])); |
0 | 470 |
|
471 |
val rank_ss = ZF_ss |
|
27 | 472 |
addsimps [case_Inl, case_Inr, VsetI] |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
473 |
addsimps rank_trans_rls; |
0 | 474 |
|
475 |
(** Recursion over Vset levels! **) |
|
476 |
||
477 |
(*NOT SUITABLE FOR REWRITING: recursive!*) |
|
478 |
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"; |
|
479 |
by (rtac (transrec RS ssubst) 1); |
|
27 | 480 |
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, |
481 |
VsetI RS beta, le_refl]) 1); |
|
0 | 482 |
val Vrec = result(); |
483 |
||
484 |
(*This form avoids giant explosions in proofs. NOTE USE OF == *) |
|
485 |
val rew::prems = goal Univ.thy |
|
486 |
"[| !!x. h(x)==Vrec(x,H) |] ==> \ |
|
487 |
\ h(a) = H(a, lam x: Vset(rank(a)). h(x))"; |
|
488 |
by (rewtac rew); |
|
489 |
by (rtac Vrec 1); |
|
490 |
val def_Vrec = result(); |
|
491 |
||
492 |
||
493 |
(*** univ(A) ***) |
|
494 |
||
495 |
goalw Univ.thy [univ_def] "!!A B. A<=B ==> univ(A) <= univ(B)"; |
|
496 |
by (etac Vfrom_mono 1); |
|
497 |
by (rtac subset_refl 1); |
|
498 |
val univ_mono = result(); |
|
499 |
||
500 |
goalw Univ.thy [univ_def] "!!A. Transset(A) ==> Transset(univ(A))"; |
|
501 |
by (etac Transset_Vfrom 1); |
|
502 |
val Transset_univ = result(); |
|
503 |
||
504 |
(** univ(A) as a limit **) |
|
505 |
||
506 |
goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
507 |
by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); |
0 | 508 |
val univ_eq_UN = result(); |
509 |
||
510 |
goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
511 |
by (rtac (subset_UN_iff_eq RS iffD1) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
512 |
by (etac (univ_eq_UN RS subst) 1); |
0 | 513 |
val subset_univ_eq_Int = result(); |
514 |
||
515 |
val [aprem, iprem] = goal Univ.thy |
|
516 |
"[| a <= univ(X); \ |
|
517 |
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ |
|
518 |
\ |] ==> a <= b"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
519 |
by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
520 |
by (rtac UN_least 1); |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
521 |
by (etac iprem 1); |
0 | 522 |
val univ_Int_Vfrom_subset = result(); |
523 |
||
524 |
val prems = goal Univ.thy |
|
525 |
"[| a <= univ(X); b <= univ(X); \ |
|
526 |
\ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ |
|
527 |
\ |] ==> a = b"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
528 |
by (rtac equalityI 1); |
0 | 529 |
by (ALLGOALS |
530 |
(resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' |
|
531 |
eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' |
|
532 |
rtac Int_lower1)); |
|
533 |
val univ_Int_Vfrom_eq = result(); |
|
534 |
||
535 |
(** Closure properties **) |
|
536 |
||
537 |
goalw Univ.thy [univ_def] "0 : univ(A)"; |
|
538 |
by (rtac (nat_0I RS zero_in_Vfrom) 1); |
|
539 |
val zero_in_univ = result(); |
|
540 |
||
541 |
goalw Univ.thy [univ_def] "A <= univ(A)"; |
|
542 |
by (rtac A_subset_Vfrom 1); |
|
543 |
val A_subset_univ = result(); |
|
544 |
||
545 |
val A_into_univ = A_subset_univ RS subsetD; |
|
546 |
||
547 |
(** Closure under unordered and ordered pairs **) |
|
548 |
||
549 |
goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; |
|
550 |
by (rtac singleton_in_Vfrom_limit 1); |
|
551 |
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); |
|
552 |
val singleton_in_univ = result(); |
|
553 |
||
554 |
goalw Univ.thy [univ_def] |
|
555 |
"!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; |
|
556 |
by (rtac doubleton_in_Vfrom_limit 1); |
|
557 |
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); |
|
558 |
val doubleton_in_univ = result(); |
|
559 |
||
560 |
goalw Univ.thy [univ_def] |
|
561 |
"!!A a. [| a: univ(A); b: univ(A) |] ==> <a,b> : univ(A)"; |
|
562 |
by (rtac Pair_in_Vfrom_limit 1); |
|
563 |
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); |
|
564 |
val Pair_in_univ = result(); |
|
565 |
||
566 |
goal Univ.thy "univ(A)*univ(A) <= univ(A)"; |
|
567 |
by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1 |
|
568 |
ORELSE eresolve_tac [SigmaE, ssubst] 1)); |
|
569 |
val product_univ = result(); |
|
570 |
||
571 |
val Sigma_subset_univ = standard |
|
572 |
(Sigma_mono RS (product_univ RSN (2,subset_trans))); |
|
573 |
||
574 |
goalw Univ.thy [univ_def] |
|
575 |
"!!a b.[| <a,b> <= univ(A); Transset(A) |] ==> <a,b> : univ(A)"; |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
576 |
by (etac Transset_Pair_subset_Vfrom_limit 1); |
0 | 577 |
by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); |
578 |
val Transset_Pair_subset_univ = result(); |
|
579 |
||
580 |
||
581 |
(** The natural numbers **) |
|
582 |
||
583 |
goalw Univ.thy [univ_def] "nat <= univ(A)"; |
|
584 |
by (rtac i_subset_Vfrom 1); |
|
585 |
val nat_subset_univ = result(); |
|
586 |
||
587 |
(* n:nat ==> n:univ(A) *) |
|
588 |
val nat_into_univ = standard (nat_subset_univ RS subsetD); |
|
589 |
||
590 |
(** instances for 1 and 2 **) |
|
591 |
||
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
592 |
goal Univ.thy "1 : univ(A)"; |
0 | 593 |
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); |
594 |
val one_in_univ = result(); |
|
595 |
||
596 |
(*unused!*) |
|
27 | 597 |
goal Univ.thy "succ(1) : univ(A)"; |
0 | 598 |
by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); |
599 |
val two_in_univ = result(); |
|
600 |
||
601 |
goalw Univ.thy [bool_def] "bool <= univ(A)"; |
|
602 |
by (fast_tac (ZF_cs addSIs [zero_in_univ,one_in_univ]) 1); |
|
603 |
val bool_subset_univ = result(); |
|
604 |
||
605 |
val bool_into_univ = standard (bool_subset_univ RS subsetD); |
|
606 |
||
607 |
||
608 |
(** Closure under disjoint union **) |
|
609 |
||
610 |
goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; |
|
611 |
by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1)); |
|
612 |
val Inl_in_univ = result(); |
|
613 |
||
614 |
goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; |
|
615 |
by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1)); |
|
616 |
val Inr_in_univ = result(); |
|
617 |
||
618 |
goal Univ.thy "univ(C)+univ(C) <= univ(C)"; |
|
619 |
by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1 |
|
620 |
ORELSE eresolve_tac [sumE, ssubst] 1)); |
|
621 |
val sum_univ = result(); |
|
622 |
||
623 |
val sum_subset_univ = standard |
|
624 |
(sum_mono RS (sum_univ RSN (2,subset_trans))); |
|
625 |
||
626 |
||
627 |
(** Closure under binary union -- use Un_least **) |
|
628 |
(** Closure under Collect -- use (Collect_subset RS subset_trans) **) |
|
629 |
(** Closure under RepFun -- use RepFun_subset **) |
|
630 |
||
631 |