55 by (rtac exI 1); |
55 by (rtac exI 1); |
56 by (rtac bij_0_sum 1); |
56 by (rtac bij_0_sum 1); |
57 qed "sum_0_eqpoll"; |
57 qed "sum_0_eqpoll"; |
58 |
58 |
59 goalw CardinalArith.thy [cadd_def] "!!K. Card(K) ==> 0 |+| K = K"; |
59 goalw CardinalArith.thy [cadd_def] "!!K. Card(K) ==> 0 |+| K = K"; |
60 by (asm_simp_tac (ZF_ss addsimps [sum_0_eqpoll RS cardinal_cong, |
60 by (asm_simp_tac (!simpset addsimps [sum_0_eqpoll RS cardinal_cong, |
61 Card_cardinal_eq]) 1); |
61 Card_cardinal_eq]) 1); |
62 qed "cadd_0"; |
62 qed "cadd_0"; |
63 |
63 |
64 (** Addition by another cardinal **) |
64 (** Addition by another cardinal **) |
65 |
65 |
66 goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A+B"; |
66 goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A+B"; |
67 by (res_inst_tac [("x", "lam x:A. Inl(x)")] exI 1); |
67 by (res_inst_tac [("x", "lam x:A. Inl(x)")] exI 1); |
68 by (asm_simp_tac (sum_ss addsimps [lam_type]) 1); |
68 by (asm_simp_tac (!simpset addsimps [lam_type]) 1); |
69 qed "sum_lepoll_self"; |
69 qed "sum_lepoll_self"; |
70 |
70 |
71 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*) |
71 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*) |
72 goalw CardinalArith.thy [cadd_def] |
72 goalw CardinalArith.thy [cadd_def] |
73 "!!K. [| Card(K); Ord(L) |] ==> K le (K |+| L)"; |
73 "!!K. [| Card(K); Ord(L) |] ==> K le (K |+| L)"; |
86 by (res_inst_tac |
86 by (res_inst_tac |
87 [("d", "case(%w. Inl(converse(f)`w), %y. Inr(converse(fa)`y))")] |
87 [("d", "case(%w. Inl(converse(f)`w), %y. Inr(converse(fa)`y))")] |
88 lam_injective 1); |
88 lam_injective 1); |
89 by (typechk_tac ([inj_is_fun, case_type, InlI, InrI] @ ZF_typechecks)); |
89 by (typechk_tac ([inj_is_fun, case_type, InlI, InrI] @ ZF_typechecks)); |
90 by (etac sumE 1); |
90 by (etac sumE 1); |
91 by (ALLGOALS (asm_simp_tac (sum_ss addsimps [left_inverse]))); |
91 by (ALLGOALS (asm_simp_tac (!simpset addsimps [left_inverse]))); |
92 qed "sum_lepoll_mono"; |
92 qed "sum_lepoll_mono"; |
93 |
93 |
94 goalw CardinalArith.thy [cadd_def] |
94 goalw CardinalArith.thy [cadd_def] |
95 "!!K. [| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)"; |
95 "!!K. [| K' le K; L' le L |] ==> (K' |+| L') le (K |+| L)"; |
96 by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); |
96 by (safe_tac (!claset addSDs [le_subset_iff RS iffD1])); |
97 by (rtac well_ord_lepoll_imp_Card_le 1); |
97 by (rtac well_ord_lepoll_imp_Card_le 1); |
98 by (REPEAT (ares_tac [sum_lepoll_mono, subset_imp_lepoll] 2)); |
98 by (REPEAT (ares_tac [sum_lepoll_mono, subset_imp_lepoll] 2)); |
99 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1)); |
99 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1)); |
100 qed "cadd_le_mono"; |
100 qed "cadd_le_mono"; |
101 |
101 |
105 by (rtac exI 1); |
105 by (rtac exI 1); |
106 by (res_inst_tac [("c", "%z.if(z=Inl(A),A+B,z)"), |
106 by (res_inst_tac [("c", "%z.if(z=Inl(A),A+B,z)"), |
107 ("d", "%z.if(z=A+B,Inl(A),z)")] |
107 ("d", "%z.if(z=A+B,Inl(A),z)")] |
108 lam_bijective 1); |
108 lam_bijective 1); |
109 by (ALLGOALS |
109 by (ALLGOALS |
110 (asm_simp_tac (case_ss addsimps [succI2, mem_imp_not_eq] |
110 (asm_simp_tac (!simpset addsimps [succI2, mem_imp_not_eq] |
111 setloop eresolve_tac [sumE,succE]))); |
111 setloop eresolve_tac [sumE,succE]))); |
112 qed "sum_succ_eqpoll"; |
112 qed "sum_succ_eqpoll"; |
113 |
113 |
114 (*Pulling the succ(...) outside the |...| requires m, n: nat *) |
114 (*Pulling the succ(...) outside the |...| requires m, n: nat *) |
115 (*Unconditional version requires AC*) |
115 (*Unconditional version requires AC*) |
206 by (rtac exI 1); |
206 by (rtac exI 1); |
207 by (resolve_tac [singleton_prod_bij RS bij_converse_bij] 1); |
207 by (resolve_tac [singleton_prod_bij RS bij_converse_bij] 1); |
208 qed "prod_singleton_eqpoll"; |
208 qed "prod_singleton_eqpoll"; |
209 |
209 |
210 goalw CardinalArith.thy [cmult_def, succ_def] "!!K. Card(K) ==> 1 |*| K = K"; |
210 goalw CardinalArith.thy [cmult_def, succ_def] "!!K. Card(K) ==> 1 |*| K = K"; |
211 by (asm_simp_tac (ZF_ss addsimps [prod_singleton_eqpoll RS cardinal_cong, |
211 by (asm_simp_tac (!simpset addsimps [prod_singleton_eqpoll RS cardinal_cong, |
212 Card_cardinal_eq]) 1); |
212 Card_cardinal_eq]) 1); |
213 qed "cmult_1"; |
213 qed "cmult_1"; |
214 |
214 |
215 (*** Some inequalities for multiplication ***) |
215 (*** Some inequalities for multiplication ***) |
216 |
216 |
217 goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A*A"; |
217 goalw CardinalArith.thy [lepoll_def, inj_def] "A lepoll A*A"; |
218 by (res_inst_tac [("x", "lam x:A. <x,x>")] exI 1); |
218 by (res_inst_tac [("x", "lam x:A. <x,x>")] exI 1); |
219 by (simp_tac (ZF_ss addsimps [lam_type]) 1); |
219 by (simp_tac (!simpset addsimps [lam_type]) 1); |
220 qed "prod_square_lepoll"; |
220 qed "prod_square_lepoll"; |
221 |
221 |
222 (*Could probably weaken the premise to well_ord(K,r), or remove using AC*) |
222 (*Could probably weaken the premise to well_ord(K,r), or remove using AC*) |
223 goalw CardinalArith.thy [cmult_def] "!!K. Card(K) ==> K le K |*| K"; |
223 goalw CardinalArith.thy [cmult_def] "!!K. Card(K) ==> K le K |*| K"; |
224 by (rtac le_trans 1); |
224 by (rtac le_trans 1); |
225 by (rtac well_ord_lepoll_imp_Card_le 2); |
225 by (rtac well_ord_lepoll_imp_Card_le 2); |
226 by (rtac prod_square_lepoll 3); |
226 by (rtac prod_square_lepoll 3); |
227 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord] 2)); |
227 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord] 2)); |
228 by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); |
228 by (asm_simp_tac (!simpset addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); |
229 qed "cmult_square_le"; |
229 qed "cmult_square_le"; |
230 |
230 |
231 (** Multiplication by a non-zero cardinal **) |
231 (** Multiplication by a non-zero cardinal **) |
232 |
232 |
233 goalw CardinalArith.thy [lepoll_def, inj_def] "!!b. b: B ==> A lepoll A*B"; |
233 goalw CardinalArith.thy [lepoll_def, inj_def] "!!b. b: B ==> A lepoll A*B"; |
234 by (res_inst_tac [("x", "lam x:A. <x,b>")] exI 1); |
234 by (res_inst_tac [("x", "lam x:A. <x,b>")] exI 1); |
235 by (asm_simp_tac (ZF_ss addsimps [lam_type]) 1); |
235 by (asm_simp_tac (!simpset addsimps [lam_type]) 1); |
236 qed "prod_lepoll_self"; |
236 qed "prod_lepoll_self"; |
237 |
237 |
238 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*) |
238 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*) |
239 goalw CardinalArith.thy [cmult_def] |
239 goalw CardinalArith.thy [cmult_def] |
240 "!!K. [| Card(K); Ord(L); 0<L |] ==> K le (K |*| L)"; |
240 "!!K. [| Card(K); Ord(L); 0<L |] ==> K le (K |*| L)"; |
251 by (res_inst_tac [("x", "lam <w,y>:A*B. <f`w, fa`y>")] exI 1); |
251 by (res_inst_tac [("x", "lam <w,y>:A*B. <f`w, fa`y>")] exI 1); |
252 by (res_inst_tac [("d", "%<w,y>.<converse(f)`w, converse(fa)`y>")] |
252 by (res_inst_tac [("d", "%<w,y>.<converse(f)`w, converse(fa)`y>")] |
253 lam_injective 1); |
253 lam_injective 1); |
254 by (typechk_tac (inj_is_fun::ZF_typechecks)); |
254 by (typechk_tac (inj_is_fun::ZF_typechecks)); |
255 by (etac SigmaE 1); |
255 by (etac SigmaE 1); |
256 by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1); |
256 by (asm_simp_tac (!simpset addsimps [left_inverse]) 1); |
257 qed "prod_lepoll_mono"; |
257 qed "prod_lepoll_mono"; |
258 |
258 |
259 goalw CardinalArith.thy [cmult_def] |
259 goalw CardinalArith.thy [cmult_def] |
260 "!!K. [| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)"; |
260 "!!K. [| K' le K; L' le L |] ==> (K' |*| L') le (K |*| L)"; |
261 by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); |
261 by (safe_tac (!claset addSDs [le_subset_iff RS iffD1])); |
262 by (rtac well_ord_lepoll_imp_Card_le 1); |
262 by (rtac well_ord_lepoll_imp_Card_le 1); |
263 by (REPEAT (ares_tac [prod_lepoll_mono, subset_imp_lepoll] 2)); |
263 by (REPEAT (ares_tac [prod_lepoll_mono, subset_imp_lepoll] 2)); |
264 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); |
264 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); |
265 qed "cmult_le_mono"; |
265 qed "cmult_le_mono"; |
266 |
266 |
269 goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B"; |
269 goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B"; |
270 by (rtac exI 1); |
270 by (rtac exI 1); |
271 by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"), |
271 by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"), |
272 ("d", "case(%y. <A,y>, %z.z)")] |
272 ("d", "case(%y. <A,y>, %z.z)")] |
273 lam_bijective 1); |
273 lam_bijective 1); |
274 by (safe_tac (ZF_cs addSEs [sumE])); |
274 by (safe_tac (!claset addSEs [sumE])); |
275 by (ALLGOALS |
275 by (ALLGOALS |
276 (asm_simp_tac (case_ss addsimps [succI2, if_type, mem_imp_not_eq]))); |
276 (asm_simp_tac (!simpset addsimps [succI2, if_type, mem_imp_not_eq]))); |
277 qed "prod_succ_eqpoll"; |
277 qed "prod_succ_eqpoll"; |
278 |
278 |
279 (*Unconditional version requires AC*) |
279 (*Unconditional version requires AC*) |
280 goalw CardinalArith.thy [cmult_def, cadd_def] |
280 goalw CardinalArith.thy [cmult_def, cadd_def] |
281 "!!m n. [| Ord(m); Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"; |
281 "!!m n. [| Ord(m); Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"; |
287 |
287 |
288 val [mnat,nnat] = goal CardinalArith.thy |
288 val [mnat,nnat] = goal CardinalArith.thy |
289 "[| m: nat; n: nat |] ==> m |*| n = m#*n"; |
289 "[| m: nat; n: nat |] ==> m |*| n = m#*n"; |
290 by (cut_facts_tac [nnat] 1); |
290 by (cut_facts_tac [nnat] 1); |
291 by (nat_ind_tac "m" [mnat] 1); |
291 by (nat_ind_tac "m" [mnat] 1); |
292 by (asm_simp_tac (arith_ss addsimps [cmult_0]) 1); |
292 by (asm_simp_tac (!simpset addsimps [cmult_0]) 1); |
293 by (asm_simp_tac (arith_ss addsimps [nat_into_Ord, cmult_succ_lemma, |
293 by (asm_simp_tac (!simpset addsimps [nat_into_Ord, cmult_succ_lemma, |
294 nat_cadd_eq_add]) 1); |
294 nat_cadd_eq_add]) 1); |
295 qed "nat_cmult_eq_mult"; |
295 qed "nat_cmult_eq_mult"; |
296 |
296 |
297 goal CardinalArith.thy "!!m n. Card(n) ==> 2 |*| n = n |+| n"; |
297 goal CardinalArith.thy "!!m n. Card(n) ==> 2 |*| n = n |+| n"; |
298 by (asm_simp_tac |
298 by (asm_simp_tac |
299 (ZF_ss addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, Card_is_Ord, |
299 (!simpset addsimps [Ord_0, Ord_succ, cmult_0, cmult_succ_lemma, Card_is_Ord, |
300 read_instantiate [("j","0")] cadd_commute, cadd_0]) 1); |
300 read_instantiate [("j","0")] cadd_commute, cadd_0]) 1); |
301 qed "cmult_2"; |
301 qed "cmult_2"; |
302 |
302 |
303 |
303 |
304 (*** Infinite Cardinals are Limit Ordinals ***) |
304 (*** Infinite Cardinals are Limit Ordinals ***) |
314 "lam z:cons(u,A). if(z=u, f`0, \ |
314 "lam z:cons(u,A). if(z=u, f`0, \ |
315 \ if(z: range(f), f`succ(converse(f)`z), z))")] exI 1); |
315 \ if(z: range(f), f`succ(converse(f)`z), z))")] exI 1); |
316 by (res_inst_tac [("d", "%y. if(y: range(f), \ |
316 by (res_inst_tac [("d", "%y. if(y: range(f), \ |
317 \ nat_case(u, %z.f`z, converse(f)`y), y)")] |
317 \ nat_case(u, %z.f`z, converse(f)`y), y)")] |
318 lam_injective 1); |
318 lam_injective 1); |
319 by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI, apply_type] |
319 by (fast_tac (!claset addSIs [if_type, nat_0I, nat_succI, apply_type] |
320 addIs [inj_is_fun, inj_converse_fun]) 1); |
320 addIs [inj_is_fun, inj_converse_fun]) 1); |
321 by (asm_simp_tac |
321 by (asm_simp_tac |
322 (ZF_ss addsimps [inj_is_fun RS apply_rangeI, |
322 (!simpset addsimps [inj_is_fun RS apply_rangeI, |
323 inj_converse_fun RS apply_rangeI, |
323 inj_converse_fun RS apply_rangeI, |
324 inj_converse_fun RS apply_funtype, |
324 inj_converse_fun RS apply_funtype, |
325 left_inverse, right_inverse, nat_0I, nat_succI, |
325 left_inverse, right_inverse, nat_0I, nat_succI, |
326 nat_case_0, nat_case_succ] |
326 nat_case_0, nat_case_succ] |
327 setloop split_tac [expand_if]) 1); |
327 setloop split_tac [expand_if]) 1); |
336 goalw CardinalArith.thy [succ_def] "!!i. nat <= A ==> succ(A) eqpoll A"; |
336 goalw CardinalArith.thy [succ_def] "!!i. nat <= A ==> succ(A) eqpoll A"; |
337 by (eresolve_tac [subset_imp_lepoll RS nat_cons_eqpoll] 1); |
337 by (eresolve_tac [subset_imp_lepoll RS nat_cons_eqpoll] 1); |
338 qed "nat_succ_eqpoll"; |
338 qed "nat_succ_eqpoll"; |
339 |
339 |
340 goalw CardinalArith.thy [InfCard_def] "InfCard(nat)"; |
340 goalw CardinalArith.thy [InfCard_def] "InfCard(nat)"; |
341 by (fast_tac (ZF_cs addIs [Card_nat, le_refl, Card_is_Ord]) 1); |
341 by (fast_tac (!claset addIs [Card_nat, le_refl, Card_is_Ord]) 1); |
342 qed "InfCard_nat"; |
342 qed "InfCard_nat"; |
343 |
343 |
344 goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)"; |
344 goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)"; |
345 by (etac conjunct1 1); |
345 by (etac conjunct1 1); |
346 qed "InfCard_is_Card"; |
346 qed "InfCard_is_Card"; |
347 |
347 |
348 goalw CardinalArith.thy [InfCard_def] |
348 goalw CardinalArith.thy [InfCard_def] |
349 "!!K L. [| InfCard(K); Card(L) |] ==> InfCard(K Un L)"; |
349 "!!K L. [| InfCard(K); Card(L) |] ==> InfCard(K Un L)"; |
350 by (asm_simp_tac (ZF_ss addsimps [Card_Un, Un_upper1_le RSN (2,le_trans), |
350 by (asm_simp_tac (!simpset addsimps [Card_Un, Un_upper1_le RSN (2,le_trans), |
351 Card_is_Ord]) 1); |
351 Card_is_Ord]) 1); |
352 qed "InfCard_Un"; |
352 qed "InfCard_Un"; |
353 |
353 |
354 (*Kunen's Lemma 10.11*) |
354 (*Kunen's Lemma 10.11*) |
355 goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Limit(K)"; |
355 goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Limit(K)"; |
356 by (etac conjE 1); |
356 by (etac conjE 1); |
357 by (forward_tac [Card_is_Ord] 1); |
357 by (forward_tac [Card_is_Ord] 1); |
358 by (rtac (ltI RS non_succ_LimitI) 1); |
358 by (rtac (ltI RS non_succ_LimitI) 1); |
359 by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1); |
359 by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1); |
360 by (safe_tac (ZF_cs addSDs [Limit_nat RS Limit_le_succD])); |
360 by (safe_tac (!claset addSDs [Limit_nat RS Limit_le_succD])); |
361 by (rewtac Card_def); |
361 by (rewtac Card_def); |
362 by (dtac trans 1); |
362 by (dtac trans 1); |
363 by (etac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1); |
363 by (etac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1); |
364 by (etac (Ord_succD RS Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1); |
364 by (etac (Ord_succD RS Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1); |
365 by (REPEAT (ares_tac [le_eqI, Ord_cardinal] 1)); |
365 by (REPEAT (ares_tac [le_eqI, Ord_cardinal] 1)); |
370 |
370 |
371 (*A general fact about ordermap*) |
371 (*A general fact about ordermap*) |
372 goalw Cardinal.thy [eqpoll_def] |
372 goalw Cardinal.thy [eqpoll_def] |
373 "!!A. [| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)"; |
373 "!!A. [| well_ord(A,r); x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)"; |
374 by (rtac exI 1); |
374 by (rtac exI 1); |
375 by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, well_ord_is_wf]) 1); |
375 by (asm_simp_tac (!simpset addsimps [ordermap_eq_image, well_ord_is_wf]) 1); |
376 by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1); |
376 by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1); |
377 by (rtac pred_subset 1); |
377 by (rtac pred_subset 1); |
378 qed "ordermap_eqpoll_pred"; |
378 qed "ordermap_eqpoll_pred"; |
379 |
379 |
380 (** Establishing the well-ordering **) |
380 (** Establishing the well-ordering **) |
381 |
381 |
382 goalw CardinalArith.thy [inj_def] |
382 goalw CardinalArith.thy [inj_def] |
383 "!!K. Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)"; |
383 "!!K. Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)"; |
384 by (fast_tac (ZF_cs addss ZF_ss |
384 by (fast_tac (!claset addss (!simpset) |
385 addIs [lam_type, Un_least_lt RS ltD, ltI]) 1); |
385 addIs [lam_type, Un_least_lt RS ltD, ltI]) 1); |
386 qed "csquare_lam_inj"; |
386 qed "csquare_lam_inj"; |
387 |
387 |
388 goalw CardinalArith.thy [csquare_rel_def] |
388 goalw CardinalArith.thy [csquare_rel_def] |
389 "!!K. Ord(K) ==> well_ord(K*K, csquare_rel(K))"; |
389 "!!K. Ord(K) ==> well_ord(K*K, csquare_rel(K))"; |
395 |
395 |
396 goalw CardinalArith.thy [csquare_rel_def] |
396 goalw CardinalArith.thy [csquare_rel_def] |
397 "!!K. [| x<K; y<K; z<K |] ==> \ |
397 "!!K. [| x<K; y<K; z<K |] ==> \ |
398 \ <<x,y>, <z,z>> : csquare_rel(K) --> x le z & y le z"; |
398 \ <<x,y>, <z,z>> : csquare_rel(K) --> x le z & y le z"; |
399 by (REPEAT (etac ltE 1)); |
399 by (REPEAT (etac ltE 1)); |
400 by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
400 by (asm_simp_tac (!simpset addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
401 Un_absorb, Un_least_mem_iff, ltD]) 1); |
401 Un_absorb, Un_least_mem_iff, ltD]) 1); |
402 by (safe_tac (ZF_cs addSEs [mem_irrefl] |
402 by (safe_tac (!claset addSEs [mem_irrefl] |
403 addSIs [Un_upper1_le, Un_upper2_le])); |
403 addSIs [Un_upper1_le, Un_upper2_le])); |
404 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [lt_def, succI2, Ord_succ]))); |
404 by (ALLGOALS (asm_simp_tac (!simpset addsimps [lt_def, succI2, Ord_succ]))); |
405 val csquareD_lemma = result(); |
405 val csquareD_lemma = result(); |
406 |
406 |
407 bind_thm ("csquareD", csquareD_lemma RS mp); |
407 bind_thm ("csquareD", csquareD_lemma RS mp); |
408 |
408 |
409 goalw CardinalArith.thy [pred_def] |
409 goalw CardinalArith.thy [pred_def] |
410 "!!K. z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"; |
410 "!!K. z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"; |
411 by (safe_tac (lemmas_cs addSEs [SigmaE])); (*avoids using succCI*) |
411 by (safe_tac (claset_of"ZF" addSEs [SigmaE])); (*avoids using succCI,...*) |
412 by (rtac (csquareD RS conjE) 1); |
412 by (rtac (csquareD RS conjE) 1); |
413 by (rewtac lt_def); |
413 by (rewtac lt_def); |
414 by (assume_tac 4); |
414 by (assume_tac 4); |
415 by (ALLGOALS (fast_tac ZF_cs)); |
415 by (ALLGOALS Fast_tac); |
416 qed "pred_csquare_subset"; |
416 qed "pred_csquare_subset"; |
417 |
417 |
418 goalw CardinalArith.thy [csquare_rel_def] |
418 goalw CardinalArith.thy [csquare_rel_def] |
419 "!!K. [| x<z; y<z; z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K)"; |
419 "!!K. [| x<z; y<z; z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K)"; |
420 by (subgoals_tac ["x<K", "y<K"] 1); |
420 by (subgoals_tac ["x<K", "y<K"] 1); |
421 by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2)); |
421 by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2)); |
422 by (REPEAT (etac ltE 1)); |
422 by (REPEAT (etac ltE 1)); |
423 by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
423 by (asm_simp_tac (!simpset addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
424 Un_absorb, Un_least_mem_iff, ltD]) 1); |
424 Un_absorb, Un_least_mem_iff, ltD]) 1); |
425 qed "csquare_ltI"; |
425 qed "csquare_ltI"; |
426 |
426 |
427 (*Part of the traditional proof. UNUSED since it's harder to prove & apply *) |
427 (*Part of the traditional proof. UNUSED since it's harder to prove & apply *) |
428 goalw CardinalArith.thy [csquare_rel_def] |
428 goalw CardinalArith.thy [csquare_rel_def] |
429 "!!K. [| x le z; y le z; z<K |] ==> \ |
429 "!!K. [| x le z; y le z; z<K |] ==> \ |
430 \ <<x,y>, <z,z>> : csquare_rel(K) | x=z & y=z"; |
430 \ <<x,y>, <z,z>> : csquare_rel(K) | x=z & y=z"; |
431 by (subgoals_tac ["x<K", "y<K"] 1); |
431 by (subgoals_tac ["x<K", "y<K"] 1); |
432 by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2)); |
432 by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2)); |
433 by (REPEAT (etac ltE 1)); |
433 by (REPEAT (etac ltE 1)); |
434 by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
434 by (asm_simp_tac (!simpset addsimps [rvimage_iff, rmult_iff, Memrel_iff, |
435 Un_absorb, Un_least_mem_iff, ltD]) 1); |
435 Un_absorb, Un_least_mem_iff, ltD]) 1); |
436 by (REPEAT_FIRST (etac succE)); |
436 by (REPEAT_FIRST (etac succE)); |
437 by (ALLGOALS |
437 by (ALLGOALS |
438 (asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iff_sym, |
438 (asm_simp_tac (!simpset addsimps [subset_Un_iff RS iff_sym, |
439 subset_Un_iff2 RS iff_sym, OrdmemD]))); |
439 subset_Un_iff2 RS iff_sym, OrdmemD]))); |
440 qed "csquare_or_eqI"; |
440 qed "csquare_or_eqI"; |
441 |
441 |
442 (** The cardinality of initial segments **) |
442 (** The cardinality of initial segments **) |
443 |
443 |
445 "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \ |
445 "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \ |
446 \ ordermap(K*K, csquare_rel(K)) ` <x,y> < \ |
446 \ ordermap(K*K, csquare_rel(K)) ` <x,y> < \ |
447 \ ordermap(K*K, csquare_rel(K)) ` <z,z>"; |
447 \ ordermap(K*K, csquare_rel(K)) ` <z,z>"; |
448 by (subgoals_tac ["z<K", "well_ord(K*K, csquare_rel(K))"] 1); |
448 by (subgoals_tac ["z<K", "well_ord(K*K, csquare_rel(K))"] 1); |
449 by (etac (Limit_is_Ord RS well_ord_csquare) 2); |
449 by (etac (Limit_is_Ord RS well_ord_csquare) 2); |
450 by (fast_tac (ZF_cs addSIs [Un_least_lt, Limit_has_succ]) 2); |
450 by (fast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2); |
451 by (rtac (csquare_ltI RS ordermap_mono RS ltI) 1); |
451 by (rtac (csquare_ltI RS ordermap_mono RS ltI) 1); |
452 by (etac well_ord_is_wf 4); |
452 by (etac well_ord_is_wf 4); |
453 by (ALLGOALS |
453 by (ALLGOALS |
454 (fast_tac (ZF_cs addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap] |
454 (fast_tac (!claset addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap] |
455 addSEs [ltE]))); |
455 addSEs [ltE]))); |
456 qed "ordermap_z_lt"; |
456 qed "ordermap_z_lt"; |
457 |
457 |
458 (*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *) |
458 (*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *) |
459 goalw CardinalArith.thy [cmult_def] |
459 goalw CardinalArith.thy [cmult_def] |
460 "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \ |
460 "!!K. [| Limit(K); x<K; y<K; z=succ(x Un y) |] ==> \ |
461 \ | ordermap(K*K, csquare_rel(K)) ` <x,y> | le |succ(z)| |*| |succ(z)|"; |
461 \ | ordermap(K*K, csquare_rel(K)) ` <x,y> | le |succ(z)| |*| |succ(z)|"; |
462 by (rtac (well_ord_rmult RS well_ord_lepoll_imp_Card_le) 1); |
462 by (rtac (well_ord_rmult RS well_ord_lepoll_imp_Card_le) 1); |
463 by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1)); |
463 by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1)); |
464 by (subgoals_tac ["z<K"] 1); |
464 by (subgoals_tac ["z<K"] 1); |
465 by (fast_tac (ZF_cs addSIs [Un_least_lt, Limit_has_succ]) 2); |
465 by (fast_tac (!claset addSIs [Un_least_lt, Limit_has_succ]) 2); |
466 by (rtac (ordermap_z_lt RS leI RS le_imp_lepoll RS lepoll_trans) 1); |
466 by (rtac (ordermap_z_lt RS leI RS le_imp_lepoll RS lepoll_trans) 1); |
467 by (REPEAT_SOME assume_tac); |
467 by (REPEAT_SOME assume_tac); |
468 by (rtac (ordermap_eqpoll_pred RS eqpoll_imp_lepoll RS lepoll_trans) 1); |
468 by (rtac (ordermap_eqpoll_pred RS eqpoll_imp_lepoll RS lepoll_trans) 1); |
469 by (etac (Limit_is_Ord RS well_ord_csquare) 1); |
469 by (etac (Limit_is_Ord RS well_ord_csquare) 1); |
470 by (fast_tac (ZF_cs addIs [ltD]) 1); |
470 by (fast_tac (!claset addIs [ltD]) 1); |
471 by (rtac (pred_csquare_subset RS subset_imp_lepoll RS lepoll_trans) 1 THEN |
471 by (rtac (pred_csquare_subset RS subset_imp_lepoll RS lepoll_trans) 1 THEN |
472 assume_tac 1); |
472 assume_tac 1); |
473 by (REPEAT_FIRST (etac ltE)); |
473 by (REPEAT_FIRST (etac ltE)); |
474 by (rtac (prod_eqpoll_cong RS eqpoll_sym RS eqpoll_imp_lepoll) 1); |
474 by (rtac (prod_eqpoll_cong RS eqpoll_sym RS eqpoll_imp_lepoll) 1); |
475 by (REPEAT_FIRST (etac (Ord_succ RS Ord_cardinal_eqpoll))); |
475 by (REPEAT_FIRST (etac (Ord_succ RS Ord_cardinal_eqpoll))); |
484 by (assume_tac 1); |
484 by (assume_tac 1); |
485 by (etac (well_ord_csquare RS Ord_ordertype) 1); |
485 by (etac (well_ord_csquare RS Ord_ordertype) 1); |
486 by (rtac Card_lt_imp_lt 1); |
486 by (rtac Card_lt_imp_lt 1); |
487 by (etac InfCard_is_Card 3); |
487 by (etac InfCard_is_Card 3); |
488 by (etac ltE 2 THEN assume_tac 2); |
488 by (etac ltE 2 THEN assume_tac 2); |
489 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_unfold]) 1); |
489 by (asm_full_simp_tac (!simpset addsimps [ordertype_unfold]) 1); |
490 by (safe_tac (ZF_cs addSEs [ltE])); |
490 by (safe_tac (!claset addSEs [ltE])); |
491 by (subgoals_tac ["Ord(xb)", "Ord(y)"] 1); |
491 by (subgoals_tac ["Ord(xb)", "Ord(y)"] 1); |
492 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 2)); |
492 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 2)); |
493 by (rtac (InfCard_is_Limit RS ordermap_csquare_le RS lt_trans1) 1 THEN |
493 by (rtac (InfCard_is_Limit RS ordermap_csquare_le RS lt_trans1) 1 THEN |
494 REPEAT (ares_tac [refl] 1 ORELSE etac ltI 1)); |
494 REPEAT (ares_tac [refl] 1 ORELSE etac ltI 1)); |
495 by (res_inst_tac [("i","xb Un y"), ("j","nat")] Ord_linear2 1 THEN |
495 by (res_inst_tac [("i","xb Un y"), ("j","nat")] Ord_linear2 1 THEN |
496 REPEAT (ares_tac [Ord_Un, Ord_nat] 1)); |
496 REPEAT (ares_tac [Ord_Un, Ord_nat] 1)); |
497 (*the finite case: xb Un y < nat *) |
497 (*the finite case: xb Un y < nat *) |
498 by (res_inst_tac [("j", "nat")] lt_trans2 1); |
498 by (res_inst_tac [("j", "nat")] lt_trans2 1); |
499 by (asm_full_simp_tac (FOL_ss addsimps [InfCard_def]) 2); |
499 by (asm_full_simp_tac (!simpset addsimps [InfCard_def]) 2); |
500 by (asm_full_simp_tac |
500 by (asm_full_simp_tac |
501 (ZF_ss addsimps [lt_def, nat_cmult_eq_mult, nat_succI, mult_type, |
501 (!simpset addsimps [lt_def, nat_cmult_eq_mult, nat_succI, mult_type, |
502 nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1); |
502 nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1); |
503 (*case nat le (xb Un y) *) |
503 (*case nat le (xb Un y) *) |
504 by (asm_full_simp_tac |
504 by (asm_full_simp_tac |
505 (ZF_ss addsimps [le_imp_subset RS nat_succ_eqpoll RS cardinal_cong, |
505 (!simpset addsimps [le_imp_subset RS nat_succ_eqpoll RS cardinal_cong, |
506 le_succ_iff, InfCard_def, Card_cardinal, Un_least_lt, |
506 le_succ_iff, InfCard_def, Card_cardinal, Un_least_lt, |
507 Ord_Un, ltI, nat_le_cardinal, |
507 Ord_Un, ltI, nat_le_cardinal, |
508 Ord_cardinal_le RS lt_trans1 RS ltD]) 1); |
508 Ord_cardinal_le RS lt_trans1 RS ltD]) 1); |
509 qed "ordertype_csquare_le"; |
509 qed "ordertype_csquare_le"; |
510 |
510 |
531 "!!A. [| well_ord(A,r); InfCard(|A|) |] ==> A*A eqpoll A"; |
531 "!!A. [| well_ord(A,r); InfCard(|A|) |] ==> A*A eqpoll A"; |
532 by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1); |
532 by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1); |
533 by (REPEAT (etac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1)); |
533 by (REPEAT (etac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1)); |
534 by (rtac well_ord_cardinal_eqE 1); |
534 by (rtac well_ord_cardinal_eqE 1); |
535 by (REPEAT (ares_tac [Ord_cardinal, well_ord_rmult, well_ord_Memrel] 1)); |
535 by (REPEAT (ares_tac [Ord_cardinal, well_ord_rmult, well_ord_Memrel] 1)); |
536 by (asm_simp_tac (ZF_ss addsimps [symmetric cmult_def, InfCard_csquare_eq]) 1); |
536 by (asm_simp_tac (!simpset addsimps [symmetric cmult_def, InfCard_csquare_eq]) 1); |
537 qed "well_ord_InfCard_square_eq"; |
537 qed "well_ord_InfCard_square_eq"; |
538 |
538 |
539 (** Toward's Kunen's Corollary 10.13 (1) **) |
539 (** Toward's Kunen's Corollary 10.13 (1) **) |
540 |
540 |
541 goal CardinalArith.thy "!!K. [| InfCard(K); L le K; 0<L |] ==> K |*| L = K"; |
541 goal CardinalArith.thy "!!K. [| InfCard(K); L le K; 0<L |] ==> K |*| L = K"; |
542 by (rtac le_anti_sym 1); |
542 by (rtac le_anti_sym 1); |
543 by (etac ltE 2 THEN |
543 by (etac ltE 2 THEN |
544 REPEAT (ares_tac [cmult_le_self, InfCard_is_Card] 2)); |
544 REPEAT (ares_tac [cmult_le_self, InfCard_is_Card] 2)); |
545 by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); |
545 by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); |
546 by (resolve_tac [cmult_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); |
546 by (resolve_tac [cmult_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); |
547 by (asm_simp_tac (ZF_ss addsimps [InfCard_csquare_eq]) 1); |
547 by (asm_simp_tac (!simpset addsimps [InfCard_csquare_eq]) 1); |
548 qed "InfCard_le_cmult_eq"; |
548 qed "InfCard_le_cmult_eq"; |
549 |
549 |
550 (*Corollary 10.13 (1), for cardinal multiplication*) |
550 (*Corollary 10.13 (1), for cardinal multiplication*) |
551 goal CardinalArith.thy |
551 goal CardinalArith.thy |
552 "!!K. [| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L"; |
552 "!!K. [| InfCard(K); InfCard(L) |] ==> K |*| L = K Un L"; |
554 by (typechk_tac [InfCard_is_Card, Card_is_Ord]); |
554 by (typechk_tac [InfCard_is_Card, Card_is_Ord]); |
555 by (resolve_tac [cmult_commute RS ssubst] 1); |
555 by (resolve_tac [cmult_commute RS ssubst] 1); |
556 by (resolve_tac [Un_commute RS ssubst] 1); |
556 by (resolve_tac [Un_commute RS ssubst] 1); |
557 by (ALLGOALS |
557 by (ALLGOALS |
558 (asm_simp_tac |
558 (asm_simp_tac |
559 (ZF_ss addsimps [InfCard_is_Limit RS Limit_has_0, InfCard_le_cmult_eq, |
559 (!simpset addsimps [InfCard_is_Limit RS Limit_has_0, InfCard_le_cmult_eq, |
560 subset_Un_iff2 RS iffD1, le_imp_subset]))); |
560 subset_Un_iff2 RS iffD1, le_imp_subset]))); |
561 qed "InfCard_cmult_eq"; |
561 qed "InfCard_cmult_eq"; |
562 |
562 |
563 (*This proof appear to be the simplest!*) |
563 (*This proof appear to be the simplest!*) |
564 goal CardinalArith.thy "!!K. InfCard(K) ==> K |+| K = K"; |
564 goal CardinalArith.thy "!!K. InfCard(K) ==> K |+| K = K"; |
565 by (asm_simp_tac |
565 by (asm_simp_tac |
566 (ZF_ss addsimps [cmult_2 RS sym, InfCard_is_Card, cmult_commute]) 1); |
566 (!simpset addsimps [cmult_2 RS sym, InfCard_is_Card, cmult_commute]) 1); |
567 by (rtac InfCard_le_cmult_eq 1); |
567 by (rtac InfCard_le_cmult_eq 1); |
568 by (typechk_tac [Ord_0, le_refl, leI]); |
568 by (typechk_tac [Ord_0, le_refl, leI]); |
569 by (typechk_tac [InfCard_is_Limit, Limit_has_0, Limit_has_succ]); |
569 by (typechk_tac [InfCard_is_Limit, Limit_has_0, Limit_has_succ]); |
570 qed "InfCard_cdouble_eq"; |
570 qed "InfCard_cdouble_eq"; |
571 |
571 |
574 by (rtac le_anti_sym 1); |
574 by (rtac le_anti_sym 1); |
575 by (etac ltE 2 THEN |
575 by (etac ltE 2 THEN |
576 REPEAT (ares_tac [cadd_le_self, InfCard_is_Card] 2)); |
576 REPEAT (ares_tac [cadd_le_self, InfCard_is_Card] 2)); |
577 by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); |
577 by (forward_tac [InfCard_is_Card RS Card_is_Ord RS le_refl] 1); |
578 by (resolve_tac [cadd_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); |
578 by (resolve_tac [cadd_le_mono RS le_trans] 1 THEN REPEAT (assume_tac 1)); |
579 by (asm_simp_tac (ZF_ss addsimps [InfCard_cdouble_eq]) 1); |
579 by (asm_simp_tac (!simpset addsimps [InfCard_cdouble_eq]) 1); |
580 qed "InfCard_le_cadd_eq"; |
580 qed "InfCard_le_cadd_eq"; |
581 |
581 |
582 goal CardinalArith.thy |
582 goal CardinalArith.thy |
583 "!!K. [| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L"; |
583 "!!K. [| InfCard(K); InfCard(L) |] ==> K |+| L = K Un L"; |
584 by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1); |
584 by (res_inst_tac [("i","K"),("j","L")] Ord_linear_le 1); |
585 by (typechk_tac [InfCard_is_Card, Card_is_Ord]); |
585 by (typechk_tac [InfCard_is_Card, Card_is_Ord]); |
586 by (resolve_tac [cadd_commute RS ssubst] 1); |
586 by (resolve_tac [cadd_commute RS ssubst] 1); |
587 by (resolve_tac [Un_commute RS ssubst] 1); |
587 by (resolve_tac [Un_commute RS ssubst] 1); |
588 by (ALLGOALS |
588 by (ALLGOALS |
589 (asm_simp_tac |
589 (asm_simp_tac |
590 (ZF_ss addsimps [InfCard_le_cadd_eq, |
590 (!simpset addsimps [InfCard_le_cadd_eq, |
591 subset_Un_iff2 RS iffD1, le_imp_subset]))); |
591 subset_Un_iff2 RS iffD1, le_imp_subset]))); |
592 qed "InfCard_cadd_eq"; |
592 qed "InfCard_cadd_eq"; |
593 |
593 |
594 (*The other part, Corollary 10.13 (2), refers to the cardinality of the set |
594 (*The other part, Corollary 10.13 (2), refers to the cardinality of the set |
595 of all n-tuples of elements of K. A better version for the Isabelle theory |
595 of all n-tuples of elements of K. A better version for the Isabelle theory |
599 (*** For every cardinal number there exists a greater one |
599 (*** For every cardinal number there exists a greater one |
600 [Kunen's Theorem 10.16, which would be trivial using AC] ***) |
600 [Kunen's Theorem 10.16, which would be trivial using AC] ***) |
601 |
601 |
602 goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))"; |
602 goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))"; |
603 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
603 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
604 by (fast_tac (ZF_cs addSIs [Ord_ordertype]) 2); |
604 by (fast_tac (!claset addSIs [Ord_ordertype]) 2); |
605 by (rewtac Transset_def); |
605 by (rewtac Transset_def); |
606 by (safe_tac subset_cs); |
606 by (safe_tac subset_cs); |
607 by (asm_full_simp_tac (ZF_ss addsimps [ordertype_pred_unfold]) 1); |
607 by (asm_full_simp_tac (!simpset addsimps [ordertype_pred_unfold]) 1); |
608 by (safe_tac ZF_cs); |
608 by (safe_tac (!claset)); |
609 by (rtac UN_I 1); |
609 by (rtac UN_I 1); |
610 by (rtac ReplaceI 2); |
610 by (rtac ReplaceI 2); |
611 by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset, predE]))); |
611 by (ALLGOALS (fast_tac (!claset addSEs [well_ord_subset, predE]))); |
612 qed "Ord_jump_cardinal"; |
612 qed "Ord_jump_cardinal"; |
613 |
613 |
614 (*Allows selective unfolding. Less work than deriving intro/elim rules*) |
614 (*Allows selective unfolding. Less work than deriving intro/elim rules*) |
615 goalw CardinalArith.thy [jump_cardinal_def] |
615 goalw CardinalArith.thy [jump_cardinal_def] |
616 "i : jump_cardinal(K) <-> \ |
616 "i : jump_cardinal(K) <-> \ |
622 goal CardinalArith.thy "!!K. Ord(K) ==> K < jump_cardinal(K)"; |
622 goal CardinalArith.thy "!!K. Ord(K) ==> K < jump_cardinal(K)"; |
623 by (resolve_tac [Ord_jump_cardinal RSN (2,ltI)] 1); |
623 by (resolve_tac [Ord_jump_cardinal RSN (2,ltI)] 1); |
624 by (resolve_tac [jump_cardinal_iff RS iffD2] 1); |
624 by (resolve_tac [jump_cardinal_iff RS iffD2] 1); |
625 by (REPEAT_FIRST (ares_tac [exI, conjI, well_ord_Memrel])); |
625 by (REPEAT_FIRST (ares_tac [exI, conjI, well_ord_Memrel])); |
626 by (rtac subset_refl 2); |
626 by (rtac subset_refl 2); |
627 by (asm_simp_tac (ZF_ss addsimps [Memrel_def, subset_iff]) 1); |
627 by (asm_simp_tac (!simpset addsimps [Memrel_def, subset_iff]) 1); |
628 by (asm_simp_tac (ZF_ss addsimps [ordertype_Memrel]) 1); |
628 by (asm_simp_tac (!simpset addsimps [ordertype_Memrel]) 1); |
629 qed "K_lt_jump_cardinal"; |
629 qed "K_lt_jump_cardinal"; |
630 |
630 |
631 (*The proof by contradiction: the bijection f yields a wellordering of X |
631 (*The proof by contradiction: the bijection f yields a wellordering of X |
632 whose ordertype is jump_cardinal(K). *) |
632 whose ordertype is jump_cardinal(K). *) |
633 goal CardinalArith.thy |
633 goal CardinalArith.thy |
641 by (rtac ([rvimage_type, Sigma_mono] MRS subset_trans) 1); |
641 by (rtac ([rvimage_type, Sigma_mono] MRS subset_trans) 1); |
642 by (REPEAT (assume_tac 1)); |
642 by (REPEAT (assume_tac 1)); |
643 by (etac (bij_is_inj RS well_ord_rvimage) 1); |
643 by (etac (bij_is_inj RS well_ord_rvimage) 1); |
644 by (rtac (Ord_jump_cardinal RS well_ord_Memrel) 1); |
644 by (rtac (Ord_jump_cardinal RS well_ord_Memrel) 1); |
645 by (asm_simp_tac |
645 by (asm_simp_tac |
646 (ZF_ss addsimps [well_ord_Memrel RSN (2, bij_ordertype_vimage), |
646 (!simpset addsimps [well_ord_Memrel RSN (2, bij_ordertype_vimage), |
647 ordertype_Memrel, Ord_jump_cardinal]) 1); |
647 ordertype_Memrel, Ord_jump_cardinal]) 1); |
648 qed "Card_jump_cardinal_lemma"; |
648 qed "Card_jump_cardinal_lemma"; |
649 |
649 |
650 (*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) |
650 (*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) |
651 goal CardinalArith.thy "Card(jump_cardinal(K))"; |
651 goal CardinalArith.thy "Card(jump_cardinal(K))"; |
652 by (rtac (Ord_jump_cardinal RS CardI) 1); |
652 by (rtac (Ord_jump_cardinal RS CardI) 1); |
653 by (rewtac eqpoll_def); |
653 by (rewtac eqpoll_def); |
654 by (safe_tac (ZF_cs addSDs [ltD, jump_cardinal_iff RS iffD1])); |
654 by (safe_tac (!claset addSDs [ltD, jump_cardinal_iff RS iffD1])); |
655 by (REPEAT (ares_tac [Card_jump_cardinal_lemma RS mem_irrefl] 1)); |
655 by (REPEAT (ares_tac [Card_jump_cardinal_lemma RS mem_irrefl] 1)); |
656 qed "Card_jump_cardinal"; |
656 qed "Card_jump_cardinal"; |
657 |
657 |
658 (*** Basic properties of successor cardinals ***) |
658 (*** Basic properties of successor cardinals ***) |
659 |
659 |
694 qed "lt_csucc_iff"; |
694 qed "lt_csucc_iff"; |
695 |
695 |
696 goal CardinalArith.thy |
696 goal CardinalArith.thy |
697 "!!K' K. [| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"; |
697 "!!K' K. [| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"; |
698 by (asm_simp_tac |
698 by (asm_simp_tac |
699 (ZF_ss addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1); |
699 (!simpset addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1); |
700 qed "Card_lt_csucc_iff"; |
700 qed "Card_lt_csucc_iff"; |
701 |
701 |
702 goalw CardinalArith.thy [InfCard_def] |
702 goalw CardinalArith.thy [InfCard_def] |
703 "!!K. InfCard(K) ==> InfCard(csucc(K))"; |
703 "!!K. InfCard(K) ==> InfCard(csucc(K))"; |
704 by (asm_simp_tac (ZF_ss addsimps [Card_csucc, Card_is_Ord, |
704 by (asm_simp_tac (!simpset addsimps [Card_csucc, Card_is_Ord, |
705 lt_csucc RS leI RSN (2,le_trans)]) 1); |
705 lt_csucc RS leI RSN (2,le_trans)]) 1); |
706 qed "InfCard_csucc"; |
706 qed "InfCard_csucc"; |
707 |
707 |
708 |
708 |
709 (*** Finite sets ***) |
709 (*** Finite sets ***) |
710 |
710 |
711 goal CardinalArith.thy |
711 goal CardinalArith.thy |
712 "!!n. n: nat ==> ALL A. A eqpoll n --> A : Fin(A)"; |
712 "!!n. n: nat ==> ALL A. A eqpoll n --> A : Fin(A)"; |
713 by (etac nat_induct 1); |
713 by (etac nat_induct 1); |
714 by (simp_tac (ZF_ss addsimps (eqpoll_0_iff::Fin.intrs)) 1); |
714 by (simp_tac (!simpset addsimps (eqpoll_0_iff::Fin.intrs)) 1); |
715 by (step_tac ZF_cs 1); |
715 by (step_tac (!claset) 1); |
716 by (subgoal_tac "EX u. u:A" 1); |
716 by (subgoal_tac "EX u. u:A" 1); |
717 by (etac exE 1); |
717 by (etac exE 1); |
718 by (resolve_tac [Diff_sing_eqpoll RS revcut_rl] 1); |
718 by (resolve_tac [Diff_sing_eqpoll RS revcut_rl] 1); |
719 by (assume_tac 2); |
719 by (assume_tac 2); |
720 by (assume_tac 1); |
720 by (assume_tac 1); |
721 by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); |
721 by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); |
722 by (assume_tac 1); |
722 by (assume_tac 1); |
723 by (resolve_tac [Fin.consI] 1); |
723 by (resolve_tac [Fin.consI] 1); |
724 by (fast_tac ZF_cs 1); |
724 by (Fast_tac 1); |
725 by (deepen_tac (ZF_cs addIs [Fin_mono RS subsetD]) 0 1); (*SLOW*) |
725 by (fast_tac (!claset addIs [subset_consI RS Fin_mono RS subsetD]) 1); |
726 (*Now for the lemma assumed above*) |
726 (*Now for the lemma assumed above*) |
727 by (rewtac eqpoll_def); |
727 by (rewtac eqpoll_def); |
728 by (fast_tac (ZF_cs addSEs [bij_converse_bij RS bij_is_fun RS apply_type]) 1); |
728 by (best_tac (!claset addSEs [bij_converse_bij RS bij_is_fun RS apply_type]) 1); |
729 val lemma = result(); |
729 val lemma = result(); |
730 |
730 |
731 goalw CardinalArith.thy [Finite_def] "!!A. Finite(A) ==> A : Fin(A)"; |
731 goalw CardinalArith.thy [Finite_def] "!!A. Finite(A) ==> A : Fin(A)"; |
732 by (fast_tac (ZF_cs addIs [lemma RS spec RS mp]) 1); |
732 by (fast_tac (!claset addIs [lemma RS spec RS mp]) 1); |
733 qed "Finite_into_Fin"; |
733 qed "Finite_into_Fin"; |
734 |
734 |
735 goal CardinalArith.thy "!!A. A : Fin(U) ==> Finite(A)"; |
735 goal CardinalArith.thy "!!A. A : Fin(U) ==> Finite(A)"; |
736 by (fast_tac (ZF_cs addSIs [Finite_0, Finite_cons] addEs [Fin.induct]) 1); |
736 by (fast_tac (!claset addSIs [Finite_0, Finite_cons] addEs [Fin.induct]) 1); |
737 qed "Fin_into_Finite"; |
737 qed "Fin_into_Finite"; |
738 |
738 |
739 goal CardinalArith.thy "Finite(A) <-> A : Fin(A)"; |
739 goal CardinalArith.thy "Finite(A) <-> A : Fin(A)"; |
740 by (fast_tac (ZF_cs addIs [Finite_into_Fin] addEs [Fin_into_Finite]) 1); |
740 by (fast_tac (!claset addIs [Finite_into_Fin] addEs [Fin_into_Finite]) 1); |
741 qed "Finite_Fin_iff"; |
741 qed "Finite_Fin_iff"; |
742 |
742 |
743 goal CardinalArith.thy |
743 goal CardinalArith.thy |
744 "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; |
744 "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; |
745 by (fast_tac (ZF_cs addSIs [Fin_into_Finite, Fin_UnI] |
745 by (fast_tac (!claset addSIs [Fin_into_Finite, Fin_UnI] |
746 addSDs [Finite_into_Fin] |
746 addSDs [Finite_into_Fin] |
747 addSEs [Un_upper1 RS Fin_mono RS subsetD, |
747 addSEs [Un_upper1 RS Fin_mono RS subsetD, |
748 Un_upper2 RS Fin_mono RS subsetD]) 1); |
748 Un_upper2 RS Fin_mono RS subsetD]) 1); |
749 qed "Finite_Un"; |
749 qed "Finite_Un"; |
750 |
750 |
752 (** Removing elements from a finite set decreases its cardinality **) |
752 (** Removing elements from a finite set decreases its cardinality **) |
753 |
753 |
754 goal CardinalArith.thy |
754 goal CardinalArith.thy |
755 "!!A. A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A"; |
755 "!!A. A: Fin(U) ==> x~:A --> ~ cons(x,A) lepoll A"; |
756 by (etac Fin_induct 1); |
756 by (etac Fin_induct 1); |
757 by (simp_tac (ZF_ss addsimps [lepoll_0_iff]) 1); |
757 by (simp_tac (!simpset addsimps [lepoll_0_iff]) 1); |
758 by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1); |
758 by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1); |
759 by (asm_simp_tac ZF_ss 1); |
759 by (Asm_simp_tac 1); |
760 by (fast_tac (ZF_cs addSDs [cons_lepoll_consD]) 1); |
760 by (fast_tac (!claset addSDs [cons_lepoll_consD]) 1); |
761 by (fast_tac eq_cs 1); |
761 by (fast_tac eq_cs 1); |
762 qed "Fin_imp_not_cons_lepoll"; |
762 qed "Fin_imp_not_cons_lepoll"; |
763 |
763 |
764 goal CardinalArith.thy |
764 goal CardinalArith.thy |
765 "!!a A. [| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"; |
765 "!!a A. [| Finite(A); a~:A |] ==> |cons(a,A)| = succ(|A|)"; |
766 by (rewtac cardinal_def); |
766 by (rewtac cardinal_def); |
767 by (rtac Least_equality 1); |
767 by (rtac Least_equality 1); |
768 by (fold_tac [cardinal_def]); |
768 by (fold_tac [cardinal_def]); |
769 by (simp_tac (ZF_ss addsimps [succ_def]) 1); |
769 by (simp_tac (!simpset addsimps [succ_def]) 1); |
770 by (fast_tac (ZF_cs addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] |
770 by (fast_tac (!claset addIs [cons_eqpoll_cong, well_ord_cardinal_eqpoll] |
771 addSEs [mem_irrefl] |
771 addSEs [mem_irrefl] |
772 addSDs [Finite_imp_well_ord]) 1); |
772 addSDs [Finite_imp_well_ord]) 1); |
773 by (fast_tac (ZF_cs addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1); |
773 by (fast_tac (!claset addIs [Ord_succ, Card_cardinal, Card_is_Ord]) 1); |
774 by (rtac notI 1); |
774 by (rtac notI 1); |
775 by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1); |
775 by (resolve_tac [Finite_into_Fin RS Fin_imp_not_cons_lepoll RS mp RS notE] 1); |
776 by (assume_tac 1); |
776 by (assume_tac 1); |
777 by (assume_tac 1); |
777 by (assume_tac 1); |
778 by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] 1); |
778 by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] 1); |
779 by (eresolve_tac [le_imp_lepoll RS lepoll_trans] 1); |
779 by (eresolve_tac [le_imp_lepoll RS lepoll_trans] 1); |
780 by (fast_tac (ZF_cs addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll] |
780 by (fast_tac (!claset addIs [well_ord_cardinal_eqpoll RS eqpoll_imp_lepoll] |
781 addSDs [Finite_imp_well_ord]) 1); |
781 addSDs [Finite_imp_well_ord]) 1); |
782 qed "Finite_imp_cardinal_cons"; |
782 qed "Finite_imp_cardinal_cons"; |
783 |
783 |
784 |
784 |
785 goal CardinalArith.thy "!!a A. [| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|"; |
785 goal CardinalArith.thy "!!a A. [| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|"; |
786 by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); |
786 by (res_inst_tac [("b", "A")] (cons_Diff RS subst) 1); |
787 by (assume_tac 1); |
787 by (assume_tac 1); |
788 by (asm_simp_tac (ZF_ss addsimps [Finite_imp_cardinal_cons, |
788 by (asm_simp_tac (!simpset addsimps [Finite_imp_cardinal_cons, |
789 Diff_subset RS subset_Finite]) 1); |
789 Diff_subset RS subset_Finite]) 1); |
790 by (asm_simp_tac (ZF_ss addsimps [cons_Diff]) 1); |
790 by (asm_simp_tac (!simpset addsimps [cons_Diff]) 1); |
791 qed "Finite_imp_succ_cardinal_Diff"; |
791 qed "Finite_imp_succ_cardinal_Diff"; |
792 |
792 |
793 goal CardinalArith.thy "!!a A. [| Finite(A); a:A |] ==> |A-{a}| < |A|"; |
793 goal CardinalArith.thy "!!a A. [| Finite(A); a:A |] ==> |A-{a}| < |A|"; |
794 by (rtac succ_leE 1); |
794 by (rtac succ_leE 1); |
795 by (asm_simp_tac (ZF_ss addsimps [Finite_imp_succ_cardinal_Diff, |
795 by (asm_simp_tac (!simpset addsimps [Finite_imp_succ_cardinal_Diff, |
796 Ord_cardinal RS le_refl]) 1); |
796 Ord_cardinal RS le_refl]) 1); |
797 qed "Finite_imp_cardinal_Diff"; |
797 qed "Finite_imp_cardinal_Diff"; |
798 |
798 |
799 |
799 |
800 (** Thanks to Krzysztof Grabczewski **) |
800 (** Thanks to Krzysztof Grabczewski **) |