src/ZF/CardinalArith.thy
 author paulson Tue Mar 06 16:06:52 2012 +0000 (2012-03-06) changeset 46821 ff6b0c1087f2 parent 46820 c656222c4dc1 child 46841 49b91b716cbe permissions -rw-r--r--
Using mathematical notation for <-> and cardinal arithmetic
 clasohm@1478 ` 1` ```(* Title: ZF/CardinalArith.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@437 ` 3` ``` Copyright 1994 University of Cambridge ``` paulson@13328 ` 4` ```*) ``` paulson@13216 ` 5` paulson@13328 ` 6` ```header{*Cardinal Arithmetic Without the Axiom of Choice*} ``` lcp@437 ` 7` haftmann@16417 ` 8` ```theory CardinalArith imports Cardinal OrderArith ArithSimp Finite begin ``` lcp@467 ` 9` wenzelm@24893 ` 10` ```definition ``` wenzelm@24893 ` 11` ``` InfCard :: "i=>o" where ``` paulson@46820 ` 12` ``` "InfCard(i) == Card(i) & nat \ i" ``` lcp@437 ` 13` wenzelm@24893 ` 14` ```definition ``` wenzelm@24893 ` 15` ``` cmult :: "[i,i]=>i" (infixl "|*|" 70) where ``` paulson@12667 ` 16` ``` "i |*| j == |i*j|" ``` paulson@46820 ` 17` wenzelm@24893 ` 18` ```definition ``` wenzelm@24893 ` 19` ``` cadd :: "[i,i]=>i" (infixl "|+|" 65) where ``` paulson@12667 ` 20` ``` "i |+| j == |i+j|" ``` lcp@437 ` 21` wenzelm@24893 ` 22` ```definition ``` wenzelm@24893 ` 23` ``` csquare_rel :: "i=>i" where ``` paulson@46820 ` 24` ``` "csquare_rel(K) == ``` paulson@46820 ` 25` ``` rvimage(K*K, ``` paulson@46820 ` 26` ``` lam :K*K. y, x, y>, ``` wenzelm@32960 ` 27` ``` rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" ``` lcp@437 ` 28` wenzelm@24893 ` 29` ```definition ``` wenzelm@24893 ` 30` ``` jump_cardinal :: "i=>i" where ``` paulson@14883 ` 31` ``` --{*This def is more complex than Kunen's but it more easily proved to ``` paulson@14883 ` 32` ``` be a cardinal*} ``` paulson@46820 ` 33` ``` "jump_cardinal(K) == ``` paulson@13615 ` 34` ``` \X\Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" ``` paulson@46820 ` 35` wenzelm@24893 ` 36` ```definition ``` wenzelm@24893 ` 37` ``` csucc :: "i=>i" where ``` paulson@14883 ` 38` ``` --{*needed because @{term "jump_cardinal(K)"} might not be the successor ``` paulson@14883 ` 39` ``` of @{term K}*} ``` paulson@12667 ` 40` ``` "csucc(K) == LEAST L. Card(L) & K" 65) and ``` wenzelm@24893 ` 44` ``` cmult (infixl "\" 70) ``` wenzelm@24893 ` 45` paulson@46821 ` 46` ```notation (HTML) ``` wenzelm@24893 ` 47` ``` cadd (infixl "\" 65) and ``` wenzelm@24893 ` 48` ``` cmult (infixl "\" 70) ``` paulson@12667 ` 49` paulson@12667 ` 50` paulson@46820 ` 51` ```lemma Card_Union [simp,intro,TC]: "(\x\A. Card(x)) ==> Card(\(A))" ``` paulson@46820 ` 52` ```apply (rule CardI) ``` paulson@46820 ` 53` ``` apply (simp add: Card_is_Ord) ``` paulson@12667 ` 54` ```apply (clarify dest!: ltD) ``` paulson@46820 ` 55` ```apply (drule bspec, assumption) ``` paulson@46820 ` 56` ```apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) ``` paulson@12667 ` 57` ```apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) ``` paulson@46820 ` 58` ```apply (drule lesspoll_trans1, assumption) ``` paulson@13216 ` 59` ```apply (subgoal_tac "B \ \A") ``` paulson@46820 ` 60` ``` apply (drule lesspoll_trans1, assumption, blast) ``` paulson@46820 ` 61` ```apply (blast intro: subset_imp_lepoll) ``` paulson@12667 ` 62` ```done ``` paulson@12667 ` 63` paulson@46820 ` 64` ```lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\x\A. K(x))" ``` paulson@46820 ` 65` ```by (blast intro: Card_Union) ``` paulson@12667 ` 66` paulson@12667 ` 67` ```lemma Card_OUN [simp,intro,TC]: ``` paulson@13615 ` 68` ``` "(!!x. x:A ==> Card(K(x))) ==> Card(\x nat ==> n \ nat" ``` paulson@12776 ` 72` ```apply (unfold lesspoll_def) ``` paulson@12776 ` 73` ```apply (rule conjI) ``` paulson@12776 ` 74` ```apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat) ``` paulson@12776 ` 75` ```apply (rule notI) ``` paulson@12776 ` 76` ```apply (erule eqpollE) ``` paulson@12776 ` 77` ```apply (rule succ_lepoll_natE) ``` paulson@46820 ` 78` ```apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] ``` paulson@46820 ` 79` ``` lepoll_trans, assumption) ``` paulson@12776 ` 80` ```done ``` paulson@12776 ` 81` paulson@12776 ` 82` ```lemma in_Card_imp_lesspoll: "[| Card(K); b \ K |] ==> b \ K" ``` paulson@12776 ` 83` ```apply (unfold lesspoll_def) ``` paulson@12776 ` 84` ```apply (simp add: Card_iff_initial) ``` paulson@12776 ` 85` ```apply (fast intro!: le_imp_lepoll ltI leI) ``` paulson@12776 ` 86` ```done ``` paulson@12776 ` 87` paulson@14883 ` 88` ```lemma lesspoll_lemma: "[| ~ A \ B; C \ B |] ==> A - C \ 0" ``` paulson@12776 ` 89` ```apply (unfold lesspoll_def) ``` paulson@12776 ` 90` ```apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll] ``` paulson@46820 ` 91` ``` intro!: eqpollI elim: notE ``` paulson@12776 ` 92` ``` elim!: eqpollE lepoll_trans) ``` paulson@12776 ` 93` ```done ``` paulson@12776 ` 94` paulson@13216 ` 95` paulson@13356 ` 96` ```subsection{*Cardinal addition*} ``` paulson@13216 ` 97` paulson@13328 ` 98` ```text{*Note: Could omit proving the algebraic laws for cardinal addition and ``` paulson@13328 ` 99` ```multiplication. On finite cardinals these operations coincide with ``` paulson@13328 ` 100` ```addition and multiplication of natural numbers; on infinite cardinals they ``` paulson@13328 ` 101` ```coincide with union (maximum). Either way we get most laws for free.*} ``` paulson@13328 ` 102` paulson@14883 ` 103` ```subsubsection{*Cardinal addition is commutative*} ``` paulson@13216 ` 104` paulson@13216 ` 105` ```lemma sum_commute_eqpoll: "A+B \ B+A" ``` paulson@13216 ` 106` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 107` ```apply (rule exI) ``` paulson@13216 ` 108` ```apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective) ``` paulson@13216 ` 109` ```apply auto ``` paulson@13216 ` 110` ```done ``` paulson@13216 ` 111` paulson@46821 ` 112` ```lemma cadd_commute: "i \ j = j \ i" ``` paulson@13216 ` 113` ```apply (unfold cadd_def) ``` paulson@13216 ` 114` ```apply (rule sum_commute_eqpoll [THEN cardinal_cong]) ``` paulson@13216 ` 115` ```done ``` paulson@13216 ` 116` paulson@14883 ` 117` ```subsubsection{*Cardinal addition is associative*} ``` paulson@13216 ` 118` paulson@13216 ` 119` ```lemma sum_assoc_eqpoll: "(A+B)+C \ A+(B+C)" ``` paulson@13216 ` 120` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 121` ```apply (rule exI) ``` paulson@13216 ` 122` ```apply (rule sum_assoc_bij) ``` paulson@13216 ` 123` ```done ``` paulson@13216 ` 124` paulson@13216 ` 125` ```(*Unconditional version requires AC*) ``` paulson@46820 ` 126` ```lemma well_ord_cadd_assoc: ``` paulson@13216 ` 127` ``` "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ``` paulson@46821 ` 128` ``` ==> (i \ j) \ k = i \ (j \ k)" ``` paulson@13216 ` 129` ```apply (unfold cadd_def) ``` paulson@13216 ` 130` ```apply (rule cardinal_cong) ``` paulson@13216 ` 131` ```apply (rule eqpoll_trans) ``` paulson@13216 ` 132` ``` apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) ``` paulson@46820 ` 133` ``` apply (blast intro: well_ord_radd ) ``` paulson@13216 ` 134` ```apply (rule sum_assoc_eqpoll [THEN eqpoll_trans]) ``` paulson@13216 ` 135` ```apply (rule eqpoll_sym) ``` paulson@13216 ` 136` ```apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) ``` paulson@46820 ` 137` ```apply (blast intro: well_ord_radd ) ``` paulson@13216 ` 138` ```done ``` paulson@13216 ` 139` paulson@14883 ` 140` ```subsubsection{*0 is the identity for addition*} ``` paulson@13216 ` 141` paulson@13216 ` 142` ```lemma sum_0_eqpoll: "0+A \ A" ``` paulson@13216 ` 143` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 144` ```apply (rule exI) ``` paulson@13216 ` 145` ```apply (rule bij_0_sum) ``` paulson@13216 ` 146` ```done ``` paulson@13216 ` 147` paulson@46821 ` 148` ```lemma cadd_0 [simp]: "Card(K) ==> 0 \ K = K" ``` paulson@13216 ` 149` ```apply (unfold cadd_def) ``` paulson@13216 ` 150` ```apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq) ``` paulson@13216 ` 151` ```done ``` paulson@13216 ` 152` paulson@14883 ` 153` ```subsubsection{*Addition by another cardinal*} ``` paulson@13216 ` 154` paulson@13216 ` 155` ```lemma sum_lepoll_self: "A \ A+B" ``` paulson@13216 ` 156` ```apply (unfold lepoll_def inj_def) ``` paulson@46820 ` 157` ```apply (rule_tac x = "\x\A. Inl (x) " in exI) ``` paulson@13221 ` 158` ```apply simp ``` paulson@13216 ` 159` ```done ``` paulson@13216 ` 160` paulson@13216 ` 161` ```(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) ``` paulson@13216 ` 162` paulson@46820 ` 163` ```lemma cadd_le_self: ``` paulson@46821 ` 164` ``` "[| Card(K); Ord(L) |] ==> K \ (K \ L)" ``` paulson@13216 ` 165` ```apply (unfold cadd_def) ``` paulson@13221 ` 166` ```apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le], ``` paulson@13221 ` 167` ``` assumption) ``` paulson@13216 ` 168` ```apply (rule_tac [2] sum_lepoll_self) ``` paulson@13216 ` 169` ```apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord) ``` paulson@13216 ` 170` ```done ``` paulson@13216 ` 171` paulson@14883 ` 172` ```subsubsection{*Monotonicity of addition*} ``` paulson@13216 ` 173` paulson@46820 ` 174` ```lemma sum_lepoll_mono: ``` paulson@13221 ` 175` ``` "[| A \ C; B \ D |] ==> A + B \ C + D" ``` paulson@13216 ` 176` ```apply (unfold lepoll_def) ``` paulson@13221 ` 177` ```apply (elim exE) ``` paulson@46820 ` 178` ```apply (rule_tac x = "\z\A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI) ``` paulson@13221 ` 179` ```apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) ` y))" ``` paulson@13216 ` 180` ``` in lam_injective) ``` paulson@13221 ` 181` ```apply (typecheck add: inj_is_fun, auto) ``` paulson@13216 ` 182` ```done ``` paulson@13216 ` 183` paulson@13216 ` 184` ```lemma cadd_le_mono: ``` paulson@46821 ` 185` ``` "[| K' \ K; L' \ L |] ==> (K' \ L') \ (K \ L)" ``` paulson@13216 ` 186` ```apply (unfold cadd_def) ``` paulson@13216 ` 187` ```apply (safe dest!: le_subset_iff [THEN iffD1]) ``` paulson@13216 ` 188` ```apply (rule well_ord_lepoll_imp_Card_le) ``` paulson@13216 ` 189` ```apply (blast intro: well_ord_radd well_ord_Memrel) ``` paulson@13216 ` 190` ```apply (blast intro: sum_lepoll_mono subset_imp_lepoll) ``` paulson@13216 ` 191` ```done ``` paulson@13216 ` 192` paulson@14883 ` 193` ```subsubsection{*Addition of finite cardinals is "ordinary" addition*} ``` paulson@13216 ` 194` paulson@13216 ` 195` ```lemma sum_succ_eqpoll: "succ(A)+B \ succ(A+B)" ``` paulson@13216 ` 196` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 197` ```apply (rule exI) ``` paulson@46820 ` 198` ```apply (rule_tac c = "%z. if z=Inl (A) then A+B else z" ``` paulson@13216 ` 199` ``` and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective) ``` paulson@13221 ` 200` ``` apply simp_all ``` paulson@13216 ` 201` ```apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+ ``` paulson@13216 ` 202` ```done ``` paulson@13216 ` 203` paulson@13216 ` 204` ```(*Pulling the succ(...) outside the |...| requires m, n: nat *) ``` paulson@13216 ` 205` ```(*Unconditional version requires AC*) ``` paulson@13216 ` 206` ```lemma cadd_succ_lemma: ``` paulson@46821 ` 207` ``` "[| Ord(m); Ord(n) |] ==> succ(m) \ n = |succ(m \ n)|" ``` paulson@13216 ` 208` ```apply (unfold cadd_def) ``` paulson@13216 ` 209` ```apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans]) ``` paulson@13216 ` 210` ```apply (rule succ_eqpoll_cong [THEN cardinal_cong]) ``` paulson@13216 ` 211` ```apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym]) ``` paulson@13216 ` 212` ```apply (blast intro: well_ord_radd well_ord_Memrel) ``` paulson@13216 ` 213` ```done ``` paulson@13216 ` 214` paulson@46821 ` 215` ```lemma nat_cadd_eq_add: "[| m: nat; n: nat |] ==> m \ n = m#+n" ``` paulson@13244 ` 216` ```apply (induct_tac m) ``` paulson@13216 ` 217` ```apply (simp add: nat_into_Card [THEN cadd_0]) ``` paulson@13216 ` 218` ```apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq]) ``` paulson@13216 ` 219` ```done ``` paulson@13216 ` 220` paulson@13216 ` 221` paulson@13356 ` 222` ```subsection{*Cardinal multiplication*} ``` paulson@13216 ` 223` paulson@14883 ` 224` ```subsubsection{*Cardinal multiplication is commutative*} ``` paulson@13216 ` 225` paulson@13216 ` 226` ```(*Easier to prove the two directions separately*) ``` paulson@13216 ` 227` ```lemma prod_commute_eqpoll: "A*B \ B*A" ``` paulson@13216 ` 228` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 229` ```apply (rule exI) ``` paulson@46820 ` 230` ```apply (rule_tac c = "%." and d = "%." in lam_bijective, ``` paulson@46820 ` 231` ``` auto) ``` paulson@13216 ` 232` ```done ``` paulson@13216 ` 233` paulson@46821 ` 234` ```lemma cmult_commute: "i \ j = j \ i" ``` paulson@13216 ` 235` ```apply (unfold cmult_def) ``` paulson@13216 ` 236` ```apply (rule prod_commute_eqpoll [THEN cardinal_cong]) ``` paulson@13216 ` 237` ```done ``` paulson@13216 ` 238` paulson@14883 ` 239` ```subsubsection{*Cardinal multiplication is associative*} ``` paulson@13216 ` 240` paulson@13216 ` 241` ```lemma prod_assoc_eqpoll: "(A*B)*C \ A*(B*C)" ``` paulson@13216 ` 242` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 243` ```apply (rule exI) ``` paulson@13216 ` 244` ```apply (rule prod_assoc_bij) ``` paulson@13216 ` 245` ```done ``` paulson@13216 ` 246` paulson@13216 ` 247` ```(*Unconditional version requires AC*) ``` paulson@13216 ` 248` ```lemma well_ord_cmult_assoc: ``` paulson@13216 ` 249` ``` "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ``` paulson@46821 ` 250` ``` ==> (i \ j) \ k = i \ (j \ k)" ``` paulson@13216 ` 251` ```apply (unfold cmult_def) ``` paulson@13216 ` 252` ```apply (rule cardinal_cong) ``` paulson@46820 ` 253` ```apply (rule eqpoll_trans) ``` paulson@13216 ` 254` ``` apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) ``` paulson@13216 ` 255` ``` apply (blast intro: well_ord_rmult) ``` paulson@13216 ` 256` ```apply (rule prod_assoc_eqpoll [THEN eqpoll_trans]) ``` paulson@46820 ` 257` ```apply (rule eqpoll_sym) ``` paulson@13216 ` 258` ```apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) ``` paulson@13216 ` 259` ```apply (blast intro: well_ord_rmult) ``` paulson@13216 ` 260` ```done ``` paulson@13216 ` 261` paulson@14883 ` 262` ```subsubsection{*Cardinal multiplication distributes over addition*} ``` paulson@13216 ` 263` paulson@13216 ` 264` ```lemma sum_prod_distrib_eqpoll: "(A+B)*C \ (A*C)+(B*C)" ``` paulson@13216 ` 265` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 266` ```apply (rule exI) ``` paulson@13216 ` 267` ```apply (rule sum_prod_distrib_bij) ``` paulson@13216 ` 268` ```done ``` paulson@13216 ` 269` paulson@13216 ` 270` ```lemma well_ord_cadd_cmult_distrib: ``` paulson@13216 ` 271` ``` "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ``` paulson@46821 ` 272` ``` ==> (i \ j) \ k = (i \ k) \ (j \ k)" ``` paulson@13216 ` 273` ```apply (unfold cadd_def cmult_def) ``` paulson@13216 ` 274` ```apply (rule cardinal_cong) ``` paulson@46820 ` 275` ```apply (rule eqpoll_trans) ``` paulson@13216 ` 276` ``` apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl]) ``` paulson@13216 ` 277` ```apply (blast intro: well_ord_radd) ``` paulson@13216 ` 278` ```apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans]) ``` paulson@46820 ` 279` ```apply (rule eqpoll_sym) ``` paulson@46820 ` 280` ```apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll ``` paulson@13216 ` 281` ``` well_ord_cardinal_eqpoll]) ``` paulson@13216 ` 282` ```apply (blast intro: well_ord_rmult)+ ``` paulson@13216 ` 283` ```done ``` paulson@13216 ` 284` paulson@14883 ` 285` ```subsubsection{*Multiplication by 0 yields 0*} ``` paulson@13216 ` 286` paulson@13216 ` 287` ```lemma prod_0_eqpoll: "0*A \ 0" ``` paulson@13216 ` 288` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 289` ```apply (rule exI) ``` paulson@13221 ` 290` ```apply (rule lam_bijective, safe) ``` paulson@13216 ` 291` ```done ``` paulson@13216 ` 292` paulson@46821 ` 293` ```lemma cmult_0 [simp]: "0 \ i = 0" ``` paulson@13221 ` 294` ```by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong]) ``` paulson@13216 ` 295` paulson@14883 ` 296` ```subsubsection{*1 is the identity for multiplication*} ``` paulson@13216 ` 297` paulson@13216 ` 298` ```lemma prod_singleton_eqpoll: "{x}*A \ A" ``` paulson@13216 ` 299` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 300` ```apply (rule exI) ``` paulson@13216 ` 301` ```apply (rule singleton_prod_bij [THEN bij_converse_bij]) ``` paulson@13216 ` 302` ```done ``` paulson@13216 ` 303` paulson@46821 ` 304` ```lemma cmult_1 [simp]: "Card(K) ==> 1 \ K = K" ``` paulson@13216 ` 305` ```apply (unfold cmult_def succ_def) ``` paulson@13216 ` 306` ```apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq) ``` paulson@13216 ` 307` ```done ``` paulson@13216 ` 308` paulson@13356 ` 309` ```subsection{*Some inequalities for multiplication*} ``` paulson@13216 ` 310` paulson@13216 ` 311` ```lemma prod_square_lepoll: "A \ A*A" ``` paulson@13216 ` 312` ```apply (unfold lepoll_def inj_def) ``` paulson@46820 ` 313` ```apply (rule_tac x = "\x\A. " in exI, simp) ``` paulson@13216 ` 314` ```done ``` paulson@13216 ` 315` paulson@13216 ` 316` ```(*Could probably weaken the premise to well_ord(K,r), or remove using AC*) ``` paulson@46821 ` 317` ```lemma cmult_square_le: "Card(K) ==> K \ K \ K" ``` paulson@13216 ` 318` ```apply (unfold cmult_def) ``` paulson@13216 ` 319` ```apply (rule le_trans) ``` paulson@13216 ` 320` ```apply (rule_tac [2] well_ord_lepoll_imp_Card_le) ``` paulson@13216 ` 321` ```apply (rule_tac [3] prod_square_lepoll) ``` paulson@13221 ` 322` ```apply (simp add: le_refl Card_is_Ord Card_cardinal_eq) ``` paulson@13221 ` 323` ```apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) ``` paulson@13216 ` 324` ```done ``` paulson@13216 ` 325` paulson@14883 ` 326` ```subsubsection{*Multiplication by a non-zero cardinal*} ``` paulson@13216 ` 327` paulson@13216 ` 328` ```lemma prod_lepoll_self: "b: B ==> A \ A*B" ``` paulson@13216 ` 329` ```apply (unfold lepoll_def inj_def) ``` paulson@46820 ` 330` ```apply (rule_tac x = "\x\A. " in exI, simp) ``` paulson@13216 ` 331` ```done ``` paulson@13216 ` 332` paulson@13216 ` 333` ```(*Could probably weaken the premises to well_ord(K,r), or removing using AC*) ``` paulson@13216 ` 334` ```lemma cmult_le_self: ``` paulson@46821 ` 335` ``` "[| Card(K); Ord(L); 0 K \ (K \ L)" ``` paulson@13216 ` 336` ```apply (unfold cmult_def) ``` paulson@13216 ` 337` ```apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le]) ``` paulson@13221 ` 338` ``` apply assumption ``` paulson@13216 ` 339` ``` apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord) ``` paulson@13216 ` 340` ```apply (blast intro: prod_lepoll_self ltD) ``` paulson@13216 ` 341` ```done ``` paulson@13216 ` 342` paulson@14883 ` 343` ```subsubsection{*Monotonicity of multiplication*} ``` paulson@13216 ` 344` paulson@13216 ` 345` ```lemma prod_lepoll_mono: ``` paulson@13216 ` 346` ``` "[| A \ C; B \ D |] ==> A * B \ C * D" ``` paulson@13216 ` 347` ```apply (unfold lepoll_def) ``` paulson@13221 ` 348` ```apply (elim exE) ``` paulson@13216 ` 349` ```apply (rule_tac x = "lam :A*B. " in exI) ``` paulson@46820 ` 350` ```apply (rule_tac d = "%. " ``` paulson@13216 ` 351` ``` in lam_injective) ``` paulson@13221 ` 352` ```apply (typecheck add: inj_is_fun, auto) ``` paulson@13216 ` 353` ```done ``` paulson@13216 ` 354` paulson@13216 ` 355` ```lemma cmult_le_mono: ``` paulson@46821 ` 356` ``` "[| K' \ K; L' \ L |] ==> (K' \ L') \ (K \ L)" ``` paulson@13216 ` 357` ```apply (unfold cmult_def) ``` paulson@13216 ` 358` ```apply (safe dest!: le_subset_iff [THEN iffD1]) ``` paulson@13216 ` 359` ```apply (rule well_ord_lepoll_imp_Card_le) ``` paulson@13216 ` 360` ``` apply (blast intro: well_ord_rmult well_ord_Memrel) ``` paulson@13216 ` 361` ```apply (blast intro: prod_lepoll_mono subset_imp_lepoll) ``` paulson@13216 ` 362` ```done ``` paulson@13216 ` 363` paulson@13356 ` 364` ```subsection{*Multiplication of finite cardinals is "ordinary" multiplication*} ``` paulson@13216 ` 365` paulson@13216 ` 366` ```lemma prod_succ_eqpoll: "succ(A)*B \ B + A*B" ``` paulson@13216 ` 367` ```apply (unfold eqpoll_def) ``` paulson@13221 ` 368` ```apply (rule exI) ``` paulson@13216 ` 369` ```apply (rule_tac c = "%. if x=A then Inl (y) else Inr ()" ``` paulson@13216 ` 370` ``` and d = "case (%y. , %z. z)" in lam_bijective) ``` paulson@13216 ` 371` ```apply safe ``` paulson@13216 ` 372` ```apply (simp_all add: succI2 if_type mem_imp_not_eq) ``` paulson@13216 ` 373` ```done ``` paulson@13216 ` 374` paulson@13216 ` 375` ```(*Unconditional version requires AC*) ``` paulson@13216 ` 376` ```lemma cmult_succ_lemma: ``` paulson@46821 ` 377` ``` "[| Ord(m); Ord(n) |] ==> succ(m) \ n = n \ (m \ n)" ``` paulson@13216 ` 378` ```apply (unfold cmult_def cadd_def) ``` paulson@13216 ` 379` ```apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans]) ``` paulson@13216 ` 380` ```apply (rule cardinal_cong [symmetric]) ``` paulson@13216 ` 381` ```apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll]) ``` paulson@13216 ` 382` ```apply (blast intro: well_ord_rmult well_ord_Memrel) ``` paulson@13216 ` 383` ```done ``` paulson@13216 ` 384` paulson@46821 ` 385` ```lemma nat_cmult_eq_mult: "[| m: nat; n: nat |] ==> m \ n = m#*n" ``` paulson@13244 ` 386` ```apply (induct_tac m) ``` paulson@13221 ` 387` ```apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add) ``` paulson@13216 ` 388` ```done ``` paulson@13216 ` 389` paulson@46821 ` 390` ```lemma cmult_2: "Card(n) ==> 2 \ n = n \ n" ``` paulson@13221 ` 391` ```by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0]) ``` paulson@13216 ` 392` paulson@13216 ` 393` ```lemma sum_lepoll_prod: "2 \ C ==> B+B \ C*B" ``` paulson@46820 ` 394` ```apply (rule lepoll_trans) ``` paulson@46820 ` 395` ```apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll]) ``` paulson@46820 ` 396` ```apply (erule prod_lepoll_mono) ``` paulson@46820 ` 397` ```apply (rule lepoll_refl) ``` paulson@13216 ` 398` ```done ``` paulson@13216 ` 399` paulson@13216 ` 400` ```lemma lepoll_imp_sum_lepoll_prod: "[| A \ B; 2 \ A |] ==> A+B \ A*B" ``` paulson@13221 ` 401` ```by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl) ``` paulson@13216 ` 402` paulson@13216 ` 403` paulson@13356 ` 404` ```subsection{*Infinite Cardinals are Limit Ordinals*} ``` paulson@13216 ` 405` paulson@13216 ` 406` ```(*This proof is modelled upon one assuming nat<=A, with injection ``` paulson@46820 ` 407` ``` \z\cons(u,A). if z=u then 0 else if z \ nat then succ(z) else z ``` paulson@13216 ` 408` ``` and inverse %y. if y:nat then nat_case(u, %z. z, y) else y. \ ``` paulson@13216 ` 409` ``` If f: inj(nat,A) then range(f) behaves like the natural numbers.*) ``` paulson@13216 ` 410` ```lemma nat_cons_lepoll: "nat \ A ==> cons(u,A) \ A" ``` paulson@13216 ` 411` ```apply (unfold lepoll_def) ``` paulson@13216 ` 412` ```apply (erule exE) ``` paulson@46820 ` 413` ```apply (rule_tac x = ``` paulson@46820 ` 414` ``` "\z\cons (u,A). ``` paulson@46820 ` 415` ``` if z=u then f`0 ``` paulson@46820 ` 416` ``` else if z: range (f) then f`succ (converse (f) `z) else z" ``` paulson@13216 ` 417` ``` in exI) ``` paulson@13216 ` 418` ```apply (rule_tac d = ``` paulson@46820 ` 419` ``` "%y. if y: range(f) then nat_case (u, %z. f`z, converse(f) `y) ``` paulson@46820 ` 420` ``` else y" ``` paulson@13216 ` 421` ``` in lam_injective) ``` paulson@13216 ` 422` ```apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun) ``` paulson@13216 ` 423` ```apply (simp add: inj_is_fun [THEN apply_rangeI] ``` paulson@13216 ` 424` ``` inj_converse_fun [THEN apply_rangeI] ``` paulson@13216 ` 425` ``` inj_converse_fun [THEN apply_funtype]) ``` paulson@13216 ` 426` ```done ``` paulson@13216 ` 427` paulson@13216 ` 428` ```lemma nat_cons_eqpoll: "nat \ A ==> cons(u,A) \ A" ``` paulson@13216 ` 429` ```apply (erule nat_cons_lepoll [THEN eqpollI]) ``` paulson@13216 ` 430` ```apply (rule subset_consI [THEN subset_imp_lepoll]) ``` paulson@13216 ` 431` ```done ``` paulson@13216 ` 432` paulson@13216 ` 433` ```(*Specialized version required below*) ``` paulson@46820 ` 434` ```lemma nat_succ_eqpoll: "nat \ A ==> succ(A) \ A" ``` paulson@13216 ` 435` ```apply (unfold succ_def) ``` paulson@13216 ` 436` ```apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll]) ``` paulson@13216 ` 437` ```done ``` paulson@13216 ` 438` paulson@13216 ` 439` ```lemma InfCard_nat: "InfCard(nat)" ``` paulson@13216 ` 440` ```apply (unfold InfCard_def) ``` paulson@13216 ` 441` ```apply (blast intro: Card_nat le_refl Card_is_Ord) ``` paulson@13216 ` 442` ```done ``` paulson@13216 ` 443` paulson@13216 ` 444` ```lemma InfCard_is_Card: "InfCard(K) ==> Card(K)" ``` paulson@13216 ` 445` ```apply (unfold InfCard_def) ``` paulson@13216 ` 446` ```apply (erule conjunct1) ``` paulson@13216 ` 447` ```done ``` paulson@13216 ` 448` paulson@13216 ` 449` ```lemma InfCard_Un: ``` paulson@46820 ` 450` ``` "[| InfCard(K); Card(L) |] ==> InfCard(K \ L)" ``` paulson@13216 ` 451` ```apply (unfold InfCard_def) ``` paulson@13216 ` 452` ```apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans] Card_is_Ord) ``` paulson@13216 ` 453` ```done ``` paulson@13216 ` 454` paulson@13216 ` 455` ```(*Kunen's Lemma 10.11*) ``` paulson@13216 ` 456` ```lemma InfCard_is_Limit: "InfCard(K) ==> Limit(K)" ``` paulson@13216 ` 457` ```apply (unfold InfCard_def) ``` paulson@13216 ` 458` ```apply (erule conjE) ``` paulson@13216 ` 459` ```apply (frule Card_is_Ord) ``` paulson@13216 ` 460` ```apply (rule ltI [THEN non_succ_LimitI]) ``` paulson@13216 ` 461` ```apply (erule le_imp_subset [THEN subsetD]) ``` paulson@13216 ` 462` ```apply (safe dest!: Limit_nat [THEN Limit_le_succD]) ``` paulson@13216 ` 463` ```apply (unfold Card_def) ``` paulson@13216 ` 464` ```apply (drule trans) ``` paulson@13216 ` 465` ```apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong]) ``` paulson@13216 ` 466` ```apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl]) ``` paulson@13221 ` 467` ```apply (rule le_eqI, assumption) ``` paulson@13216 ` 468` ```apply (rule Ord_cardinal) ``` paulson@13216 ` 469` ```done ``` paulson@13216 ` 470` paulson@13216 ` 471` paulson@13216 ` 472` ```(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***) ``` paulson@13216 ` 473` paulson@13216 ` 474` ```(*A general fact about ordermap*) ``` paulson@13216 ` 475` ```lemma ordermap_eqpoll_pred: ``` paulson@13269 ` 476` ``` "[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x \ Order.pred(A,x,r)" ``` paulson@13216 ` 477` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 478` ```apply (rule exI) ``` paulson@13221 ` 479` ```apply (simp add: ordermap_eq_image well_ord_is_wf) ``` paulson@46820 ` 480` ```apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, ``` paulson@13221 ` 481` ``` THEN bij_converse_bij]) ``` paulson@13216 ` 482` ```apply (rule pred_subset) ``` paulson@13216 ` 483` ```done ``` paulson@13216 ` 484` paulson@14883 ` 485` ```subsubsection{*Establishing the well-ordering*} ``` paulson@13216 ` 486` paulson@13216 ` 487` ```lemma csquare_lam_inj: ``` paulson@46820 ` 488` ``` "Ord(K) ==> (lam :K*K. y, x, y>) \ inj(K*K, K*K*K)" ``` paulson@13216 ` 489` ```apply (unfold inj_def) ``` paulson@13216 ` 490` ```apply (force intro: lam_type Un_least_lt [THEN ltD] ltI) ``` paulson@13216 ` 491` ```done ``` paulson@13216 ` 492` paulson@13216 ` 493` ```lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))" ``` paulson@13216 ` 494` ```apply (unfold csquare_rel_def) ``` paulson@13221 ` 495` ```apply (rule csquare_lam_inj [THEN well_ord_rvimage], assumption) ``` paulson@13216 ` 496` ```apply (blast intro: well_ord_rmult well_ord_Memrel) ``` paulson@13216 ` 497` ```done ``` paulson@13216 ` 498` paulson@14883 ` 499` ```subsubsection{*Characterising initial segments of the well-ordering*} ``` paulson@13216 ` 500` paulson@13216 ` 501` ```lemma csquareD: ``` paulson@46820 ` 502` ``` "[| <, > \ csquare_rel(K); x x \ z & y \ z" ``` paulson@13216 ` 503` ```apply (unfold csquare_rel_def) ``` paulson@13216 ` 504` ```apply (erule rev_mp) ``` paulson@13216 ` 505` ```apply (elim ltE) ``` paulson@13221 ` 506` ```apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD) ``` paulson@13216 ` 507` ```apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le) ``` paulson@13221 ` 508` ```apply (simp_all add: lt_def succI2) ``` paulson@13216 ` 509` ```done ``` paulson@13216 ` 510` paulson@46820 ` 511` ```lemma pred_csquare_subset: ``` paulson@46820 ` 512` ``` "z Order.pred(K*K, , csquare_rel(K)) \ succ(z)*succ(z)" ``` paulson@13216 ` 513` ```apply (unfold Order.pred_def) ``` paulson@13216 ` 514` ```apply (safe del: SigmaI succCI) ``` paulson@13216 ` 515` ```apply (erule csquareD [THEN conjE]) ``` paulson@46820 ` 516` ```apply (unfold lt_def, auto) ``` paulson@13216 ` 517` ```done ``` paulson@13216 ` 518` paulson@13216 ` 519` ```lemma csquare_ltI: ``` paulson@46820 ` 520` ``` "[| x <, > \ csquare_rel(K)" ``` paulson@13216 ` 521` ```apply (unfold csquare_rel_def) ``` paulson@13216 ` 522` ```apply (subgoal_tac "x z; y \ z; z <, > \ csquare_rel(K) | x=z & y=z" ``` paulson@13216 ` 531` ```apply (unfold csquare_rel_def) ``` paulson@13216 ` 532` ```apply (subgoal_tac "x y) |] ==> ``` paulson@13216 ` 545` ``` ordermap(K*K, csquare_rel(K)) ` < ``` paulson@13216 ` 546` ``` ordermap(K*K, csquare_rel(K)) ` " ``` paulson@13216 ` 547` ```apply (subgoal_tac "z: K*K has no more than z*z predecessors..." (page 29) *) ``` paulson@13216 ` 556` ```lemma ordermap_csquare_le: ``` paulson@46820 ` 557` ``` "[| Limit(K); x y) |] ``` paulson@46821 ` 558` ``` ==> | ordermap(K*K, csquare_rel(K)) ` | \ |succ(z)| \ |succ(z)|" ``` paulson@13216 ` 559` ```apply (unfold cmult_def) ``` paulson@13216 ` 560` ```apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le]) ``` paulson@13216 ` 561` ```apply (rule Ord_cardinal [THEN well_ord_Memrel])+ ``` paulson@13216 ` 562` ```apply (subgoal_tac "z"} K" *) ``` paulson@13216 ` 577` ```lemma ordertype_csquare_le: ``` paulson@46821 ` 578` ``` "[| InfCard(K); \y\K. InfCard(y) \ y \ y = y |] ``` paulson@46820 ` 579` ``` ==> ordertype(K*K, csquare_rel(K)) \ K" ``` paulson@13216 ` 580` ```apply (frule InfCard_is_Card [THEN Card_is_Ord]) ``` paulson@13221 ` 581` ```apply (rule all_lt_imp_le, assumption) ``` paulson@13216 ` 582` ```apply (erule well_ord_csquare [THEN Ord_ordertype]) ``` paulson@13216 ` 583` ```apply (rule Card_lt_imp_lt) ``` paulson@13216 ` 584` ```apply (erule_tac [3] InfCard_is_Card) ``` paulson@13216 ` 585` ```apply (erule_tac [2] ltE) ``` paulson@13216 ` 586` ```apply (simp add: ordertype_unfold) ``` paulson@13216 ` 587` ```apply (safe elim!: ltE) ``` paulson@13216 ` 588` ```apply (subgoal_tac "Ord (xa) & Ord (ya)") ``` paulson@13221 ` 589` ``` prefer 2 apply (blast intro: Ord_in_Ord, clarify) ``` paulson@46820 ` 590` ```(*??WHAT A MESS!*) ``` paulson@13216 ` 591` ```apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1], ``` paulson@46820 ` 592` ``` (assumption | rule refl | erule ltI)+) ``` paulson@46820 ` 593` ```apply (rule_tac i = "xa \ ya" and j = nat in Ord_linear2, ``` paulson@13216 ` 594` ``` simp_all add: Ord_Un Ord_nat) ``` paulson@46820 ` 595` ```prefer 2 (*case @{term"nat \ (xa \ ya)"} *) ``` paulson@46820 ` 596` ``` apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] ``` paulson@13216 ` 597` ``` le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un ``` paulson@13216 ` 598` ``` ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD]) ``` paulson@46820 ` 599` ```(*the finite case: @{term"xa \ ya < nat"} *) ``` paulson@13784 ` 600` ```apply (rule_tac j = nat in lt_trans2) ``` paulson@13216 ` 601` ``` apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type ``` paulson@13216 ` 602` ``` nat_into_Card [THEN Card_cardinal_eq] Ord_nat) ``` paulson@13216 ` 603` ```apply (simp add: InfCard_def) ``` paulson@13216 ` 604` ```done ``` paulson@13216 ` 605` paulson@13216 ` 606` ```(*Main result: Kunen's Theorem 10.12*) ``` paulson@46821 ` 607` ```lemma InfCard_csquare_eq: "InfCard(K) ==> K \ K = K" ``` paulson@13216 ` 608` ```apply (frule InfCard_is_Card [THEN Card_is_Ord]) ``` paulson@13216 ` 609` ```apply (erule rev_mp) ``` paulson@46820 ` 610` ```apply (erule_tac i=K in trans_induct) ``` paulson@13216 ` 611` ```apply (rule impI) ``` paulson@13216 ` 612` ```apply (rule le_anti_sym) ``` paulson@13216 ` 613` ```apply (erule_tac [2] InfCard_is_Card [THEN cmult_square_le]) ``` paulson@13216 ` 614` ```apply (rule ordertype_csquare_le [THEN [2] le_trans]) ``` paulson@46820 ` 615` ```apply (simp add: cmult_def Ord_cardinal_le ``` paulson@13221 ` 616` ``` well_ord_csquare [THEN Ord_ordertype] ``` paulson@46820 ` 617` ``` well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll, ``` paulson@13221 ` 618` ``` THEN cardinal_cong], assumption+) ``` paulson@13216 ` 619` ```done ``` paulson@13216 ` 620` paulson@13216 ` 621` ```(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*) ``` paulson@13216 ` 622` ```lemma well_ord_InfCard_square_eq: ``` paulson@13216 ` 623` ``` "[| well_ord(A,r); InfCard(|A|) |] ==> A*A \ A" ``` paulson@13216 ` 624` ```apply (rule prod_eqpoll_cong [THEN eqpoll_trans]) ``` paulson@13216 ` 625` ```apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+ ``` paulson@13216 ` 626` ```apply (rule well_ord_cardinal_eqE) ``` paulson@13221 ` 627` ```apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel, assumption) ``` paulson@13221 ` 628` ```apply (simp add: cmult_def [symmetric] InfCard_csquare_eq) ``` paulson@13216 ` 629` ```done ``` paulson@13216 ` 630` paulson@13356 ` 631` ```lemma InfCard_square_eqpoll: "InfCard(K) ==> K \ K \ K" ``` paulson@46820 ` 632` ```apply (rule well_ord_InfCard_square_eq) ``` paulson@46820 ` 633` ``` apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) ``` paulson@46820 ` 634` ```apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) ``` paulson@13356 ` 635` ```done ``` paulson@13356 ` 636` paulson@13356 ` 637` ```lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)" ``` paulson@13356 ` 638` ```by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord]) ``` paulson@13356 ` 639` paulson@14883 ` 640` ```subsubsection{*Toward's Kunen's Corollary 10.13 (1)*} ``` paulson@13216 ` 641` paulson@46821 ` 642` ```lemma InfCard_le_cmult_eq: "[| InfCard(K); L \ K; 0 K \ L = K" ``` paulson@13216 ` 643` ```apply (rule le_anti_sym) ``` paulson@13216 ` 644` ``` prefer 2 ``` paulson@13216 ` 645` ``` apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card) ``` paulson@13216 ` 646` ```apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl]) ``` paulson@13216 ` 647` ```apply (rule cmult_le_mono [THEN le_trans], assumption+) ``` paulson@13216 ` 648` ```apply (simp add: InfCard_csquare_eq) ``` paulson@13216 ` 649` ```done ``` paulson@13216 ` 650` paulson@13216 ` 651` ```(*Corollary 10.13 (1), for cardinal multiplication*) ``` paulson@46821 ` 652` ```lemma InfCard_cmult_eq: "[| InfCard(K); InfCard(L) |] ==> K \ L = K \ L" ``` paulson@13784 ` 653` ```apply (rule_tac i = K and j = L in Ord_linear_le) ``` paulson@13216 ` 654` ```apply (typecheck add: InfCard_is_Card Card_is_Ord) ``` paulson@13216 ` 655` ```apply (rule cmult_commute [THEN ssubst]) ``` paulson@13216 ` 656` ```apply (rule Un_commute [THEN ssubst]) ``` paulson@46820 ` 657` ```apply (simp_all add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq ``` paulson@13221 ` 658` ``` subset_Un_iff2 [THEN iffD1] le_imp_subset) ``` paulson@13216 ` 659` ```done ``` paulson@13216 ` 660` paulson@46821 ` 661` ```lemma InfCard_cdouble_eq: "InfCard(K) ==> K \ K = K" ``` paulson@13221 ` 662` ```apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute) ``` paulson@13221 ` 663` ```apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ) ``` paulson@13216 ` 664` ```done ``` paulson@13216 ` 665` paulson@13216 ` 666` ```(*Corollary 10.13 (1), for cardinal addition*) ``` paulson@46821 ` 667` ```lemma InfCard_le_cadd_eq: "[| InfCard(K); L \ K |] ==> K \ L = K" ``` paulson@13216 ` 668` ```apply (rule le_anti_sym) ``` paulson@13216 ` 669` ``` prefer 2 ``` paulson@13216 ` 670` ``` apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card) ``` paulson@13216 ` 671` ```apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl]) ``` paulson@13216 ` 672` ```apply (rule cadd_le_mono [THEN le_trans], assumption+) ``` paulson@13216 ` 673` ```apply (simp add: InfCard_cdouble_eq) ``` paulson@13216 ` 674` ```done ``` paulson@13216 ` 675` paulson@46821 ` 676` ```lemma InfCard_cadd_eq: "[| InfCard(K); InfCard(L) |] ==> K \ L = K \ L" ``` paulson@13784 ` 677` ```apply (rule_tac i = K and j = L in Ord_linear_le) ``` paulson@13216 ` 678` ```apply (typecheck add: InfCard_is_Card Card_is_Ord) ``` paulson@13216 ` 679` ```apply (rule cadd_commute [THEN ssubst]) ``` paulson@13216 ` 680` ```apply (rule Un_commute [THEN ssubst]) ``` paulson@13221 ` 681` ```apply (simp_all add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset) ``` paulson@13216 ` 682` ```done ``` paulson@13216 ` 683` paulson@13216 ` 684` ```(*The other part, Corollary 10.13 (2), refers to the cardinality of the set ``` paulson@13216 ` 685` ``` of all n-tuples of elements of K. A better version for the Isabelle theory ``` paulson@13216 ` 686` ``` might be InfCard(K) ==> |list(K)| = K. ``` paulson@13216 ` 687` ```*) ``` paulson@13216 ` 688` ballarin@27517 ` 689` ```subsection{*For Every Cardinal Number There Exists A Greater One*} ``` paulson@13356 ` 690` paulson@13356 ` 691` ```text{*This result is Kunen's Theorem 10.16, which would be trivial using AC*} ``` paulson@13216 ` 692` paulson@13216 ` 693` ```lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))" ``` paulson@13216 ` 694` ```apply (unfold jump_cardinal_def) ``` paulson@13216 ` 695` ```apply (rule Ord_is_Transset [THEN [2] OrdI]) ``` paulson@13216 ` 696` ``` prefer 2 apply (blast intro!: Ord_ordertype) ``` paulson@13216 ` 697` ```apply (unfold Transset_def) ``` paulson@13216 ` 698` ```apply (safe del: subsetI) ``` paulson@13221 ` 699` ```apply (simp add: ordertype_pred_unfold, safe) ``` paulson@13216 ` 700` ```apply (rule UN_I) ``` paulson@13216 ` 701` ```apply (rule_tac [2] ReplaceI) ``` paulson@13216 ` 702` ``` prefer 4 apply (blast intro: well_ord_subset elim!: predE)+ ``` paulson@13216 ` 703` ```done ``` paulson@13216 ` 704` paulson@13216 ` 705` ```(*Allows selective unfolding. Less work than deriving intro/elim rules*) ``` paulson@13216 ` 706` ```lemma jump_cardinal_iff: ``` paulson@46821 ` 707` ``` "i \ jump_cardinal(K) \ ``` paulson@46820 ` 708` ``` (\r X. r \ K*K & X \ K & well_ord(X,r) & i = ordertype(X,r))" ``` paulson@13216 ` 709` ```apply (unfold jump_cardinal_def) ``` paulson@46820 ` 710` ```apply (blast del: subsetI) ``` paulson@13216 ` 711` ```done ``` paulson@13216 ` 712` paulson@13216 ` 713` ```(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*) ``` paulson@13216 ` 714` ```lemma K_lt_jump_cardinal: "Ord(K) ==> K < jump_cardinal(K)" ``` paulson@13216 ` 715` ```apply (rule Ord_jump_cardinal [THEN [2] ltI]) ``` paulson@13216 ` 716` ```apply (rule jump_cardinal_iff [THEN iffD2]) ``` paulson@13216 ` 717` ```apply (rule_tac x="Memrel(K)" in exI) ``` paulson@46820 ` 718` ```apply (rule_tac x=K in exI) ``` paulson@13216 ` 719` ```apply (simp add: ordertype_Memrel well_ord_Memrel) ``` paulson@13216 ` 720` ```apply (simp add: Memrel_def subset_iff) ``` paulson@13216 ` 721` ```done ``` paulson@13216 ` 722` paulson@13216 ` 723` ```(*The proof by contradiction: the bijection f yields a wellordering of X ``` paulson@13216 ` 724` ``` whose ordertype is jump_cardinal(K). *) ``` paulson@13216 ` 725` ```lemma Card_jump_cardinal_lemma: ``` paulson@46820 ` 726` ``` "[| well_ord(X,r); r \ K * K; X \ K; ``` paulson@46820 ` 727` ``` f \ bij(ordertype(X,r), jump_cardinal(K)) |] ``` paulson@46820 ` 728` ``` ==> jump_cardinal(K) \ jump_cardinal(K)" ``` paulson@46820 ` 729` ```apply (subgoal_tac "f O ordermap (X,r) \ bij (X, jump_cardinal (K))") ``` paulson@13216 ` 730` ``` prefer 2 apply (blast intro: comp_bij ordermap_bij) ``` paulson@13216 ` 731` ```apply (rule jump_cardinal_iff [THEN iffD2]) ``` paulson@13216 ` 732` ```apply (intro exI conjI) ``` paulson@13221 ` 733` ```apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+) ``` paulson@13216 ` 734` ```apply (erule bij_is_inj [THEN well_ord_rvimage]) ``` paulson@13216 ` 735` ```apply (rule Ord_jump_cardinal [THEN well_ord_Memrel]) ``` paulson@13216 ` 736` ```apply (simp add: well_ord_Memrel [THEN [2] bij_ordertype_vimage] ``` paulson@13216 ` 737` ``` ordertype_Memrel Ord_jump_cardinal) ``` paulson@13216 ` 738` ```done ``` paulson@13216 ` 739` paulson@13216 ` 740` ```(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) ``` paulson@13216 ` 741` ```lemma Card_jump_cardinal: "Card(jump_cardinal(K))" ``` paulson@13216 ` 742` ```apply (rule Ord_jump_cardinal [THEN CardI]) ``` paulson@13216 ` 743` ```apply (unfold eqpoll_def) ``` paulson@13216 ` 744` ```apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1]) ``` paulson@13216 ` 745` ```apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl]) ``` paulson@13216 ` 746` ```done ``` paulson@13216 ` 747` paulson@13356 ` 748` ```subsection{*Basic Properties of Successor Cardinals*} ``` paulson@13216 ` 749` paulson@13216 ` 750` ```lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)" ``` paulson@13216 ` 751` ```apply (unfold csucc_def) ``` paulson@13216 ` 752` ```apply (rule LeastI) ``` paulson@13216 ` 753` ```apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ ``` paulson@13216 ` 754` ```done ``` paulson@13216 ` 755` wenzelm@45602 ` 756` ```lemmas Card_csucc = csucc_basic [THEN conjunct1] ``` paulson@13216 ` 757` wenzelm@45602 ` 758` ```lemmas lt_csucc = csucc_basic [THEN conjunct2] ``` paulson@13216 ` 759` paulson@13216 ` 760` ```lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)" ``` paulson@13221 ` 761` ```by (blast intro: Ord_0_le lt_csucc lt_trans1) ``` paulson@13216 ` 762` paulson@46820 ` 763` ```lemma csucc_le: "[| Card(L); K csucc(K) \ L" ``` paulson@13216 ` 764` ```apply (unfold csucc_def) ``` paulson@13216 ` 765` ```apply (rule Least_le) ``` paulson@13216 ` 766` ```apply (blast intro: Card_is_Ord)+ ``` paulson@13216 ` 767` ```done ``` paulson@13216 ` 768` paulson@46821 ` 769` ```lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) \ |i| \ K" ``` paulson@13216 ` 770` ```apply (rule iffI) ``` paulson@13216 ` 771` ```apply (rule_tac [2] Card_lt_imp_lt) ``` paulson@13216 ` 772` ```apply (erule_tac [2] lt_trans1) ``` paulson@13216 ` 773` ```apply (simp_all add: lt_csucc Card_csucc Card_is_Ord) ``` paulson@13216 ` 774` ```apply (rule notI [THEN not_lt_imp_le]) ``` paulson@13221 ` 775` ```apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl], assumption) ``` paulson@13216 ` 776` ```apply (rule Ord_cardinal_le [THEN lt_trans1]) ``` paulson@46820 ` 777` ```apply (simp_all add: Ord_cardinal Card_is_Ord) ``` paulson@13216 ` 778` ```done ``` paulson@13216 ` 779` paulson@13216 ` 780` ```lemma Card_lt_csucc_iff: ``` paulson@46821 ` 781` ``` "[| Card(K'); Card(K) |] ==> K' < csucc(K) \ K' \ K" ``` paulson@13221 ` 782` ```by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord) ``` paulson@13216 ` 783` paulson@13216 ` 784` ```lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))" ``` paulson@46820 ` 785` ```by (simp add: InfCard_def Card_csucc Card_is_Ord ``` paulson@13216 ` 786` ``` lt_csucc [THEN leI, THEN [2] le_trans]) ``` paulson@13216 ` 787` paulson@13216 ` 788` paulson@14883 ` 789` ```subsubsection{*Removing elements from a finite set decreases its cardinality*} ``` paulson@13216 ` 790` paulson@46820 ` 791` ```lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x\A \ ~ cons(x,A) \ A" ``` paulson@13216 ` 792` ```apply (erule Fin_induct) ``` paulson@13221 ` 793` ```apply (simp add: lepoll_0_iff) ``` paulson@13216 ` 794` ```apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))") ``` paulson@13221 ` 795` ```apply simp ``` paulson@13221 ` 796` ```apply (blast dest!: cons_lepoll_consD, blast) ``` paulson@13216 ` 797` ```done ``` paulson@13216 ` 798` paulson@14883 ` 799` ```lemma Finite_imp_cardinal_cons [simp]: ``` paulson@46820 ` 800` ``` "[| Finite(A); a\A |] ==> |cons(a,A)| = succ(|A|)" ``` paulson@13216 ` 801` ```apply (unfold cardinal_def) ``` paulson@13216 ` 802` ```apply (rule Least_equality) ``` paulson@13216 ` 803` ```apply (fold cardinal_def) ``` paulson@13221 ` 804` ```apply (simp add: succ_def) ``` paulson@13216 ` 805` ```apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll ``` paulson@13216 ` 806` ``` elim!: mem_irrefl dest!: Finite_imp_well_ord) ``` paulson@13216 ` 807` ```apply (blast intro: Card_cardinal Card_is_Ord) ``` paulson@13216 ` 808` ```apply (rule notI) ``` paulson@13221 ` 809` ```apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE], ``` paulson@13221 ` 810` ``` assumption, assumption) ``` paulson@13216 ` 811` ```apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) ``` paulson@13216 ` 812` ```apply (erule le_imp_lepoll [THEN lepoll_trans]) ``` paulson@13216 ` 813` ```apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll] ``` paulson@13216 ` 814` ``` dest!: Finite_imp_well_ord) ``` paulson@13216 ` 815` ```done ``` paulson@13216 ` 816` paulson@13216 ` 817` paulson@13221 ` 818` ```lemma Finite_imp_succ_cardinal_Diff: ``` paulson@13221 ` 819` ``` "[| Finite(A); a:A |] ==> succ(|A-{a}|) = |A|" ``` paulson@13784 ` 820` ```apply (rule_tac b = A in cons_Diff [THEN subst], assumption) ``` paulson@13221 ` 821` ```apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite]) ``` paulson@13221 ` 822` ```apply (simp add: cons_Diff) ``` paulson@13216 ` 823` ```done ``` paulson@13216 ` 824` paulson@13216 ` 825` ```lemma Finite_imp_cardinal_Diff: "[| Finite(A); a:A |] ==> |A-{a}| < |A|" ``` paulson@13216 ` 826` ```apply (rule succ_leE) ``` paulson@13221 ` 827` ```apply (simp add: Finite_imp_succ_cardinal_Diff) ``` paulson@13216 ` 828` ```done ``` paulson@13216 ` 829` paulson@46820 ` 830` ```lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| \ nat" ``` paulson@14883 ` 831` ```apply (erule Finite_induct) ``` paulson@14883 ` 832` ```apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons) ``` paulson@14883 ` 833` ```done ``` paulson@13216 ` 834` paulson@14883 ` 835` ```lemma card_Un_Int: ``` paulson@46820 ` 836` ``` "[|Finite(A); Finite(B)|] ==> |A| #+ |B| = |A \ B| #+ |A \ B|" ``` paulson@46820 ` 837` ```apply (erule Finite_induct, simp) ``` paulson@14883 ` 838` ```apply (simp add: Finite_Int cons_absorb Un_cons Int_cons_left) ``` paulson@14883 ` 839` ```done ``` paulson@14883 ` 840` paulson@46820 ` 841` ```lemma card_Un_disjoint: ``` paulson@46820 ` 842` ``` "[|Finite(A); Finite(B); A \ B = 0|] ==> |A \ B| = |A| #+ |B|" ``` paulson@14883 ` 843` ```by (simp add: Finite_Un card_Un_Int) ``` paulson@14883 ` 844` paulson@14883 ` 845` ```lemma card_partition [rule_format]: ``` paulson@46820 ` 846` ``` "Finite(C) ==> ``` paulson@46820 ` 847` ``` Finite (\ C) \ ``` paulson@46820 ` 848` ``` (\c\C. |c| = k) \ ``` paulson@46820 ` 849` ``` (\c1 \ C. \c2 \ C. c1 \ c2 \ c1 \ c2 = 0) \ ``` paulson@14883 ` 850` ``` k #* |C| = |\ C|" ``` paulson@14883 ` 851` ```apply (erule Finite_induct, auto) ``` paulson@46820 ` 852` ```apply (subgoal_tac " x \ \B = 0") ``` paulson@14883 ` 853` ```apply (auto simp add: card_Un_disjoint Finite_Union ``` paulson@14883 ` 854` ``` subset_Finite [of _ "\ (cons(x,F))"]) ``` paulson@14883 ` 855` ```done ``` paulson@14883 ` 856` paulson@14883 ` 857` paulson@14883 ` 858` ```subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*} ``` paulson@13216 ` 859` wenzelm@45602 ` 860` ```lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel] ``` paulson@13216 ` 861` paulson@13216 ` 862` ```lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \ m #+ n" ``` paulson@13216 ` 863` ```apply (rule eqpoll_trans) ``` paulson@13216 ` 864` ```apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym]) ``` paulson@13216 ` 865` ```apply (erule nat_implies_well_ord)+ ``` paulson@13221 ` 866` ```apply (simp add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl) ``` paulson@13216 ` 867` ```done ``` paulson@13216 ` 868` paulson@46820 ` 869` ```lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \ nat \ i \ nat | i=nat" ``` paulson@13221 ` 870` ```apply (erule trans_induct3, auto) ``` paulson@13216 ` 871` ```apply (blast dest!: nat_le_Limit [THEN le_imp_subset]) ``` paulson@13216 ` 872` ```done ``` paulson@13216 ` 873` paulson@46820 ` 874` ```lemma Ord_nat_subset_into_Card: "[| Ord(i); i \ nat |] ==> Card(i)" ``` paulson@13221 ` 875` ```by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card) ``` paulson@13216 ` 876` paulson@13216 ` 877` ```lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1" ``` paulson@13216 ` 878` ```apply (rule succ_inject) ``` paulson@13216 ` 879` ```apply (rule_tac b = "|A|" in trans) ``` paulson@13615 ` 880` ``` apply (simp add: Finite_imp_succ_cardinal_Diff) ``` paulson@13216 ` 881` ```apply (subgoal_tac "1 \ A") ``` paulson@13221 ` 882` ``` prefer 2 apply (blast intro: not_0_is_lepoll_1) ``` paulson@13221 ` 883` ```apply (frule Finite_imp_well_ord, clarify) ``` paulson@13216 ` 884` ```apply (drule well_ord_lepoll_imp_Card_le) ``` paulson@13615 ` 885` ``` apply (auto simp add: cardinal_1) ``` paulson@13216 ` 886` ```apply (rule trans) ``` paulson@13615 ` 887` ``` apply (rule_tac [2] diff_succ) ``` paulson@13615 ` 888` ``` apply (auto simp add: Finite_cardinal_in_nat) ``` paulson@13216 ` 889` ```done ``` paulson@13216 ` 890` paulson@13221 ` 891` ```lemma cardinal_lt_imp_Diff_not_0 [rule_format]: ``` paulson@46820 ` 892` ``` "Finite(B) ==> \A. |B|<|A| \ A - B \ 0" ``` paulson@13221 ` 893` ```apply (erule Finite_induct, auto) ``` paulson@13221 ` 894` ```apply (case_tac "Finite (A)") ``` paulson@13221 ` 895` ``` apply (subgoal_tac [2] "Finite (cons (x, B))") ``` paulson@13221 ` 896` ``` apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite) ``` paulson@13221 ` 897` ``` apply (auto simp add: Finite_0 Finite_cons) ``` paulson@13216 ` 898` ```apply (subgoal_tac "|B|<|A|") ``` paulson@13221 ` 899` ``` prefer 2 apply (blast intro: lt_trans Ord_cardinal) ``` paulson@13216 ` 900` ```apply (case_tac "x:A") ``` paulson@13221 ` 901` ``` apply (subgoal_tac [2] "A - cons (x, B) = A - B") ``` paulson@13221 ` 902` ``` apply auto ``` paulson@46820 ` 903` ```apply (subgoal_tac "|A| \ |cons (x, B) |") ``` paulson@13221 ` 904` ``` prefer 2 ``` paulson@46820 ` 905` ``` apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] ``` paulson@13216 ` 906` ``` intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll) ``` paulson@13216 ` 907` ```apply (auto simp add: Finite_imp_cardinal_cons) ``` paulson@13216 ` 908` ```apply (auto dest!: Finite_cardinal_in_nat simp add: le_iff) ``` paulson@13216 ` 909` ```apply (blast intro: lt_trans) ``` paulson@13216 ` 910` ```done ``` paulson@13216 ` 911` lcp@437 ` 912` ```end ```