437

1 
(* Title: ZF/CardinalArith.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Cardinal arithmetic  WITHOUT the Axiom of Choice


7 
*)


8 


9 
open CardinalArith;


10 


11 
(*Use AC to discharge first premise*)


12 
goal CardinalArith.thy


13 
"!!A B. [ well_ord(B,r); A lepoll B ] ==> A le B";


14 
by (res_inst_tac [("i","A"),("j","B")] Ord_linear_le 1);


15 
by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI]));


16 
by (rtac (eqpollI RS cardinal_cong) 1 THEN assume_tac 1);


17 
by (rtac lepoll_trans 1);


18 
by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll) 1);


19 
by (assume_tac 1);


20 
by (etac (le_imp_subset RS subset_imp_lepoll RS lepoll_trans) 1);


21 
by (rtac eqpoll_imp_lepoll 1);


22 
by (rewtac lepoll_def);


23 
by (etac exE 1);


24 
by (rtac well_ord_cardinal_eqpoll 1);


25 
by (etac well_ord_rvimage 1);


26 
by (assume_tac 1);


27 
val well_ord_lepoll_imp_le = result();


28 


29 
val case_ss = ZF_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff,


30 
case_Inl, case_Inr, InlI, InrI];


31 


32 


33 
(** Congruence laws for successor, cardinal addition and multiplication **)


34 


35 
val bij_inverse_ss =


36 
case_ss addsimps [bij_is_fun RS apply_type,


37 
bij_converse_bij RS bij_is_fun RS apply_type,


38 
left_inverse_bij, right_inverse_bij];


39 


40 


41 
(*Congruence law for succ under equipollence*)


42 
goalw CardinalArith.thy [eqpoll_def]


43 
"!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)";


44 
by (safe_tac ZF_cs);


45 
by (rtac exI 1);


46 
by (res_inst_tac [("c", "%z.if(z=A,B,f`z)"),


47 
("d", "%z.if(z=B,A,converse(f)`z)")] lam_bijective 1);


48 
by (ALLGOALS


49 
(asm_simp_tac (bij_inverse_ss addsimps [succI2, mem_imp_not_eq]


50 
setloop etac succE )));


51 
val succ_eqpoll_cong = result();


52 


53 
(*Congruence law for + under equipollence*)


54 
goalw CardinalArith.thy [eqpoll_def]


55 
"!!A B C D. [ A eqpoll C; B eqpoll D ] ==> A+B eqpoll C+D";


56 
by (safe_tac ZF_cs);


57 
by (rtac exI 1);


58 
by (res_inst_tac [("c", "case(%x. Inl(f`x), %y. Inr(fa`y))"),


59 
("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(fa)`y))")]


60 
lam_bijective 1);


61 
by (safe_tac (ZF_cs addSEs [sumE]));


62 
by (ALLGOALS (asm_simp_tac bij_inverse_ss));


63 
val sum_eqpoll_cong = result();


64 


65 
(*Congruence law for * under equipollence*)


66 
goalw CardinalArith.thy [eqpoll_def]


67 
"!!A B C D. [ A eqpoll C; B eqpoll D ] ==> A*B eqpoll C*D";


68 
by (safe_tac ZF_cs);


69 
by (rtac exI 1);


70 
by (res_inst_tac [("c", "split(%x y. <f`x, fa`y>)"),


71 
("d", "split(%x y. <converse(f)`x, converse(fa)`y>)")]


72 
lam_bijective 1);


73 
by (safe_tac ZF_cs);


74 
by (ALLGOALS (asm_simp_tac bij_inverse_ss));


75 
val prod_eqpoll_cong = result();


76 


77 


78 
(*** Cardinal addition ***)


79 


80 
(** Cardinal addition is commutative **)


81 


82 
(*Easier to prove the two directions separately*)


83 
goalw CardinalArith.thy [eqpoll_def] "A+B eqpoll B+A";


84 
by (rtac exI 1);


85 
by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")]


86 
lam_bijective 1);


87 
by (safe_tac (ZF_cs addSEs [sumE]));


88 
by (ALLGOALS (asm_simp_tac case_ss));


89 
val sum_commute_eqpoll = result();


90 


91 
goalw CardinalArith.thy [cadd_def] "i + j = j + i";


92 
by (rtac (sum_commute_eqpoll RS cardinal_cong) 1);


93 
val cadd_commute = result();


94 


95 
(** Cardinal addition is associative **)


96 


97 
goalw CardinalArith.thy [eqpoll_def] "(A+B)+C eqpoll A+(B+C)";


98 
by (rtac exI 1);


99 
by (res_inst_tac [("c", "case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)))"),


100 
("d", "case(%x.Inl(Inl(x)), case(%x.Inl(Inr(x)), Inr))")]


101 
lam_bijective 1);


102 
by (ALLGOALS (asm_simp_tac (case_ss setloop etac sumE)));


103 
val sum_assoc_eqpoll = result();


104 


105 
(*Unconditional version requires AC*)


106 
goalw CardinalArith.thy [cadd_def]


107 
"!!i j k. [ Ord(i); Ord(j); Ord(k) ] ==> \


108 
\ (i + j) + k = i + (j + k)";


109 
by (rtac cardinal_cong 1);


110 
br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS


111 
eqpoll_trans) 1;


112 
by (rtac (sum_assoc_eqpoll RS eqpoll_trans) 2);


113 
br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS


114 
eqpoll_sym) 2;


115 
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));


116 
val Ord_cadd_assoc = result();


117 


118 
(** 0 is the identity for addition **)


119 


120 
goalw CardinalArith.thy [eqpoll_def] "0+A eqpoll A";


121 
by (rtac exI 1);


122 
by (res_inst_tac [("c", "case(%x.x, %y.y)"), ("d", "Inr")]


123 
lam_bijective 1);


124 
by (ALLGOALS (asm_simp_tac (case_ss setloop eresolve_tac [sumE,emptyE])));


125 
val sum_0_eqpoll = result();


126 


127 
goalw CardinalArith.thy [cadd_def] "!!i. Card(i) ==> 0 + i = i";


128 
by (asm_simp_tac (ZF_ss addsimps [sum_0_eqpoll RS cardinal_cong,


129 
Card_cardinal_eq]) 1);


130 
val cadd_0 = result();


131 


132 
(** Addition of finite cardinals is "ordinary" addition **)


133 


134 
goalw CardinalArith.thy [eqpoll_def] "succ(A)+B eqpoll succ(A+B)";


135 
by (rtac exI 1);


136 
by (res_inst_tac [("c", "%z.if(z=Inl(A),A+B,z)"),


137 
("d", "%z.if(z=A+B,Inl(A),z)")]


138 
lam_bijective 1);


139 
by (ALLGOALS


140 
(asm_simp_tac (case_ss addsimps [succI2, mem_imp_not_eq]


141 
setloop eresolve_tac [sumE,succE])));


142 
val sum_succ_eqpoll = result();


143 


144 
(*Pulling the succ(...) outside the ... requires m, n: nat *)


145 
(*Unconditional version requires AC*)


146 
goalw CardinalArith.thy [cadd_def]


147 
"!!m n. [ Ord(m); Ord(n) ] ==> succ(m) + n = succ(m + n)";


148 
by (rtac (sum_succ_eqpoll RS cardinal_cong RS trans) 1);


149 
by (rtac (succ_eqpoll_cong RS cardinal_cong) 1);


150 
by (rtac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1);


151 
by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1));


152 
val cadd_succ_lemma = result();


153 


154 
val [mnat,nnat] = goal CardinalArith.thy


155 
"[ m: nat; n: nat ] ==> m + n = m#+n";


156 
by (cut_facts_tac [nnat] 1);


157 
by (nat_ind_tac "m" [mnat] 1);


158 
by (asm_simp_tac (arith_ss addsimps [nat_into_Card RS cadd_0]) 1);


159 
by (asm_simp_tac (arith_ss addsimps [nat_into_Ord, cadd_succ_lemma,


160 
nat_into_Card RS Card_cardinal_eq]) 1);


161 
val nat_cadd_eq_add = result();


162 


163 


164 
(*** Cardinal multiplication ***)


165 


166 
(** Cardinal multiplication is commutative **)


167 


168 
(*Easier to prove the two directions separately*)


169 
goalw CardinalArith.thy [eqpoll_def] "A*B eqpoll B*A";


170 
by (rtac exI 1);


171 
by (res_inst_tac [("c", "split(%x y.<y,x>)"), ("d", "split(%x y.<y,x>)")]


172 
lam_bijective 1);


173 
by (safe_tac ZF_cs);


174 
by (ALLGOALS (asm_simp_tac ZF_ss));


175 
val prod_commute_eqpoll = result();


176 


177 
goalw CardinalArith.thy [cmult_def] "i * j = j * i";


178 
by (rtac (prod_commute_eqpoll RS cardinal_cong) 1);


179 
val cmult_commute = result();


180 


181 
(** Cardinal multiplication is associative **)


182 


183 
goalw CardinalArith.thy [eqpoll_def] "(A*B)*C eqpoll A*(B*C)";


184 
by (rtac exI 1);


185 
by (res_inst_tac [("c", "split(%w z. split(%x y. <x,<y,z>>, w))"),


186 
("d", "split(%x. split(%y z. <<x,y>, z>))")]


187 
lam_bijective 1);


188 
by (safe_tac ZF_cs);


189 
by (ALLGOALS (asm_simp_tac ZF_ss));


190 
val prod_assoc_eqpoll = result();


191 


192 
(*Unconditional version requires AC*)


193 
goalw CardinalArith.thy [cmult_def]


194 
"!!i j k. [ Ord(i); Ord(j); Ord(k) ] ==> \


195 
\ (i * j) * k = i * (j * k)";


196 
by (rtac cardinal_cong 1);


197 
br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS


198 
eqpoll_trans) 1;


199 
by (rtac (prod_assoc_eqpoll RS eqpoll_trans) 2);


200 
br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS prod_eqpoll_cong RS


201 
eqpoll_sym) 2;


202 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));


203 
val Ord_cmult_assoc = result();


204 


205 
(** Cardinal multiplication distributes over addition **)


206 


207 
goalw CardinalArith.thy [eqpoll_def] "(A+B)*C eqpoll (A*C)+(B*C)";


208 
by (rtac exI 1);


209 
by (res_inst_tac


210 
[("c", "split(%x z. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x))"),


211 
("d", "case(split(%x y.<Inl(x),y>), split(%x y.<Inr(x),y>))")]


212 
lam_bijective 1);


213 
by (safe_tac (ZF_cs addSEs [sumE]));


214 
by (ALLGOALS (asm_simp_tac case_ss));


215 
val sum_prod_distrib_eqpoll = result();


216 


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);


219 
by (simp_tac (ZF_ss addsimps [lam_type]) 1);


220 
val prod_square_lepoll = result();


221 


222 
goalw CardinalArith.thy [cmult_def] "!!k. Card(k) ==> k le k * k";


223 
by (rtac le_trans 1);


224 
by (rtac well_ord_lepoll_imp_le 2);


225 
by (rtac prod_square_lepoll 3);


226 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Card_is_Ord] 2));


227 
by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1);


228 
val cmult_square_le = result();


229 


230 
(** Multiplication by 0 yields 0 **)


231 


232 
goalw CardinalArith.thy [eqpoll_def] "0*A eqpoll 0";


233 
by (rtac exI 1);


234 
by (rtac lam_bijective 1);


235 
by (safe_tac ZF_cs);


236 
val prod_0_eqpoll = result();


237 


238 
goalw CardinalArith.thy [cmult_def] "0 * i = 0";


239 
by (asm_simp_tac (ZF_ss addsimps [prod_0_eqpoll RS cardinal_cong,


240 
Card_0 RS Card_cardinal_eq]) 1);


241 
val cmult_0 = result();


242 


243 
(** 1 is the identity for multiplication **)


244 


245 
goalw CardinalArith.thy [eqpoll_def] "{x}*A eqpoll A";


246 
by (rtac exI 1);


247 
by (res_inst_tac [("c", "snd"), ("d", "%z.<x,z>")] lam_bijective 1);


248 
by (safe_tac ZF_cs);


249 
by (ALLGOALS (asm_simp_tac ZF_ss));


250 
val prod_singleton_eqpoll = result();


251 


252 
goalw CardinalArith.thy [cmult_def, succ_def] "!!i. Card(i) ==> 1 * i = i";


253 
by (asm_simp_tac (ZF_ss addsimps [prod_singleton_eqpoll RS cardinal_cong,


254 
Card_cardinal_eq]) 1);


255 
val cmult_1 = result();


256 


257 
(** Multiplication of finite cardinals is "ordinary" multiplication **)


258 


259 
goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B";


260 
by (rtac exI 1);


261 
by (res_inst_tac [("c", "split(%x y. if(x=A, Inl(y), Inr(<x,y>)))"),


262 
("d", "case(%y. <A,y>, %z.z)")]


263 
lam_bijective 1);


264 
by (safe_tac (ZF_cs addSEs [sumE]));


265 
by (ALLGOALS


266 
(asm_simp_tac (case_ss addsimps [succI2, if_type, mem_imp_not_eq])));


267 
val prod_succ_eqpoll = result();


268 


269 


270 
(*Unconditional version requires AC*)


271 
goalw CardinalArith.thy [cmult_def, cadd_def]


272 
"!!m n. [ Ord(m); Ord(n) ] ==> succ(m) * n = n + (m * n)";


273 
by (rtac (prod_succ_eqpoll RS cardinal_cong RS trans) 1);


274 
by (rtac (cardinal_cong RS sym) 1);


275 
by (rtac ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong) 1);


276 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));


277 
val cmult_succ_lemma = result();


278 


279 
val [mnat,nnat] = goal CardinalArith.thy


280 
"[ m: nat; n: nat ] ==> m * n = m#*n";


281 
by (cut_facts_tac [nnat] 1);


282 
by (nat_ind_tac "m" [mnat] 1);


283 
by (asm_simp_tac (arith_ss addsimps [cmult_0]) 1);


284 
by (asm_simp_tac (arith_ss addsimps [nat_into_Ord, cmult_succ_lemma,


285 
nat_cadd_eq_add]) 1);


286 
val nat_cmult_eq_mult = result();


287 


288 


289 
(*** Infinite Cardinals are Limit Ordinals ***)


290 


291 
goalw CardinalArith.thy [lepoll_def, inj_def]


292 
"!!i. nat <= A ==> succ(A) lepoll A";


293 
by (res_inst_tac [("x",


294 
"lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);


295 
by (rtac (lam_type RS CollectI) 1);


296 
by (rtac if_type 1);


297 
by (etac ([asm_rl, nat_0I] MRS subsetD) 1);


298 
by (etac succE 1);


299 
by (contr_tac 1);


300 
by (rtac if_type 1);


301 
by (assume_tac 2);


302 
by (etac ([asm_rl, nat_succI] MRS subsetD) 1 THEN assume_tac 1);


303 
by (REPEAT (rtac ballI 1));


304 
by (asm_simp_tac


305 
(ZF_ss addsimps [succ_inject_iff, succ_not_0, succ_not_0 RS not_sym]


306 
setloop split_tac [expand_if]) 1);


307 
by (safe_tac (ZF_cs addSIs [nat_0I, nat_succI]));


308 
val nat_succ_lepoll = result();


309 


310 
goal CardinalArith.thy "!!i. nat <= A ==> succ(A) eqpoll A";


311 
by (etac (nat_succ_lepoll RS eqpollI) 1);


312 
by (rtac (subset_succI RS subset_imp_lepoll) 1);


313 
val nat_succ_eqpoll = result();


314 


315 
goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Card(i)";


316 
by (etac conjunct1 1);


317 
val InfCard_is_Card = result();


318 


319 
(*Kunen's Lemma 10.11*)


320 
goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Limit(i)";


321 
by (etac conjE 1);


322 
by (rtac (ltI RS non_succ_LimitI) 1);


323 
by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1);


324 
by (etac Card_is_Ord 1);


325 
by (safe_tac (ZF_cs addSDs [Limit_nat RS Limit_le_succD]));


326 
by (forward_tac [Card_is_Ord RS Ord_succD] 1);


327 
by (rewtac Card_def);


328 
by (res_inst_tac [("i", "succ(y)")] lt_irrefl 1);


329 
by (dtac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1);


330 
(*Tricky combination of substitutions; backtracking needed*)


331 
by (etac ssubst 1 THEN etac ssubst 1 THEN rtac Ord_cardinal_le 1);


332 
by (assume_tac 1);


333 
val InfCard_is_Limit = result();


334 


335 


336 


337 
(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)


338 


339 
(*A general fact about ordermap*)


340 
goalw Cardinal.thy [eqpoll_def]


341 
"!!A. [ well_ord(A,r); x:A ] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";


342 
by (rtac exI 1);


343 
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, well_ord_is_wf]) 1);


344 
by (etac (ordertype_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);


345 
by (rtac pred_subset 1);


346 
val ordermap_eqpoll_pred = result();


347 


348 
(** Establishing the wellordering **)


349 


350 
goalw CardinalArith.thy [inj_def]


351 
"!!k. Ord(k) ==> \


352 
\ (lam z:k*k. split(%x y. <x Un y, <x, y>>, z)) : inj(k*k, k*k*k)";


353 
by (safe_tac ZF_cs);


354 
by (fast_tac (ZF_cs addIs [lam_type, Un_least_lt RS ltD, ltI]


355 
addSEs [split_type]) 1);


356 
by (asm_full_simp_tac ZF_ss 1);


357 
val csquare_lam_inj = result();


358 


359 
goalw CardinalArith.thy [csquare_rel_def]


360 
"!!k. Ord(k) ==> well_ord(k*k, csquare_rel(k))";


361 
by (rtac (csquare_lam_inj RS well_ord_rvimage) 1);


362 
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));


363 
val well_ord_csquare = result();


364 


365 
(** Characterising initial segments of the wellordering **)


366 


367 
goalw CardinalArith.thy [csquare_rel_def]


368 
"!!k. [ x<k; y<k; z<k ] ==> \


369 
\ <<x,y>, <z,z>> : csquare_rel(k) > x le z & y le z";


370 
by (REPEAT (etac ltE 1));


371 
by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,


372 
Un_absorb, Un_least_mem_iff, ltD]) 1);


373 
by (safe_tac (ZF_cs addSEs [mem_irrefl]


374 
addSIs [Un_upper1_le, Un_upper2_le]));


375 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [lt_def, succI2, Ord_succ])));


376 
val csquareD_lemma = result();


377 
val csquareD = csquareD_lemma RS mp > standard;


378 


379 
goalw CardinalArith.thy [pred_def]


380 
"!!k. z<k ==> pred(k*k, <z,z>, csquare_rel(k)) <= succ(z)*succ(z)";


381 
by (safe_tac (lemmas_cs addSEs [SigmaE])); (*avoids using succCI*)


382 
by (rtac (csquareD RS conjE) 1);


383 
by (rewtac lt_def);


384 
by (assume_tac 4);


385 
by (ALLGOALS (fast_tac ZF_cs));


386 
val pred_csquare_subset = result();


387 


388 
goalw CardinalArith.thy [csquare_rel_def]


389 
"!!k. [ x<z; y<z; z<k ] ==> \


390 
\ <<x,y>, <z,z>> : csquare_rel(k)";


391 
by (subgoals_tac ["x<k", "y<k"] 1);


392 
by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));


393 
by (REPEAT (etac ltE 1));


394 
by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,


395 
Un_absorb, Un_least_mem_iff, ltD]) 1);


396 
val csquare_ltI = result();


397 


398 
(*Part of the traditional proof. UNUSED since it's harder to prove & apply *)


399 
goalw CardinalArith.thy [csquare_rel_def]


400 
"!!k. [ x le z; y le z; z<k ] ==> \


401 
\ <<x,y>, <z,z>> : csquare_rel(k)  x=z & y=z";


402 
by (subgoals_tac ["x<k", "y<k"] 1);


403 
by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2));


404 
by (REPEAT (etac ltE 1));


405 
by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff,


406 
Un_absorb, Un_least_mem_iff, ltD]) 1);


407 
by (REPEAT_FIRST (etac succE));


408 
by (ALLGOALS


409 
(asm_simp_tac (ZF_ss addsimps [subset_Un_iff RS iff_sym,


410 
subset_Un_iff2 RS iff_sym, OrdmemD])));


411 
val csquare_or_eqI = result();


412 


413 
(** The cardinality of initial segments **)


414 


415 
goal CardinalArith.thy


416 
"!!k. [ InfCard(k); x<k; y<k; z=succ(x Un y) ] ==> \


417 
\ ordermap(k*k, csquare_rel(k)) ` <x,y> lepoll \


418 
\ ordermap(k*k, csquare_rel(k)) ` <z,z>";


419 
by (subgoals_tac ["z<k", "well_ord(k*k, csquare_rel(k))"] 1);


420 
by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 2);


421 
by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, Limit_has_succ]) 2);


422 
by (rtac (OrdmemD RS subset_imp_lepoll) 1);


423 
by (res_inst_tac [("z1","z")] (csquare_ltI RS less_imp_ordermap_in) 1);


424 
by (etac well_ord_is_wf 4);


425 
by (ALLGOALS


426 
(fast_tac (ZF_cs addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap]


427 
addSEs [ltE])));


428 
val ordermap_z_lepoll = result();


429 


430 
(*Kunen: "each <x,y>: k*k has no more than z*z predecessors..." (page 29) *)


431 
goalw CardinalArith.thy [cmult_def]


432 
"!!k. [ InfCard(k); x<k; y<k; z=succ(x Un y) ] ==> \


433 
\  ordermap(k*k, csquare_rel(k)) ` <x,y>  le succ(z) * succ(z)";


434 
by (rtac (well_ord_rmult RS well_ord_lepoll_imp_le) 1);


435 
by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1));


436 
by (subgoals_tac ["z<k"] 1);


437 
by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit,


438 
Limit_has_succ]) 2);


439 
by (rtac (ordermap_z_lepoll RS lepoll_trans) 1);


440 
by (REPEAT_SOME assume_tac);


441 
by (rtac (ordermap_eqpoll_pred RS eqpoll_imp_lepoll RS lepoll_trans) 1);


442 
by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 1);


443 
by (fast_tac (ZF_cs addIs [ltD]) 1);


444 
by (rtac (pred_csquare_subset RS subset_imp_lepoll RS lepoll_trans) 1 THEN


445 
assume_tac 1);


446 
by (REPEAT_FIRST (etac ltE));


447 
by (rtac (prod_eqpoll_cong RS eqpoll_sym RS eqpoll_imp_lepoll) 1);


448 
by (REPEAT_FIRST (etac (Ord_succ RS Ord_cardinal_eqpoll)));


449 
val ordermap_csquare_le = result();


450 


451 
(*Kunen: "... so the order type <= k" *)


452 
goal CardinalArith.thy


453 
"!!k. [ InfCard(k); ALL y:k. InfCard(y) > y * y = y ] ==> \


454 
\ ordertype(k*k, csquare_rel(k)) le k";


455 
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);


456 
by (rtac all_lt_imp_le 1);


457 
by (assume_tac 1);


458 
by (etac (well_ord_csquare RS Ord_ordertype) 1);


459 
by (rtac Card_lt_imp_lt 1);


460 
by (etac InfCard_is_Card 3);


461 
by (etac ltE 2 THEN assume_tac 2);


462 
by (asm_full_simp_tac (ZF_ss addsimps [ordertype_unfold]) 1);


463 
by (safe_tac (ZF_cs addSEs [ltE]));


464 
by (subgoals_tac ["Ord(xb)", "Ord(y)"] 1);


465 
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 2));


466 
by (rtac (ordermap_csquare_le RS lt_trans1) 1 THEN


467 
REPEAT (ares_tac [refl] 1 ORELSE etac ltI 1));


468 
by (res_inst_tac [("i","xb Un y"), ("j","nat")] Ord_linear2 1 THEN


469 
REPEAT (ares_tac [Ord_Un, Ord_nat] 1));


470 
(*the finite case: xb Un y < nat *)


471 
by (res_inst_tac [("j", "nat")] lt_trans2 1);


472 
by (asm_full_simp_tac (FOL_ss addsimps [InfCard_def]) 2);


473 
by (asm_full_simp_tac


474 
(ZF_ss addsimps [lt_def, nat_cmult_eq_mult, nat_succI, mult_type,


475 
nat_into_Card RS Card_cardinal_eq, Ord_nat]) 1);


476 
(*case nat le (xb Un y), equivalently InfCard(xb Un y) *)


477 
by (asm_full_simp_tac


478 
(ZF_ss addsimps [le_imp_subset RS nat_succ_eqpoll RS cardinal_cong,


479 
le_succ_iff, InfCard_def, Card_cardinal, Un_least_lt,


480 
Ord_Un, ltI, nat_le_cardinal,


481 
Ord_cardinal_le RS lt_trans1 RS ltD]) 1);


482 
val ordertype_csquare_le = result();


483 


484 
(*This lemma can easily be generalized to premise well_ord(A*A,r) *)


485 
goalw CardinalArith.thy [cmult_def]


486 
"!!k. Ord(k) ==> k * k = ordertype(k*k, csquare_rel(k))";


487 
by (rtac cardinal_cong 1);


488 
by (rewtac eqpoll_def);


489 
by (rtac exI 1);


490 
by (etac (well_ord_csquare RS ordertype_bij) 1);


491 
val csquare_eq_ordertype = result();


492 


493 
(*Main result: Kunen's Theorem 10.12*)


494 
goal CardinalArith.thy


495 
"!!k. InfCard(k) ==> k * k = k";


496 
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);


497 
by (etac rev_mp 1);


498 
by (trans_ind_tac "k" [] 1);


499 
by (rtac impI 1);


500 
by (rtac le_anti_sym 1);


501 
by (etac (InfCard_is_Card RS cmult_square_le) 2);


502 
by (rtac (ordertype_csquare_le RSN (2, le_trans)) 1);


503 
by (assume_tac 2);


504 
by (assume_tac 2);


505 
by (asm_simp_tac


506 
(ZF_ss addsimps [csquare_eq_ordertype, Ord_cardinal_le,


507 
well_ord_csquare RS Ord_ordertype]) 1);


508 
val InfCard_csquare_eq = result();
