src/ZF/CardinalArith.thy
changeset 46953 2b6e55924af3
parent 46952 5e1bcfdcb175
child 47101 ded5cc757bc9
     1.1 --- a/src/ZF/CardinalArith.thy	Thu Mar 15 15:54:22 2012 +0000
     1.2 +++ b/src/ZF/CardinalArith.thy	Thu Mar 15 16:35:02 2012 +0000
     1.3 @@ -31,7 +31,7 @@
     1.4      --{*This def is more complex than Kunen's but it more easily proved to
     1.5          be a cardinal*}
     1.6      "jump_cardinal(K) ==
     1.7 -         \<Union>X\<in>Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
     1.8 +         \<Union>X\<in>Pow(K). {z. r \<in> Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
     1.9  
    1.10  definition
    1.11    csucc         :: "i=>i"  where
    1.12 @@ -48,10 +48,10 @@
    1.13    cmult  (infixl "\<otimes>" 70)
    1.14  
    1.15  
    1.16 -lemma Card_Union [simp,intro,TC]: 
    1.17 +lemma Card_Union [simp,intro,TC]:
    1.18    assumes A: "\<And>x. x\<in>A \<Longrightarrow> Card(x)" shows "Card(\<Union>(A))"
    1.19  proof (rule CardI)
    1.20 -  show "Ord(\<Union>A)" using A 
    1.21 +  show "Ord(\<Union>A)" using A
    1.22      by (simp add: Card_is_Ord)
    1.23  next
    1.24    fix j
    1.25 @@ -60,24 +60,24 @@
    1.26      by (auto simp add: lt_def intro: Card_is_Ord)
    1.27    then obtain c where c: "c\<in>A" "j < c" "Card(c)"
    1.28      by blast
    1.29 -  hence jls: "j \<prec> c" 
    1.30 -    by (simp add: lt_Card_imp_lesspoll) 
    1.31 +  hence jls: "j \<prec> c"
    1.32 +    by (simp add: lt_Card_imp_lesspoll)
    1.33    { assume eqp: "j \<approx> \<Union>A"
    1.34      have  "c \<lesssim> \<Union>A" using c
    1.35        by (blast intro: subset_imp_lepoll)
    1.36      also have "... \<approx> j"  by (rule eqpoll_sym [OF eqp])
    1.37      also have "... \<prec> c"  by (rule jls)
    1.38      finally have "c \<prec> c" .
    1.39 -    hence False 
    1.40 +    hence False
    1.41        by auto
    1.42    } thus "\<not> j \<approx> \<Union>A" by blast
    1.43  qed
    1.44  
    1.45 -lemma Card_UN: "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))"
    1.46 +lemma Card_UN: "(!!x. x \<in> A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))"
    1.47    by blast
    1.48  
    1.49  lemma Card_OUN [simp,intro,TC]:
    1.50 -     "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"
    1.51 +     "(!!x. x \<in> A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"
    1.52    by (auto simp add: OUnion_def Card_0)
    1.53  
    1.54  lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
    1.55 @@ -99,7 +99,7 @@
    1.56  lemma sum_commute_eqpoll: "A+B \<approx> B+A"
    1.57  proof (unfold eqpoll_def, rule exI)
    1.58    show "(\<lambda>z\<in>A+B. case(Inr,Inl,z)) \<in> bij(A+B, B+A)"
    1.59 -    by (auto intro: lam_bijective [where d = "case(Inr,Inl)"]) 
    1.60 +    by (auto intro: lam_bijective [where d = "case(Inr,Inl)"])
    1.61  qed
    1.62  
    1.63  lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
    1.64 @@ -121,11 +121,11 @@
    1.65    shows "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
    1.66  proof (unfold cadd_def, rule cardinal_cong)
    1.67    have "|i + j| + k \<approx> (i + j) + k"
    1.68 -    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 
    1.69 +    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j)
    1.70    also have "...  \<approx> i + (j + k)"
    1.71 -    by (rule sum_assoc_eqpoll) 
    1.72 +    by (rule sum_assoc_eqpoll)
    1.73    also have "...  \<approx> i + |j + k|"
    1.74 -    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym) 
    1.75 +    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym)
    1.76    finally show "|i + j| + k \<approx> i + |j + k|" .
    1.77  qed
    1.78  
    1.79 @@ -148,7 +148,7 @@
    1.80  lemma sum_lepoll_self: "A \<lesssim> A+B"
    1.81  proof (unfold lepoll_def, rule exI)
    1.82    show "(\<lambda>x\<in>A. Inl (x)) \<in> inj(A, A + B)"
    1.83 -    by (simp add: inj_def) 
    1.84 +    by (simp add: inj_def)
    1.85  qed
    1.86  
    1.87  (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
    1.88 @@ -157,12 +157,12 @@
    1.89    assumes K: "Card(K)" and L: "Ord(L)" shows "K \<le> (K \<oplus> L)"
    1.90  proof (unfold cadd_def)
    1.91    have "K \<le> |K|"
    1.92 -    by (rule Card_cardinal_le [OF K]) 
    1.93 +    by (rule Card_cardinal_le [OF K])
    1.94    moreover have "|K| \<le> |K + L|" using K L
    1.95      by (blast intro: well_ord_lepoll_imp_Card_le sum_lepoll_self
    1.96 -                     well_ord_radd well_ord_Memrel Card_is_Ord) 
    1.97 -  ultimately show "K \<le> |K + L|" 
    1.98 -    by (blast intro: le_trans) 
    1.99 +                     well_ord_radd well_ord_Memrel Card_is_Ord)
   1.100 +  ultimately show "K \<le> |K + L|"
   1.101 +    by (blast intro: le_trans)
   1.102  qed
   1.103  
   1.104  subsubsection{*Monotonicity of addition*}
   1.105 @@ -197,7 +197,7 @@
   1.106  apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+
   1.107  done
   1.108  
   1.109 -(*Pulling the  succ(...)  outside the |...| requires m, n: nat  *)
   1.110 +(*Pulling the  succ(...)  outside the |...| requires m, n \<in> nat  *)
   1.111  (*Unconditional version requires AC*)
   1.112  lemma cadd_succ_lemma:
   1.113    assumes "Ord(m)" "Ord(n)" shows "succ(m) \<oplus> n = |succ(m \<oplus> n)|"
   1.114 @@ -206,14 +206,14 @@
   1.115      by (blast intro: eqpoll_sym well_ord_cardinal_eqpoll well_ord_radd well_ord_Memrel)
   1.116  
   1.117    have "|succ(m) + n| = |succ(m + n)|"
   1.118 -    by (rule sum_succ_eqpoll [THEN cardinal_cong]) 
   1.119 -  also have "... = |succ(|m + n|)|" 
   1.120 +    by (rule sum_succ_eqpoll [THEN cardinal_cong])
   1.121 +  also have "... = |succ(|m + n|)|"
   1.122      by (blast intro: succ_eqpoll_cong cardinal_cong)
   1.123    finally show "|succ(m) + n| = |succ(|m + n|)|" .
   1.124  qed
   1.125  
   1.126  lemma nat_cadd_eq_add:
   1.127 -  assumes m: "m: nat" and [simp]: "n: nat" shows"m \<oplus> n = m #+ n"
   1.128 +  assumes m: "m \<in> nat" and [simp]: "n \<in> nat" shows"m \<oplus> n = m #+ n"
   1.129  using m
   1.130  proof (induct m)
   1.131    case 0 thus ?case by (simp add: nat_into_Card cadd_0)
   1.132 @@ -252,11 +252,11 @@
   1.133    shows "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
   1.134  proof (unfold cmult_def, rule cardinal_cong)
   1.135    have "|i * j| * k \<approx> (i * j) * k"
   1.136 -    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j) 
   1.137 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j)
   1.138    also have "...  \<approx> i * (j * k)"
   1.139 -    by (rule prod_assoc_eqpoll) 
   1.140 +    by (rule prod_assoc_eqpoll)
   1.141    also have "...  \<approx> i * |j * k|"
   1.142 -    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym) 
   1.143 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym)
   1.144    finally show "|i * j| * k \<approx> i * |j * k|" .
   1.145  qed
   1.146  
   1.147 @@ -273,11 +273,11 @@
   1.148    shows "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
   1.149  proof (unfold cadd_def cmult_def, rule cardinal_cong)
   1.150    have "|i + j| * k \<approx> (i + j) * k"
   1.151 -    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 
   1.152 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j)
   1.153    also have "...  \<approx> i * k + j * k"
   1.154 -    by (rule sum_prod_distrib_eqpoll) 
   1.155 +    by (rule sum_prod_distrib_eqpoll)
   1.156    also have "...  \<approx> |i * k| + |j * k|"
   1.157 -    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym) 
   1.158 +    by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym)
   1.159    finally show "|i + j| * k \<approx> |i * k| + |j * k|" .
   1.160  qed
   1.161  
   1.162 @@ -324,7 +324,7 @@
   1.163  
   1.164  subsubsection{*Multiplication by a non-zero cardinal*}
   1.165  
   1.166 -lemma prod_lepoll_self: "b: B ==> A \<lesssim> A*B"
   1.167 +lemma prod_lepoll_self: "b \<in> B ==> A \<lesssim> A*B"
   1.168  apply (unfold lepoll_def inj_def)
   1.169  apply (rule_tac x = "\<lambda>x\<in>A. <x,b>" in exI, simp)
   1.170  done
   1.171 @@ -381,7 +381,7 @@
   1.172  apply (blast intro: well_ord_rmult well_ord_Memrel)
   1.173  done
   1.174  
   1.175 -lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m \<otimes> n = m#*n"
   1.176 +lemma nat_cmult_eq_mult: "[| m \<in> nat;  n \<in> nat |] ==> m \<otimes> n = m#*n"
   1.177  apply (induct_tac m)
   1.178  apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add)
   1.179  done
   1.180 @@ -389,13 +389,13 @@
   1.181  lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n"
   1.182  by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
   1.183  
   1.184 -lemma sum_lepoll_prod: 
   1.185 +lemma sum_lepoll_prod:
   1.186    assumes C: "2 \<lesssim> C" shows "B+B \<lesssim> C*B"
   1.187  proof -
   1.188    have "B+B \<lesssim> 2*B"
   1.189 -    by (simp add: sum_eq_2_times) 
   1.190 +    by (simp add: sum_eq_2_times)
   1.191    also have "... \<lesssim> C*B"
   1.192 -    by (blast intro: prod_lepoll_mono lepoll_refl C) 
   1.193 +    by (blast intro: prod_lepoll_mono lepoll_refl C)
   1.194    finally show "B+B \<lesssim> C*B" .
   1.195  qed
   1.196  
   1.197 @@ -407,18 +407,18 @@
   1.198  
   1.199  (*This proof is modelled upon one assuming nat<=A, with injection
   1.200    \<lambda>z\<in>cons(u,A). if z=u then 0 else if z \<in> nat then succ(z) else z
   1.201 -  and inverse %y. if y:nat then nat_case(u, %z. z, y) else y.  \
   1.202 -  If f: inj(nat,A) then range(f) behaves like the natural numbers.*)
   1.203 +  and inverse %y. if y \<in> nat then nat_case(u, %z. z, y) else y.  \
   1.204 +  If f \<in> inj(nat,A) then range(f) behaves like the natural numbers.*)
   1.205  lemma nat_cons_lepoll: "nat \<lesssim> A ==> cons(u,A) \<lesssim> A"
   1.206  apply (unfold lepoll_def)
   1.207  apply (erule exE)
   1.208  apply (rule_tac x =
   1.209            "\<lambda>z\<in>cons (u,A).
   1.210               if z=u then f`0
   1.211 -             else if z: range (f) then f`succ (converse (f) `z) else z"
   1.212 +             else if z \<in> range (f) then f`succ (converse (f) `z) else z"
   1.213         in exI)
   1.214  apply (rule_tac d =
   1.215 -          "%y. if y: range(f) then nat_case (u, %z. f`z, converse(f) `y)
   1.216 +          "%y. if y \<in> range(f) then nat_case (u, %z. f`z, converse(f) `y)
   1.217                                else y"
   1.218         in lam_injective)
   1.219  apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun)
   1.220 @@ -475,7 +475,7 @@
   1.221  
   1.222  (*A general fact about ordermap*)
   1.223  lemma ordermap_eqpoll_pred:
   1.224 -    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
   1.225 +    "[| well_ord(A,r);  x \<in> A |] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
   1.226  apply (unfold eqpoll_def)
   1.227  apply (rule exI)
   1.228  apply (simp add: ordermap_eq_image well_ord_is_wf)
   1.229 @@ -486,7 +486,7 @@
   1.230  
   1.231  subsubsection{*Establishing the well-ordering*}
   1.232  
   1.233 -lemma well_ord_csquare: 
   1.234 +lemma well_ord_csquare:
   1.235    assumes K: "Ord(K)" shows "well_ord(K*K, csquare_rel(K))"
   1.236  proof (unfold csquare_rel_def, rule well_ord_rvimage)
   1.237    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.238 @@ -553,23 +553,23 @@
   1.239  
   1.240  text{*Kunen: "each @{term"\<langle>x,y\<rangle> \<in> K \<times> K"} has no more than @{term"z \<times> z"} predecessors..." (page 29) *}
   1.241  lemma ordermap_csquare_le:
   1.242 -  assumes K: "Limit(K)" and x: "x<K" and y: " y<K" 
   1.243 +  assumes K: "Limit(K)" and x: "x<K" and y: " y<K"
   1.244    defines "z \<equiv> succ(x \<union> y)"
   1.245    shows "|ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>| \<le> |succ(z)| \<otimes> |succ(z)|"
   1.246  proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)
   1.247 -  show "well_ord(|succ(z)| \<times> |succ(z)|, 
   1.248 +  show "well_ord(|succ(z)| \<times> |succ(z)|,
   1.249                   rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"
   1.250 -    by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult) 
   1.251 +    by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult)
   1.252  next
   1.253    have zK: "z<K" using x y K z_def
   1.254      by (blast intro: Un_least_lt Limit_has_succ)
   1.255 -  hence oz: "Ord(z)" by (elim ltE) 
   1.256 +  hence oz: "Ord(z)" by (elim ltE)
   1.257    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.258      using z_def
   1.259 -    by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y) 
   1.260 +    by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y)
   1.261    also have "... \<approx>  Order.pred(K \<times> K, \<langle>z,z\<rangle>, csquare_rel(K))"
   1.262      proof (rule ordermap_eqpoll_pred)
   1.263 -      show "well_ord(K \<times> K, csquare_rel(K))" using K 
   1.264 +      show "well_ord(K \<times> K, csquare_rel(K))" using K
   1.265          by (rule Limit_is_Ord [THEN well_ord_csquare])
   1.266      next
   1.267        show "\<langle>z, z\<rangle> \<in> K \<times> K" using zK
   1.268 @@ -578,7 +578,7 @@
   1.269    also have "...  \<lesssim> succ(z) \<times> succ(z)" using zK
   1.270      by (rule pred_csquare_subset [THEN subset_imp_lepoll])
   1.271    also have "... \<approx> |succ(z)| \<times> |succ(z)|" using oz
   1.272 -    by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym) 
   1.273 +    by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym)
   1.274    finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> |succ(z)| \<times> |succ(z)|" .
   1.275  qed
   1.276  
   1.277 @@ -587,8 +587,8 @@
   1.278    assumes IK: "InfCard(K)" and eq: "\<And>y. y\<in>K \<Longrightarrow> InfCard(y) \<Longrightarrow> y \<otimes> y = y"
   1.279    shows "ordertype(K*K, csquare_rel(K)) \<le> K"
   1.280  proof -
   1.281 -  have  CK: "Card(K)" using IK by (rule InfCard_is_Card) 
   1.282 -  hence OK: "Ord(K)"  by (rule Card_is_Ord) 
   1.283 +  have  CK: "Card(K)" using IK by (rule InfCard_is_Card)
   1.284 +  hence OK: "Ord(K)"  by (rule Card_is_Ord)
   1.285    moreover have "Ord(ordertype(K \<times> K, csquare_rel(K)))" using OK
   1.286      by (rule well_ord_csquare [THEN Ord_ordertype])
   1.287    ultimately show ?thesis
   1.288 @@ -596,18 +596,18 @@
   1.289      fix i
   1.290      assume i: "i < ordertype(K \<times> K, csquare_rel(K))"
   1.291      hence Oi: "Ord(i)" by (elim ltE)
   1.292 -    obtain x y where x: "x \<in> K" and y: "y \<in> K" 
   1.293 +    obtain x y where x: "x \<in> K" and y: "y \<in> K"
   1.294                   and ieq: "i = ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>"
   1.295        using i by (auto simp add: ordertype_unfold elim: ltE)
   1.296 -    hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK 
   1.297 +    hence xy: "Ord(x)" "Ord(y)" "x < K" "y < K" using OK
   1.298        by (blast intro: Ord_in_Ord ltI)+
   1.299      hence ou: "Ord(x \<union> y)"
   1.300 -      by (simp add: Ord_Un) 
   1.301 +      by (simp add: Ord_Un)
   1.302      show "i < K"
   1.303        proof (rule Card_lt_imp_lt [OF _ Oi CK])
   1.304          have "|i| \<le> |succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))|" using IK xy
   1.305            by (auto simp add: ieq intro: InfCard_is_Limit [THEN ordermap_csquare_le])
   1.306 -        moreover have "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| < K" 
   1.307 +        moreover have "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| < K"
   1.308            proof (cases rule: Ord_linear2 [OF ou Ord_nat])
   1.309              assume "x \<union> y < nat"
   1.310              hence "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| \<in> nat"
   1.311 @@ -615,46 +615,46 @@
   1.312                           nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
   1.313              also have "... \<subseteq> K" using IK
   1.314                by (simp add: InfCard_def le_imp_subset)
   1.315 -            finally show "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| < K" 
   1.316 -              by (simp add: ltI OK) 
   1.317 +            finally show "|succ(succ(x \<union> y))| \<otimes> |succ(succ(x \<union> y))| < K"
   1.318 +              by (simp add: ltI OK)
   1.319            next
   1.320              assume natxy: "nat \<le> x \<union> y"
   1.321 -            hence seq: "|succ(succ(x \<union> y))| = |x \<union> y|" using xy 
   1.322 +            hence seq: "|succ(succ(x \<union> y))| = |x \<union> y|" using xy
   1.323                by (simp add: le_imp_subset nat_succ_eqpoll [THEN cardinal_cong] le_succ_iff)
   1.324 -            also have "... < K" using xy  
   1.325 +            also have "... < K" using xy
   1.326                by (simp add: Un_least_lt Ord_cardinal_le [THEN lt_trans1])
   1.327              finally have "|succ(succ(x \<union> y))| < K" .
   1.328              moreover have "InfCard(|succ(succ(x \<union> y))|)" using xy natxy
   1.329                by (simp add: seq InfCard_def Card_cardinal nat_le_cardinal)
   1.330 -            ultimately show ?thesis  by (simp add: eq ltD) 
   1.331 +            ultimately show ?thesis  by (simp add: eq ltD)
   1.332            qed
   1.333 -        ultimately show "|i| < K" by (blast intro: lt_trans1) 
   1.334 +        ultimately show "|i| < K" by (blast intro: lt_trans1)
   1.335      qed
   1.336    qed
   1.337  qed
   1.338  
   1.339  (*Main result: Kunen's Theorem 10.12*)
   1.340 -lemma InfCard_csquare_eq: 
   1.341 +lemma InfCard_csquare_eq:
   1.342    assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
   1.343  proof -
   1.344 -  have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) 
   1.345 +  have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card)
   1.346    show "InfCard(K) ==> K \<otimes> K = K" using OK
   1.347    proof (induct rule: trans_induct)
   1.348      case (step i)
   1.349      show "i \<otimes> i = i"
   1.350      proof (rule le_anti_sym)
   1.351 -      have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
   1.352 -        by (rule cardinal_cong, 
   1.353 +      have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|"
   1.354 +        by (rule cardinal_cong,
   1.355            simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
   1.356 -      hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" 
   1.357 +      hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))"
   1.358          by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
   1.359        moreover
   1.360        have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step
   1.361 -        by (simp add: ordertype_csquare_le) 
   1.362 +        by (simp add: ordertype_csquare_le)
   1.363        ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
   1.364      next
   1.365        show "i \<le> i \<otimes> i" using step
   1.366 -        by (blast intro: cmult_square_le InfCard_is_Card) 
   1.367 +        by (blast intro: cmult_square_le InfCard_is_Card)
   1.368      qed
   1.369    qed
   1.370  qed
   1.371 @@ -664,7 +664,7 @@
   1.372    assumes r: "well_ord(A,r)" and I: "InfCard(|A|)" shows "A \<times> A \<approx> A"
   1.373  proof -
   1.374    have "A \<times> A \<approx> |A| \<times> |A|"
   1.375 -    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_sym r) 
   1.376 +    by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_sym r)
   1.377    also have "... \<approx> A"
   1.378      proof (rule well_ord_cardinal_eqE [OF _ r])
   1.379        show "well_ord(|A| \<times> |A|, rmult(|A|, Memrel(|A|), |A|, Memrel(|A|)))"
   1.380 @@ -672,7 +672,7 @@
   1.381      next
   1.382        show "||A| \<times> |A|| = |A|" using InfCard_csquare_eq I
   1.383          by (simp add: cmult_def)
   1.384 -    qed    
   1.385 +    qed
   1.386    finally show ?thesis .
   1.387  qed
   1.388  
   1.389 @@ -842,21 +842,21 @@
   1.390    { fix X
   1.391      have "Finite(X) ==> a \<notin> X \<Longrightarrow> cons(a,X) \<lesssim> X \<Longrightarrow> False"
   1.392        proof (induct X rule: Finite_induct)
   1.393 -        case 0 thus False  by (simp add: lepoll_0_iff) 
   1.394 +        case 0 thus False  by (simp add: lepoll_0_iff)
   1.395        next
   1.396 -        case (cons x Y) 
   1.397 -        hence "cons(x, cons(a, Y)) \<lesssim> cons(x, Y)" by (simp add: cons_commute) 
   1.398 +        case (cons x Y)
   1.399 +        hence "cons(x, cons(a, Y)) \<lesssim> cons(x, Y)" by (simp add: cons_commute)
   1.400          hence "cons(a, Y) \<lesssim> Y" using cons        by (blast dest: cons_lepoll_consD)
   1.401          thus False using cons by auto
   1.402        qed
   1.403 -  } 
   1.404 +  }
   1.405    hence [simp]: "~ cons(a,A) \<lesssim> A" using a FA by auto
   1.406    have [simp]: "|A| \<approx> A" using Finite_imp_well_ord [OF FA]
   1.407      by (blast intro: well_ord_cardinal_eqpoll)
   1.408 -  have "(\<mu> i. i \<approx> cons(a, A)) = succ(|A|)" 
   1.409 +  have "(\<mu> i. i \<approx> cons(a, A)) = succ(|A|)"
   1.410      proof (rule Least_equality [OF _ _ notI])
   1.411 -      show "succ(|A|) \<approx> cons(a, A)" 
   1.412 -        by (simp add: succ_def cons_eqpoll_cong mem_not_refl a) 
   1.413 +      show "succ(|A|) \<approx> cons(a, A)"
   1.414 +        by (simp add: succ_def cons_eqpoll_cong mem_not_refl a)
   1.415      next
   1.416        show "Ord(succ(|A|))" by simp
   1.417      next
   1.418 @@ -868,17 +868,17 @@
   1.419        finally have "cons(a, A) \<lesssim> A" .
   1.420        thus False by simp
   1.421      qed
   1.422 -  thus ?thesis by (simp add: cardinal_def) 
   1.423 +  thus ?thesis by (simp add: cardinal_def)
   1.424  qed
   1.425  
   1.426  lemma Finite_imp_succ_cardinal_Diff:
   1.427 -     "[| Finite(A);  a:A |] ==> succ(|A-{a}|) = |A|"
   1.428 +     "[| Finite(A);  a \<in> A |] ==> succ(|A-{a}|) = |A|"
   1.429  apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
   1.430  apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
   1.431  apply (simp add: cons_Diff)
   1.432  done
   1.433  
   1.434 -lemma Finite_imp_cardinal_Diff: "[| Finite(A);  a:A |] ==> |A-{a}| < |A|"
   1.435 +lemma Finite_imp_cardinal_Diff: "[| Finite(A);  a \<in> A |] ==> |A-{a}| < |A|"
   1.436  apply (rule succ_leE)
   1.437  apply (simp add: Finite_imp_succ_cardinal_Diff)
   1.438  done
   1.439 @@ -922,11 +922,11 @@
   1.440  
   1.441  lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel]
   1.442  
   1.443 -lemma nat_sum_eqpoll_sum: 
   1.444 +lemma nat_sum_eqpoll_sum:
   1.445    assumes m: "m \<in> nat" and n: "n \<in> nat" shows "m + n \<approx> m #+ n"
   1.446  proof -
   1.447    have "m + n \<approx> |m+n|" using m n
   1.448 -    by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_eqpoll eqpoll_sym) 
   1.449 +    by (blast intro: nat_implies_well_ord well_ord_radd well_ord_cardinal_eqpoll eqpoll_sym)
   1.450    also have "... = m #+ n" using m n
   1.451      by (simp add: nat_cadd_eq_add [symmetric] cadd_def)
   1.452    finally show ?thesis .