435
|
1 |
(* Title: ZF/Cardinal.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
|
|
6 |
Cardinals in Zermelo-Fraenkel Set Theory
|
|
7 |
|
|
8 |
This theory does NOT assume the Axiom of Choice
|
|
9 |
*)
|
|
10 |
|
|
11 |
open Cardinal;
|
|
12 |
|
|
13 |
(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
|
|
14 |
|
|
15 |
(** Lemma: Banach's Decomposition Theorem **)
|
|
16 |
|
|
17 |
goal Cardinal.thy "bnd_mono(X, %W. X - g``(Y - f``W))";
|
|
18 |
by (rtac bnd_monoI 1);
|
|
19 |
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1));
|
|
20 |
val decomp_bnd_mono = result();
|
|
21 |
|
|
22 |
val [gfun] = goal Cardinal.thy
|
|
23 |
"g: Y->X ==> \
|
|
24 |
\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \
|
|
25 |
\ X - lfp(X, %W. X - g``(Y - f``W)) ";
|
|
26 |
by (res_inst_tac [("P", "%u. ?v = X-u")]
|
|
27 |
(decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
|
|
28 |
by (simp_tac (ZF_ss addsimps [subset_refl, double_complement,
|
|
29 |
gfun RS fun_is_rel RS image_subset]) 1);
|
|
30 |
val Banach_last_equation = result();
|
|
31 |
|
|
32 |
val prems = goal Cardinal.thy
|
|
33 |
"[| f: X->Y; g: Y->X |] ==> \
|
|
34 |
\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \
|
|
35 |
\ (YA Int YB = 0) & (YA Un YB = Y) & \
|
|
36 |
\ f``XA=YA & g``YB=XB";
|
|
37 |
by (REPEAT
|
|
38 |
(FIRSTGOAL
|
|
39 |
(resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition])));
|
|
40 |
by (rtac Banach_last_equation 3);
|
|
41 |
by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1));
|
|
42 |
val decomposition = result();
|
|
43 |
|
|
44 |
val prems = goal Cardinal.thy
|
|
45 |
"[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)";
|
|
46 |
by (cut_facts_tac prems 1);
|
|
47 |
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1);
|
|
48 |
by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un]
|
|
49 |
addIs [bij_converse_bij]) 1);
|
|
50 |
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
|
|
51 |
is forced by the context!! *)
|
|
52 |
val schroeder_bernstein = result();
|
|
53 |
|
|
54 |
|
|
55 |
(** Equipollence is an equivalence relation **)
|
|
56 |
|
|
57 |
goalw Cardinal.thy [eqpoll_def] "X eqpoll X";
|
437
|
58 |
by (rtac exI 1);
|
|
59 |
by (rtac id_bij 1);
|
435
|
60 |
val eqpoll_refl = result();
|
|
61 |
|
|
62 |
goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X";
|
|
63 |
by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1);
|
|
64 |
val eqpoll_sym = result();
|
|
65 |
|
|
66 |
goalw Cardinal.thy [eqpoll_def]
|
|
67 |
"!!X Y. [| X eqpoll Y; Y eqpoll Z |] ==> X eqpoll Z";
|
|
68 |
by (fast_tac (ZF_cs addIs [comp_bij]) 1);
|
|
69 |
val eqpoll_trans = result();
|
|
70 |
|
|
71 |
(** Le-pollence is a partial ordering **)
|
|
72 |
|
|
73 |
goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y";
|
437
|
74 |
by (rtac exI 1);
|
|
75 |
by (etac id_subset_inj 1);
|
435
|
76 |
val subset_imp_lepoll = result();
|
|
77 |
|
|
78 |
val lepoll_refl = subset_refl RS subset_imp_lepoll;
|
|
79 |
|
|
80 |
goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def]
|
|
81 |
"!!X Y. X eqpoll Y ==> X lepoll Y";
|
|
82 |
by (fast_tac ZF_cs 1);
|
|
83 |
val eqpoll_imp_lepoll = result();
|
|
84 |
|
|
85 |
goalw Cardinal.thy [lepoll_def]
|
|
86 |
"!!X Y. [| X lepoll Y; Y lepoll Z |] ==> X lepoll Z";
|
|
87 |
by (fast_tac (ZF_cs addIs [comp_inj]) 1);
|
|
88 |
val lepoll_trans = result();
|
|
89 |
|
|
90 |
(*Asymmetry law*)
|
|
91 |
goalw Cardinal.thy [lepoll_def,eqpoll_def]
|
|
92 |
"!!X Y. [| X lepoll Y; Y lepoll X |] ==> X eqpoll Y";
|
|
93 |
by (REPEAT (etac exE 1));
|
|
94 |
by (rtac schroeder_bernstein 1);
|
|
95 |
by (REPEAT (assume_tac 1));
|
|
96 |
val eqpollI = result();
|
|
97 |
|
|
98 |
val [major,minor] = goal Cardinal.thy
|
|
99 |
"[| X eqpoll Y; [| X lepoll Y; Y lepoll X |] ==> P |] ==> P";
|
437
|
100 |
by (rtac minor 1);
|
435
|
101 |
by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1));
|
|
102 |
val eqpollE = result();
|
|
103 |
|
|
104 |
goal Cardinal.thy "X eqpoll Y <-> X lepoll Y & Y lepoll X";
|
|
105 |
by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1);
|
|
106 |
val eqpoll_iff = result();
|
|
107 |
|
|
108 |
|
|
109 |
(** LEAST -- the least number operator [from HOL/Univ.ML] **)
|
|
110 |
|
|
111 |
val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
|
|
112 |
"[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (LEAST x.P(x)) = i";
|
|
113 |
by (rtac the_equality 1);
|
|
114 |
by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1);
|
|
115 |
by (REPEAT (etac conjE 1));
|
437
|
116 |
by (etac (premOrd RS Ord_linear_lt) 1);
|
435
|
117 |
by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot])));
|
|
118 |
val Least_equality = result();
|
|
119 |
|
|
120 |
goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> P(LEAST x.P(x))";
|
|
121 |
by (etac rev_mp 1);
|
|
122 |
by (trans_ind_tac "i" [] 1);
|
|
123 |
by (rtac impI 1);
|
|
124 |
by (rtac classical 1);
|
|
125 |
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
|
|
126 |
by (assume_tac 2);
|
|
127 |
by (fast_tac (ZF_cs addSEs [ltE]) 1);
|
|
128 |
val LeastI = result();
|
|
129 |
|
|
130 |
(*Proof is almost identical to the one above!*)
|
|
131 |
goal Cardinal.thy "!!i. [| P(i); Ord(i) |] ==> (LEAST x.P(x)) le i";
|
|
132 |
by (etac rev_mp 1);
|
|
133 |
by (trans_ind_tac "i" [] 1);
|
|
134 |
by (rtac impI 1);
|
|
135 |
by (rtac classical 1);
|
|
136 |
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
|
|
137 |
by (etac le_refl 2);
|
|
138 |
by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);
|
|
139 |
val Least_le = result();
|
|
140 |
|
|
141 |
(*LEAST really is the smallest*)
|
|
142 |
goal Cardinal.thy "!!i. [| P(i); i < (LEAST x.P(x)) |] ==> Q";
|
437
|
143 |
by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1);
|
435
|
144 |
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
|
|
145 |
val less_LeastE = result();
|
|
146 |
|
437
|
147 |
(*If there is no such P then LEAST is vacuously 0*)
|
|
148 |
goalw Cardinal.thy [Least_def]
|
|
149 |
"!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0";
|
|
150 |
by (rtac the_0 1);
|
|
151 |
by (fast_tac ZF_cs 1);
|
|
152 |
val Least_0 = result();
|
|
153 |
|
435
|
154 |
goal Cardinal.thy "Ord(LEAST x.P(x))";
|
437
|
155 |
by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);
|
435
|
156 |
by (safe_tac ZF_cs);
|
437
|
157 |
by (rtac (Least_le RS ltE) 2);
|
435
|
158 |
by (REPEAT_SOME assume_tac);
|
437
|
159 |
by (etac (Least_0 RS ssubst) 1);
|
|
160 |
by (rtac Ord_0 1);
|
435
|
161 |
val Ord_Least = result();
|
|
162 |
|
|
163 |
|
|
164 |
(** Basic properties of cardinals **)
|
|
165 |
|
|
166 |
(*Not needed for simplification, but helpful below*)
|
|
167 |
val prems = goal Cardinal.thy
|
|
168 |
"[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))";
|
|
169 |
by (simp_tac (FOL_ss addsimps prems) 1);
|
|
170 |
val Least_cong = result();
|
|
171 |
|
|
172 |
(*Need AC to prove X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le *)
|
|
173 |
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
|
437
|
174 |
by (rtac Least_cong 1);
|
435
|
175 |
by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1);
|
|
176 |
val cardinal_cong = result();
|
|
177 |
|
|
178 |
(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
|
|
179 |
goalw Cardinal.thy [eqpoll_def, cardinal_def]
|
|
180 |
"!!A. well_ord(A,r) ==> |A| eqpoll A";
|
437
|
181 |
by (rtac LeastI 1);
|
|
182 |
by (etac Ord_ordertype 2);
|
|
183 |
by (rtac exI 1);
|
467
|
184 |
by (etac (ordermap_bij RS bij_converse_bij) 1);
|
435
|
185 |
val well_ord_cardinal_eqpoll = result();
|
|
186 |
|
|
187 |
val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll
|
|
188 |
|> standard;
|
|
189 |
|
|
190 |
goal Cardinal.thy
|
|
191 |
"!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y";
|
437
|
192 |
by (rtac (eqpoll_sym RS eqpoll_trans) 1);
|
|
193 |
by (etac well_ord_cardinal_eqpoll 1);
|
435
|
194 |
by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1);
|
|
195 |
val well_ord_cardinal_eqE = result();
|
|
196 |
|
|
197 |
|
|
198 |
(** Observations from Kunen, page 28 **)
|
|
199 |
|
|
200 |
goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i";
|
437
|
201 |
by (etac (eqpoll_refl RS Least_le) 1);
|
435
|
202 |
val Ord_cardinal_le = result();
|
|
203 |
|
484
|
204 |
goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> |K| = K";
|
437
|
205 |
by (etac sym 1);
|
435
|
206 |
val Card_cardinal_eq = result();
|
|
207 |
|
|
208 |
val prems = goalw Cardinal.thy [Card_def,cardinal_def]
|
|
209 |
"[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
|
437
|
210 |
by (rtac (Least_equality RS ssubst) 1);
|
435
|
211 |
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
|
|
212 |
val CardI = result();
|
|
213 |
|
|
214 |
goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)";
|
437
|
215 |
by (etac ssubst 1);
|
|
216 |
by (rtac Ord_Least 1);
|
435
|
217 |
val Card_is_Ord = result();
|
|
218 |
|
484
|
219 |
goalw Cardinal.thy [cardinal_def] "Ord(|A|)";
|
437
|
220 |
by (rtac Ord_Least 1);
|
435
|
221 |
val Ord_cardinal = result();
|
|
222 |
|
437
|
223 |
goal Cardinal.thy "Card(0)";
|
|
224 |
by (rtac (Ord_0 RS CardI) 1);
|
|
225 |
by (fast_tac (ZF_cs addSEs [ltE]) 1);
|
|
226 |
val Card_0 = result();
|
|
227 |
|
484
|
228 |
goalw Cardinal.thy [cardinal_def] "Card(|A|)";
|
437
|
229 |
by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1);
|
|
230 |
by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1);
|
|
231 |
by (rtac (Ord_Least RS CardI) 1);
|
|
232 |
by (safe_tac ZF_cs);
|
|
233 |
by (rtac less_LeastE 1);
|
|
234 |
by (assume_tac 2);
|
|
235 |
by (etac eqpoll_trans 1);
|
|
236 |
by (REPEAT (ares_tac [LeastI] 1));
|
|
237 |
val Card_cardinal = result();
|
|
238 |
|
435
|
239 |
(*Kunen's Lemma 10.5*)
|
|
240 |
goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|";
|
437
|
241 |
by (rtac (eqpollI RS cardinal_cong) 1);
|
|
242 |
by (etac (le_imp_subset RS subset_imp_lepoll) 1);
|
|
243 |
by (rtac lepoll_trans 1);
|
|
244 |
by (etac (le_imp_subset RS subset_imp_lepoll) 2);
|
|
245 |
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1);
|
|
246 |
by (rtac Ord_cardinal_eqpoll 1);
|
435
|
247 |
by (REPEAT (eresolve_tac [ltE, Ord_succD] 1));
|
|
248 |
val cardinal_eq_lemma = result();
|
|
249 |
|
|
250 |
goal Cardinal.thy "!!i j. i le j ==> |i| le |j|";
|
|
251 |
by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1);
|
|
252 |
by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));
|
437
|
253 |
by (rtac cardinal_eq_lemma 1);
|
|
254 |
by (assume_tac 2);
|
|
255 |
by (etac le_trans 1);
|
|
256 |
by (etac ltE 1);
|
|
257 |
by (etac Ord_cardinal_le 1);
|
435
|
258 |
val cardinal_mono = result();
|
|
259 |
|
|
260 |
(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
|
|
261 |
goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j";
|
437
|
262 |
by (rtac Ord_linear2 1);
|
435
|
263 |
by (REPEAT_SOME assume_tac);
|
437
|
264 |
by (etac (lt_trans2 RS lt_irrefl) 1);
|
|
265 |
by (etac cardinal_mono 1);
|
435
|
266 |
val cardinal_lt_imp_lt = result();
|
|
267 |
|
484
|
268 |
goal Cardinal.thy "!!i j. [| |i| < K; Ord(i); Card(K) |] ==> i < K";
|
435
|
269 |
by (asm_simp_tac (ZF_ss addsimps
|
|
270 |
[cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1);
|
|
271 |
val Card_lt_imp_lt = result();
|
|
272 |
|
484
|
273 |
goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)";
|
|
274 |
by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1);
|
|
275 |
val Card_lt_iff = result();
|
|
276 |
|
|
277 |
goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)";
|
|
278 |
by (asm_simp_tac (ZF_ss addsimps
|
|
279 |
[Card_lt_iff, Card_is_Ord, Ord_cardinal,
|
|
280 |
not_lt_iff_le RS iff_sym]) 1);
|
|
281 |
val Card_le_iff = result();
|
|
282 |
|
435
|
283 |
|
|
284 |
(** The swap operator [NOT USED] **)
|
|
285 |
|
|
286 |
goalw Cardinal.thy [swap_def]
|
|
287 |
"!!A. [| x:A; y:A |] ==> swap(A,x,y) : A->A";
|
|
288 |
by (REPEAT (ares_tac [lam_type,if_type] 1));
|
|
289 |
val swap_type = result();
|
|
290 |
|
|
291 |
goalw Cardinal.thy [swap_def]
|
|
292 |
"!!A. [| x:A; y:A; z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z";
|
|
293 |
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
|
|
294 |
val swap_swap_identity = result();
|
|
295 |
|
|
296 |
goal Cardinal.thy "!!A. [| x:A; y:A |] ==> swap(A,x,y) : bij(A,A)";
|
437
|
297 |
by (rtac nilpotent_imp_bijective 1);
|
435
|
298 |
by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2,
|
|
299 |
ballI, swap_swap_identity] 1));
|
|
300 |
val swap_bij = result();
|
|
301 |
|
|
302 |
(*** The finite cardinals ***)
|
|
303 |
|
|
304 |
(*Lemma suggested by Mike Fourman*)
|
|
305 |
val [prem] = goalw Cardinal.thy [inj_def]
|
|
306 |
"f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)";
|
437
|
307 |
by (rtac CollectI 1);
|
435
|
308 |
(*Proving it's in the function space m->n*)
|
|
309 |
by (cut_facts_tac [prem] 1);
|
437
|
310 |
by (rtac (if_type RS lam_type) 1);
|
|
311 |
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1);
|
|
312 |
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1);
|
435
|
313 |
(*Proving it's injective*)
|
|
314 |
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1);
|
|
315 |
(*Adding prem earlier would cause the simplifier to loop*)
|
|
316 |
by (cut_facts_tac [prem] 1);
|
437
|
317 |
by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1);
|
435
|
318 |
val inj_succ_succD = result();
|
|
319 |
|
|
320 |
val [prem] = goalw Cardinal.thy [lepoll_def]
|
|
321 |
"m:nat ==> ALL n: nat. m lepoll n --> m le n";
|
|
322 |
by (nat_ind_tac "m" [prem] 1);
|
|
323 |
by (fast_tac (ZF_cs addSIs [nat_0_le]) 1);
|
437
|
324 |
by (rtac ballI 1);
|
435
|
325 |
by (eres_inst_tac [("n","n")] natE 1);
|
|
326 |
by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1);
|
|
327 |
by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1);
|
|
328 |
val nat_lepoll_imp_le_lemma = result();
|
|
329 |
val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard;
|
|
330 |
|
|
331 |
goal Cardinal.thy
|
|
332 |
"!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
|
437
|
333 |
by (rtac iffI 1);
|
435
|
334 |
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
|
437
|
335 |
by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym]
|
|
336 |
addSEs [eqpollE]) 1);
|
435
|
337 |
val nat_eqpoll_iff = result();
|
|
338 |
|
|
339 |
goalw Cardinal.thy [Card_def,cardinal_def]
|
|
340 |
"!!n. n: nat ==> Card(n)";
|
437
|
341 |
by (rtac (Least_equality RS ssubst) 1);
|
435
|
342 |
by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
|
|
343 |
by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
|
437
|
344 |
by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1);
|
435
|
345 |
val nat_into_Card = result();
|
|
346 |
|
|
347 |
(*Part of Kunen's Lemma 10.6*)
|
|
348 |
goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P";
|
437
|
349 |
by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1);
|
435
|
350 |
by (REPEAT (ares_tac [nat_succI] 1));
|
|
351 |
val succ_lepoll_natE = result();
|
|
352 |
|
|
353 |
|
|
354 |
(*** The first infinite cardinal: Omega, or nat ***)
|
|
355 |
|
|
356 |
(*This implies Kunen's Lemma 10.6*)
|
|
357 |
goal Cardinal.thy "!!n. [| n<i; n:nat |] ==> ~ i lepoll n";
|
437
|
358 |
by (rtac notI 1);
|
435
|
359 |
by (rtac succ_lepoll_natE 1 THEN assume_tac 2);
|
|
360 |
by (rtac lepoll_trans 1 THEN assume_tac 2);
|
437
|
361 |
by (etac ltE 1);
|
435
|
362 |
by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1));
|
|
363 |
val lt_not_lepoll = result();
|
|
364 |
|
|
365 |
goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n";
|
437
|
366 |
by (rtac iffI 1);
|
435
|
367 |
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2);
|
|
368 |
by (rtac Ord_linear_lt 1);
|
|
369 |
by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord]));
|
|
370 |
by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN
|
|
371 |
REPEAT (assume_tac 1));
|
|
372 |
by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1)));
|
437
|
373 |
by (etac eqpoll_imp_lepoll 1);
|
435
|
374 |
val Ord_nat_eqpoll_iff = result();
|
|
375 |
|
437
|
376 |
goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";
|
|
377 |
by (rtac (Least_equality RS ssubst) 1);
|
|
378 |
by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
|
|
379 |
by (etac ltE 1);
|
|
380 |
by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
|
|
381 |
val Card_nat = result();
|
435
|
382 |
|
437
|
383 |
(*Allows showing that |i| is a limit cardinal*)
|
|
384 |
goal Cardinal.thy "!!i. nat le i ==> nat le |i|";
|
|
385 |
by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1);
|
|
386 |
by (etac cardinal_mono 1);
|
|
387 |
val nat_le_cardinal = result();
|
|
388 |
|