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.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.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.97 -  ultimately show "K \<le> |K + L|"
1.98 -    by (blast intro: le_trans)
1.100 +  ultimately show "K \<le> |K + L|"
1.101 +    by (blast intro: le_trans)
1.102  qed
1.103
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.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.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.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.179  done
1.180 @@ -389,13 +389,13 @@
1.181  lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n"
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.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.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.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