src/ZF/Cardinal_AC.thy
 author wenzelm Tue Jul 31 19:40:22 2007 +0200 (2007-07-31) changeset 24091 109f19a13872 parent 16417 9bc16273c2d4 child 35762 af3ff2ba4c54 permissions -rw-r--r--
```     1 (*  Title:      ZF/Cardinal_AC.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1994  University of Cambridge
```
```     5
```
```     6 These results help justify infinite-branching datatypes
```
```     7 *)
```
```     8
```
```     9 header{*Cardinal Arithmetic Using AC*}
```
```    10
```
```    11 theory Cardinal_AC imports CardinalArith Zorn begin
```
```    12
```
```    13 subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
```
```    14
```
```    15 lemma cardinal_eqpoll: "|A| eqpoll A"
```
```    16 apply (rule AC_well_ord [THEN exE])
```
```    17 apply (erule well_ord_cardinal_eqpoll)
```
```    18 done
```
```    19
```
```    20 text{*The theorem @{term "||A|| = |A|"} *}
```
```    21 lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard, simp]
```
```    22
```
```    23 lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
```
```    24 apply (rule AC_well_ord [THEN exE])
```
```    25 apply (rule AC_well_ord [THEN exE])
```
```    26 apply (rule well_ord_cardinal_eqE, assumption+)
```
```    27 done
```
```    28
```
```    29 lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
```
```    30 by (blast intro: cardinal_cong cardinal_eqE)
```
```    31
```
```    32 lemma cardinal_disjoint_Un:
```
```    33      "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |]
```
```    34       ==> |A Un C| = |B Un D|"
```
```    35 by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
```
```    36
```
```    37 lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
```
```    38 apply (rule AC_well_ord [THEN exE])
```
```    39 apply (erule well_ord_lepoll_imp_Card_le, assumption)
```
```    40 done
```
```    41
```
```    42 lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
```
```    43 apply (rule AC_well_ord [THEN exE])
```
```    44 apply (rule AC_well_ord [THEN exE])
```
```    45 apply (rule AC_well_ord [THEN exE])
```
```    46 apply (rule well_ord_cadd_assoc, assumption+)
```
```    47 done
```
```    48
```
```    49 lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
```
```    50 apply (rule AC_well_ord [THEN exE])
```
```    51 apply (rule AC_well_ord [THEN exE])
```
```    52 apply (rule AC_well_ord [THEN exE])
```
```    53 apply (rule well_ord_cmult_assoc, assumption+)
```
```    54 done
```
```    55
```
```    56 lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
```
```    57 apply (rule AC_well_ord [THEN exE])
```
```    58 apply (rule AC_well_ord [THEN exE])
```
```    59 apply (rule AC_well_ord [THEN exE])
```
```    60 apply (rule well_ord_cadd_cmult_distrib, assumption+)
```
```    61 done
```
```    62
```
```    63 lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
```
```    64 apply (rule AC_well_ord [THEN exE])
```
```    65 apply (erule well_ord_InfCard_square_eq, assumption)
```
```    66 done
```
```    67
```
```    68
```
```    69 subsection {*The relationship between cardinality and le-pollence*}
```
```    70
```
```    71 lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B"
```
```    72 apply (rule cardinal_eqpoll
```
```    73               [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans])
```
```    74 apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans])
```
```    75 apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
```
```    76 done
```
```    77
```
```    78 lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K"
```
```    79 apply (erule Card_cardinal_eq [THEN subst], rule iffI,
```
```    80        erule Card_le_imp_lepoll)
```
```    81 apply (erule lepoll_imp_Card_le)
```
```    82 done
```
```    83
```
```    84 lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0";
```
```    85 apply auto
```
```    86 apply (drule cardinal_0 [THEN ssubst])
```
```    87 apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
```
```    88 done
```
```    89
```
```    90 lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A"
```
```    91 apply (cut_tac A = "A" in cardinal_eqpoll)
```
```    92 apply (auto simp add: eqpoll_iff)
```
```    93 apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
```
```    94 apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2
```
```    95              simp add: cardinal_idem)
```
```    96 done
```
```    97
```
```    98 lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
```
```    99 apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
```
```   100 done
```
```   101
```
```   102
```
```   103 subsection{*Other Applications of AC*}
```
```   104
```
```   105 lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
```
```   106 apply (unfold surj_def)
```
```   107 apply (erule CollectE)
```
```   108 apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
```
```   109 apply (fast elim!: apply_Pair)
```
```   110 apply (blast dest: apply_type Pi_memberD
```
```   111              intro: apply_equality Pi_type f_imp_injective)
```
```   112 done
```
```   113
```
```   114 (*Kunen's Lemma 10.20*)
```
```   115 lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| le |X|"
```
```   116 apply (rule lepoll_imp_Card_le)
```
```   117 apply (erule surj_implies_inj [THEN exE])
```
```   118 apply (unfold lepoll_def)
```
```   119 apply (erule exI)
```
```   120 done
```
```   121
```
```   122 (*Kunen's Lemma 10.21*)
```
```   123 lemma cardinal_UN_le:
```
```   124      "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |\<Union>i\<in>K. X(i)| le K"
```
```   125 apply (simp add: InfCard_is_Card le_Card_iff)
```
```   126 apply (rule lepoll_trans)
```
```   127  prefer 2
```
```   128  apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])
```
```   129  apply (simp add: InfCard_is_Card Card_cardinal_eq)
```
```   130 apply (unfold lepoll_def)
```
```   131 apply (frule InfCard_is_Card [THEN Card_is_Ord])
```
```   132 apply (erule AC_ball_Pi [THEN exE])
```
```   133 apply (rule exI)
```
```   134 (*Lemma needed in both subgoals, for a fixed z*)
```
```   135 apply (subgoal_tac "ALL z: (\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) &
```
```   136                     (LEAST i. z:X (i)) : K")
```
```   137  prefer 2
```
```   138  apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
```
```   139              elim!: LeastI Ord_in_Ord)
```
```   140 apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>"
```
```   141             and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
```
```   142 (*Instantiate the lemma proved above*)
```
```   143 by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
```
```   144
```
```   145
```
```   146 (*The same again, using csucc*)
```
```   147 lemma cardinal_UN_lt_csucc:
```
```   148      "[| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |]
```
```   149       ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
```
```   150 by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
```
```   151
```
```   152 (*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
```
```   153   the least ordinal j such that i:Vfrom(A,j). *)
```
```   154 lemma cardinal_UN_Ord_lt_csucc:
```
```   155      "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
```
```   156       ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
```
```   157 apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
```
```   158 apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
```
```   159 apply (blast intro!: Ord_UN elim: ltE)
```
```   160 apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
```
```   161 done
```
```   162
```
```   163
```
```   164 (** Main result for infinite-branching datatypes.  As above, but the index
```
```   165     set need not be a cardinal.  Surprisingly complicated proof!
```
```   166 **)
```
```   167
```
```   168 (*Work backwards along the injection from W into K, given that W~=0.*)
```
```   169 lemma inj_UN_subset:
```
```   170      "[| f: inj(A,B);  a:A |] ==>
```
```   171       (\<Union>x\<in>A. C(x)) <= (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
```
```   172 apply (rule UN_least)
```
```   173 apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
```
```   174  apply (simp add: inj_is_fun [THEN apply_rangeI])
```
```   175 apply (blast intro: inj_is_fun [THEN apply_type])
```
```   176 done
```
```   177
```
```   178 (*Simpler to require |W|=K; we'd have a bijection; but the theorem would
```
```   179   be weaker.*)
```
```   180 lemma le_UN_Ord_lt_csucc:
```
```   181      "[| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |]
```
```   182       ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
```
```   183 apply (case_tac "W=0")
```
```   184 (*solve the easy 0 case*)
```
```   185  apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]
```
```   186                   Card_is_Ord Ord_0_lt_csucc)
```
```   187 apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
```
```   188 apply (safe intro!: equalityI)
```
```   189 apply (erule swap)
```
```   190 apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
```
```   191  apply (simp add: inj_converse_fun [THEN apply_type])
```
```   192 apply (blast intro!: Ord_UN elim: ltE)
```
```   193 done
```
```   194
```
```   195 ML
```
```   196 {*
```
```   197 val cardinal_0_iff_0 = thm "cardinal_0_iff_0";
```
```   198 val cardinal_lt_iff_lesspoll = thm "cardinal_lt_iff_lesspoll";
```
```   199 *}
```
```   200
```
```   201 end
```