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