author | lcp |
Thu, 08 Dec 1994 13:38:13 +0100 | |
changeset 765 | 06a484afc603 |
parent 760 | f0200e91b272 |
child 782 | 200a16083201 |
permissions | -rw-r--r-- |
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)); |
|
760 | 20 |
qed "decomp_bnd_mono"; |
435 | 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); |
|
760 | 30 |
qed "Banach_last_equation"; |
435 | 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)); |
|
760 | 42 |
qed "decomposition"; |
435 | 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!! *) |
|
760 | 52 |
qed "schroeder_bernstein"; |
435 | 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); |
|
760 | 60 |
qed "eqpoll_refl"; |
435 | 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); |
|
760 | 64 |
qed "eqpoll_sym"; |
435 | 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); |
|
760 | 69 |
qed "eqpoll_trans"; |
435 | 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); |
|
760 | 76 |
qed "subset_imp_lepoll"; |
435 | 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); |
|
760 | 83 |
qed "eqpoll_imp_lepoll"; |
435 | 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); |
|
760 | 88 |
qed "lepoll_trans"; |
435 | 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)); |
|
760 | 96 |
qed "eqpollI"; |
435 | 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)); |
760 | 102 |
qed "eqpollE"; |
435 | 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); |
|
760 | 106 |
qed "eqpoll_iff"; |
435 | 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]))); |
760 | 118 |
qed "Least_equality"; |
435 | 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); |
|
760 | 128 |
qed "LeastI"; |
435 | 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); |
|
760 | 139 |
qed "Least_le"; |
435 | 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)); |
760 | 145 |
qed "less_LeastE"; |
435 | 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); |
|
760 | 152 |
qed "Least_0"; |
437 | 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); |
|
760 | 161 |
qed "Ord_Least"; |
435 | 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); |
|
760 | 170 |
qed "Least_cong"; |
435 | 171 |
|
765 | 172 |
(*Need AC to prove X lepoll Y ==> |X| le |Y| ; |
173 |
see well_ord_lepoll_imp_Card_le *) |
|
435 | 174 |
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|"; |
437 | 175 |
by (rtac Least_cong 1); |
435 | 176 |
by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); |
760 | 177 |
qed "cardinal_cong"; |
435 | 178 |
|
179 |
(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) |
|
180 |
goalw Cardinal.thy [eqpoll_def, cardinal_def] |
|
181 |
"!!A. well_ord(A,r) ==> |A| eqpoll A"; |
|
437 | 182 |
by (rtac LeastI 1); |
183 |
by (etac Ord_ordertype 2); |
|
184 |
by (rtac exI 1); |
|
467 | 185 |
by (etac (ordermap_bij RS bij_converse_bij) 1); |
760 | 186 |
qed "well_ord_cardinal_eqpoll"; |
435 | 187 |
|
188 |
val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll |
|
189 |
|> standard; |
|
190 |
||
191 |
goal Cardinal.thy |
|
192 |
"!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y"; |
|
437 | 193 |
by (rtac (eqpoll_sym RS eqpoll_trans) 1); |
194 |
by (etac well_ord_cardinal_eqpoll 1); |
|
435 | 195 |
by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); |
760 | 196 |
qed "well_ord_cardinal_eqE"; |
435 | 197 |
|
198 |
||
199 |
(** Observations from Kunen, page 28 **) |
|
200 |
||
201 |
goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i"; |
|
437 | 202 |
by (etac (eqpoll_refl RS Least_le) 1); |
760 | 203 |
qed "Ord_cardinal_le"; |
435 | 204 |
|
484 | 205 |
goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> |K| = K"; |
437 | 206 |
by (etac sym 1); |
760 | 207 |
qed "Card_cardinal_eq"; |
435 | 208 |
|
209 |
val prems = goalw Cardinal.thy [Card_def,cardinal_def] |
|
210 |
"[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)"; |
|
437 | 211 |
by (rtac (Least_equality RS ssubst) 1); |
435 | 212 |
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); |
760 | 213 |
qed "CardI"; |
435 | 214 |
|
215 |
goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; |
|
437 | 216 |
by (etac ssubst 1); |
217 |
by (rtac Ord_Least 1); |
|
760 | 218 |
qed "Card_is_Ord"; |
435 | 219 |
|
765 | 220 |
goal Cardinal.thy "!!K. Card(K) ==> K le |K|"; |
221 |
by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); |
|
222 |
val Card_cardinal_le = result(); |
|
223 |
||
484 | 224 |
goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; |
437 | 225 |
by (rtac Ord_Least 1); |
760 | 226 |
qed "Ord_cardinal"; |
435 | 227 |
|
437 | 228 |
goal Cardinal.thy "Card(0)"; |
229 |
by (rtac (Ord_0 RS CardI) 1); |
|
230 |
by (fast_tac (ZF_cs addSEs [ltE]) 1); |
|
760 | 231 |
qed "Card_0"; |
437 | 232 |
|
522 | 233 |
val [premK,premL] = goal Cardinal.thy |
234 |
"[| Card(K); Card(L) |] ==> Card(K Un L)"; |
|
235 |
by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1); |
|
236 |
by (asm_simp_tac |
|
237 |
(ZF_ss addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1); |
|
238 |
by (asm_simp_tac |
|
239 |
(ZF_ss addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1); |
|
760 | 240 |
qed "Card_Un"; |
522 | 241 |
|
242 |
(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) |
|
243 |
||
484 | 244 |
goalw Cardinal.thy [cardinal_def] "Card(|A|)"; |
437 | 245 |
by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1); |
246 |
by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1); |
|
247 |
by (rtac (Ord_Least RS CardI) 1); |
|
248 |
by (safe_tac ZF_cs); |
|
249 |
by (rtac less_LeastE 1); |
|
250 |
by (assume_tac 2); |
|
251 |
by (etac eqpoll_trans 1); |
|
252 |
by (REPEAT (ares_tac [LeastI] 1)); |
|
760 | 253 |
qed "Card_cardinal"; |
437 | 254 |
|
435 | 255 |
(*Kunen's Lemma 10.5*) |
256 |
goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|"; |
|
437 | 257 |
by (rtac (eqpollI RS cardinal_cong) 1); |
258 |
by (etac (le_imp_subset RS subset_imp_lepoll) 1); |
|
259 |
by (rtac lepoll_trans 1); |
|
260 |
by (etac (le_imp_subset RS subset_imp_lepoll) 2); |
|
261 |
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1); |
|
262 |
by (rtac Ord_cardinal_eqpoll 1); |
|
435 | 263 |
by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); |
760 | 264 |
qed "cardinal_eq_lemma"; |
435 | 265 |
|
266 |
goal Cardinal.thy "!!i j. i le j ==> |i| le |j|"; |
|
267 |
by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1); |
|
268 |
by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); |
|
437 | 269 |
by (rtac cardinal_eq_lemma 1); |
270 |
by (assume_tac 2); |
|
271 |
by (etac le_trans 1); |
|
272 |
by (etac ltE 1); |
|
273 |
by (etac Ord_cardinal_le 1); |
|
760 | 274 |
qed "cardinal_mono"; |
435 | 275 |
|
276 |
(*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*) |
|
277 |
goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"; |
|
437 | 278 |
by (rtac Ord_linear2 1); |
435 | 279 |
by (REPEAT_SOME assume_tac); |
437 | 280 |
by (etac (lt_trans2 RS lt_irrefl) 1); |
281 |
by (etac cardinal_mono 1); |
|
760 | 282 |
qed "cardinal_lt_imp_lt"; |
435 | 283 |
|
484 | 284 |
goal Cardinal.thy "!!i j. [| |i| < K; Ord(i); Card(K) |] ==> i < K"; |
435 | 285 |
by (asm_simp_tac (ZF_ss addsimps |
286 |
[cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); |
|
760 | 287 |
qed "Card_lt_imp_lt"; |
435 | 288 |
|
484 | 289 |
goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"; |
290 |
by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1); |
|
760 | 291 |
qed "Card_lt_iff"; |
484 | 292 |
|
293 |
goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"; |
|
294 |
by (asm_simp_tac (ZF_ss addsimps |
|
295 |
[Card_lt_iff, Card_is_Ord, Ord_cardinal, |
|
296 |
not_lt_iff_le RS iff_sym]) 1); |
|
760 | 297 |
qed "Card_le_iff"; |
484 | 298 |
|
435 | 299 |
|
300 |
(** The swap operator [NOT USED] **) |
|
301 |
||
302 |
goalw Cardinal.thy [swap_def] |
|
303 |
"!!A. [| x:A; y:A |] ==> swap(A,x,y) : A->A"; |
|
304 |
by (REPEAT (ares_tac [lam_type,if_type] 1)); |
|
760 | 305 |
qed "swap_type"; |
435 | 306 |
|
307 |
goalw Cardinal.thy [swap_def] |
|
308 |
"!!A. [| x:A; y:A; z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z"; |
|
309 |
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
|
760 | 310 |
qed "swap_swap_identity"; |
435 | 311 |
|
312 |
goal Cardinal.thy "!!A. [| x:A; y:A |] ==> swap(A,x,y) : bij(A,A)"; |
|
437 | 313 |
by (rtac nilpotent_imp_bijective 1); |
435 | 314 |
by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2, |
315 |
ballI, swap_swap_identity] 1)); |
|
760 | 316 |
qed "swap_bij"; |
435 | 317 |
|
318 |
(*** The finite cardinals ***) |
|
319 |
||
320 |
(*Lemma suggested by Mike Fourman*) |
|
321 |
val [prem] = goalw Cardinal.thy [inj_def] |
|
322 |
"f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)"; |
|
437 | 323 |
by (rtac CollectI 1); |
435 | 324 |
(*Proving it's in the function space m->n*) |
325 |
by (cut_facts_tac [prem] 1); |
|
437 | 326 |
by (rtac (if_type RS lam_type) 1); |
327 |
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1); |
|
328 |
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS succE]) 1); |
|
435 | 329 |
(*Proving it's injective*) |
330 |
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
|
331 |
(*Adding prem earlier would cause the simplifier to loop*) |
|
332 |
by (cut_facts_tac [prem] 1); |
|
437 | 333 |
by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1); |
760 | 334 |
qed "inj_succ_succD"; |
435 | 335 |
|
336 |
val [prem] = goalw Cardinal.thy [lepoll_def] |
|
337 |
"m:nat ==> ALL n: nat. m lepoll n --> m le n"; |
|
338 |
by (nat_ind_tac "m" [prem] 1); |
|
339 |
by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); |
|
437 | 340 |
by (rtac ballI 1); |
435 | 341 |
by (eres_inst_tac [("n","n")] natE 1); |
342 |
by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
|
343 |
by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1); |
|
760 | 344 |
qed "nat_lepoll_imp_le_lemma"; |
435 | 345 |
val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard; |
346 |
||
347 |
goal Cardinal.thy |
|
348 |
"!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n"; |
|
437 | 349 |
by (rtac iffI 1); |
435 | 350 |
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
437 | 351 |
by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] |
352 |
addSEs [eqpollE]) 1); |
|
760 | 353 |
qed "nat_eqpoll_iff"; |
435 | 354 |
|
355 |
goalw Cardinal.thy [Card_def,cardinal_def] |
|
356 |
"!!n. n: nat ==> Card(n)"; |
|
437 | 357 |
by (rtac (Least_equality RS ssubst) 1); |
435 | 358 |
by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); |
359 |
by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); |
|
437 | 360 |
by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1); |
760 | 361 |
qed "nat_into_Card"; |
435 | 362 |
|
363 |
(*Part of Kunen's Lemma 10.6*) |
|
364 |
goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P"; |
|
437 | 365 |
by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); |
435 | 366 |
by (REPEAT (ares_tac [nat_succI] 1)); |
760 | 367 |
qed "succ_lepoll_natE"; |
435 | 368 |
|
369 |
||
370 |
(*** The first infinite cardinal: Omega, or nat ***) |
|
371 |
||
372 |
(*This implies Kunen's Lemma 10.6*) |
|
373 |
goal Cardinal.thy "!!n. [| n<i; n:nat |] ==> ~ i lepoll n"; |
|
437 | 374 |
by (rtac notI 1); |
435 | 375 |
by (rtac succ_lepoll_natE 1 THEN assume_tac 2); |
376 |
by (rtac lepoll_trans 1 THEN assume_tac 2); |
|
437 | 377 |
by (etac ltE 1); |
435 | 378 |
by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); |
760 | 379 |
qed "lt_not_lepoll"; |
435 | 380 |
|
381 |
goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n"; |
|
437 | 382 |
by (rtac iffI 1); |
435 | 383 |
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
384 |
by (rtac Ord_linear_lt 1); |
|
385 |
by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); |
|
386 |
by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN |
|
387 |
REPEAT (assume_tac 1)); |
|
388 |
by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); |
|
437 | 389 |
by (etac eqpoll_imp_lepoll 1); |
760 | 390 |
qed "Ord_nat_eqpoll_iff"; |
435 | 391 |
|
437 | 392 |
goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; |
393 |
by (rtac (Least_equality RS ssubst) 1); |
|
394 |
by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); |
|
395 |
by (etac ltE 1); |
|
396 |
by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); |
|
760 | 397 |
qed "Card_nat"; |
435 | 398 |
|
437 | 399 |
(*Allows showing that |i| is a limit cardinal*) |
400 |
goal Cardinal.thy "!!i. nat le i ==> nat le |i|"; |
|
401 |
by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1); |
|
402 |
by (etac cardinal_mono 1); |
|
760 | 403 |
qed "nat_le_cardinal"; |
437 | 404 |
|
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
405 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
406 |
(*** Towards Cardinal Arithmetic ***) |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
407 |
(** Congruence laws for successor, cardinal addition and multiplication **) |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
408 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
409 |
val case_ss = ZF_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff, |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
410 |
case_Inl, case_Inr, InlI, InrI]; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
411 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
412 |
val bij_inverse_ss = |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
413 |
case_ss addsimps [bij_is_fun RS apply_type, |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
414 |
bij_converse_bij RS bij_is_fun RS apply_type, |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
415 |
left_inverse_bij, right_inverse_bij]; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
416 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
417 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
418 |
(*Congruence law for cons under equipollence*) |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
419 |
goalw Cardinal.thy [lepoll_def] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
420 |
"!!A B. [| A lepoll B; b ~: B |] ==> cons(a,A) lepoll cons(b,B)"; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
421 |
by (safe_tac ZF_cs); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
422 |
by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
423 |
by (res_inst_tac [("d","%z.if(z:B, converse(f)`z, a)")] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
424 |
lam_injective 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
425 |
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, cons_iff] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
426 |
setloop etac consE') 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
427 |
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
428 |
setloop etac consE') 1); |
760 | 429 |
qed "cons_lepoll_cong"; |
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
430 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
431 |
goal Cardinal.thy |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
432 |
"!!A B. [| A eqpoll B; a ~: A; b ~: B |] ==> cons(a,A) eqpoll cons(b,B)"; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
433 |
by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff, cons_lepoll_cong]) 1); |
760 | 434 |
qed "cons_eqpoll_cong"; |
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
435 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
436 |
(*Congruence law for succ under equipollence*) |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
437 |
goalw Cardinal.thy [succ_def] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
438 |
"!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)"; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
439 |
by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); |
760 | 440 |
qed "succ_eqpoll_cong"; |
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
441 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
442 |
(*Congruence law for + under equipollence*) |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
443 |
goalw Cardinal.thy [eqpoll_def] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
444 |
"!!A B C D. [| A eqpoll C; B eqpoll D |] ==> A+B eqpoll C+D"; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
445 |
by (safe_tac ZF_cs); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
446 |
by (rtac exI 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
447 |
by (res_inst_tac [("c", "case(%x. Inl(f`x), %y. Inr(fa`y))"), |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
448 |
("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
449 |
lam_bijective 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
450 |
by (safe_tac (ZF_cs addSEs [sumE])); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
451 |
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); |
760 | 452 |
qed "sum_eqpoll_cong"; |
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
453 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
454 |
(*Congruence law for * under equipollence*) |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
455 |
goalw Cardinal.thy [eqpoll_def] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
456 |
"!!A B C D. [| A eqpoll C; B eqpoll D |] ==> A*B eqpoll C*D"; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
457 |
by (safe_tac ZF_cs); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
458 |
by (rtac exI 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
459 |
by (res_inst_tac [("c", "split(%x y. <f`x, fa`y>)"), |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
460 |
("d", "split(%x y. <converse(f)`x, converse(fa)`y>)")] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
461 |
lam_bijective 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
462 |
by (safe_tac ZF_cs); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
463 |
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); |
760 | 464 |
qed "prod_eqpoll_cong"; |
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
465 |
|
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
466 |
goalw Cardinal.thy [eqpoll_def] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
467 |
"!!f. [| f: inj(A,B); A Int B = 0 |] ==> A Un (B - range(f)) eqpoll B"; |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
468 |
by (rtac exI 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
469 |
by (res_inst_tac [("c", "%x. if(x:A, f`x, x)"), |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
470 |
("d", "%y. if(y: range(f), converse(f)`y, y)")] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
471 |
lam_bijective 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
472 |
by (fast_tac (ZF_cs addSIs [if_type, apply_type] addIs [inj_is_fun]) 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
473 |
by (asm_simp_tac |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
474 |
(ZF_ss addsimps [inj_converse_fun RS apply_funtype] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
475 |
setloop split_tac [expand_if]) 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
476 |
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
477 |
setloop etac UnE') 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
478 |
by (asm_simp_tac |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
479 |
(ZF_ss addsimps [inj_converse_fun RS apply_funtype, right_inverse] |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
480 |
setloop split_tac [expand_if]) 1); |
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset
|
481 |
by (fast_tac (ZF_cs addEs [equals0D]) 1); |
760 | 482 |
qed "inj_disjoint_eqpoll"; |