src/ZF/Cardinal_AC.thy
author wenzelm
Tue Sep 01 22:32:58 2015 +0200 (2015-09-01)
changeset 61076 bdc1e2f0a86a
parent 60770 240563fbf41d
child 61394 6142b282b164
permissions -rw-r--r--
eliminated \<Colon>;
     1 (*  Title:      ZF/Cardinal_AC.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1994  University of Cambridge
     4 
     5 These results help justify infinite-branching datatypes
     6 *)
     7 
     8 section\<open>Cardinal Arithmetic Using AC\<close>
     9 
    10 theory Cardinal_AC imports CardinalArith Zorn begin
    11 
    12 subsection\<open>Strengthened Forms of Existing Theorems on Cardinals\<close>
    13 
    14 lemma cardinal_eqpoll: "|A| \<approx> A"
    15 apply (rule AC_well_ord [THEN exE])
    16 apply (erule well_ord_cardinal_eqpoll)
    17 done
    18 
    19 text\<open>The theorem @{term "||A|| = |A|"}\<close>
    20 lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
    21 
    22 lemma cardinal_eqE: "|X| = |Y| ==> X \<approx> Y"
    23 apply (rule AC_well_ord [THEN exE])
    24 apply (rule AC_well_ord [THEN exE])
    25 apply (rule well_ord_cardinal_eqE, assumption+)
    26 done
    27 
    28 lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X \<approx> Y"
    29 by (blast intro: cardinal_cong cardinal_eqE)
    30 
    31 lemma cardinal_disjoint_Un:
    32      "[| |A|=|B|;  |C|=|D|;  A \<inter> C = 0;  B \<inter> D = 0 |]
    33       ==> |A \<union> C| = |B \<union> D|"
    34 by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
    35 
    36 lemma lepoll_imp_Card_le: "A \<lesssim> B ==> |A| \<le> |B|"
    37 apply (rule AC_well_ord [THEN exE])
    38 apply (erule well_ord_lepoll_imp_Card_le, assumption)
    39 done
    40 
    41 lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
    42 apply (rule AC_well_ord [THEN exE])
    43 apply (rule AC_well_ord [THEN exE])
    44 apply (rule AC_well_ord [THEN exE])
    45 apply (rule well_ord_cadd_assoc, assumption+)
    46 done
    47 
    48 lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
    49 apply (rule AC_well_ord [THEN exE])
    50 apply (rule AC_well_ord [THEN exE])
    51 apply (rule AC_well_ord [THEN exE])
    52 apply (rule well_ord_cmult_assoc, assumption+)
    53 done
    54 
    55 lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
    56 apply (rule AC_well_ord [THEN exE])
    57 apply (rule AC_well_ord [THEN exE])
    58 apply (rule AC_well_ord [THEN exE])
    59 apply (rule well_ord_cadd_cmult_distrib, assumption+)
    60 done
    61 
    62 lemma InfCard_square_eq: "InfCard(|A|) ==> A*A \<approx> A"
    63 apply (rule AC_well_ord [THEN exE])
    64 apply (erule well_ord_InfCard_square_eq, assumption)
    65 done
    66 
    67 
    68 subsection \<open>The relationship between cardinality and le-pollence\<close>
    69 
    70 lemma Card_le_imp_lepoll:
    71   assumes "|A| \<le> |B|" shows "A \<lesssim> B"
    72 proof -
    73   have "A \<approx> |A|" 
    74     by (rule cardinal_eqpoll [THEN eqpoll_sym])
    75   also have "... \<lesssim> |B|"
    76     by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms)
    77   also have "... \<approx> B" 
    78     by (rule cardinal_eqpoll)
    79   finally show ?thesis .
    80 qed
    81 
    82 lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A \<lesssim> K"
    83 apply (erule Card_cardinal_eq [THEN subst], rule iffI,
    84        erule Card_le_imp_lepoll)
    85 apply (erule lepoll_imp_Card_le)
    86 done
    87 
    88 lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0"
    89 apply auto
    90 apply (drule cardinal_0 [THEN ssubst])
    91 apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
    92 done
    93 
    94 lemma cardinal_lt_iff_lesspoll:
    95   assumes i: "Ord(i)" shows "i < |A| \<longleftrightarrow> i \<prec> A"
    96 proof
    97   assume "i < |A|"
    98   hence  "i \<prec> |A|" 
    99     by (blast intro: lt_Card_imp_lesspoll Card_cardinal) 
   100   also have "...  \<approx> A" 
   101     by (rule cardinal_eqpoll)
   102   finally show "i \<prec> A" .
   103 next
   104   assume "i \<prec> A"
   105   also have "...  \<approx> |A|" 
   106     by (blast intro: cardinal_eqpoll eqpoll_sym) 
   107   finally have "i \<prec> |A|" .
   108   thus  "i < |A|" using i
   109     by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)
   110 qed
   111 
   112 lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
   113   by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
   114 
   115 
   116 subsection\<open>Other Applications of AC\<close>
   117 
   118 lemma surj_implies_inj:
   119   assumes f: "f \<in> surj(X,Y)" shows "\<exists>g. g \<in> inj(Y,X)"
   120 proof -
   121   from f AC_Pi [of Y "%y. f-``{y}"]
   122   obtain z where z: "z \<in> (\<Pi> y\<in>Y. f -`` {y})"  
   123     by (auto simp add: surj_def) (fast dest: apply_Pair)
   124   show ?thesis
   125     proof
   126       show "z \<in> inj(Y, X)" using z surj_is_fun [OF f]
   127         by (blast dest: apply_type Pi_memberD
   128                   intro: apply_equality Pi_type f_imp_injective)
   129     qed
   130 qed
   131 
   132 text\<open>Kunen's Lemma 10.20\<close>
   133 lemma surj_implies_cardinal_le: 
   134   assumes f: "f \<in> surj(X,Y)" shows "|Y| \<le> |X|"
   135 proof (rule lepoll_imp_Card_le)
   136   from f [THEN surj_implies_inj] obtain g where "g \<in> inj(Y,X)" ..
   137   thus "Y \<lesssim> X"
   138     by (auto simp add: lepoll_def)
   139 qed
   140 
   141 text\<open>Kunen's Lemma 10.21\<close>
   142 lemma cardinal_UN_le:
   143   assumes K: "InfCard(K)" 
   144   shows "(!!i. i\<in>K ==> |X(i)| \<le> K) ==> |\<Union>i\<in>K. X(i)| \<le> K"
   145 proof (simp add: K InfCard_is_Card le_Card_iff)
   146   have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K) 
   147   assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
   148   hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def) 
   149   with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
   150     by force 
   151   { fix z
   152     assume z: "z \<in> (\<Union>i\<in>K. X(i))"
   153     then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
   154       by (blast intro: Ord_in_Ord [of K]) 
   155     hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le) 
   156     hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i) 
   157     hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))"  
   158       by (auto intro: LeastI ltD i) 
   159   } note mems = this
   160   have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K" 
   161     proof (unfold lepoll_def)
   162       show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
   163         apply (rule exI) 
   164         apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>"
   165                     and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective) 
   166         apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
   167         done
   168     qed
   169   also have "... \<approx> K" 
   170     by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
   171   finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" .
   172 qed
   173 
   174 text\<open>The same again, using @{term csucc}\<close>
   175 lemma cardinal_UN_lt_csucc:
   176      "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> |X(i)| < csucc(K) |]
   177       ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
   178 by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
   179 
   180 text\<open>The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
   181   the least ordinal j such that i:Vfrom(A,j).\<close>
   182 lemma cardinal_UN_Ord_lt_csucc:
   183      "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> j(i) < csucc(K) |]
   184       ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
   185 apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
   186 apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
   187 apply (blast intro!: Ord_UN elim: ltE)
   188 apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
   189 done
   190 
   191 
   192 subsection\<open>The Main Result for Infinite-Branching Datatypes\<close>
   193 
   194 text\<open>As above, but the index set need not be a cardinal. Work
   195 backwards along the injection from @{term W} into @{term K}, given
   196 that @{term"W\<noteq>0"}.\<close>
   197 
   198 lemma inj_UN_subset:
   199   assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
   200   shows "(\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))"
   201 proof (rule UN_least)
   202   fix x
   203   assume x: "x \<in> A"
   204   hence fx: "f ` x \<in> B" by (blast intro: f inj_is_fun [THEN apply_type])
   205   have "C(x) \<subseteq> C(if f ` x \<in> range(f) then converse(f) ` (f ` x) else a)" 
   206     using f x by (simp add: inj_is_fun [THEN apply_rangeI])
   207   also have "... \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f) ` y else a))"
   208     by (rule UN_upper [OF fx]) 
   209   finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
   210 qed
   211 
   212 theorem le_UN_Ord_lt_csucc:
   213   assumes IK: "InfCard(K)" and WK: "|W| \<le> K" and j: "\<And>w. w\<in>W \<Longrightarrow> j(w) < csucc(K)"
   214   shows "(\<Union>w\<in>W. j(w)) < csucc(K)"
   215 proof -
   216   have CK: "Card(K)" 
   217     by (simp add: InfCard_is_Card IK)
   218   then obtain f where f: "f \<in> inj(W, K)" using WK
   219     by(auto simp add: le_Card_iff lepoll_def)
   220   have OU: "Ord(\<Union>w\<in>W. j(w))" using j
   221     by (blast elim: ltE)
   222   note lt_subset_trans [OF _ _ OU, trans]
   223   show ?thesis
   224     proof (cases "W=0")
   225       case True  --\<open>solve the easy 0 case\<close>
   226       thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
   227     next
   228       case False
   229         then obtain x where x: "x \<in> W" by blast
   230         have "(\<Union>x\<in>W. j(x)) \<subseteq> (\<Union>k\<in>K. j(if k \<in> range(f) then converse(f) ` k else x))"
   231           by (rule inj_UN_subset [OF f x]) 
   232         also have "... < csucc(K)" using IK
   233           proof (rule cardinal_UN_Ord_lt_csucc)
   234             fix k
   235             assume "k \<in> K"
   236             thus "j(if k \<in> range(f) then converse(f) ` k else x) < csucc(K)" using f x j
   237               by (simp add: inj_converse_fun [THEN apply_type])
   238           qed
   239         finally show ?thesis .
   240     qed
   241 qed
   242 
   243 end