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