1.1 --- a/src/ZF/AC/DC.thy Mon Mar 12 23:33:50 2012 +0100
1.2 +++ b/src/ZF/AC/DC.thy Tue Mar 13 12:04:07 2012 +0000
1.3 @@ -492,6 +492,13 @@
1.4 lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
1.5 by (fast elim!: image_fun [THEN ssubst])
1.6
1.7 +lemma lesspoll_lemma: "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
1.8 +apply (unfold lesspoll_def)
1.9 +apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
1.10 + intro!: eqpollI elim: notE
1.11 + elim!: eqpollE lepoll_trans)
1.12 +done
1.13 +
1.14 theorem DC_WO3: "(\<forall>K. Card(K) \<longrightarrow> DC(K)) ==> WO3"
1.15 apply (unfold DC_def WO3_def)
1.16 apply (rule allI)
2.1 --- a/src/ZF/CardinalArith.thy Mon Mar 12 23:33:50 2012 +0100
2.2 +++ b/src/ZF/CardinalArith.thy Tue Mar 13 12:04:07 2012 +0000
2.3 @@ -63,12 +63,11 @@
2.4 hence jls: "j \<prec> c"
2.5 by (simp add: lt_Card_imp_lesspoll)
2.6 { assume eqp: "j \<approx> \<Union>A"
2.7 - hence Uls: "\<Union>A \<prec> c" using jls
2.8 - by (blast intro: eqpoll_sym eqpoll_imp_lepoll lesspoll_trans1)
2.9 - moreover have "c \<lesssim> \<Union>A" using c
2.10 + have "c \<lesssim> \<Union>A" using c
2.11 by (blast intro: subset_imp_lepoll)
2.12 - ultimately have "c \<prec> c"
2.13 - by (blast intro: lesspoll_trans1)
2.14 + also have "... \<approx> j" by (rule eqpoll_sym [OF eqp])
2.15 + also have "... \<prec> c" by (rule jls)
2.16 + finally have "c \<prec> c" .
2.17 hence False
2.18 by auto
2.19 } thus "\<not> j \<approx> \<Union>A" by blast
2.20 @@ -87,13 +86,6 @@
2.21 apply (fast intro!: le_imp_lepoll ltI leI)
2.22 done
2.23
2.24 -lemma lesspoll_lemma: "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
2.25 -apply (unfold lesspoll_def)
2.26 -apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
2.27 - intro!: eqpollI elim: notE
2.28 - elim!: eqpollE lepoll_trans)
2.29 -done
2.30 -
2.31
2.32 subsection{*Cardinal addition*}
2.33
2.34 @@ -123,20 +115,20 @@
2.35 apply (rule sum_assoc_bij)
2.36 done
2.37
2.38 -(*Unconditional version requires AC*)
2.39 +text{*Unconditional version requires AC*}
2.40 lemma well_ord_cadd_assoc:
2.41 - "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
2.42 - ==> (i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
2.43 -apply (unfold cadd_def)
2.44 -apply (rule cardinal_cong)
2.45 -apply (rule eqpoll_trans)
2.46 - apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
2.47 - apply (blast intro: well_ord_radd )
2.48 -apply (rule sum_assoc_eqpoll [THEN eqpoll_trans])
2.49 -apply (rule eqpoll_sym)
2.50 -apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
2.51 -apply (blast intro: well_ord_radd )
2.52 -done
2.53 + assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
2.54 + shows "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
2.55 +proof (unfold cadd_def, rule cardinal_cong)
2.56 + have "|i + j| + k \<approx> (i + j) + k"
2.57 + by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j)
2.58 + also have "... \<approx> i + (j + k)"
2.59 + by (rule sum_assoc_eqpoll)
2.60 + also have "... \<approx> i + |j + k|"
2.61 + by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym)
2.62 + finally show "|i + j| + k \<approx> i + |j + k|" .
2.63 +qed
2.64 +
2.65
2.66 subsubsection{*0 is the identity for addition*}
2.67
2.68 @@ -224,7 +216,6 @@
2.69
2.70 subsubsection{*Cardinal multiplication is commutative*}
2.71
2.72 -(*Easier to prove the two directions separately*)
2.73 lemma prod_commute_eqpoll: "A*B \<approx> B*A"
2.74 apply (unfold eqpoll_def)
2.75 apply (rule exI)
2.76 @@ -245,20 +236,19 @@
2.77 apply (rule prod_assoc_bij)
2.78 done
2.79
2.80 -(*Unconditional version requires AC*)
2.81 +text{*Unconditional version requires AC*}
2.82 lemma well_ord_cmult_assoc:
2.83 - "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
2.84 - ==> (i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
2.85 -apply (unfold cmult_def)
2.86 -apply (rule cardinal_cong)
2.87 -apply (rule eqpoll_trans)
2.88 - apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
2.89 - apply (blast intro: well_ord_rmult)
2.90 -apply (rule prod_assoc_eqpoll [THEN eqpoll_trans])
2.91 -apply (rule eqpoll_sym)
2.92 -apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
2.93 -apply (blast intro: well_ord_rmult)
2.94 -done
2.95 + assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
2.96 + shows "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
2.97 +proof (unfold cmult_def, rule cardinal_cong)
2.98 + have "|i * j| * k \<approx> (i * j) * k"
2.99 + by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j)
2.100 + also have "... \<approx> i * (j * k)"
2.101 + by (rule prod_assoc_eqpoll)
2.102 + also have "... \<approx> i * |j * k|"
2.103 + by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym)
2.104 + finally show "|i * j| * k \<approx> i * |j * k|" .
2.105 +qed
2.106
2.107 subsubsection{*Cardinal multiplication distributes over addition*}
2.108
2.109 @@ -269,19 +259,17 @@
2.110 done
2.111
2.112 lemma well_ord_cadd_cmult_distrib:
2.113 - "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
2.114 - ==> (i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
2.115 -apply (unfold cadd_def cmult_def)
2.116 -apply (rule cardinal_cong)
2.117 -apply (rule eqpoll_trans)
2.118 - apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
2.119 -apply (blast intro: well_ord_radd)
2.120 -apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans])
2.121 -apply (rule eqpoll_sym)
2.122 -apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll
2.123 - well_ord_cardinal_eqpoll])
2.124 -apply (blast intro: well_ord_rmult)+
2.125 -done
2.126 + assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
2.127 + shows "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
2.128 +proof (unfold cadd_def cmult_def, rule cardinal_cong)
2.129 + have "|i + j| * k \<approx> (i + j) * k"
2.130 + by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j)
2.131 + also have "... \<approx> i * k + j * k"
2.132 + by (rule sum_prod_distrib_eqpoll)
2.133 + also have "... \<approx> |i * k| + |j * k|"
2.134 + by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym)
2.135 + finally show "|i + j| * k \<approx> |i * k| + |j * k|" .
2.136 +qed
2.137
2.138 subsubsection{*Multiplication by 0 yields 0*}
2.139
2.140 @@ -391,12 +379,15 @@
2.141 lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n"
2.142 by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
2.143
2.144 -lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
2.145 -apply (rule lepoll_trans)
2.146 -apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll])
2.147 -apply (erule prod_lepoll_mono)
2.148 -apply (rule lepoll_refl)
2.149 -done
2.150 +lemma sum_lepoll_prod:
2.151 + assumes C: "2 \<lesssim> C" shows "B+B \<lesssim> C*B"
2.152 +proof -
2.153 + have "B+B \<lesssim> 2*B"
2.154 + by (simp add: sum_eq_2_times)
2.155 + also have "... \<lesssim> C*B"
2.156 + by (blast intro: prod_lepoll_mono lepoll_refl C)
2.157 + finally show "B+B \<lesssim> C*B" .
2.158 +qed
2.159
2.160 lemma lepoll_imp_sum_lepoll_prod: "[| A \<lesssim> B; 2 \<lesssim> A |] ==> A+B \<lesssim> A*B"
2.161 by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
2.162 @@ -485,17 +476,15 @@
2.163
2.164 subsubsection{*Establishing the well-ordering*}
2.165
2.166 -lemma csquare_lam_inj:
2.167 - "Ord(K) ==> (lam <x,y>:K*K. <x \<union> y, x, y>) \<in> inj(K*K, K*K*K)"
2.168 -apply (unfold inj_def)
2.169 -apply (force intro: lam_type Un_least_lt [THEN ltD] ltI)
2.170 -done
2.171 -
2.172 -lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))"
2.173 -apply (unfold csquare_rel_def)
2.174 -apply (rule csquare_lam_inj [THEN well_ord_rvimage], assumption)
2.175 -apply (blast intro: well_ord_rmult well_ord_Memrel)
2.176 -done
2.177 +lemma well_ord_csquare:
2.178 + assumes K: "Ord(K)" shows "well_ord(K*K, csquare_rel(K))"
2.179 +proof (unfold csquare_rel_def, rule well_ord_rvimage)
2.180 + show "(\<lambda>\<langle>x,y\<rangle>\<in>K \<times> K. \<langle>x \<union> y, x, y\<rangle>) \<in> inj(K \<times> K, K \<times> K \<times> K)" using K
2.181 + by (force simp add: inj_def intro: lam_type Un_least_lt [THEN ltD] ltI)
2.182 +next
2.183 + show "well_ord(K \<times> K \<times> K, rmult(K, Memrel(K), K \<times> K, rmult(K, Memrel(K), K, Memrel(K))))"
2.184 + using K by (blast intro: well_ord_rmult well_ord_Memrel)
2.185 +qed
2.186
2.187 subsubsection{*Characterising initial segments of the well-ordering*}
2.188
2.189 @@ -512,8 +501,7 @@
2.190 lemma pred_csquare_subset:
2.191 "z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) \<subseteq> succ(z)*succ(z)"
2.192 apply (unfold Order.pred_def)
2.193 -apply (safe del: SigmaI succCI)
2.194 -apply (erule csquareD [THEN conjE])
2.195 +apply (safe del: SigmaI dest!: csquareD)
2.196 apply (unfold lt_def, auto)
2.197 done
2.198
2.199 @@ -553,28 +541,36 @@
2.200 apply (blast intro!: Un_upper1_le Un_upper2_le Ord_ordermap elim!: ltE)+
2.201 done
2.202
2.203 -(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
2.204 +text{*Kunen: "each @{term"\<langle>x,y\<rangle> \<in> K \<times> K"} has no more than @{term"z \<times> z"} predecessors..." (page 29) *}
2.205 lemma ordermap_csquare_le:
2.206 - "[| Limit(K); x<K; y<K; z=succ(x \<union> y) |]
2.207 - ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| \<otimes> |succ(z)|"
2.208 -apply (unfold cmult_def)
2.209 -apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
2.210 -apply (rule Ord_cardinal [THEN well_ord_Memrel])+
2.211 -apply (subgoal_tac "z<K")
2.212 - prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ)
2.213 -apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans],
2.214 - assumption+)
2.215 -apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
2.216 -apply (erule Limit_is_Ord [THEN well_ord_csquare])
2.217 -apply (blast intro: ltD)
2.218 -apply (rule pred_csquare_subset [THEN subset_imp_lepoll, THEN lepoll_trans],
2.219 - assumption)
2.220 -apply (elim ltE)
2.221 -apply (rule prod_eqpoll_cong [THEN eqpoll_sym, THEN eqpoll_imp_lepoll])
2.222 -apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+
2.223 -done
2.224 + assumes K: "Limit(K)" and x: "x<K" and y: " y<K" and z: "z=succ(x \<union> y)"
2.225 + shows "|ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>| \<le> |succ(z)| \<otimes> |succ(z)|"
2.226 +proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)
2.227 + show "well_ord(|succ(z)| \<times> |succ(z)|,
2.228 + rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"
2.229 + by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult)
2.230 +next
2.231 + have zK: "z<K" using x y z K
2.232 + by (blast intro: Un_least_lt Limit_has_succ)
2.233 + hence oz: "Ord(z)" by (elim ltE)
2.234 + have "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> ordermap(K \<times> K, csquare_rel(K)) ` \<langle>z,z\<rangle>"
2.235 + by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y z)
2.236 + also have "... \<approx> Order.pred(K \<times> K, \<langle>z,z\<rangle>, csquare_rel(K))"
2.237 + proof (rule ordermap_eqpoll_pred)
2.238 + show "well_ord(K \<times> K, csquare_rel(K))" using K
2.239 + by (rule Limit_is_Ord [THEN well_ord_csquare])
2.240 + next
2.241 + show "\<langle>z, z\<rangle> \<in> K \<times> K" using zK
2.242 + by (blast intro: ltD)
2.243 + qed
2.244 + also have "... \<lesssim> succ(z) \<times> succ(z)" using zK
2.245 + by (rule pred_csquare_subset [THEN subset_imp_lepoll])
2.246 + also have "... \<approx> |succ(z)| \<times> |succ(z)|" using oz
2.247 + by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym)
2.248 + finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> |succ(z)| \<times> |succ(z)|" .
2.249 +qed
2.250
2.251 -(*Kunen: "... so the order type is @{text"\<le>"} K" *)
2.252 +text{*Kunen: "... so the order type is @{text"\<le>"} K" *}
2.253 lemma ordertype_csquare_le:
2.254 "[| InfCard(K); \<forall>y\<in>K. InfCard(y) \<longrightarrow> y \<otimes> y = y |]
2.255 ==> ordertype(K*K, csquare_rel(K)) \<le> K"