src/ZF/CardinalArith.thy
changeset 13216 6104bd4088a2
parent 13161 a40db0418145
child 13221 e29378f347e4
     1.1 --- a/src/ZF/CardinalArith.thy	Sat Jun 15 22:57:33 2002 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Sun Jun 16 11:58:54 2002 +0200
     1.3 @@ -3,7 +3,12 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -Cardinal Arithmetic
     1.8 +Cardinal arithmetic -- WITHOUT the Axiom of Choice
     1.9 +
    1.10 +Note: Could omit proving the algebraic laws for cardinal addition and
    1.11 +multiplication.  On finite cardinals these operations coincide with
    1.12 +addition and multiplication of natural numbers; on infinite cardinals they
    1.13 +coincide with union (maximum).  Either way we get most laws for free.
    1.14  *)
    1.15  
    1.16  theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
    1.17 @@ -123,7 +128,7 @@
    1.18  apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 
    1.19  apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
    1.20  apply (drule lesspoll_trans1, assumption) 
    1.21 -apply (subgoal_tac "B lepoll \<Union>A")
    1.22 +apply (subgoal_tac "B \<lesssim> \<Union>A")
    1.23   apply (drule lesspoll_trans1, assumption, blast) 
    1.24  apply (blast intro: subset_imp_lepoll) 
    1.25  done
    1.26 @@ -192,4 +197,985 @@
    1.27  apply (blast intro: eqpoll_trans eqpoll_sym) 
    1.28  done
    1.29  
    1.30 +
    1.31 +(*** Cardinal addition ***)
    1.32 +
    1.33 +(** Cardinal addition is commutative **)
    1.34 +
    1.35 +lemma sum_commute_eqpoll: "A+B \<approx> B+A"
    1.36 +apply (unfold eqpoll_def)
    1.37 +apply (rule exI)
    1.38 +apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective)
    1.39 +apply auto
    1.40 +done
    1.41 +
    1.42 +lemma cadd_commute: "i |+| j = j |+| i"
    1.43 +apply (unfold cadd_def)
    1.44 +apply (rule sum_commute_eqpoll [THEN cardinal_cong])
    1.45 +done
    1.46 +
    1.47 +(** Cardinal addition is associative **)
    1.48 +
    1.49 +lemma sum_assoc_eqpoll: "(A+B)+C \<approx> A+(B+C)"
    1.50 +apply (unfold eqpoll_def)
    1.51 +apply (rule exI)
    1.52 +apply (rule sum_assoc_bij)
    1.53 +done
    1.54 +
    1.55 +(*Unconditional version requires AC*)
    1.56 +lemma well_ord_cadd_assoc: 
    1.57 +    "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
    1.58 +     ==> (i |+| j) |+| k = i |+| (j |+| k)"
    1.59 +apply (unfold cadd_def)
    1.60 +apply (rule cardinal_cong)
    1.61 +apply (rule eqpoll_trans)
    1.62 + apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
    1.63 + apply (blast intro: well_ord_radd elim:) 
    1.64 +apply (rule sum_assoc_eqpoll [THEN eqpoll_trans])
    1.65 +apply (rule eqpoll_sym)
    1.66 +apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
    1.67 +apply (blast intro: well_ord_radd elim:) 
    1.68 +done
    1.69 +
    1.70 +(** 0 is the identity for addition **)
    1.71 +
    1.72 +lemma sum_0_eqpoll: "0+A \<approx> A"
    1.73 +apply (unfold eqpoll_def)
    1.74 +apply (rule exI)
    1.75 +apply (rule bij_0_sum)
    1.76 +done
    1.77 +
    1.78 +lemma cadd_0 [simp]: "Card(K) ==> 0 |+| K = K"
    1.79 +apply (unfold cadd_def)
    1.80 +apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
    1.81 +done
    1.82 +
    1.83 +(** Addition by another cardinal **)
    1.84 +
    1.85 +lemma sum_lepoll_self: "A \<lesssim> A+B"
    1.86 +apply (unfold lepoll_def inj_def)
    1.87 +apply (rule_tac x = "lam x:A. Inl (x) " in exI)
    1.88 +apply (simp (no_asm_simp))
    1.89 +done
    1.90 +
    1.91 +(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
    1.92 +
    1.93 +lemma cadd_le_self: 
    1.94 +    "[| Card(K);  Ord(L) |] ==> K le (K |+| L)"
    1.95 +apply (unfold cadd_def)
    1.96 +apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
    1.97 +apply assumption; 
    1.98 +apply (rule_tac [2] sum_lepoll_self)
    1.99 +apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord)
   1.100 +done
   1.101 +
   1.102 +(** Monotonicity of addition **)
   1.103 +
   1.104 +lemma sum_lepoll_mono: 
   1.105 +     "[| A \<lesssim> C;  B \<lesssim> D |] ==> A + B  \<lesssim>  C + D"
   1.106 +apply (unfold lepoll_def)
   1.107 +apply (elim exE);
   1.108 +apply (rule_tac x = "lam z:A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI)
   1.109 +apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) `y))"
   1.110 +       in lam_injective)
   1.111 +apply (typecheck add: inj_is_fun)
   1.112 +apply auto
   1.113 +done
   1.114 +
   1.115 +lemma cadd_le_mono:
   1.116 +    "[| K' le K;  L' le L |] ==> (K' |+| L') le (K |+| L)"
   1.117 +apply (unfold cadd_def)
   1.118 +apply (safe dest!: le_subset_iff [THEN iffD1])
   1.119 +apply (rule well_ord_lepoll_imp_Card_le)
   1.120 +apply (blast intro: well_ord_radd well_ord_Memrel)
   1.121 +apply (blast intro: sum_lepoll_mono subset_imp_lepoll)
   1.122 +done
   1.123 +
   1.124 +(** Addition of finite cardinals is "ordinary" addition **)
   1.125 +
   1.126 +(*????????????????upair.ML*)
   1.127 +lemma eq_imp_not_mem: "a=A ==> a ~: A"
   1.128 +apply (blast intro: elim: mem_irrefl); 
   1.129 +done
   1.130 +
   1.131 +lemma sum_succ_eqpoll: "succ(A)+B \<approx> succ(A+B)"
   1.132 +apply (unfold eqpoll_def)
   1.133 +apply (rule exI)
   1.134 +apply (rule_tac c = "%z. if z=Inl (A) then A+B else z" 
   1.135 +            and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective)
   1.136 +   apply (simp_all)
   1.137 +apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+
   1.138 +done
   1.139 +
   1.140 +(*Pulling the  succ(...)  outside the |...| requires m, n: nat  *)
   1.141 +(*Unconditional version requires AC*)
   1.142 +lemma cadd_succ_lemma:
   1.143 +    "[| Ord(m);  Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"
   1.144 +apply (unfold cadd_def)
   1.145 +apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans])
   1.146 +apply (rule succ_eqpoll_cong [THEN cardinal_cong])
   1.147 +apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym])
   1.148 +apply (blast intro: well_ord_radd well_ord_Memrel)
   1.149 +done
   1.150 +
   1.151 +lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m |+| n = m#+n"
   1.152 +apply (induct_tac "m")
   1.153 +apply (simp add: nat_into_Card [THEN cadd_0])
   1.154 +apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq])
   1.155 +done
   1.156 +
   1.157 +
   1.158 +(*** Cardinal multiplication ***)
   1.159 +
   1.160 +(** Cardinal multiplication is commutative **)
   1.161 +
   1.162 +(*Easier to prove the two directions separately*)
   1.163 +lemma prod_commute_eqpoll: "A*B \<approx> B*A"
   1.164 +apply (unfold eqpoll_def)
   1.165 +apply (rule exI)
   1.166 +apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective)
   1.167 +apply (auto ); 
   1.168 +done
   1.169 +
   1.170 +lemma cmult_commute: "i |*| j = j |*| i"
   1.171 +apply (unfold cmult_def)
   1.172 +apply (rule prod_commute_eqpoll [THEN cardinal_cong])
   1.173 +done
   1.174 +
   1.175 +(** Cardinal multiplication is associative **)
   1.176 +
   1.177 +lemma prod_assoc_eqpoll: "(A*B)*C \<approx> A*(B*C)"
   1.178 +apply (unfold eqpoll_def)
   1.179 +apply (rule exI)
   1.180 +apply (rule prod_assoc_bij)
   1.181 +done
   1.182 +
   1.183 +(*Unconditional version requires AC*)
   1.184 +lemma well_ord_cmult_assoc:
   1.185 +    "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
   1.186 +     ==> (i |*| j) |*| k = i |*| (j |*| k)"
   1.187 +apply (unfold cmult_def)
   1.188 +apply (rule cardinal_cong)
   1.189 +apply (rule eqpoll_trans); 
   1.190 + apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
   1.191 + apply (blast intro: well_ord_rmult)
   1.192 +apply (rule prod_assoc_eqpoll [THEN eqpoll_trans])
   1.193 +apply (rule eqpoll_sym); 
   1.194 +apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
   1.195 +apply (blast intro: well_ord_rmult)
   1.196 +done
   1.197 +
   1.198 +(** Cardinal multiplication distributes over addition **)
   1.199 +
   1.200 +lemma sum_prod_distrib_eqpoll: "(A+B)*C \<approx> (A*C)+(B*C)"
   1.201 +apply (unfold eqpoll_def)
   1.202 +apply (rule exI)
   1.203 +apply (rule sum_prod_distrib_bij)
   1.204 +done
   1.205 +
   1.206 +lemma well_ord_cadd_cmult_distrib:
   1.207 +    "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
   1.208 +     ==> (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
   1.209 +apply (unfold cadd_def cmult_def)
   1.210 +apply (rule cardinal_cong)
   1.211 +apply (rule eqpoll_trans); 
   1.212 + apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
   1.213 +apply (blast intro: well_ord_radd)
   1.214 +apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans])
   1.215 +apply (rule eqpoll_sym); 
   1.216 +apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll 
   1.217 +                                well_ord_cardinal_eqpoll])
   1.218 +apply (blast intro: well_ord_rmult)+
   1.219 +done
   1.220 +
   1.221 +(** Multiplication by 0 yields 0 **)
   1.222 +
   1.223 +lemma prod_0_eqpoll: "0*A \<approx> 0"
   1.224 +apply (unfold eqpoll_def)
   1.225 +apply (rule exI)
   1.226 +apply (rule lam_bijective)
   1.227 +apply safe
   1.228 +done
   1.229 +
   1.230 +lemma cmult_0 [simp]: "0 |*| i = 0"
   1.231 +apply (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])
   1.232 +done
   1.233 +
   1.234 +(** 1 is the identity for multiplication **)
   1.235 +
   1.236 +lemma prod_singleton_eqpoll: "{x}*A \<approx> A"
   1.237 +apply (unfold eqpoll_def)
   1.238 +apply (rule exI)
   1.239 +apply (rule singleton_prod_bij [THEN bij_converse_bij])
   1.240 +done
   1.241 +
   1.242 +lemma cmult_1 [simp]: "Card(K) ==> 1 |*| K = K"
   1.243 +apply (unfold cmult_def succ_def)
   1.244 +apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
   1.245 +done
   1.246 +
   1.247 +(*** Some inequalities for multiplication ***)
   1.248 +
   1.249 +lemma prod_square_lepoll: "A \<lesssim> A*A"
   1.250 +apply (unfold lepoll_def inj_def)
   1.251 +apply (rule_tac x = "lam x:A. <x,x>" in exI)
   1.252 +apply (simp (no_asm))
   1.253 +done
   1.254 +
   1.255 +(*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
   1.256 +lemma cmult_square_le: "Card(K) ==> K le K |*| K"
   1.257 +apply (unfold cmult_def)
   1.258 +apply (rule le_trans)
   1.259 +apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
   1.260 +apply (rule_tac [3] prod_square_lepoll)
   1.261 +apply (simp (no_asm_simp) add: le_refl Card_is_Ord Card_cardinal_eq)
   1.262 +apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord);
   1.263 +done
   1.264 +
   1.265 +(** Multiplication by a non-zero cardinal **)
   1.266 +
   1.267 +lemma prod_lepoll_self: "b: B ==> A \<lesssim> A*B"
   1.268 +apply (unfold lepoll_def inj_def)
   1.269 +apply (rule_tac x = "lam x:A. <x,b>" in exI)
   1.270 +apply (simp (no_asm_simp))
   1.271 +done
   1.272 +
   1.273 +(*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
   1.274 +lemma cmult_le_self:
   1.275 +    "[| Card(K);  Ord(L);  0<L |] ==> K le (K |*| L)"
   1.276 +apply (unfold cmult_def)
   1.277 +apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
   1.278 +  apply assumption; 
   1.279 + apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
   1.280 +apply (blast intro: prod_lepoll_self ltD)
   1.281 +done
   1.282 +
   1.283 +(** Monotonicity of multiplication **)
   1.284 +
   1.285 +lemma prod_lepoll_mono:
   1.286 +     "[| A \<lesssim> C;  B \<lesssim> D |] ==> A * B  \<lesssim>  C * D"
   1.287 +apply (unfold lepoll_def)
   1.288 +apply (elim exE);
   1.289 +apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI)
   1.290 +apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>" 
   1.291 +       in lam_injective)
   1.292 +apply (typecheck add: inj_is_fun)
   1.293 +apply auto
   1.294 +done
   1.295 +
   1.296 +lemma cmult_le_mono:
   1.297 +    "[| K' le K;  L' le L |] ==> (K' |*| L') le (K |*| L)"
   1.298 +apply (unfold cmult_def)
   1.299 +apply (safe dest!: le_subset_iff [THEN iffD1])
   1.300 +apply (rule well_ord_lepoll_imp_Card_le)
   1.301 + apply (blast intro: well_ord_rmult well_ord_Memrel)
   1.302 +apply (blast intro: prod_lepoll_mono subset_imp_lepoll)
   1.303 +done
   1.304 +
   1.305 +(*** Multiplication of finite cardinals is "ordinary" multiplication ***)
   1.306 +
   1.307 +lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B"
   1.308 +apply (unfold eqpoll_def)
   1.309 +apply (rule exI);
   1.310 +apply (rule_tac c = "%<x,y>. if x=A then Inl (y) else Inr (<x,y>)"
   1.311 +            and d = "case (%y. <A,y>, %z. z)" in lam_bijective)
   1.312 +apply safe
   1.313 +apply (simp_all add: succI2 if_type mem_imp_not_eq)
   1.314 +done
   1.315 +
   1.316 +(*Unconditional version requires AC*)
   1.317 +lemma cmult_succ_lemma:
   1.318 +    "[| Ord(m);  Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"
   1.319 +apply (unfold cmult_def cadd_def)
   1.320 +apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])
   1.321 +apply (rule cardinal_cong [symmetric])
   1.322 +apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
   1.323 +apply (blast intro: well_ord_rmult well_ord_Memrel)
   1.324 +done
   1.325 +
   1.326 +lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m |*| n = m#*n"
   1.327 +apply (induct_tac "m")
   1.328 +apply (simp (no_asm_simp))
   1.329 +apply (simp (no_asm_simp) add: cmult_succ_lemma nat_cadd_eq_add)
   1.330 +done
   1.331 +
   1.332 +lemma cmult_2: "Card(n) ==> 2 |*| n = n |+| n"
   1.333 +apply (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
   1.334 +done
   1.335 +
   1.336 +lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
   1.337 +apply (rule lepoll_trans); 
   1.338 +apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll]) 
   1.339 +apply (erule prod_lepoll_mono) 
   1.340 +apply (rule lepoll_refl); 
   1.341 +done
   1.342 +
   1.343 +lemma lepoll_imp_sum_lepoll_prod: "[| A \<lesssim> B; 2 \<lesssim> A |] ==> A+B \<lesssim> A*B"
   1.344 +apply (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
   1.345 +done
   1.346 +
   1.347 +
   1.348 +(*** Infinite Cardinals are Limit Ordinals ***)
   1.349 +
   1.350 +(*This proof is modelled upon one assuming nat<=A, with injection
   1.351 +  lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z
   1.352 +  and inverse %y. if y:nat then nat_case(u, %z. z, y) else y.  \
   1.353 +  If f: inj(nat,A) then range(f) behaves like the natural numbers.*)
   1.354 +lemma nat_cons_lepoll: "nat \<lesssim> A ==> cons(u,A) \<lesssim> A"
   1.355 +apply (unfold lepoll_def)
   1.356 +apply (erule exE)
   1.357 +apply (rule_tac x = 
   1.358 +          "lam z:cons (u,A).
   1.359 +             if z=u then f`0 
   1.360 +             else if z: range (f) then f`succ (converse (f) `z) else z" 
   1.361 +       in exI)
   1.362 +apply (rule_tac d =
   1.363 +          "%y. if y: range(f) then nat_case (u, %z. f`z, converse(f) `y) 
   1.364 +                              else y" 
   1.365 +       in lam_injective)
   1.366 +apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun)
   1.367 +apply (simp add: inj_is_fun [THEN apply_rangeI]
   1.368 +                 inj_converse_fun [THEN apply_rangeI]
   1.369 +                 inj_converse_fun [THEN apply_funtype])
   1.370 +done
   1.371 +
   1.372 +lemma nat_cons_eqpoll: "nat \<lesssim> A ==> cons(u,A) \<approx> A"
   1.373 +apply (erule nat_cons_lepoll [THEN eqpollI])
   1.374 +apply (rule subset_consI [THEN subset_imp_lepoll])
   1.375 +done
   1.376 +
   1.377 +(*Specialized version required below*)
   1.378 +lemma nat_succ_eqpoll: "nat <= A ==> succ(A) \<approx> A"
   1.379 +apply (unfold succ_def)
   1.380 +apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll])
   1.381 +done
   1.382 +
   1.383 +lemma InfCard_nat: "InfCard(nat)"
   1.384 +apply (unfold InfCard_def)
   1.385 +apply (blast intro: Card_nat le_refl Card_is_Ord)
   1.386 +done
   1.387 +
   1.388 +lemma InfCard_is_Card: "InfCard(K) ==> Card(K)"
   1.389 +apply (unfold InfCard_def)
   1.390 +apply (erule conjunct1)
   1.391 +done
   1.392 +
   1.393 +lemma InfCard_Un:
   1.394 +    "[| InfCard(K);  Card(L) |] ==> InfCard(K Un L)"
   1.395 +apply (unfold InfCard_def)
   1.396 +apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans]  Card_is_Ord)
   1.397 +done
   1.398 +
   1.399 +(*Kunen's Lemma 10.11*)
   1.400 +lemma InfCard_is_Limit: "InfCard(K) ==> Limit(K)"
   1.401 +apply (unfold InfCard_def)
   1.402 +apply (erule conjE)
   1.403 +apply (frule Card_is_Ord)
   1.404 +apply (rule ltI [THEN non_succ_LimitI])
   1.405 +apply (erule le_imp_subset [THEN subsetD])
   1.406 +apply (safe dest!: Limit_nat [THEN Limit_le_succD])
   1.407 +apply (unfold Card_def)
   1.408 +apply (drule trans)
   1.409 +apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong])
   1.410 +apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl])
   1.411 +apply (rule le_eqI) 
   1.412 +apply assumption; 
   1.413 +apply (rule Ord_cardinal)
   1.414 +done
   1.415 +
   1.416 +
   1.417 +(*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)
   1.418 +
   1.419 +(*A general fact about ordermap*)
   1.420 +lemma ordermap_eqpoll_pred:
   1.421 +    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> pred(A,x,r)"
   1.422 +apply (unfold eqpoll_def)
   1.423 +apply (rule exI)
   1.424 +apply (simp (no_asm_simp) add: ordermap_eq_image well_ord_is_wf)
   1.425 +apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, THEN bij_converse_bij])
   1.426 +apply (rule pred_subset)
   1.427 +done
   1.428 +
   1.429 +(** Establishing the well-ordering **)
   1.430 +
   1.431 +lemma csquare_lam_inj:
   1.432 +     "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)"
   1.433 +apply (unfold inj_def)
   1.434 +apply (force intro: lam_type Un_least_lt [THEN ltD] ltI)
   1.435 +done
   1.436 +
   1.437 +lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))"
   1.438 +apply (unfold csquare_rel_def)
   1.439 +apply (rule csquare_lam_inj [THEN well_ord_rvimage])
   1.440 +apply assumption; 
   1.441 +apply (blast intro: well_ord_rmult well_ord_Memrel)
   1.442 +done
   1.443 +
   1.444 +(** Characterising initial segments of the well-ordering **)
   1.445 +
   1.446 +lemma csquareD:
   1.447 + "[| <<x,y>, <z,z>> : csquare_rel(K);  x<K;  y<K;  z<K |] ==> x le z & y le z"
   1.448 +apply (unfold csquare_rel_def)
   1.449 +apply (erule rev_mp)
   1.450 +apply (elim ltE)
   1.451 +apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
   1.452 +apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le)
   1.453 +apply (simp_all (no_asm_simp) add: lt_def succI2)
   1.454 +done
   1.455 +
   1.456 +lemma pred_csquare_subset: 
   1.457 +    "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
   1.458 +apply (unfold Order.pred_def)
   1.459 +apply (safe del: SigmaI succCI)
   1.460 +apply (erule csquareD [THEN conjE])
   1.461 +apply (unfold lt_def)
   1.462 +apply (auto ); 
   1.463 +done
   1.464 +
   1.465 +lemma csquare_ltI:
   1.466 + "[| x<z;  y<z;  z<K |] ==>  <<x,y>, <z,z>> : csquare_rel(K)"
   1.467 +apply (unfold csquare_rel_def)
   1.468 +apply (subgoal_tac "x<K & y<K")
   1.469 + prefer 2 apply (blast intro: lt_trans) 
   1.470 +apply (elim ltE)
   1.471 +apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
   1.472 +done
   1.473 +
   1.474 +(*Part of the traditional proof.  UNUSED since it's harder to prove & apply *)
   1.475 +lemma csquare_or_eqI:
   1.476 + "[| x le z;  y le z;  z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K) | x=z & y=z"
   1.477 +apply (unfold csquare_rel_def)
   1.478 +apply (subgoal_tac "x<K & y<K")
   1.479 + prefer 2 apply (blast intro: lt_trans1) 
   1.480 +apply (elim ltE)
   1.481 +apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
   1.482 +apply (elim succE)
   1.483 +apply (simp_all (no_asm_simp) add: subset_Un_iff [THEN iff_sym] subset_Un_iff2 [THEN iff_sym] OrdmemD)
   1.484 +done
   1.485 +
   1.486 +(** The cardinality of initial segments **)
   1.487 +
   1.488 +lemma ordermap_z_lt:
   1.489 +      "[| Limit(K);  x<K;  y<K;  z=succ(x Un y) |] ==>
   1.490 +          ordermap(K*K, csquare_rel(K)) ` <x,y> <
   1.491 +          ordermap(K*K, csquare_rel(K)) ` <z,z>"
   1.492 +apply (subgoal_tac "z<K & well_ord (K*K, csquare_rel (K))")
   1.493 +prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ
   1.494 +                              Limit_is_Ord [THEN well_ord_csquare])
   1.495 +apply (clarify ); 
   1.496 +apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI])
   1.497 +apply (erule_tac [4] well_ord_is_wf)
   1.498 +apply (blast intro!: Un_upper1_le Un_upper2_le Ord_ordermap elim!: ltE)+
   1.499 +done
   1.500 +
   1.501 +(*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
   1.502 +lemma ordermap_csquare_le:
   1.503 +  "[| Limit(K);  x<K;  y<K;  z=succ(x Un y) |] ==>
   1.504 +        | ordermap(K*K, csquare_rel(K)) ` <x,y> | le  |succ(z)| |*| |succ(z)|"
   1.505 +apply (unfold cmult_def)
   1.506 +apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
   1.507 +apply (rule Ord_cardinal [THEN well_ord_Memrel])+
   1.508 +apply (subgoal_tac "z<K")
   1.509 + prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ)
   1.510 +apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans])
   1.511 +apply assumption +
   1.512 +apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
   1.513 +apply (erule Limit_is_Ord [THEN well_ord_csquare])
   1.514 +apply (blast intro: ltD)
   1.515 +apply (rule pred_csquare_subset [THEN subset_imp_lepoll, THEN lepoll_trans],
   1.516 +            assumption)
   1.517 +apply (elim ltE)
   1.518 +apply (rule prod_eqpoll_cong [THEN eqpoll_sym, THEN eqpoll_imp_lepoll])
   1.519 +apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+
   1.520 +done
   1.521 +
   1.522 +(*Kunen: "... so the order type <= K" *)
   1.523 +lemma ordertype_csquare_le:
   1.524 +     "[| InfCard(K);  ALL y:K. InfCard(y) --> y |*| y = y |] 
   1.525 +      ==> ordertype(K*K, csquare_rel(K)) le K"
   1.526 +apply (frule InfCard_is_Card [THEN Card_is_Ord])
   1.527 +apply (rule all_lt_imp_le)
   1.528 +apply assumption
   1.529 +apply (erule well_ord_csquare [THEN Ord_ordertype])
   1.530 +apply (rule Card_lt_imp_lt)
   1.531 +apply (erule_tac [3] InfCard_is_Card)
   1.532 +apply (erule_tac [2] ltE)
   1.533 +apply (simp add: ordertype_unfold)
   1.534 +apply (safe elim!: ltE)
   1.535 +apply (subgoal_tac "Ord (xa) & Ord (ya)")
   1.536 + prefer 2 apply (blast intro: Ord_in_Ord)
   1.537 +apply (clarify );
   1.538 +(*??WHAT A MESS!*)  
   1.539 +apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
   1.540 +       (assumption | rule refl | erule ltI)+) 
   1.541 +apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2,
   1.542 +       simp_all add: Ord_Un Ord_nat)
   1.543 +prefer 2 (*case nat le (xa Un ya) *)
   1.544 + apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] 
   1.545 +                  le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un
   1.546 +                ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD])
   1.547 +(*the finite case: xa Un ya < nat *)
   1.548 +apply (rule_tac j = "nat" in lt_trans2)
   1.549 + apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
   1.550 +                  nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
   1.551 +apply (simp add: InfCard_def)
   1.552 +done
   1.553 +
   1.554 +(*Main result: Kunen's Theorem 10.12*)
   1.555 +lemma InfCard_csquare_eq: "InfCard(K) ==> K |*| K = K"
   1.556 +apply (frule InfCard_is_Card [THEN Card_is_Ord])
   1.557 +apply (erule rev_mp)
   1.558 +apply (erule_tac i=K in trans_induct) 
   1.559 +apply (rule impI)
   1.560 +apply (rule le_anti_sym)
   1.561 +apply (erule_tac [2] InfCard_is_Card [THEN cmult_square_le])
   1.562 +apply (rule ordertype_csquare_le [THEN [2] le_trans])
   1.563 +prefer 2 apply (assumption)
   1.564 +prefer 2 apply (assumption)
   1.565 +apply (simp (no_asm_simp) add: cmult_def Ord_cardinal_le well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll, THEN cardinal_cong] well_ord_csquare [THEN Ord_ordertype])
   1.566 +done
   1.567 +
   1.568 +(*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
   1.569 +lemma well_ord_InfCard_square_eq:
   1.570 +     "[| well_ord(A,r);  InfCard(|A|) |] ==> A*A \<approx> A"
   1.571 +apply (rule prod_eqpoll_cong [THEN eqpoll_trans])
   1.572 +apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+
   1.573 +apply (rule well_ord_cardinal_eqE)
   1.574 +apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel)
   1.575 +apply assumption; 
   1.576 +apply (simp (no_asm_simp) add: cmult_def [symmetric] InfCard_csquare_eq)
   1.577 +done
   1.578 +
   1.579 +(** Toward's Kunen's Corollary 10.13 (1) **)
   1.580 +
   1.581 +lemma InfCard_le_cmult_eq: "[| InfCard(K);  L le K;  0<L |] ==> K |*| L = K"
   1.582 +apply (rule le_anti_sym)
   1.583 + prefer 2
   1.584 + apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card)
   1.585 +apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl])
   1.586 +apply (rule cmult_le_mono [THEN le_trans], assumption+)
   1.587 +apply (simp add: InfCard_csquare_eq)
   1.588 +done
   1.589 +
   1.590 +(*Corollary 10.13 (1), for cardinal multiplication*)
   1.591 +lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K Un L"
   1.592 +apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
   1.593 +apply (typecheck add: InfCard_is_Card Card_is_Ord)
   1.594 +apply (rule cmult_commute [THEN ssubst])
   1.595 +apply (rule Un_commute [THEN ssubst])
   1.596 +apply (simp_all (no_asm_simp) add: InfCard_is_Limit [THEN Limit_has_0] InfCard_le_cmult_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
   1.597 +done
   1.598 +
   1.599 +lemma InfCard_cdouble_eq: "InfCard(K) ==> K |+| K = K"
   1.600 +apply (simp (no_asm_simp) add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)
   1.601 +apply (simp (no_asm_simp) add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)
   1.602 +done
   1.603 +
   1.604 +(*Corollary 10.13 (1), for cardinal addition*)
   1.605 +lemma InfCard_le_cadd_eq: "[| InfCard(K);  L le K |] ==> K |+| L = K"
   1.606 +apply (rule le_anti_sym)
   1.607 + prefer 2
   1.608 + apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card)
   1.609 +apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl])
   1.610 +apply (rule cadd_le_mono [THEN le_trans], assumption+)
   1.611 +apply (simp add: InfCard_cdouble_eq)
   1.612 +done
   1.613 +
   1.614 +lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L"
   1.615 +apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
   1.616 +apply (typecheck add: InfCard_is_Card Card_is_Ord)
   1.617 +apply (rule cadd_commute [THEN ssubst])
   1.618 +apply (rule Un_commute [THEN ssubst])
   1.619 +apply (simp_all (no_asm_simp) add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
   1.620 +done
   1.621 +
   1.622 +(*The other part, Corollary 10.13 (2), refers to the cardinality of the set
   1.623 +  of all n-tuples of elements of K.  A better version for the Isabelle theory
   1.624 +  might be  InfCard(K) ==> |list(K)| = K.
   1.625 +*)
   1.626 +
   1.627 +(*** For every cardinal number there exists a greater one
   1.628 +     [Kunen's Theorem 10.16, which would be trivial using AC] ***)
   1.629 +
   1.630 +lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))"
   1.631 +apply (unfold jump_cardinal_def)
   1.632 +apply (rule Ord_is_Transset [THEN [2] OrdI])
   1.633 + prefer 2 apply (blast intro!: Ord_ordertype)
   1.634 +apply (unfold Transset_def)
   1.635 +apply (safe del: subsetI)
   1.636 +apply (simp add: ordertype_pred_unfold)
   1.637 +apply safe
   1.638 +apply (rule UN_I)
   1.639 +apply (rule_tac [2] ReplaceI)
   1.640 +   prefer 4 apply (blast intro: well_ord_subset elim!: predE)+
   1.641 +done
   1.642 +
   1.643 +(*Allows selective unfolding.  Less work than deriving intro/elim rules*)
   1.644 +lemma jump_cardinal_iff:
   1.645 +     "i : jump_cardinal(K) <->
   1.646 +      (EX r X. r <= K*K & X <= K & well_ord(X,r) & i = ordertype(X,r))"
   1.647 +apply (unfold jump_cardinal_def)
   1.648 +apply (blast del: subsetI) 
   1.649 +done
   1.650 +
   1.651 +(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*)
   1.652 +lemma K_lt_jump_cardinal: "Ord(K) ==> K < jump_cardinal(K)"
   1.653 +apply (rule Ord_jump_cardinal [THEN [2] ltI])
   1.654 +apply (rule jump_cardinal_iff [THEN iffD2])
   1.655 +apply (rule_tac x="Memrel(K)" in exI)
   1.656 +apply (rule_tac x=K in exI)  
   1.657 +apply (simp add: ordertype_Memrel well_ord_Memrel)
   1.658 +apply (simp add: Memrel_def subset_iff)
   1.659 +done
   1.660 +
   1.661 +(*The proof by contradiction: the bijection f yields a wellordering of X
   1.662 +  whose ordertype is jump_cardinal(K).  *)
   1.663 +lemma Card_jump_cardinal_lemma:
   1.664 +     "[| well_ord(X,r);  r <= K * K;  X <= K;
   1.665 +         f : bij(ordertype(X,r), jump_cardinal(K)) |]
   1.666 +      ==> jump_cardinal(K) : jump_cardinal(K)"
   1.667 +apply (subgoal_tac "f O ordermap (X,r) : bij (X, jump_cardinal (K))")
   1.668 + prefer 2 apply (blast intro: comp_bij ordermap_bij)
   1.669 +apply (rule jump_cardinal_iff [THEN iffD2])
   1.670 +apply (intro exI conjI)
   1.671 +apply (rule subset_trans [OF rvimage_type Sigma_mono])
   1.672 +apply assumption+
   1.673 +apply (erule bij_is_inj [THEN well_ord_rvimage])
   1.674 +apply (rule Ord_jump_cardinal [THEN well_ord_Memrel])
   1.675 +apply (simp add: well_ord_Memrel [THEN [2] bij_ordertype_vimage]
   1.676 +                 ordertype_Memrel Ord_jump_cardinal)
   1.677 +done
   1.678 +
   1.679 +(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*)
   1.680 +lemma Card_jump_cardinal: "Card(jump_cardinal(K))"
   1.681 +apply (rule Ord_jump_cardinal [THEN CardI])
   1.682 +apply (unfold eqpoll_def)
   1.683 +apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1])
   1.684 +apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl])
   1.685 +done
   1.686 +
   1.687 +(*** Basic properties of successor cardinals ***)
   1.688 +
   1.689 +lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)"
   1.690 +apply (unfold csucc_def)
   1.691 +apply (rule LeastI)
   1.692 +apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+
   1.693 +done
   1.694 +
   1.695 +lemmas Card_csucc = csucc_basic [THEN conjunct1, standard]
   1.696 +
   1.697 +lemmas lt_csucc = csucc_basic [THEN conjunct2, standard]
   1.698 +
   1.699 +lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)"
   1.700 +apply (blast intro: Ord_0_le lt_csucc lt_trans1)
   1.701 +done
   1.702 +
   1.703 +lemma csucc_le: "[| Card(L);  K<L |] ==> csucc(K) le L"
   1.704 +apply (unfold csucc_def)
   1.705 +apply (rule Least_le)
   1.706 +apply (blast intro: Card_is_Ord)+
   1.707 +done
   1.708 +
   1.709 +lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K"
   1.710 +apply (rule iffI)
   1.711 +apply (rule_tac [2] Card_lt_imp_lt)
   1.712 +apply (erule_tac [2] lt_trans1)
   1.713 +apply (simp_all add: lt_csucc Card_csucc Card_is_Ord)
   1.714 +apply (rule notI [THEN not_lt_imp_le])
   1.715 +apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl])
   1.716 +apply assumption
   1.717 +apply (rule Ord_cardinal_le [THEN lt_trans1])
   1.718 +apply (simp_all add: Ord_cardinal Card_is_Ord) 
   1.719 +done
   1.720 +
   1.721 +lemma Card_lt_csucc_iff:
   1.722 +     "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"
   1.723 +by (simp (no_asm_simp) add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
   1.724 +
   1.725 +lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))"
   1.726 +by (simp add: InfCard_def Card_csucc Card_is_Ord 
   1.727 +              lt_csucc [THEN leI, THEN [2] le_trans])
   1.728 +
   1.729 +
   1.730 +(*** Finite sets ***)
   1.731 +
   1.732 +lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
   1.733 +apply (induct_tac "n")
   1.734 +apply (simp (no_asm) add: eqpoll_0_iff)
   1.735 +apply clarify
   1.736 +apply (subgoal_tac "EX u. u:A")
   1.737 +apply (erule exE)
   1.738 +apply (rule Diff_sing_eqpoll [THEN revcut_rl])
   1.739 +prefer 2 apply (assumption)
   1.740 +apply assumption
   1.741 +apply (rule_tac b = "A" in cons_Diff [THEN subst])
   1.742 +apply assumption
   1.743 +apply (rule Fin.consI)
   1.744 +apply blast
   1.745 +apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
   1.746 +(*Now for the lemma assumed above*)
   1.747 +apply (unfold eqpoll_def)
   1.748 +apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
   1.749 +done
   1.750 +
   1.751 +lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)"
   1.752 +apply (unfold Finite_def)
   1.753 +apply (blast intro: Fin_lemma)
   1.754 +done
   1.755 +
   1.756 +lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
   1.757 +apply (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
   1.758 +done
   1.759 +
   1.760 +lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
   1.761 +apply (blast intro: Finite_into_Fin Fin_into_Finite)
   1.762 +done
   1.763 +
   1.764 +lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
   1.765 +by (blast intro!: Fin_into_Finite Fin_UnI 
   1.766 +          dest!: Finite_into_Fin
   1.767 +          intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 
   1.768 +                 Un_upper2 [THEN Fin_mono, THEN subsetD])
   1.769 +
   1.770 +lemma Finite_Union: "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))"
   1.771 +apply (simp add: Finite_Fin_iff)
   1.772 +apply (rule Fin_UnionI)
   1.773 +apply (erule Fin_induct)
   1.774 +apply (simp (no_asm))
   1.775 +apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
   1.776 +done
   1.777 +
   1.778 +(* Induction principle for Finite(A), by Sidi Ehmety *)
   1.779 +lemma Finite_induct:
   1.780 +"[| Finite(A); P(0);
   1.781 +    !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
   1.782 + ==> P(A)"
   1.783 +apply (erule Finite_into_Fin [THEN Fin_induct]) 
   1.784 +apply (blast intro: Fin_into_Finite)+
   1.785 +done
   1.786 +
   1.787 +
   1.788 +(** Removing elements from a finite set decreases its cardinality **)
   1.789 +
   1.790 +lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A --> ~ cons(x,A) \<lesssim> A"
   1.791 +apply (erule Fin_induct)
   1.792 +apply (simp (no_asm) add: lepoll_0_iff)
   1.793 +apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))")
   1.794 +apply (simp (no_asm_simp))
   1.795 +apply (blast dest!: cons_lepoll_consD)
   1.796 +apply blast
   1.797 +done
   1.798 +
   1.799 +lemma Finite_imp_cardinal_cons: "[| Finite(A);  a~:A |] ==> |cons(a,A)| = succ(|A|)"
   1.800 +apply (unfold cardinal_def)
   1.801 +apply (rule Least_equality)
   1.802 +apply (fold cardinal_def)
   1.803 +apply (simp (no_asm) add: succ_def)
   1.804 +apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll
   1.805 +             elim!: mem_irrefl  dest!: Finite_imp_well_ord)
   1.806 +apply (blast intro: Card_cardinal Card_is_Ord)
   1.807 +apply (rule notI)
   1.808 +apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE])
   1.809 +apply assumption
   1.810 +apply assumption
   1.811 +apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
   1.812 +apply (erule le_imp_lepoll [THEN lepoll_trans])
   1.813 +apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll]
   1.814 +             dest!: Finite_imp_well_ord)
   1.815 +done
   1.816 +
   1.817 +
   1.818 +lemma Finite_imp_succ_cardinal_Diff: "[| Finite(A);  a:A |] ==> succ(|A-{a}|) = |A|"
   1.819 +apply (rule_tac b = "A" in cons_Diff [THEN subst])
   1.820 +apply assumption
   1.821 +apply (simp (no_asm_simp) add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
   1.822 +apply (simp (no_asm_simp) add: cons_Diff)
   1.823 +done
   1.824 +
   1.825 +lemma Finite_imp_cardinal_Diff: "[| Finite(A);  a:A |] ==> |A-{a}| < |A|"
   1.826 +apply (rule succ_leE)
   1.827 +apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff)
   1.828 +done
   1.829 +
   1.830 +
   1.831 +(** Theorems by Krzysztof Grabczewski, proofs by lcp **)
   1.832 +
   1.833 +lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard]
   1.834 +
   1.835 +lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n"
   1.836 +apply (rule eqpoll_trans)
   1.837 +apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
   1.838 +apply (erule nat_implies_well_ord)+
   1.839 +apply (simp (no_asm_simp) add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl)
   1.840 +done
   1.841 +
   1.842 +
   1.843 +(*** Theorems by Sidi Ehmety ***)
   1.844 +
   1.845 +(*The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
   1.846 +lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
   1.847 +apply (unfold Finite_def)
   1.848 +apply (case_tac "a:A")
   1.849 +apply (subgoal_tac [2] "A-{a}=A")
   1.850 +apply auto
   1.851 +apply (rule_tac x = "succ (n) " in bexI)
   1.852 +apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
   1.853 +apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
   1.854 +apply (auto dest: mem_irrefl)
   1.855 +done
   1.856 +
   1.857 +(*And the contrapositive of this says
   1.858 +   [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
   1.859 +lemma Diff_Finite [rule_format (no_asm)]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
   1.860 +apply (erule Finite_induct)
   1.861 +apply auto
   1.862 +apply (case_tac "x:A")
   1.863 + apply (subgoal_tac [2] "A-cons (x, B) = A - B")
   1.864 +apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
   1.865 +apply (rotate_tac -1)
   1.866 +apply simp
   1.867 +apply (drule Diff_sing_Finite)
   1.868 +apply auto
   1.869 +done
   1.870 +
   1.871 +lemma Ord_subset_natD [rule_format (no_asm)]: "Ord(i) ==> i <= nat --> i : nat | i=nat"
   1.872 +apply (erule trans_induct3)
   1.873 +apply auto
   1.874 +apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
   1.875 +done
   1.876 +
   1.877 +lemma Ord_nat_subset_into_Card: "[| Ord(i); i <= nat |] ==> Card(i)"
   1.878 +apply (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
   1.879 +done
   1.880 +
   1.881 +lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| : nat"
   1.882 +apply (erule Finite_induct)
   1.883 +apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons)
   1.884 +done
   1.885 +
   1.886 +lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1"
   1.887 +apply (rule succ_inject)
   1.888 +apply (rule_tac b = "|A|" in trans)
   1.889 +apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff)
   1.890 +apply (subgoal_tac "1 \<lesssim> A")
   1.891 +prefer 2 apply (blast intro: not_0_is_lepoll_1)
   1.892 +apply (frule Finite_imp_well_ord)
   1.893 +apply clarify
   1.894 +apply (rotate_tac -1)
   1.895 +apply (drule well_ord_lepoll_imp_Card_le)
   1.896 +apply (auto simp add: cardinal_1)
   1.897 +apply (rule trans)
   1.898 +apply (rule_tac [2] diff_succ)
   1.899 +apply (auto simp add: Finite_cardinal_in_nat)
   1.900 +done
   1.901 +
   1.902 +lemma cardinal_lt_imp_Diff_not_0 [rule_format (no_asm)]: "Finite(B) ==> ALL A. |B|<|A| --> A - B ~= 0"
   1.903 +apply (erule Finite_induct)
   1.904 +apply auto
   1.905 +apply (simp_all add: Finite_imp_cardinal_cons)
   1.906 +apply (case_tac "Finite (A) ")
   1.907 +apply (subgoal_tac [2] "Finite (cons (x, B))")
   1.908 +apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite)
   1.909 +apply (auto simp add: Finite_0 Finite_cons)
   1.910 +apply (subgoal_tac "|B|<|A|")
   1.911 +prefer 2 apply (blast intro: lt_trans Ord_cardinal)
   1.912 +apply (case_tac "x:A")
   1.913 +apply (subgoal_tac [2] "A - cons (x, B) = A - B")
   1.914 +apply auto
   1.915 +apply (subgoal_tac "|A| le |cons (x, B) |")
   1.916 +prefer 2
   1.917 + apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] 
   1.918 +              intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll)
   1.919 +apply (auto simp add: Finite_imp_cardinal_cons)
   1.920 +apply (auto dest!: Finite_cardinal_in_nat simp add: le_iff)
   1.921 +apply (blast intro: lt_trans)
   1.922 +done
   1.923 +
   1.924 +
   1.925 +ML{*
   1.926 +val InfCard_def = thm "InfCard_def"
   1.927 +val cmult_def = thm "cmult_def"
   1.928 +val cadd_def = thm "cadd_def"
   1.929 +val jump_cardinal_def = thm "jump_cardinal_def"
   1.930 +val csucc_def = thm "csucc_def"
   1.931 +
   1.932 +val sum_commute_eqpoll = thm "sum_commute_eqpoll";
   1.933 +val cadd_commute = thm "cadd_commute";
   1.934 +val sum_assoc_eqpoll = thm "sum_assoc_eqpoll";
   1.935 +val well_ord_cadd_assoc = thm "well_ord_cadd_assoc";
   1.936 +val sum_0_eqpoll = thm "sum_0_eqpoll";
   1.937 +val cadd_0 = thm "cadd_0";
   1.938 +val sum_lepoll_self = thm "sum_lepoll_self";
   1.939 +val cadd_le_self = thm "cadd_le_self";
   1.940 +val sum_lepoll_mono = thm "sum_lepoll_mono";
   1.941 +val cadd_le_mono = thm "cadd_le_mono";
   1.942 +val eq_imp_not_mem = thm "eq_imp_not_mem";
   1.943 +val sum_succ_eqpoll = thm "sum_succ_eqpoll";
   1.944 +val nat_cadd_eq_add = thm "nat_cadd_eq_add";
   1.945 +val prod_commute_eqpoll = thm "prod_commute_eqpoll";
   1.946 +val cmult_commute = thm "cmult_commute";
   1.947 +val prod_assoc_eqpoll = thm "prod_assoc_eqpoll";
   1.948 +val well_ord_cmult_assoc = thm "well_ord_cmult_assoc";
   1.949 +val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll";
   1.950 +val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib";
   1.951 +val prod_0_eqpoll = thm "prod_0_eqpoll";
   1.952 +val cmult_0 = thm "cmult_0";
   1.953 +val prod_singleton_eqpoll = thm "prod_singleton_eqpoll";
   1.954 +val cmult_1 = thm "cmult_1";
   1.955 +val prod_lepoll_self = thm "prod_lepoll_self";
   1.956 +val cmult_le_self = thm "cmult_le_self";
   1.957 +val prod_lepoll_mono = thm "prod_lepoll_mono";
   1.958 +val cmult_le_mono = thm "cmult_le_mono";
   1.959 +val prod_succ_eqpoll = thm "prod_succ_eqpoll";
   1.960 +val nat_cmult_eq_mult = thm "nat_cmult_eq_mult";
   1.961 +val cmult_2 = thm "cmult_2";
   1.962 +val sum_lepoll_prod = thm "sum_lepoll_prod";
   1.963 +val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod";
   1.964 +val nat_cons_lepoll = thm "nat_cons_lepoll";
   1.965 +val nat_cons_eqpoll = thm "nat_cons_eqpoll";
   1.966 +val nat_succ_eqpoll = thm "nat_succ_eqpoll";
   1.967 +val InfCard_nat = thm "InfCard_nat";
   1.968 +val InfCard_is_Card = thm "InfCard_is_Card";
   1.969 +val InfCard_Un = thm "InfCard_Un";
   1.970 +val InfCard_is_Limit = thm "InfCard_is_Limit";
   1.971 +val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred";
   1.972 +val ordermap_z_lt = thm "ordermap_z_lt";
   1.973 +val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq";
   1.974 +val InfCard_cmult_eq = thm "InfCard_cmult_eq";
   1.975 +val InfCard_cdouble_eq = thm "InfCard_cdouble_eq";
   1.976 +val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq";
   1.977 +val InfCard_cadd_eq = thm "InfCard_cadd_eq";
   1.978 +val Ord_jump_cardinal = thm "Ord_jump_cardinal";
   1.979 +val jump_cardinal_iff = thm "jump_cardinal_iff";
   1.980 +val K_lt_jump_cardinal = thm "K_lt_jump_cardinal";
   1.981 +val Card_jump_cardinal = thm "Card_jump_cardinal";
   1.982 +val csucc_basic = thm "csucc_basic";
   1.983 +val Card_csucc = thm "Card_csucc";
   1.984 +val lt_csucc = thm "lt_csucc";
   1.985 +val Ord_0_lt_csucc = thm "Ord_0_lt_csucc";
   1.986 +val csucc_le = thm "csucc_le";
   1.987 +val lt_csucc_iff = thm "lt_csucc_iff";
   1.988 +val Card_lt_csucc_iff = thm "Card_lt_csucc_iff";
   1.989 +val InfCard_csucc = thm "InfCard_csucc";
   1.990 +val Finite_into_Fin = thm "Finite_into_Fin";
   1.991 +val Fin_into_Finite = thm "Fin_into_Finite";
   1.992 +val Finite_Fin_iff = thm "Finite_Fin_iff";
   1.993 +val Finite_Un = thm "Finite_Un";
   1.994 +val Finite_Union = thm "Finite_Union";
   1.995 +val Finite_induct = thm "Finite_induct";
   1.996 +val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll";
   1.997 +val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons";
   1.998 +val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff";
   1.999 +val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff";
  1.1000 +val nat_implies_well_ord = thm "nat_implies_well_ord";
  1.1001 +val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum";
  1.1002 +val Diff_sing_Finite = thm "Diff_sing_Finite";
  1.1003 +val Diff_Finite = thm "Diff_Finite";
  1.1004 +val Ord_subset_natD = thm "Ord_subset_natD";
  1.1005 +val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card";
  1.1006 +val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat";
  1.1007 +val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1";
  1.1008 +val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0";
  1.1009 +*}
  1.1010 +
  1.1011  end