src/ZF/CardinalArith.thy
changeset 46901 1382bba4b7a5
parent 46841 49b91b716cbe
child 46907 eea3eb057fea
     1.1 --- a/src/ZF/CardinalArith.thy	Mon Mar 12 23:33:50 2012 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Tue Mar 13 12:04:07 2012 +0000
     1.3 @@ -63,12 +63,11 @@
     1.4    hence jls: "j \<prec> c" 
     1.5      by (simp add: lt_Card_imp_lesspoll) 
     1.6    { assume eqp: "j \<approx> \<Union>A"
     1.7 -    hence Uls: "\<Union>A \<prec> c" using jls
     1.8 -      by (blast intro: eqpoll_sym eqpoll_imp_lepoll lesspoll_trans1)
     1.9 -    moreover have  "c \<lesssim> \<Union>A" using c
    1.10 +    have  "c \<lesssim> \<Union>A" using c
    1.11        by (blast intro: subset_imp_lepoll)
    1.12 -    ultimately have "c \<prec> c"
    1.13 -      by (blast intro: lesspoll_trans1) 
    1.14 +    also have "... \<approx> j"  by (rule eqpoll_sym [OF eqp])
    1.15 +    also have "... \<prec> c"  by (rule jls)
    1.16 +    finally have "c \<prec> c" .
    1.17      hence False 
    1.18        by auto
    1.19    } thus "\<not> j \<approx> \<Union>A" by blast
    1.20 @@ -87,13 +86,6 @@
    1.21  apply (fast intro!: le_imp_lepoll ltI leI)
    1.22  done
    1.23  
    1.24 -lemma lesspoll_lemma: "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
    1.25 -apply (unfold lesspoll_def)
    1.26 -apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
    1.27 -            intro!: eqpollI elim: notE
    1.28 -            elim!: eqpollE lepoll_trans)
    1.29 -done
    1.30 -
    1.31  
    1.32  subsection{*Cardinal addition*}
    1.33  
    1.34 @@ -123,20 +115,20 @@
    1.35  apply (rule sum_assoc_bij)
    1.36  done
    1.37  
    1.38 -(*Unconditional version requires AC*)
    1.39 +text{*Unconditional version requires AC*}
    1.40  lemma well_ord_cadd_assoc:
    1.41 -    "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
    1.42 -     ==> (i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
    1.43 -apply (unfold cadd_def)
    1.44 -apply (rule cardinal_cong)
    1.45 -apply (rule eqpoll_trans)
    1.46 - apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
    1.47 - apply (blast intro: well_ord_radd )
    1.48 -apply (rule sum_assoc_eqpoll [THEN eqpoll_trans])
    1.49 -apply (rule eqpoll_sym)
    1.50 -apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
    1.51 -apply (blast intro: well_ord_radd )
    1.52 -done
    1.53 +  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
    1.54 +  shows "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
    1.55 +proof (unfold cadd_def, rule cardinal_cong)
    1.56 +  have "|i + j| + k \<approx> (i + j) + k"
    1.57 +    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 
    1.58 +  also have "...  \<approx> i + (j + k)"
    1.59 +    by (rule sum_assoc_eqpoll) 
    1.60 +  also have "...  \<approx> i + |j + k|"
    1.61 +    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym) 
    1.62 +  finally show "|i + j| + k \<approx> i + |j + k|" .
    1.63 +qed
    1.64 +
    1.65  
    1.66  subsubsection{*0 is the identity for addition*}
    1.67  
    1.68 @@ -224,7 +216,6 @@
    1.69  
    1.70  subsubsection{*Cardinal multiplication is commutative*}
    1.71  
    1.72 -(*Easier to prove the two directions separately*)
    1.73  lemma prod_commute_eqpoll: "A*B \<approx> B*A"
    1.74  apply (unfold eqpoll_def)
    1.75  apply (rule exI)
    1.76 @@ -245,20 +236,19 @@
    1.77  apply (rule prod_assoc_bij)
    1.78  done
    1.79  
    1.80 -(*Unconditional version requires AC*)
    1.81 +text{*Unconditional version requires AC*}
    1.82  lemma well_ord_cmult_assoc:
    1.83 -    "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
    1.84 -     ==> (i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
    1.85 -apply (unfold cmult_def)
    1.86 -apply (rule cardinal_cong)
    1.87 -apply (rule eqpoll_trans)
    1.88 - apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
    1.89 - apply (blast intro: well_ord_rmult)
    1.90 -apply (rule prod_assoc_eqpoll [THEN eqpoll_trans])
    1.91 -apply (rule eqpoll_sym)
    1.92 -apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
    1.93 -apply (blast intro: well_ord_rmult)
    1.94 -done
    1.95 +  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
    1.96 +  shows "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
    1.97 +proof (unfold cmult_def, rule cardinal_cong)
    1.98 +  have "|i * j| * k \<approx> (i * j) * k"
    1.99 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j) 
   1.100 +  also have "...  \<approx> i * (j * k)"
   1.101 +    by (rule prod_assoc_eqpoll) 
   1.102 +  also have "...  \<approx> i * |j * k|"
   1.103 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym) 
   1.104 +  finally show "|i * j| * k \<approx> i * |j * k|" .
   1.105 +qed
   1.106  
   1.107  subsubsection{*Cardinal multiplication distributes over addition*}
   1.108  
   1.109 @@ -269,19 +259,17 @@
   1.110  done
   1.111  
   1.112  lemma well_ord_cadd_cmult_distrib:
   1.113 -    "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
   1.114 -     ==> (i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
   1.115 -apply (unfold cadd_def cmult_def)
   1.116 -apply (rule cardinal_cong)
   1.117 -apply (rule eqpoll_trans)
   1.118 - apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
   1.119 -apply (blast intro: well_ord_radd)
   1.120 -apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans])
   1.121 -apply (rule eqpoll_sym)
   1.122 -apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll
   1.123 -                                well_ord_cardinal_eqpoll])
   1.124 -apply (blast intro: well_ord_rmult)+
   1.125 -done
   1.126 +  assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"
   1.127 +  shows "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
   1.128 +proof (unfold cadd_def cmult_def, rule cardinal_cong)
   1.129 +  have "|i + j| * k \<approx> (i + j) * k"
   1.130 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 
   1.131 +  also have "...  \<approx> i * k + j * k"
   1.132 +    by (rule sum_prod_distrib_eqpoll) 
   1.133 +  also have "...  \<approx> |i * k| + |j * k|"
   1.134 +    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym) 
   1.135 +  finally show "|i + j| * k \<approx> |i * k| + |j * k|" .
   1.136 +qed
   1.137  
   1.138  subsubsection{*Multiplication by 0 yields 0*}
   1.139  
   1.140 @@ -391,12 +379,15 @@
   1.141  lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n"
   1.142  by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
   1.143  
   1.144 -lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
   1.145 -apply (rule lepoll_trans)
   1.146 -apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll])
   1.147 -apply (erule prod_lepoll_mono)
   1.148 -apply (rule lepoll_refl)
   1.149 -done
   1.150 +lemma sum_lepoll_prod: 
   1.151 +  assumes C: "2 \<lesssim> C" shows "B+B \<lesssim> C*B"
   1.152 +proof -
   1.153 +  have "B+B \<lesssim> 2*B"
   1.154 +    by (simp add: sum_eq_2_times) 
   1.155 +  also have "... \<lesssim> C*B"
   1.156 +    by (blast intro: prod_lepoll_mono lepoll_refl C) 
   1.157 +  finally show "B+B \<lesssim> C*B" .
   1.158 +qed
   1.159  
   1.160  lemma lepoll_imp_sum_lepoll_prod: "[| A \<lesssim> B; 2 \<lesssim> A |] ==> A+B \<lesssim> A*B"
   1.161  by (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
   1.162 @@ -485,17 +476,15 @@
   1.163  
   1.164  subsubsection{*Establishing the well-ordering*}
   1.165  
   1.166 -lemma csquare_lam_inj:
   1.167 -     "Ord(K) ==> (lam <x,y>:K*K. <x \<union> y, x, y>) \<in> inj(K*K, K*K*K)"
   1.168 -apply (unfold inj_def)
   1.169 -apply (force intro: lam_type Un_least_lt [THEN ltD] ltI)
   1.170 -done
   1.171 -
   1.172 -lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))"
   1.173 -apply (unfold csquare_rel_def)
   1.174 -apply (rule csquare_lam_inj [THEN well_ord_rvimage], assumption)
   1.175 -apply (blast intro: well_ord_rmult well_ord_Memrel)
   1.176 -done
   1.177 +lemma well_ord_csquare: 
   1.178 +  assumes K: "Ord(K)" shows "well_ord(K*K, csquare_rel(K))"
   1.179 +proof (unfold csquare_rel_def, rule well_ord_rvimage)
   1.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
   1.181 +    by (force simp add: inj_def intro: lam_type Un_least_lt [THEN ltD] ltI)
   1.182 +next
   1.183 +  show "well_ord(K \<times> K \<times> K, rmult(K, Memrel(K), K \<times> K, rmult(K, Memrel(K), K, Memrel(K))))"
   1.184 +    using K by (blast intro: well_ord_rmult well_ord_Memrel)
   1.185 +qed
   1.186  
   1.187  subsubsection{*Characterising initial segments of the well-ordering*}
   1.188  
   1.189 @@ -512,8 +501,7 @@
   1.190  lemma pred_csquare_subset:
   1.191      "z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) \<subseteq> succ(z)*succ(z)"
   1.192  apply (unfold Order.pred_def)
   1.193 -apply (safe del: SigmaI succCI)
   1.194 -apply (erule csquareD [THEN conjE])
   1.195 +apply (safe del: SigmaI dest!: csquareD)
   1.196  apply (unfold lt_def, auto)
   1.197  done
   1.198  
   1.199 @@ -553,28 +541,36 @@
   1.200  apply (blast intro!: Un_upper1_le Un_upper2_le Ord_ordermap elim!: ltE)+
   1.201  done
   1.202  
   1.203 -(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
   1.204 +text{*Kunen: "each @{term"\<langle>x,y\<rangle> \<in> K \<times> K"} has no more than @{term"z \<times> z"} predecessors..." (page 29) *}
   1.205  lemma ordermap_csquare_le:
   1.206 -  "[| Limit(K);  x<K;  y<K;  z=succ(x \<union> y) |]
   1.207 -   ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| \<otimes> |succ(z)|"
   1.208 -apply (unfold cmult_def)
   1.209 -apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
   1.210 -apply (rule Ord_cardinal [THEN well_ord_Memrel])+
   1.211 -apply (subgoal_tac "z<K")
   1.212 - prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ)
   1.213 -apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans],
   1.214 -       assumption+)
   1.215 -apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
   1.216 -apply (erule Limit_is_Ord [THEN well_ord_csquare])
   1.217 -apply (blast intro: ltD)
   1.218 -apply (rule pred_csquare_subset [THEN subset_imp_lepoll, THEN lepoll_trans],
   1.219 -            assumption)
   1.220 -apply (elim ltE)
   1.221 -apply (rule prod_eqpoll_cong [THEN eqpoll_sym, THEN eqpoll_imp_lepoll])
   1.222 -apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+
   1.223 -done
   1.224 +  assumes K: "Limit(K)" and x: "x<K" and y: " y<K" and z: "z=succ(x \<union> y)"
   1.225 +  shows "|ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>| \<le> |succ(z)| \<otimes> |succ(z)|"
   1.226 +proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)
   1.227 +  show "well_ord(|succ(z)| \<times> |succ(z)|, 
   1.228 +                 rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"
   1.229 +    by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult) 
   1.230 +next
   1.231 +  have zK: "z<K" using x y z K 
   1.232 +    by (blast intro: Un_least_lt Limit_has_succ)
   1.233 +  hence oz: "Ord(z)" by (elim ltE) 
   1.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>"
   1.235 +    by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y z) 
   1.236 +  also have "... \<approx>  Order.pred(K \<times> K, \<langle>z,z\<rangle>, csquare_rel(K))"
   1.237 +    proof (rule ordermap_eqpoll_pred)
   1.238 +      show "well_ord(K \<times> K, csquare_rel(K))" using K 
   1.239 +        by (rule Limit_is_Ord [THEN well_ord_csquare])
   1.240 +    next
   1.241 +      show "\<langle>z, z\<rangle> \<in> K \<times> K" using zK
   1.242 +        by (blast intro: ltD)
   1.243 +    qed
   1.244 +  also have "...  \<lesssim> succ(z) \<times> succ(z)" using zK
   1.245 +    by (rule pred_csquare_subset [THEN subset_imp_lepoll])
   1.246 +  also have "... \<approx> |succ(z)| \<times> |succ(z)|" using oz
   1.247 +    by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym) 
   1.248 +  finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> |succ(z)| \<times> |succ(z)|" .
   1.249 +qed
   1.250  
   1.251 -(*Kunen: "... so the order type is @{text"\<le>"} K" *)
   1.252 +text{*Kunen: "... so the order type is @{text"\<le>"} K" *}
   1.253  lemma ordertype_csquare_le:
   1.254       "[| InfCard(K);  \<forall>y\<in>K. InfCard(y) \<longrightarrow> y \<otimes> y = y |]
   1.255        ==> ordertype(K*K, csquare_rel(K)) \<le> K"