# Theory CardinalArith

Up to index of Isabelle/ZF

theory CardinalArith
imports ArithSimp
`(*  Title:      ZF/CardinalArith.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1994  University of Cambridge*)header{*Cardinal Arithmetic Without the Axiom of Choice*}theory CardinalArith imports Cardinal OrderArith ArithSimp Finite begindefinition  InfCard       :: "i=>o"  where    "InfCard(i) == Card(i) & nat ≤ i"definition  cmult         :: "[i,i]=>i"       (infixl "|*|" 70)  where    "i |*| j == |i*j|"definition  cadd          :: "[i,i]=>i"       (infixl "|+|" 65)  where    "i |+| j == |i+j|"definition  csquare_rel   :: "i=>i"  where    "csquare_rel(K) ==          rvimage(K*K,                  lam <x,y>:K*K. <x ∪ y, x, y>,                  rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"definition  jump_cardinal :: "i=>i"  where    --{*This def is more complex than Kunen's but it more easily proved to        be a cardinal*}    "jump_cardinal(K) ==         \<Union>X∈Pow(K). {z. r ∈ Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"definition  csucc         :: "i=>i"  where    --{*needed because @{term "jump_cardinal(K)"} might not be the successor        of @{term K}*}    "csucc(K) == LEAST L. Card(L) & K<L"notation (xsymbols)  cadd  (infixl "⊕" 65) and  cmult  (infixl "⊗" 70)notation (HTML)  cadd  (infixl "⊕" 65) and  cmult  (infixl "⊗" 70)lemma Card_Union [simp,intro,TC]:  assumes A: "!!x. x∈A ==> Card(x)" shows "Card(\<Union>(A))"proof (rule CardI)  show "Ord(\<Union>A)" using A    by (simp add: Card_is_Ord)next  fix j  assume j: "j < \<Union>A"  hence "∃c∈A. j < c & Card(c)" using A    by (auto simp add: lt_def intro: Card_is_Ord)  then obtain c where c: "c∈A" "j < c" "Card(c)"    by blast  hence jls: "j \<prec> c"    by (simp add: lt_Card_imp_lesspoll)  { assume eqp: "j ≈ \<Union>A"    have  "c \<lesssim> \<Union>A" using c      by (blast intro: subset_imp_lepoll)    also have "... ≈ j"  by (rule eqpoll_sym [OF eqp])    also have "... \<prec> c"  by (rule jls)    finally have "c \<prec> c" .    hence False      by auto  } thus "¬ j ≈ \<Union>A" by blastqedlemma Card_UN: "(!!x. x ∈ A ==> Card(K(x))) ==> Card(\<Union>x∈A. K(x))"  by blastlemma Card_OUN [simp,intro,TC]:     "(!!x. x ∈ A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"  by (auto simp add: OUnion_def Card_0)lemma in_Card_imp_lesspoll: "[| Card(K); b ∈ K |] ==> b \<prec> K"apply (unfold lesspoll_def)apply (simp add: Card_iff_initial)apply (fast intro!: le_imp_lepoll ltI leI)donesubsection{*Cardinal addition*}text{*Note: Could omit proving the algebraic laws for cardinal addition andmultiplication.  On finite cardinals these operations coincide withaddition and multiplication of natural numbers; on infinite cardinals theycoincide with union (maximum).  Either way we get most laws for free.*}subsubsection{*Cardinal addition is commutative*}lemma sum_commute_eqpoll: "A+B ≈ B+A"proof (unfold eqpoll_def, rule exI)  show "(λz∈A+B. case(Inr,Inl,z)) ∈ bij(A+B, B+A)"    by (auto intro: lam_bijective [where d = "case(Inr,Inl)"])qedlemma cadd_commute: "i ⊕ j = j ⊕ i"apply (unfold cadd_def)apply (rule sum_commute_eqpoll [THEN cardinal_cong])donesubsubsection{*Cardinal addition is associative*}lemma sum_assoc_eqpoll: "(A+B)+C ≈ A+(B+C)"apply (unfold eqpoll_def)apply (rule exI)apply (rule sum_assoc_bij)donetext{*Unconditional version requires AC*}lemma well_ord_cadd_assoc:  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"  shows "(i ⊕ j) ⊕ k = i ⊕ (j ⊕ k)"proof (unfold cadd_def, rule cardinal_cong)  have "|i + j| + k ≈ (i + j) + k"    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j)  also have "...  ≈ i + (j + k)"    by (rule sum_assoc_eqpoll)  also have "...  ≈ i + |j + k|"    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym)  finally show "|i + j| + k ≈ i + |j + k|" .qedsubsubsection{*0 is the identity for addition*}lemma sum_0_eqpoll: "0+A ≈ A"apply (unfold eqpoll_def)apply (rule exI)apply (rule bij_0_sum)donelemma cadd_0 [simp]: "Card(K) ==> 0 ⊕ K = K"apply (unfold cadd_def)apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)donesubsubsection{*Addition by another cardinal*}lemma sum_lepoll_self: "A \<lesssim> A+B"proof (unfold lepoll_def, rule exI)  show "(λx∈A. Inl (x)) ∈ inj(A, A + B)"    by (simp add: inj_def)qed(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)lemma cadd_le_self:  assumes K: "Card(K)" and L: "Ord(L)" shows "K ≤ (K ⊕ L)"proof (unfold cadd_def)  have "K ≤ |K|"    by (rule Card_cardinal_le [OF K])  moreover have "|K| ≤ |K + L|" using K L    by (blast intro: well_ord_lepoll_imp_Card_le sum_lepoll_self                     well_ord_radd well_ord_Memrel Card_is_Ord)  ultimately show "K ≤ |K + L|"    by (blast intro: le_trans)qedsubsubsection{*Monotonicity of addition*}lemma sum_lepoll_mono:     "[| A \<lesssim> C;  B \<lesssim> D |] ==> A + B \<lesssim> C + D"apply (unfold lepoll_def)apply (elim exE)apply (rule_tac x = "λz∈A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI)apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) ` y))"       in lam_injective)apply (typecheck add: inj_is_fun, auto)donelemma cadd_le_mono:    "[| K' ≤ K;  L' ≤ L |] ==> (K' ⊕ L') ≤ (K ⊕ L)"apply (unfold cadd_def)apply (safe dest!: le_subset_iff [THEN iffD1])apply (rule well_ord_lepoll_imp_Card_le)apply (blast intro: well_ord_radd well_ord_Memrel)apply (blast intro: sum_lepoll_mono subset_imp_lepoll)donesubsubsection{*Addition of finite cardinals is "ordinary" addition*}lemma sum_succ_eqpoll: "succ(A)+B ≈ succ(A+B)"apply (unfold eqpoll_def)apply (rule exI)apply (rule_tac c = "%z. if z=Inl (A) then A+B else z"            and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective)   apply simp_allapply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+done(*Pulling the  succ(...)  outside the |...| requires m, n ∈ nat  *)(*Unconditional version requires AC*)lemma cadd_succ_lemma:  assumes "Ord(m)" "Ord(n)" shows "succ(m) ⊕ n = |succ(m ⊕ n)|"proof (unfold cadd_def)  have [intro]: "m + n ≈ |m + n|" using assms    by (blast intro: eqpoll_sym well_ord_cardinal_eqpoll well_ord_radd well_ord_Memrel)  have "|succ(m) + n| = |succ(m + n)|"    by (rule sum_succ_eqpoll [THEN cardinal_cong])  also have "... = |succ(|m + n|)|"    by (blast intro: succ_eqpoll_cong cardinal_cong)  finally show "|succ(m) + n| = |succ(|m + n|)|" .qedlemma nat_cadd_eq_add:  assumes m: "m ∈ nat" and [simp]: "n ∈ nat" shows"m ⊕ n = m #+ n"using mproof (induct m)  case 0 thus ?case by (simp add: nat_into_Card cadd_0)next  case (succ m) thus ?case by (simp add: cadd_succ_lemma nat_into_Card Card_cardinal_eq)qedsubsection{*Cardinal multiplication*}subsubsection{*Cardinal multiplication is commutative*}lemma prod_commute_eqpoll: "A*B ≈ B*A"apply (unfold eqpoll_def)apply (rule exI)apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective,       auto)donelemma cmult_commute: "i ⊗ j = j ⊗ i"apply (unfold cmult_def)apply (rule prod_commute_eqpoll [THEN cardinal_cong])donesubsubsection{*Cardinal multiplication is associative*}lemma prod_assoc_eqpoll: "(A*B)*C ≈ A*(B*C)"apply (unfold eqpoll_def)apply (rule exI)apply (rule prod_assoc_bij)donetext{*Unconditional version requires AC*}lemma well_ord_cmult_assoc:  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"  shows "(i ⊗ j) ⊗ k = i ⊗ (j ⊗ k)"proof (unfold cmult_def, rule cardinal_cong)  have "|i * j| * k ≈ (i * j) * k"    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j)  also have "...  ≈ i * (j * k)"    by (rule prod_assoc_eqpoll)  also have "...  ≈ i * |j * k|"    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym)  finally show "|i * j| * k ≈ i * |j * k|" .qedsubsubsection{*Cardinal multiplication distributes over addition*}lemma sum_prod_distrib_eqpoll: "(A+B)*C ≈ (A*C)+(B*C)"apply (unfold eqpoll_def)apply (rule exI)apply (rule sum_prod_distrib_bij)donelemma well_ord_cadd_cmult_distrib:  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"  shows "(i ⊕ j) ⊗ k = (i ⊗ k) ⊕ (j ⊗ k)"proof (unfold cadd_def cmult_def, rule cardinal_cong)  have "|i + j| * k ≈ (i + j) * k"    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j)  also have "...  ≈ i * k + j * k"    by (rule sum_prod_distrib_eqpoll)  also have "...  ≈ |i * k| + |j * k|"    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym)  finally show "|i + j| * k ≈ |i * k| + |j * k|" .qedsubsubsection{*Multiplication by 0 yields 0*}lemma prod_0_eqpoll: "0*A ≈ 0"apply (unfold eqpoll_def)apply (rule exI)apply (rule lam_bijective, safe)donelemma cmult_0 [simp]: "0 ⊗ i = 0"by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])subsubsection{*1 is the identity for multiplication*}lemma prod_singleton_eqpoll: "{x}*A ≈ A"apply (unfold eqpoll_def)apply (rule exI)apply (rule singleton_prod_bij [THEN bij_converse_bij])donelemma cmult_1 [simp]: "Card(K) ==> 1 ⊗ K = K"apply (unfold cmult_def succ_def)apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)donesubsection{*Some inequalities for multiplication*}lemma prod_square_lepoll: "A \<lesssim> A*A"apply (unfold lepoll_def inj_def)apply (rule_tac x = "λx∈A. <x,x>" in exI, simp)done(*Could probably weaken the premise to well_ord(K,r), or remove using AC*)lemma cmult_square_le: "Card(K) ==> K ≤ K ⊗ K"apply (unfold cmult_def)apply (rule le_trans)apply (rule_tac [2] well_ord_lepoll_imp_Card_le)apply (rule_tac [3] prod_square_lepoll)apply (simp add: le_refl Card_is_Ord Card_cardinal_eq)apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)donesubsubsection{*Multiplication by a non-zero cardinal*}lemma prod_lepoll_self: "b ∈ B ==> A \<lesssim> A*B"apply (unfold lepoll_def inj_def)apply (rule_tac x = "λx∈A. <x,b>" in exI, simp)done(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)lemma cmult_le_self:    "[| Card(K);  Ord(L);  0<L |] ==> K ≤ (K ⊗ L)"apply (unfold cmult_def)apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])  apply assumption apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)apply (blast intro: prod_lepoll_self ltD)donesubsubsection{*Monotonicity of multiplication*}lemma prod_lepoll_mono:     "[| A \<lesssim> C;  B \<lesssim> D |] ==> A * B  \<lesssim>  C * D"apply (unfold lepoll_def)apply (elim exE)apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI)apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>"       in lam_injective)apply (typecheck add: inj_is_fun, auto)donelemma cmult_le_mono:    "[| K' ≤ K;  L' ≤ L |] ==> (K' ⊗ L') ≤ (K ⊗ L)"apply (unfold cmult_def)apply (safe dest!: le_subset_iff [THEN iffD1])apply (rule well_ord_lepoll_imp_Card_le) apply (blast intro: well_ord_rmult well_ord_Memrel)apply (blast intro: prod_lepoll_mono subset_imp_lepoll)donesubsection{*Multiplication of finite cardinals is "ordinary" multiplication*}lemma prod_succ_eqpoll: "succ(A)*B ≈ B + A*B"apply (unfold eqpoll_def)apply (rule exI)apply (rule_tac c = "%<x,y>. if x=A then Inl (y) else Inr (<x,y>)"            and d = "case (%y. <A,y>, %z. z)" in lam_bijective)apply safeapply (simp_all add: succI2 if_type mem_imp_not_eq)done(*Unconditional version requires AC*)lemma cmult_succ_lemma:    "[| Ord(m);  Ord(n) |] ==> succ(m) ⊗ n = n ⊕ (m ⊗ n)"apply (unfold cmult_def cadd_def)apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])apply (rule cardinal_cong [symmetric])apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])apply (blast intro: well_ord_rmult well_ord_Memrel)donelemma nat_cmult_eq_mult: "[| m ∈ nat;  n ∈ nat |] ==> m ⊗ n = m#*n"apply (induct_tac m)apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add)donelemma cmult_2: "Card(n) ==> 2 ⊗ n = n ⊕ n"by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])lemma sum_lepoll_prod:  assumes C: "2 \<lesssim> C" shows "B+B \<lesssim> C*B"proof -  have "B+B \<lesssim> 2*B"    by (simp add: sum_eq_2_times)  also have "... \<lesssim> C*B"    by (blast intro: prod_lepoll_mono lepoll_refl C)  finally show "B+B \<lesssim> C*B" .qedlemma lepoll_imp_sum_lepoll_prod: "[| A \<lesssim> B; 2 \<lesssim> A |] ==> A+B \<lesssim> A*B"by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)subsection{*Infinite Cardinals are Limit Ordinals*}(*This proof is modelled upon one assuming nat<=A, with injection  λz∈cons(u,A). if z=u then 0 else if z ∈ nat then succ(z) else z  and inverse %y. if y ∈ nat then nat_case(u, %z. z, y) else y.  \  If f ∈ inj(nat,A) then range(f) behaves like the natural numbers.*)lemma nat_cons_lepoll: "nat \<lesssim> A ==> cons(u,A) \<lesssim> A"apply (unfold lepoll_def)apply (erule exE)apply (rule_tac x =          "λz∈cons (u,A).             if z=u then f`0             else if z ∈ range (f) then f`succ (converse (f) `z) else z"       in exI)apply (rule_tac d =          "%y. if y ∈ range(f) then nat_case (u, %z. f`z, converse(f) `y)                              else y"       in lam_injective)apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun)apply (simp add: inj_is_fun [THEN apply_rangeI]                 inj_converse_fun [THEN apply_rangeI]                 inj_converse_fun [THEN apply_funtype])donelemma nat_cons_eqpoll: "nat \<lesssim> A ==> cons(u,A) ≈ A"apply (erule nat_cons_lepoll [THEN eqpollI])apply (rule subset_consI [THEN subset_imp_lepoll])done(*Specialized version required below*)lemma nat_succ_eqpoll: "nat ⊆ A ==> succ(A) ≈ A"apply (unfold succ_def)apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll])donelemma InfCard_nat: "InfCard(nat)"apply (unfold InfCard_def)apply (blast intro: Card_nat le_refl Card_is_Ord)donelemma InfCard_is_Card: "InfCard(K) ==> Card(K)"apply (unfold InfCard_def)apply (erule conjunct1)donelemma InfCard_Un:    "[| InfCard(K);  Card(L) |] ==> InfCard(K ∪ L)"apply (unfold InfCard_def)apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans]  Card_is_Ord)done(*Kunen's Lemma 10.11*)lemma InfCard_is_Limit: "InfCard(K) ==> Limit(K)"apply (unfold InfCard_def)apply (erule conjE)apply (frule Card_is_Ord)apply (rule ltI [THEN non_succ_LimitI])apply (erule le_imp_subset [THEN subsetD])apply (safe dest!: Limit_nat [THEN Limit_le_succD])apply (unfold Card_def)apply (drule trans)apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong])apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl])apply (rule le_eqI, assumption)apply (rule Ord_cardinal)done(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)(*A general fact about ordermap*)lemma ordermap_eqpoll_pred:    "[| well_ord(A,r);  x ∈ A |] ==> ordermap(A,r)`x ≈ Order.pred(A,x,r)"apply (unfold eqpoll_def)apply (rule exI)apply (simp add: ordermap_eq_image well_ord_is_wf)apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij,                           THEN bij_converse_bij])apply (rule pred_subset)donesubsubsection{*Establishing the well-ordering*}lemma well_ord_csquare:  assumes K: "Ord(K)" shows "well_ord(K*K, csquare_rel(K))"proof (unfold csquare_rel_def, rule well_ord_rvimage)  show "(λ⟨x,y⟩∈K × K. ⟨x ∪ y, x, y⟩) ∈ inj(K × K, K × K × K)" using K    by (force simp add: inj_def intro: lam_type Un_least_lt [THEN ltD] ltI)next  show "well_ord(K × K × K, rmult(K, Memrel(K), K × K, rmult(K, Memrel(K), K, Memrel(K))))"    using K by (blast intro: well_ord_rmult well_ord_Memrel)qedsubsubsection{*Characterising initial segments of the well-ordering*}lemma csquareD: "[| <<x,y>, <z,z>> ∈ csquare_rel(K);  x<K;  y<K;  z<K |] ==> x ≤ z & y ≤ z"apply (unfold csquare_rel_def)apply (erule rev_mp)apply (elim ltE)apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le)apply (simp_all add: lt_def succI2)donelemma pred_csquare_subset:    "z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) ⊆ succ(z)*succ(z)"apply (unfold Order.pred_def)apply (safe del: SigmaI dest!: csquareD)apply (unfold lt_def, auto)donelemma csquare_ltI: "[| x<z;  y<z;  z<K |] ==>  <<x,y>, <z,z>> ∈ csquare_rel(K)"apply (unfold csquare_rel_def)apply (subgoal_tac "x<K & y<K") prefer 2 apply (blast intro: lt_trans)apply (elim ltE)apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)done(*Part of the traditional proof.  UNUSED since it's harder to prove & apply *)lemma csquare_or_eqI: "[| x ≤ z;  y ≤ z;  z<K |] ==> <<x,y>, <z,z>> ∈ csquare_rel(K) | x=z & y=z"apply (unfold csquare_rel_def)apply (subgoal_tac "x<K & y<K") prefer 2 apply (blast intro: lt_trans1)apply (elim ltE)apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)apply (elim succE)apply (simp_all add: subset_Un_iff [THEN iff_sym]                     subset_Un_iff2 [THEN iff_sym] OrdmemD)donesubsubsection{*The cardinality of initial segments*}lemma ordermap_z_lt:      "[| Limit(K);  x<K;  y<K;  z=succ(x ∪ y) |] ==>          ordermap(K*K, csquare_rel(K)) ` <x,y> <          ordermap(K*K, csquare_rel(K)) ` <z,z>"apply (subgoal_tac "z<K & well_ord (K*K, csquare_rel (K))")prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ                              Limit_is_Ord [THEN well_ord_csquare], clarify)apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI])apply (erule_tac [4] well_ord_is_wf)apply (blast intro!: Un_upper1_le Un_upper2_le Ord_ordermap elim!: ltE)+donetext{*Kunen: "each @{term"⟨x,y⟩ ∈ K × K"} has no more than @{term"z × z"} predecessors..." (page 29) *}lemma ordermap_csquare_le:  assumes K: "Limit(K)" and x: "x<K" and y: " y<K"  defines "z ≡ succ(x ∪ y)"  shows "|ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩| ≤ |succ(z)| ⊗ |succ(z)|"proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)  show "well_ord(|succ(z)| × |succ(z)|,                 rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"    by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult)next  have zK: "z<K" using x y K z_def    by (blast intro: Un_least_lt Limit_has_succ)  hence oz: "Ord(z)" by (elim ltE)  have "ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩ \<lesssim> ordermap(K × K, csquare_rel(K)) ` ⟨z,z⟩"    using z_def    by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y)  also have "... ≈  Order.pred(K × K, ⟨z,z⟩, csquare_rel(K))"    proof (rule ordermap_eqpoll_pred)      show "well_ord(K × K, csquare_rel(K))" using K        by (rule Limit_is_Ord [THEN well_ord_csquare])    next      show "⟨z, z⟩ ∈ K × K" using zK        by (blast intro: ltD)    qed  also have "...  \<lesssim> succ(z) × succ(z)" using zK    by (rule pred_csquare_subset [THEN subset_imp_lepoll])  also have "... ≈ |succ(z)| × |succ(z)|" using oz    by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym)  finally show "ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩ \<lesssim> |succ(z)| × |succ(z)|" .qedtext{*Kunen: "... so the order type is @{text"≤"} K" *}lemma ordertype_csquare_le:  assumes IK: "InfCard(K)" and eq: "!!y. y∈K ==> InfCard(y) ==> y ⊗ y = y"  shows "ordertype(K*K, csquare_rel(K)) ≤ K"proof -  have  CK: "Card(K)" using IK by (rule InfCard_is_Card)  hence OK: "Ord(K)"  by (rule Card_is_Ord)  moreover have "Ord(ordertype(K × K, csquare_rel(K)))" using OK    by (rule well_ord_csquare [THEN Ord_ordertype])  ultimately show ?thesis  proof (rule all_lt_imp_le)    fix i    assume i: "i < ordertype(K × K, csquare_rel(K))"    hence Oi: "Ord(i)" by (elim ltE)    obtain x y where x: "x ∈ K" and y: "y ∈ K"                 and ieq: "i = ordermap(K × K, csquare_rel(K)) ` ⟨x,y⟩"      using i by (auto simp add: ordertype_unfold elim: ltE)    hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK      by (blast intro: Ord_in_Ord ltI)+    hence ou: "Ord(x ∪ y)"      by (simp add: Ord_Un)    show "i < K"      proof (rule Card_lt_imp_lt [OF _ Oi CK])        have "|i| ≤ |succ(succ(x ∪ y))| ⊗ |succ(succ(x ∪ y))|" using IK xy          by (auto simp add: ieq intro: InfCard_is_Limit [THEN ordermap_csquare_le])        moreover have "|succ(succ(x ∪ y))| ⊗ |succ(succ(x ∪ y))| < K"          proof (cases rule: Ord_linear2 [OF ou Ord_nat])            assume "x ∪ y < nat"            hence "|succ(succ(x ∪ y))| ⊗ |succ(succ(x ∪ y))| ∈ nat"              by (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type                         nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)            also have "... ⊆ K" using IK              by (simp add: InfCard_def le_imp_subset)            finally show "|succ(succ(x ∪ y))| ⊗ |succ(succ(x ∪ y))| < K"              by (simp add: ltI OK)          next            assume natxy: "nat ≤ x ∪ y"            hence seq: "|succ(succ(x ∪ y))| = |x ∪ y|" using xy              by (simp add: le_imp_subset nat_succ_eqpoll [THEN cardinal_cong] le_succ_iff)            also have "... < K" using xy              by (simp add: Un_least_lt Ord_cardinal_le [THEN lt_trans1])            finally have "|succ(succ(x ∪ y))| < K" .            moreover have "InfCard(|succ(succ(x ∪ y))|)" using xy natxy              by (simp add: seq InfCard_def Card_cardinal nat_le_cardinal)            ultimately show ?thesis  by (simp add: eq ltD)          qed        ultimately show "|i| < K" by (blast intro: lt_trans1)    qed  qedqed(*Main result: Kunen's Theorem 10.12*)lemma InfCard_csquare_eq:  assumes IK: "InfCard(K)" shows "InfCard(K) ==> K ⊗ K = K"proof -  have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card)  show "InfCard(K) ==> K ⊗ K = K" using OK  proof (induct rule: trans_induct)    case (step i)    show "i ⊗ i = i"    proof (rule le_anti_sym)      have "|i × i| = |ordertype(i × i, csquare_rel(i))|"        by (rule cardinal_cong,          simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])      hence "i ⊗ i ≤ ordertype(i × i, csquare_rel(i))"        by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])      moreover      have "ordertype(i × i, csquare_rel(i)) ≤ i" using step        by (simp add: ordertype_csquare_le)      ultimately show "i ⊗ i ≤ i" by (rule le_trans)    next      show "i ≤ i ⊗ i" using step        by (blast intro: cmult_square_le InfCard_is_Card)    qed  qedqed(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)lemma well_ord_InfCard_square_eq:  assumes r: "well_ord(A,r)" and I: "InfCard(|A|)" shows "A × A ≈ A"proof -  have "A × A ≈ |A| × |A|"    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_sym r)  also have "... ≈ A"    proof (rule well_ord_cardinal_eqE [OF _ r])      show "well_ord(|A| × |A|, rmult(|A|, Memrel(|A|), |A|, Memrel(|A|)))"        by (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel r)    next      show "||A| × |A|| = |A|" using InfCard_csquare_eq I        by (simp add: cmult_def)    qed  finally show ?thesis .qedlemma InfCard_square_eqpoll: "InfCard(K) ==> K × K ≈ K"apply (rule well_ord_InfCard_square_eq) apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel])apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq])donelemma Inf_Card_is_InfCard: "[| Card(i); ~ Finite(i) |] ==> InfCard(i)"by (simp add: InfCard_def Card_is_Ord [THEN nat_le_infinite_Ord])subsubsection{*Toward's Kunen's Corollary 10.13 (1)*}lemma InfCard_le_cmult_eq: "[| InfCard(K);  L ≤ K;  0<L |] ==> K ⊗ L = K"apply (rule le_anti_sym) prefer 2 apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card)apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl])apply (rule cmult_le_mono [THEN le_trans], assumption+)apply (simp add: InfCard_csquare_eq)done(*Corollary 10.13 (1), for cardinal multiplication*)lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K ⊗ L = K ∪ L"apply (rule_tac i = K and j = L in Ord_linear_le)apply (typecheck add: InfCard_is_Card Card_is_Ord)apply (rule cmult_commute [THEN ssubst])apply (rule Un_commute [THEN ssubst])apply (simp_all add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq                     subset_Un_iff2 [THEN iffD1] le_imp_subset)donelemma InfCard_cdouble_eq: "InfCard(K) ==> K ⊕ K = K"apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)done(*Corollary 10.13 (1), for cardinal addition*)lemma InfCard_le_cadd_eq: "[| InfCard(K);  L ≤ K |] ==> K ⊕ L = K"apply (rule le_anti_sym) prefer 2 apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card)apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl])apply (rule cadd_le_mono [THEN le_trans], assumption+)apply (simp add: InfCard_cdouble_eq)donelemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K ⊕ L = K ∪ L"apply (rule_tac i = K and j = L in Ord_linear_le)apply (typecheck add: InfCard_is_Card Card_is_Ord)apply (rule cadd_commute [THEN ssubst])apply (rule Un_commute [THEN ssubst])apply (simp_all add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)done(*The other part, Corollary 10.13 (2), refers to the cardinality of the set  of all n-tuples of elements of K.  A better version for the Isabelle theory  might be  InfCard(K) ==> |list(K)| = K.*)subsection{*For Every Cardinal Number There Exists A Greater One*}text{*This result is Kunen's Theorem 10.16, which would be trivial using AC*}lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))"apply (unfold jump_cardinal_def)apply (rule Ord_is_Transset [THEN [2] OrdI]) prefer 2 apply (blast intro!: Ord_ordertype)apply (unfold Transset_def)apply (safe del: subsetI)apply (simp add: ordertype_pred_unfold, safe)apply (rule UN_I)apply (rule_tac [2] ReplaceI)   prefer 4 apply (blast intro: well_ord_subset elim!: predE)+done(*Allows selective unfolding.  Less work than deriving intro/elim rules*)lemma jump_cardinal_iff:     "i ∈ jump_cardinal(K) <->      (∃r X. r ⊆ K*K & X ⊆ K & well_ord(X,r) & i = ordertype(X,r))"apply (unfold jump_cardinal_def)apply (blast del: subsetI)done(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*)lemma K_lt_jump_cardinal: "Ord(K) ==> K < jump_cardinal(K)"apply (rule Ord_jump_cardinal [THEN [2] ltI])apply (rule jump_cardinal_iff [THEN iffD2])apply (rule_tac x="Memrel(K)" in exI)apply (rule_tac x=K in exI)apply (simp add: ordertype_Memrel well_ord_Memrel)apply (simp add: Memrel_def subset_iff)done(*The proof by contradiction: the bijection f yields a wellordering of X  whose ordertype is jump_cardinal(K).  *)lemma Card_jump_cardinal_lemma:     "[| well_ord(X,r);  r ⊆ K * K;  X ⊆ K;         f ∈ bij(ordertype(X,r), jump_cardinal(K)) |]      ==> jump_cardinal(K) ∈ jump_cardinal(K)"apply (subgoal_tac "f O ordermap (X,r) ∈ bij (X, jump_cardinal (K))") prefer 2 apply (blast intro: comp_bij ordermap_bij)apply (rule jump_cardinal_iff [THEN iffD2])apply (intro exI conjI)apply (rule subset_trans [OF rvimage_type Sigma_mono], assumption+)apply (erule bij_is_inj [THEN well_ord_rvimage])apply (rule Ord_jump_cardinal [THEN well_ord_Memrel])apply (simp add: well_ord_Memrel [THEN [2] bij_ordertype_vimage]                 ordertype_Memrel Ord_jump_cardinal)done(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*)lemma Card_jump_cardinal: "Card(jump_cardinal(K))"apply (rule Ord_jump_cardinal [THEN CardI])apply (unfold eqpoll_def)apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1])apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl])donesubsection{*Basic Properties of Successor Cardinals*}lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)"apply (unfold csucc_def)apply (rule LeastI)apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+donelemmas Card_csucc = csucc_basic [THEN conjunct1]lemmas lt_csucc = csucc_basic [THEN conjunct2]lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)"by (blast intro: Ord_0_le lt_csucc lt_trans1)lemma csucc_le: "[| Card(L);  K<L |] ==> csucc(K) ≤ L"apply (unfold csucc_def)apply (rule Least_le)apply (blast intro: Card_is_Ord)+donelemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| ≤ K"apply (rule iffI)apply (rule_tac [2] Card_lt_imp_lt)apply (erule_tac [2] lt_trans1)apply (simp_all add: lt_csucc Card_csucc Card_is_Ord)apply (rule notI [THEN not_lt_imp_le])apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl], assumption)apply (rule Ord_cardinal_le [THEN lt_trans1])apply (simp_all add: Ord_cardinal Card_is_Ord)donelemma Card_lt_csucc_iff:     "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' ≤ K"by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))"by (simp add: InfCard_def Card_csucc Card_is_Ord              lt_csucc [THEN leI, THEN [2] le_trans])subsubsection{*Removing elements from a finite set decreases its cardinality*}lemma Finite_imp_cardinal_cons [simp]:  assumes FA: "Finite(A)" and a: "a∉A" shows "|cons(a,A)| = succ(|A|)"proof -  { fix X    have "Finite(X) ==> a ∉ X ==> cons(a,X) \<lesssim> X ==> False"      proof (induct X rule: Finite_induct)        case 0 thus False  by (simp add: lepoll_0_iff)      next        case (cons x Y)        hence "cons(x, cons(a, Y)) \<lesssim> cons(x, Y)" by (simp add: cons_commute)        hence "cons(a, Y) \<lesssim> Y" using cons        by (blast dest: cons_lepoll_consD)        thus False using cons by auto      qed  }  hence [simp]: "~ cons(a,A) \<lesssim> A" using a FA by auto  have [simp]: "|A| ≈ A" using Finite_imp_well_ord [OF FA]    by (blast intro: well_ord_cardinal_eqpoll)  have "(μ i. i ≈ cons(a, A)) = succ(|A|)"    proof (rule Least_equality [OF _ _ notI])      show "succ(|A|) ≈ cons(a, A)"        by (simp add: succ_def cons_eqpoll_cong mem_not_refl a)    next      show "Ord(succ(|A|))" by simp    next      fix i      assume i: "i ≤ |A|" "i ≈ cons(a, A)"      have "cons(a, A) ≈ i" by (rule eqpoll_sym) (rule i)      also have "... \<lesssim> |A|" by (rule le_imp_lepoll) (rule i)      also have "... ≈ A"   by simp      finally have "cons(a, A) \<lesssim> A" .      thus False by simp    qed  thus ?thesis by (simp add: cardinal_def)qedlemma Finite_imp_succ_cardinal_Diff:     "[| Finite(A);  a ∈ A |] ==> succ(|A-{a}|) = |A|"apply (rule_tac b = A in cons_Diff [THEN subst], assumption)apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])apply (simp add: cons_Diff)donelemma Finite_imp_cardinal_Diff: "[| Finite(A);  a ∈ A |] ==> |A-{a}| < |A|"apply (rule succ_leE)apply (simp add: Finite_imp_succ_cardinal_Diff)donelemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| ∈ nat"proof (induct rule: Finite_induct)  case 0 thus ?case by (simp add: cardinal_0)next  case (cons x A) thus ?case by (simp add: Finite_imp_cardinal_cons)qedlemma card_Un_Int:     "[|Finite(A); Finite(B)|] ==> |A| #+ |B| = |A ∪ B| #+ |A ∩ B|"apply (erule Finite_induct, simp)apply (simp add: Finite_Int cons_absorb Un_cons Int_cons_left)donelemma card_Un_disjoint:     "[|Finite(A); Finite(B); A ∩ B = 0|] ==> |A ∪ B| = |A| #+ |B|"by (simp add: Finite_Un card_Un_Int)lemma card_partition:  assumes FC: "Finite(C)"  shows     "Finite (\<Union> C) ==>        (∀c∈C. |c| = k) ==>        (∀c1 ∈ C. ∀c2 ∈ C. c1 ≠ c2 --> c1 ∩ c2 = 0) ==>        k #* |C| = |\<Union> C|"using FCproof (induct rule: Finite_induct)  case 0 thus ?case by simpnext  case (cons x B)  hence "x ∩ \<Union>B = 0" by auto  thus ?case using cons    by (auto simp add: card_Un_disjoint)qedsubsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*}lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel]lemma nat_sum_eqpoll_sum:  assumes m: "m ∈ nat" and n: "n ∈ nat" shows "m + n ≈ m #+ n"proof -  have "m + n ≈ |m+n|" using m n    by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_eqpoll eqpoll_sym)  also have "... = m #+ n" using m n    by (simp add: nat_cadd_eq_add [symmetric] cadd_def)  finally show ?thesis .qedlemma Ord_subset_natD [rule_format]: "Ord(i) ==> i ⊆ nat ==> i ∈ nat | i=nat"proof (induct i rule: trans_induct3)  case 0 thus ?case by autonext  case (succ i) thus ?case by autonext  case (limit l) thus ?case    by (blast dest: nat_le_Limit le_imp_subset)qedlemma Ord_nat_subset_into_Card: "[| Ord(i); i ⊆ nat |] ==> Card(i)"by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)end`