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.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.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  InfCard_is_Card)
1.38 -apply (erule_tac  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.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  InfCard_is_Card [THEN cmult_square_le])
1.115 -apply (rule ordertype_csquare_le [THEN  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.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.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.177  lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel]
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)+