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
```