src/ZF/Cardinal_AC.thy
changeset 46820 c656222c4dc1
parent 46751 6b94c39b7366
child 46821 ff6b0c1087f2
     1.1 --- a/src/ZF/Cardinal_AC.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/Cardinal_AC.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -29,11 +29,11 @@
     1.4  by (blast intro: cardinal_cong cardinal_eqE)
     1.5  
     1.6  lemma cardinal_disjoint_Un:
     1.7 -     "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] 
     1.8 -      ==> |A Un C| = |B Un D|"
     1.9 +     "[| |A|=|B|;  |C|=|D|;  A \<inter> C = 0;  B \<inter> D = 0 |]
    1.10 +      ==> |A \<union> C| = |B \<union> D|"
    1.11  by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
    1.12  
    1.13 -lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
    1.14 +lemma lepoll_imp_Card_le: "A lepoll B ==> |A| \<le> |B|"
    1.15  apply (rule AC_well_ord [THEN exE])
    1.16  apply (erule well_ord_lepoll_imp_Card_le, assumption)
    1.17  done
    1.18 @@ -67,21 +67,21 @@
    1.19  
    1.20  subsection {*The relationship between cardinality and le-pollence*}
    1.21  
    1.22 -lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B"
    1.23 +lemma Card_le_imp_lepoll: "|A| \<le> |B| ==> A lepoll B"
    1.24  apply (rule cardinal_eqpoll
    1.25                [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans])
    1.26  apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans])
    1.27  apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
    1.28  done
    1.29  
    1.30 -lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K"
    1.31 -apply (erule Card_cardinal_eq [THEN subst], rule iffI, 
    1.32 +lemma le_Card_iff: "Card(K) ==> |A| \<le> K <-> A lepoll K"
    1.33 +apply (erule Card_cardinal_eq [THEN subst], rule iffI,
    1.34         erule Card_le_imp_lepoll)
    1.35 -apply (erule lepoll_imp_Card_le) 
    1.36 +apply (erule lepoll_imp_Card_le)
    1.37  done
    1.38  
    1.39  lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0";
    1.40 -apply auto 
    1.41 +apply auto
    1.42  apply (drule cardinal_0 [THEN ssubst])
    1.43  apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
    1.44  done
    1.45 @@ -90,7 +90,7 @@
    1.46  apply (cut_tac A = "A" in cardinal_eqpoll)
    1.47  apply (auto simp add: eqpoll_iff)
    1.48  apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
    1.49 -apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2 
    1.50 +apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2
    1.51               simp add: cardinal_idem)
    1.52  done
    1.53  
    1.54 @@ -101,17 +101,17 @@
    1.55  
    1.56  subsection{*Other Applications of AC*}
    1.57  
    1.58 -lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
    1.59 +lemma surj_implies_inj: "f: surj(X,Y) ==> \<exists>g. g: inj(Y,X)"
    1.60  apply (unfold surj_def)
    1.61  apply (erule CollectE)
    1.62  apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
    1.63  apply (fast elim!: apply_Pair)
    1.64 -apply (blast dest: apply_type Pi_memberD 
    1.65 +apply (blast dest: apply_type Pi_memberD
    1.66               intro: apply_equality Pi_type f_imp_injective)
    1.67  done
    1.68  
    1.69  (*Kunen's Lemma 10.20*)
    1.70 -lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| le |X|"
    1.71 +lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| \<le> |X|"
    1.72  apply (rule lepoll_imp_Card_le)
    1.73  apply (erule surj_implies_inj [THEN exE])
    1.74  apply (unfold lepoll_def)
    1.75 @@ -120,7 +120,7 @@
    1.76  
    1.77  (*Kunen's Lemma 10.21*)
    1.78  lemma cardinal_UN_le:
    1.79 -     "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |\<Union>i\<in>K. X(i)| le K"
    1.80 +     "[| InfCard(K);  \<forall>i\<in>K. |X(i)| \<le> K |] ==> |\<Union>i\<in>K. X(i)| \<le> K"
    1.81  apply (simp add: InfCard_is_Card le_Card_iff)
    1.82  apply (rule lepoll_trans)
    1.83   prefer 2
    1.84 @@ -131,12 +131,12 @@
    1.85  apply (erule AC_ball_Pi [THEN exE])
    1.86  apply (rule exI)
    1.87  (*Lemma needed in both subgoals, for a fixed z*)
    1.88 -apply (subgoal_tac "ALL z: (\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) & 
    1.89 -                    (LEAST i. z:X (i)) : K")
    1.90 +apply (subgoal_tac "\<forall>z\<in>(\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) &
    1.91 +                    (LEAST i. z:X (i)) \<in> K")
    1.92   prefer 2
    1.93   apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
    1.94               elim!: LeastI Ord_in_Ord)
    1.95 -apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>" 
    1.96 +apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>"
    1.97              and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
    1.98  (*Instantiate the lemma proved above*)
    1.99  by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
   1.100 @@ -144,14 +144,14 @@
   1.101  
   1.102  (*The same again, using csucc*)
   1.103  lemma cardinal_UN_lt_csucc:
   1.104 -     "[| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |]
   1.105 +     "[| InfCard(K);  \<forall>i\<in>K. |X(i)| < csucc(K) |]
   1.106        ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
   1.107  by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
   1.108  
   1.109  (*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
   1.110    the least ordinal j such that i:Vfrom(A,j). *)
   1.111  lemma cardinal_UN_Ord_lt_csucc:
   1.112 -     "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
   1.113 +     "[| InfCard(K);  \<forall>i\<in>K. j(i) < csucc(K) |]
   1.114        ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
   1.115  apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
   1.116  apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
   1.117 @@ -164,10 +164,10 @@
   1.118      set need not be a cardinal.  Surprisingly complicated proof!
   1.119  **)
   1.120  
   1.121 -(*Work backwards along the injection from W into K, given that W~=0.*)
   1.122 +(*Work backwards along the injection from W into K, given that @{term"W\<noteq>0"}.*)
   1.123  lemma inj_UN_subset:
   1.124 -     "[| f: inj(A,B);  a:A |] ==>            
   1.125 -      (\<Union>x\<in>A. C(x)) <= (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
   1.126 +     "[| f: inj(A,B);  a:A |] ==>
   1.127 +      (\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
   1.128  apply (rule UN_least)
   1.129  apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
   1.130   apply (simp add: inj_is_fun [THEN apply_rangeI])
   1.131 @@ -177,15 +177,15 @@
   1.132  (*Simpler to require |W|=K; we'd have a bijection; but the theorem would
   1.133    be weaker.*)
   1.134  lemma le_UN_Ord_lt_csucc:
   1.135 -     "[| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |]
   1.136 +     "[| InfCard(K);  |W| \<le> K;  \<forall>w\<in>W. j(w) < csucc(K) |]
   1.137        ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
   1.138  apply (case_tac "W=0")
   1.139  (*solve the easy 0 case*)
   1.140 - apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc] 
   1.141 + apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]
   1.142                    Card_is_Ord Ord_0_lt_csucc)
   1.143  apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
   1.144  apply (safe intro!: equalityI)
   1.145 -apply (erule swap) 
   1.146 +apply (erule swap)
   1.147  apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
   1.148   apply (simp add: inj_converse_fun [THEN apply_type])
   1.149  apply (blast intro!: Ord_UN elim: ltE)