src/ZF/CardinalArith.thy
changeset 46907 eea3eb057fea
parent 46901 1382bba4b7a5
child 46935 38ecb2dc3636
     1.1 --- a/src/ZF/CardinalArith.thy	Tue Mar 13 12:04:07 2012 +0000
     1.2 +++ b/src/ZF/CardinalArith.thy	Tue Mar 13 17:11:49 2012 +0000
     1.3 @@ -543,18 +543,20 @@
     1.4  
     1.5  text{*Kunen: "each @{term"\<langle>x,y\<rangle> \<in> K \<times> K"} has no more than @{term"z \<times> z"} predecessors..." (page 29) *}
     1.6  lemma ordermap_csquare_le:
     1.7 -  assumes K: "Limit(K)" and x: "x<K" and y: " y<K" and z: "z=succ(x \<union> y)"
     1.8 +  assumes K: "Limit(K)" and x: "x<K" and y: " y<K" 
     1.9 +  defines "z \<equiv> succ(x \<union> y)"
    1.10    shows "|ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>| \<le> |succ(z)| \<otimes> |succ(z)|"
    1.11  proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)
    1.12    show "well_ord(|succ(z)| \<times> |succ(z)|, 
    1.13                   rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"
    1.14      by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult) 
    1.15  next
    1.16 -  have zK: "z<K" using x y z K 
    1.17 +  have zK: "z<K" using x y K z_def
    1.18      by (blast intro: Un_least_lt Limit_has_succ)
    1.19    hence oz: "Ord(z)" by (elim ltE) 
    1.20    have "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> ordermap(K \<times> K, csquare_rel(K)) ` \<langle>z,z\<rangle>"
    1.21 -    by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y z) 
    1.22 +    using z_def
    1.23 +    by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y) 
    1.24    also have "... \<approx>  Order.pred(K \<times> K, \<langle>z,z\<rangle>, csquare_rel(K))"
    1.25      proof (rule ordermap_eqpoll_pred)
    1.26        show "well_ord(K \<times> K, csquare_rel(K))" using K 
    1.27 @@ -572,58 +574,100 @@
    1.28  
    1.29  text{*Kunen: "... so the order type is @{text"\<le>"} K" *}
    1.30  lemma ordertype_csquare_le:
    1.31 -     "[| InfCard(K);  \<forall>y\<in>K. InfCard(y) \<longrightarrow> y \<otimes> y = y |]
    1.32 -      ==> ordertype(K*K, csquare_rel(K)) \<le> K"
    1.33 -apply (frule InfCard_is_Card [THEN Card_is_Ord])
    1.34 -apply (rule all_lt_imp_le, assumption)
    1.35 -apply (erule well_ord_csquare [THEN Ord_ordertype])
    1.36 -apply (rule Card_lt_imp_lt)
    1.37 -apply (erule_tac [3] InfCard_is_Card)
    1.38 -apply (erule_tac [2] ltE)
    1.39 -apply (simp add: ordertype_unfold)
    1.40 -apply (safe elim!: ltE)
    1.41 -apply (subgoal_tac "Ord (xa) & Ord (ya)")
    1.42 - prefer 2 apply (blast intro: Ord_in_Ord, clarify)
    1.43 -(*??WHAT A MESS!*)
    1.44 -apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
    1.45 -       (assumption | rule refl | erule ltI)+)
    1.46 -apply (rule_tac i = "xa \<union> ya" and j = nat in Ord_linear2,
    1.47 -       simp_all add: Ord_Un Ord_nat)
    1.48 -prefer 2 (*case @{term"nat \<le> (xa \<union> ya)"} *)
    1.49 - apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong]
    1.50 -                  le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un
    1.51 -                ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD])
    1.52 -(*the finite case: @{term"xa \<union> ya < nat"} *)
    1.53 -apply (rule_tac j = nat in lt_trans2)
    1.54 - apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
    1.55 -                  nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
    1.56 -apply (simp add: InfCard_def)
    1.57 -done
    1.58 +  assumes IK: "InfCard(K)" and eq: "\<And>y. y\<in>K \<Longrightarrow> InfCard(y) \<Longrightarrow> y \<otimes> y = y"
    1.59 +  shows "ordertype(K*K, csquare_rel(K)) \<le> K"
    1.60 +proof -
    1.61 +  have  CK: "Card(K)" using IK by (rule InfCard_is_Card) 
    1.62 +  hence OK: "Ord(K)"  by (rule Card_is_Ord) 
    1.63 +  moreover have "Ord(ordertype(K \<times> K, csquare_rel(K)))" using OK
    1.64 +    by (rule well_ord_csquare [THEN Ord_ordertype])
    1.65 +  ultimately show ?thesis
    1.66 +  proof (rule all_lt_imp_le)
    1.67 +    fix i
    1.68 +    assume i: "i < ordertype(K \<times> K, csquare_rel(K))"
    1.69 +    hence Oi: "Ord(i)" by (elim ltE)
    1.70 +    obtain x y where x: "x \<in> K" and y: "y \<in> K" 
    1.71 +                 and ieq: "i = ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>"
    1.72 +      using i by (auto simp add: ordertype_unfold elim: ltE)
    1.73 +    hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK 
    1.74 +      by (blast intro: Ord_in_Ord ltI)+
    1.75 +    hence ou: "Ord(x \<union> y)"
    1.76 +      by (simp add: Ord_Un) 
    1.77 +    show "i < K"
    1.78 +      proof (rule Card_lt_imp_lt [OF _ Oi CK])
    1.79 +        have "|i| \<le> |succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))|" using IK xy
    1.80 +          by (auto simp add: ieq intro: InfCard_is_Limit [THEN ordermap_csquare_le])
    1.81 +        moreover have "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| < K" 
    1.82 +          proof (cases rule: Ord_linear2 [OF ou Ord_nat])
    1.83 +            assume "x \<union> y < nat"
    1.84 +            hence "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| \<in> nat"
    1.85 +              by (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
    1.86 +                         nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
    1.87 +            also have "... \<subseteq> K" using IK
    1.88 +              by (simp add: InfCard_def le_imp_subset)
    1.89 +            finally show "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| < K" 
    1.90 +              by (simp add: ltI OK) 
    1.91 +          next
    1.92 +            assume natxy: "nat \<le> x \<union> y"
    1.93 +            hence seq: "|succ(succ(x \<union> y))| = |x \<union> y|" using xy 
    1.94 +              by (simp add: le_imp_subset nat_succ_eqpoll [THEN cardinal_cong] le_succ_iff)
    1.95 +            also have "... < K" using xy  
    1.96 +              by (simp add: Un_least_lt Ord_cardinal_le [THEN lt_trans1])
    1.97 +            finally have "|succ(succ(x \<union> y))| < K" .
    1.98 +            moreover have "InfCard(|succ(succ(x \<union> y))|)" using xy natxy
    1.99 +              by (simp add: seq InfCard_def Card_cardinal nat_le_cardinal)
   1.100 +            ultimately show ?thesis  by (simp add: eq ltD) 
   1.101 +          qed
   1.102 +        ultimately show "|i| < K" by (blast intro: lt_trans1) 
   1.103 +    qed
   1.104 +  qed
   1.105 +qed
   1.106  
   1.107  (*Main result: Kunen's Theorem 10.12*)
   1.108 -lemma InfCard_csquare_eq: "InfCard(K) ==> K \<otimes> K = K"
   1.109 -apply (frule InfCard_is_Card [THEN Card_is_Ord])
   1.110 -apply (erule rev_mp)
   1.111 -apply (erule_tac i=K in trans_induct)
   1.112 -apply (rule impI)
   1.113 -apply (rule le_anti_sym)
   1.114 -apply (erule_tac [2] InfCard_is_Card [THEN cmult_square_le])
   1.115 -apply (rule ordertype_csquare_le [THEN [2] le_trans])
   1.116 -apply (simp add: cmult_def Ord_cardinal_le
   1.117 -                 well_ord_csquare [THEN Ord_ordertype]
   1.118 -                 well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll,
   1.119 -                                   THEN cardinal_cong], assumption+)
   1.120 -done
   1.121 +lemma InfCard_csquare_eq: 
   1.122 +  assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
   1.123 +proof -
   1.124 +  have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) 
   1.125 +  have "InfCard(K) \<longrightarrow> K \<otimes> K = K"
   1.126 +    proof (rule trans_induct [OF OK], rule impI)
   1.127 +      fix i
   1.128 +      assume i: "Ord(i)" "InfCard(i)"
   1.129 +         and ih: " \<forall>y\<in>i. InfCard(y) \<longrightarrow> y \<otimes> y = y"
   1.130 +      show "i \<otimes> i = i"
   1.131 +        proof (rule le_anti_sym)
   1.132 +          have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
   1.133 +            by (rule cardinal_cong, 
   1.134 +                simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
   1.135 +          hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" using i
   1.136 +            by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
   1.137 +          moreover
   1.138 +          have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using ih i
   1.139 +            by (simp add: ordertype_csquare_le) 
   1.140 +          ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
   1.141 +        next
   1.142 +          show "i \<le> i \<otimes> i" using i
   1.143 +            by (blast intro: cmult_square_le InfCard_is_Card) 
   1.144 +        qed
   1.145 +    qed
   1.146 +  thus ?thesis using IK ..
   1.147 +qed
   1.148  
   1.149  (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
   1.150  lemma well_ord_InfCard_square_eq:
   1.151 -     "[| well_ord(A,r);  InfCard(|A|) |] ==> A*A \<approx> A"
   1.152 -apply (rule prod_eqpoll_cong [THEN eqpoll_trans])
   1.153 -apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+
   1.154 -apply (rule well_ord_cardinal_eqE)
   1.155 -apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel, assumption)
   1.156 -apply (simp add: cmult_def [symmetric] InfCard_csquare_eq)
   1.157 -done
   1.158 +  assumes r: "well_ord(A,r)" and I: "InfCard(|A|)" shows "A \<times> A \<approx> A"
   1.159 +proof -
   1.160 +  have "A \<times> A \<approx> |A| \<times> |A|"
   1.161 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_sym r) 
   1.162 +  also have "... \<approx> A"
   1.163 +    proof (rule well_ord_cardinal_eqE [OF _ r])
   1.164 +      show "well_ord(|A| \<times> |A|, rmult(|A|, Memrel(|A|), |A|, Memrel(|A|)))"
   1.165 +        by (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel r)
   1.166 +    next
   1.167 +      show "||A| \<times> |A|| = |A|" using InfCard_csquare_eq I
   1.168 +        by (simp add: cmult_def)
   1.169 +    qed    
   1.170 +  finally show ?thesis .
   1.171 +qed
   1.172  
   1.173  lemma InfCard_square_eqpoll: "InfCard(K) ==> K \<times> K \<approx> K"
   1.174  apply (rule well_ord_InfCard_square_eq)
   1.175 @@ -856,12 +900,15 @@
   1.176  
   1.177  lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel]
   1.178  
   1.179 -lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n"
   1.180 -apply (rule eqpoll_trans)
   1.181 -apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
   1.182 -apply (erule nat_implies_well_ord)+
   1.183 -apply (simp add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl)
   1.184 -done
   1.185 +lemma nat_sum_eqpoll_sum: 
   1.186 +  assumes m: "m \<in> nat" and n: "n \<in> nat" shows "m + n \<approx> m #+ n"
   1.187 +proof -
   1.188 +  have "m + n \<approx> |m+n|" using m n
   1.189 +    by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_eqpoll eqpoll_sym) 
   1.190 +  also have "... = m #+ n" using m n
   1.191 +    by (simp add: nat_cadd_eq_add [symmetric] cadd_def)
   1.192 +  finally show ?thesis .
   1.193 +qed
   1.194  
   1.195  lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat | i=nat"
   1.196  apply (erule trans_induct3, auto)