|
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"; |
|
58 br exI 1; |
|
59 br id_bij 1; |
|
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"; |
|
74 br exI 1; |
|
75 be id_subset_inj 1; |
|
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"; |
|
100 br minor 1; |
|
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)); |
|
116 be (premOrd RS Ord_linear_lt) 1; |
|
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"; |
|
143 br (Least_le RSN (2,lt_trans2) RS lt_anti_refl) 1; |
|
144 by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); |
|
145 val less_LeastE = result(); |
|
146 |
|
147 goal Cardinal.thy "Ord(LEAST x.P(x))"; |
|
148 by (res_inst_tac [("Q","EX i. Ord(i) & P(i)")] (excluded_middle RS disjE) 1); |
|
149 by (safe_tac ZF_cs); |
|
150 br (Least_le RS ltE) 2; |
|
151 by (REPEAT_SOME assume_tac); |
|
152 bw Least_def; |
|
153 by (rtac (the_0 RS ssubst) 1 THEN rtac Ord_0 2); |
|
154 by (fast_tac FOL_cs 1); |
|
155 val Ord_Least = result(); |
|
156 |
|
157 |
|
158 (** Basic properties of cardinals **) |
|
159 |
|
160 (*Not needed for simplification, but helpful below*) |
|
161 val prems = goal Cardinal.thy |
|
162 "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))"; |
|
163 by (simp_tac (FOL_ss addsimps prems) 1); |
|
164 val Least_cong = result(); |
|
165 |
|
166 (*Need AC to prove X lepoll Y ==> |X| le |Y| ; see well_ord_lepoll_imp_le *) |
|
167 goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|"; |
|
168 br Least_cong 1; |
|
169 by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); |
|
170 val cardinal_cong = result(); |
|
171 |
|
172 (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*) |
|
173 goalw Cardinal.thy [eqpoll_def, cardinal_def] |
|
174 "!!A. well_ord(A,r) ==> |A| eqpoll A"; |
|
175 br LeastI 1; |
|
176 be Ord_ordertype 2; |
|
177 br exI 1; |
|
178 be (ordertype_bij RS bij_converse_bij) 1; |
|
179 val well_ord_cardinal_eqpoll = result(); |
|
180 |
|
181 val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll |
|
182 |> standard; |
|
183 |
|
184 goal Cardinal.thy |
|
185 "!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y"; |
|
186 br (eqpoll_sym RS eqpoll_trans) 1; |
|
187 be well_ord_cardinal_eqpoll 1; |
|
188 by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); |
|
189 val well_ord_cardinal_eqE = result(); |
|
190 |
|
191 |
|
192 (** Observations from Kunen, page 28 **) |
|
193 |
|
194 goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> |i| le i"; |
|
195 be (eqpoll_refl RS Least_le) 1; |
|
196 val Ord_cardinal_le = result(); |
|
197 |
|
198 goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> |i| = i"; |
|
199 be sym 1; |
|
200 val Card_cardinal_eq = result(); |
|
201 |
|
202 val prems = goalw Cardinal.thy [Card_def,cardinal_def] |
|
203 "[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)"; |
|
204 br (Least_equality RS ssubst) 1; |
|
205 by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); |
|
206 val CardI = result(); |
|
207 |
|
208 goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; |
|
209 be ssubst 1; |
|
210 br Ord_Least 1; |
|
211 val Card_is_Ord = result(); |
|
212 |
|
213 goalw Cardinal.thy [cardinal_def] "Ord( |i| )"; |
|
214 br Ord_Least 1; |
|
215 val Ord_cardinal = result(); |
|
216 |
|
217 (*Kunen's Lemma 10.5*) |
|
218 goal Cardinal.thy "!!i j. [| |i| le j; j le i |] ==> |j| = |i|"; |
|
219 br (eqpollI RS cardinal_cong) 1; |
|
220 be (le_imp_subset RS subset_imp_lepoll) 1; |
|
221 br lepoll_trans 1; |
|
222 be (le_imp_subset RS subset_imp_lepoll) 2; |
|
223 br (eqpoll_sym RS eqpoll_imp_lepoll) 1; |
|
224 br Ord_cardinal_eqpoll 1; |
|
225 by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); |
|
226 val cardinal_eq_lemma = result(); |
|
227 |
|
228 goal Cardinal.thy "!!i j. i le j ==> |i| le |j|"; |
|
229 by (res_inst_tac [("i","|i|"),("j","|j|")] Ord_linear_le 1); |
|
230 by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); |
|
231 br cardinal_eq_lemma 1; |
|
232 ba 2; |
|
233 be le_trans 1; |
|
234 be ltE 1; |
|
235 be Ord_cardinal_le 1; |
|
236 val cardinal_mono = result(); |
|
237 |
|
238 (*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*) |
|
239 goal Cardinal.thy "!!i j. [| |i| < |j|; Ord(i); Ord(j) |] ==> i < j"; |
|
240 br Ord_linear2 1; |
|
241 by (REPEAT_SOME assume_tac); |
|
242 be (lt_trans2 RS lt_anti_refl) 1; |
|
243 be cardinal_mono 1; |
|
244 val cardinal_lt_imp_lt = result(); |
|
245 |
|
246 goal Cardinal.thy "!!i j. [| |i| < k; Ord(i); Card(k) |] ==> i < k"; |
|
247 by (asm_simp_tac (ZF_ss addsimps |
|
248 [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); |
|
249 val Card_lt_imp_lt = result(); |
|
250 |
|
251 |
|
252 (** The swap operator [NOT USED] **) |
|
253 |
|
254 goalw Cardinal.thy [swap_def] |
|
255 "!!A. [| x:A; y:A |] ==> swap(A,x,y) : A->A"; |
|
256 by (REPEAT (ares_tac [lam_type,if_type] 1)); |
|
257 val swap_type = result(); |
|
258 |
|
259 goalw Cardinal.thy [swap_def] |
|
260 "!!A. [| x:A; y:A; z:A |] ==> swap(A,x,y)`(swap(A,x,y)`z) = z"; |
|
261 by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
|
262 val swap_swap_identity = result(); |
|
263 |
|
264 goal Cardinal.thy "!!A. [| x:A; y:A |] ==> swap(A,x,y) : bij(A,A)"; |
|
265 br nilpotent_imp_bijective 1; |
|
266 by (REPEAT (ares_tac [swap_type, comp_eq_id_iff RS iffD2, |
|
267 ballI, swap_swap_identity] 1)); |
|
268 val swap_bij = result(); |
|
269 |
|
270 (*** The finite cardinals ***) |
|
271 |
|
272 (*Lemma suggested by Mike Fourman*) |
|
273 val [prem] = goalw Cardinal.thy [inj_def] |
|
274 "f: inj(succ(m), succ(n)) ==> (lam x:m. if(f`x=n, f`m, f`x)) : inj(m,n)"; |
|
275 br CollectI 1; |
|
276 (*Proving it's in the function space m->n*) |
|
277 by (cut_facts_tac [prem] 1); |
|
278 br (if_type RS lam_type) 1; |
|
279 by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1); |
|
280 by (fast_tac (ZF_cs addSEs [mem_anti_refl] addEs [apply_funtype RS succE]) 1); |
|
281 (*Proving it's injective*) |
|
282 by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); |
|
283 (*Adding prem earlier would cause the simplifier to loop*) |
|
284 by (cut_facts_tac [prem] 1); |
|
285 by (fast_tac (ZF_cs addSEs [mem_anti_refl]) 1); |
|
286 val inj_succ_succD = result(); |
|
287 |
|
288 val [prem] = goalw Cardinal.thy [lepoll_def] |
|
289 "m:nat ==> ALL n: nat. m lepoll n --> m le n"; |
|
290 by (nat_ind_tac "m" [prem] 1); |
|
291 by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); |
|
292 br ballI 1; |
|
293 by (eres_inst_tac [("n","n")] natE 1); |
|
294 by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
|
295 by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1); |
|
296 val nat_lepoll_imp_le_lemma = result(); |
|
297 val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard; |
|
298 |
|
299 goal Cardinal.thy |
|
300 "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n"; |
|
301 br iffI 1; |
|
302 by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
|
303 by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_asym] addSEs [eqpollE]) 1); |
|
304 val nat_eqpoll_iff = result(); |
|
305 |
|
306 goalw Cardinal.thy [Card_def,cardinal_def] |
|
307 "!!n. n: nat ==> Card(n)"; |
|
308 br (Least_equality RS ssubst) 1; |
|
309 by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); |
|
310 by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); |
|
311 by (fast_tac (ZF_cs addSEs [lt_anti_refl]) 1); |
|
312 val nat_into_Card = result(); |
|
313 |
|
314 val Card_0 = nat_0I RS nat_into_Card; |
|
315 |
|
316 (*Part of Kunen's Lemma 10.6*) |
|
317 goal Cardinal.thy "!!n. [| succ(n) lepoll n; n:nat |] ==> P"; |
|
318 br (nat_lepoll_imp_le RS lt_anti_refl) 1; |
|
319 by (REPEAT (ares_tac [nat_succI] 1)); |
|
320 val succ_lepoll_natE = result(); |
|
321 |
|
322 |
|
323 (*** The first infinite cardinal: Omega, or nat ***) |
|
324 |
|
325 (*This implies Kunen's Lemma 10.6*) |
|
326 goal Cardinal.thy "!!n. [| n<i; n:nat |] ==> ~ i lepoll n"; |
|
327 br notI 1; |
|
328 by (rtac succ_lepoll_natE 1 THEN assume_tac 2); |
|
329 by (rtac lepoll_trans 1 THEN assume_tac 2); |
|
330 be ltE 1; |
|
331 by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); |
|
332 val lt_not_lepoll = result(); |
|
333 |
|
334 goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; |
|
335 br (Least_equality RS ssubst) 1; |
|
336 by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); |
|
337 be ltE 1; |
|
338 by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); |
|
339 val Card_nat = result(); |
|
340 |
|
341 goal Cardinal.thy "!!i n. [| Ord(i); n:nat |] ==> i eqpoll n <-> i=n"; |
|
342 br iffI 1; |
|
343 by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); |
|
344 by (rtac Ord_linear_lt 1); |
|
345 by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); |
|
346 by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN |
|
347 REPEAT (assume_tac 1)); |
|
348 by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); |
|
349 be eqpoll_imp_lepoll 1; |
|
350 val Ord_nat_eqpoll_iff = result(); |
|
351 |
|
352 |