# Theory Cardinal_AC

Up to index of Isabelle/ZF

theory Cardinal_AC
imports Zorn
`(*  Title:      ZF/Cardinal_AC.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1994  University of CambridgeThese results help justify infinite-branching datatypes*)header{*Cardinal Arithmetic Using AC*}theory Cardinal_AC imports CardinalArith Zorn beginsubsection{*Strengthened Forms of Existing Theorems on Cardinals*}lemma cardinal_eqpoll: "|A| ≈ A"apply (rule AC_well_ord [THEN exE])apply (erule well_ord_cardinal_eqpoll)donetext{*The theorem @{term "||A|| = |A|"} *}lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]lemma cardinal_eqE: "|X| = |Y| ==> X ≈ Y"apply (rule AC_well_ord [THEN exE])apply (rule AC_well_ord [THEN exE])apply (rule well_ord_cardinal_eqE, assumption+)donelemma cardinal_eqpoll_iff: "|X| = |Y| <-> X ≈ Y"by (blast intro: cardinal_cong cardinal_eqE)lemma cardinal_disjoint_Un:     "[| |A|=|B|;  |C|=|D|;  A ∩ C = 0;  B ∩ D = 0 |]      ==> |A ∪ C| = |B ∪ D|"by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)lemma lepoll_imp_Card_le: "A \<lesssim> B ==> |A| ≤ |B|"apply (rule AC_well_ord [THEN exE])apply (erule well_ord_lepoll_imp_Card_le, assumption)donelemma cadd_assoc: "(i ⊕ j) ⊕ k = i ⊕ (j ⊕ k)"apply (rule AC_well_ord [THEN exE])apply (rule AC_well_ord [THEN exE])apply (rule AC_well_ord [THEN exE])apply (rule well_ord_cadd_assoc, assumption+)donelemma cmult_assoc: "(i ⊗ j) ⊗ k = i ⊗ (j ⊗ k)"apply (rule AC_well_ord [THEN exE])apply (rule AC_well_ord [THEN exE])apply (rule AC_well_ord [THEN exE])apply (rule well_ord_cmult_assoc, assumption+)donelemma cadd_cmult_distrib: "(i ⊕ j) ⊗ k = (i ⊗ k) ⊕ (j ⊗ k)"apply (rule AC_well_ord [THEN exE])apply (rule AC_well_ord [THEN exE])apply (rule AC_well_ord [THEN exE])apply (rule well_ord_cadd_cmult_distrib, assumption+)donelemma InfCard_square_eq: "InfCard(|A|) ==> A*A ≈ A"apply (rule AC_well_ord [THEN exE])apply (erule well_ord_InfCard_square_eq, assumption)donesubsection {*The relationship between cardinality and le-pollence*}lemma Card_le_imp_lepoll:  assumes "|A| ≤ |B|" shows "A \<lesssim> B"proof -  have "A ≈ |A|"     by (rule cardinal_eqpoll [THEN eqpoll_sym])  also have "... \<lesssim> |B|"    by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms)  also have "... ≈ B"     by (rule cardinal_eqpoll)  finally show ?thesis .qedlemma le_Card_iff: "Card(K) ==> |A| ≤ K <-> A \<lesssim> K"apply (erule Card_cardinal_eq [THEN subst], rule iffI,       erule Card_le_imp_lepoll)apply (erule lepoll_imp_Card_le)donelemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0"apply autoapply (drule cardinal_0 [THEN ssubst])apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])donelemma cardinal_lt_iff_lesspoll:  assumes i: "Ord(i)" shows "i < |A| <-> i \<prec> A"proof  assume "i < |A|"  hence  "i \<prec> |A|"     by (blast intro: lt_Card_imp_lesspoll Card_cardinal)   also have "...  ≈ A"     by (rule cardinal_eqpoll)  finally show "i \<prec> A" .next  assume "i \<prec> A"  also have "...  ≈ |A|"     by (blast intro: cardinal_eqpoll eqpoll_sym)   finally have "i \<prec> |A|" .  thus  "i < |A|" using i    by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)qedlemma cardinal_le_imp_lepoll: " i ≤ |A| ==> i \<lesssim> A"  by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)subsection{*Other Applications of AC*}lemma surj_implies_inj:  assumes f: "f ∈ surj(X,Y)" shows "∃g. g ∈ inj(Y,X)"proof -  from f AC_Pi [of Y "%y. f-``{y}"]  obtain z where z: "z ∈ (Π y∈Y. f -`` {y})"      by (auto simp add: surj_def) (fast dest: apply_Pair)  show ?thesis    proof      show "z ∈ inj(Y, X)" using z surj_is_fun [OF f]        by (blast dest: apply_type Pi_memberD                  intro: apply_equality Pi_type f_imp_injective)    qedqedtext{*Kunen's Lemma 10.20*}lemma surj_implies_cardinal_le:   assumes f: "f ∈ surj(X,Y)" shows "|Y| ≤ |X|"proof (rule lepoll_imp_Card_le)  from f [THEN surj_implies_inj] obtain g where "g ∈ inj(Y,X)" ..  thus "Y \<lesssim> X"    by (auto simp add: lepoll_def)qedtext{*Kunen's Lemma 10.21*}lemma cardinal_UN_le:  assumes K: "InfCard(K)"   shows "(!!i. i∈K ==> |X(i)| ≤ K) ==> |\<Union>i∈K. X(i)| ≤ K"proof (simp add: K InfCard_is_Card le_Card_iff)  have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K)   assume "!!i. i∈K ==> X(i) \<lesssim> K"  hence "!!i. i∈K ==> ∃f. f ∈ inj(X(i), K)" by (simp add: lepoll_def)   with AC_Pi obtain f where f: "f ∈ (Π i∈K. inj(X(i), K))"    by force   { fix z    assume z: "z ∈ (\<Union>i∈K. X(i))"    then obtain i where i: "i ∈ K" "Ord(i)" "z ∈ X(i)"      by (blast intro: Ord_in_Ord [of K])     hence "(LEAST i. z ∈ X(i)) ≤ i" by (fast intro: Least_le)     hence "(LEAST i. z ∈ X(i)) < K" by (best intro: lt_trans1 ltI i)     hence "(LEAST i. z ∈ X(i)) ∈ K" and "z ∈ X(LEAST i. z ∈ X(i))"        by (auto intro: LeastI ltD i)   } note mems = this  have "(\<Union>i∈K. X(i)) \<lesssim> K × K"     proof (unfold lepoll_def)      show "∃f. f ∈ inj(\<Union>RepFun(K, X), K × K)"        apply (rule exI)         apply (rule_tac c = "%z. ⟨LEAST i. z ∈ X(i), f ` (LEAST i. z ∈ X(i)) ` z⟩"                    and d = "%⟨i,j⟩. converse (f`i) ` j" in lam_injective)         apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+        done    qed  also have "... ≈ K"     by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)  finally show "(\<Union>i∈K. X(i)) \<lesssim> K" .qedtext{*The same again, using @{term csucc}*}lemma cardinal_UN_lt_csucc:     "[| InfCard(K);  !!i. i∈K ==> |X(i)| < csucc(K) |]      ==> |\<Union>i∈K. X(i)| < csucc(K)"by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)text{*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),  the least ordinal j such that i:Vfrom(A,j). *}lemma cardinal_UN_Ord_lt_csucc:     "[| InfCard(K);  !!i. i∈K ==> j(i) < csucc(K) |]      ==> (\<Union>i∈K. j(i)) < csucc(K)"apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)apply (blast intro!: Ord_UN elim: ltE)apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])donesubsection{*The Main Result for Infinite-Branching Datatypes*}text{*As above, but the index set need not be a cardinal. Workbackwards along the injection from @{term W} into @{term K}, giventhat @{term"W≠0"}.*}lemma inj_UN_subset:  assumes f: "f ∈ inj(A,B)" and a: "a ∈ A"  shows "(\<Union>x∈A. C(x)) ⊆ (\<Union>y∈B. C(if y ∈ range(f) then converse(f)`y else a))"proof (rule UN_least)  fix x  assume x: "x ∈ A"  hence fx: "f ` x ∈ B" by (blast intro: f inj_is_fun [THEN apply_type])  have "C(x) ⊆ C(if f ` x ∈ range(f) then converse(f) ` (f ` x) else a)"     using f x by (simp add: inj_is_fun [THEN apply_rangeI])  also have "... ⊆ (\<Union>y∈B. C(if y ∈ range(f) then converse(f) ` y else a))"    by (rule UN_upper [OF fx])   finally show "C(x) ⊆ (\<Union>y∈B. C(if y ∈ range(f) then converse(f)`y else a))" .qedtheorem le_UN_Ord_lt_csucc:  assumes IK: "InfCard(K)" and WK: "|W| ≤ K" and j: "!!w. w∈W ==> j(w) < csucc(K)"  shows "(\<Union>w∈W. j(w)) < csucc(K)"proof -  have CK: "Card(K)"     by (simp add: InfCard_is_Card IK)  then obtain f where f: "f ∈ inj(W, K)" using WK    by(auto simp add: le_Card_iff lepoll_def)  have OU: "Ord(\<Union>w∈W. j(w))" using j    by (blast elim: ltE)  note lt_subset_trans [OF _ _ OU, trans]  show ?thesis    proof (cases "W=0")      case True  --{*solve the easy 0 case*}      thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)    next      case False        then obtain x where x: "x ∈ W" by blast        have "(\<Union>x∈W. j(x)) ⊆ (\<Union>k∈K. j(if k ∈ range(f) then converse(f) ` k else x))"          by (rule inj_UN_subset [OF f x])         also have "... < csucc(K)" using IK          proof (rule cardinal_UN_Ord_lt_csucc)            fix k            assume "k ∈ K"            thus "j(if k ∈ range(f) then converse(f) ` k else x) < csucc(K)" using f x j              by (simp add: inj_converse_fun [THEN apply_type])          qed        finally show ?thesis .    qedqedend`