src/ZF/CardinalArith.thy
author paulson
Sun Jun 16 11:58:54 2002 +0200 (2002-06-16)
changeset 13216 6104bd4088a2
parent 13161 a40db0418145
child 13221 e29378f347e4
permissions -rw-r--r--
conversion of CardinalArith to Isar script
     1 (*  Title:      ZF/CardinalArith.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Cardinal arithmetic -- WITHOUT the Axiom of Choice
     7 
     8 Note: Could omit proving the algebraic laws for cardinal addition and
     9 multiplication.  On finite cardinals these operations coincide with
    10 addition and multiplication of natural numbers; on infinite cardinals they
    11 coincide with union (maximum).  Either way we get most laws for free.
    12 *)
    13 
    14 theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
    15 
    16 constdefs
    17 
    18   InfCard       :: "i=>o"
    19     "InfCard(i) == Card(i) & nat le i"
    20 
    21   cmult         :: "[i,i]=>i"       (infixl "|*|" 70)
    22     "i |*| j == |i*j|"
    23   
    24   cadd          :: "[i,i]=>i"       (infixl "|+|" 65)
    25     "i |+| j == |i+j|"
    26 
    27   csquare_rel   :: "i=>i"
    28     "csquare_rel(K) ==   
    29 	  rvimage(K*K,   
    30 		  lam <x,y>:K*K. <x Un y, x, y>, 
    31 		  rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    32 
    33   (*This def is more complex than Kunen's but it more easily proved to
    34     be a cardinal*)
    35   jump_cardinal :: "i=>i"
    36     "jump_cardinal(K) ==   
    37          UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
    38   
    39   (*needed because jump_cardinal(K) might not be the successor of K*)
    40   csucc         :: "i=>i"
    41     "csucc(K) == LEAST L. Card(L) & K<L"
    42 
    43 syntax (xsymbols)
    44   "op |+|"     :: "[i,i] => i"          (infixl "\<oplus>" 65)
    45   "op |*|"     :: "[i,i] => i"          (infixl "\<otimes>" 70)
    46 
    47 
    48 (*** The following really belong early in the development ***)
    49 
    50 lemma relation_converse_converse [simp]:
    51      "relation(r) ==> converse(converse(r)) = r"
    52 by (simp add: relation_def, blast) 
    53 
    54 lemma relation_restrict [simp]:  "relation(restrict(r,A))"
    55 by (simp add: restrict_def relation_def, blast) 
    56 
    57 (*** The following really belong in Order ***)
    58 
    59 lemma subset_ord_iso_Memrel:
    60      "[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: ord_iso(A,Memrel(A),C,r)"
    61 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 
    62 apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 
    63 apply (simp add: right_comp_id) 
    64 done
    65 
    66 lemma restrict_ord_iso:
    67      "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
    68        trans[A](r) |]
    69       ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
    70 apply (frule ltD) 
    71 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 
    72 apply (frule ord_iso_restrict_pred, assumption) 
    73 apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
    74 apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI]) 
    75 done
    76 
    77 lemma restrict_ord_iso2:
    78      "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A; 
    79        j < i; trans[A](r) |]
    80       ==> converse(restrict(converse(f), j)) 
    81           \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
    82 by (blast intro: restrict_ord_iso ord_iso_sym ltI)
    83 
    84 (*** The following really belong in OrderType ***)
    85 
    86 lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
    87 apply (erule trans_induct3 [of j])
    88 apply (simp_all add: oadd_Limit)
    89 apply (simp add: Union_empty_iff Limit_def lt_def, blast)
    90 done
    91 
    92 lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
    93 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
    94 
    95 lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
    96 apply (rule lt_trans2) 
    97 apply (erule le_refl) 
    98 apply (simp only: lt_Ord2  oadd_1 [of i, symmetric]) 
    99 apply (blast intro: succ_leI oadd_le_mono)
   100 done
   101 
   102 lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
   103 apply (simp add: oadd_Limit)
   104 apply (frule Limit_has_1 [THEN ltD])
   105 apply (rule increasing_LimitI)
   106  apply (rule Ord_0_lt)
   107   apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
   108  apply (force simp add: Union_empty_iff oadd_eq_0_iff
   109                         Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
   110 apply (rule_tac x="succ(x)" in bexI)
   111  apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
   112 apply (simp add: Limit_def lt_def) 
   113 done
   114 
   115 (*** The following really belong in Cardinal ***)
   116 
   117 lemma lesspoll_not_refl: "~ (i lesspoll i)"
   118 by (simp add: lesspoll_def) 
   119 
   120 lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P"
   121 by (simp add: lesspoll_def) 
   122 
   123 lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))"
   124 apply (rule CardI) 
   125  apply (simp add: Card_is_Ord) 
   126 apply (clarify dest!: ltD)
   127 apply (drule bspec, assumption) 
   128 apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 
   129 apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
   130 apply (drule lesspoll_trans1, assumption) 
   131 apply (subgoal_tac "B \<lesssim> \<Union>A")
   132  apply (drule lesspoll_trans1, assumption, blast) 
   133 apply (blast intro: subset_imp_lepoll) 
   134 done
   135 
   136 lemma Card_UN:
   137      "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 
   138 by (blast intro: Card_Union) 
   139 
   140 lemma Card_OUN [simp,intro,TC]:
   141      "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
   142 by (simp add: OUnion_def Card_0) 
   143 
   144 lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
   145 apply (unfold lesspoll_def)
   146 apply (rule conjI)
   147 apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat)
   148 apply (rule notI)
   149 apply (erule eqpollE)
   150 apply (rule succ_lepoll_natE)
   151 apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 
   152                     lepoll_trans, assumption) 
   153 done
   154 
   155 lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
   156 apply (unfold lesspoll_def)
   157 apply (simp add: Card_iff_initial)
   158 apply (fast intro!: le_imp_lepoll ltI leI)
   159 done
   160 
   161 lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
   162 by (fast dest!: lepoll_0_is_0)
   163 
   164 lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
   165 by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
   166 
   167 lemma Finite_Fin_lemma [rule_format]:
   168      "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
   169 apply (induct_tac "n")
   170 apply (rule allI)
   171 apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
   172 apply (rule allI)
   173 apply (rule impI)
   174 apply (erule conjE)
   175 apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
   176 apply (frule Diff_sing_eqpoll, assumption)
   177 apply (erule allE)
   178 apply (erule impE, fast)
   179 apply (drule subsetD, assumption)
   180 apply (drule Fin.consI, assumption)
   181 apply (simp add: cons_Diff)
   182 done
   183 
   184 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
   185 by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
   186 
   187 lemma lesspoll_lemma: 
   188         "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0"
   189 apply (unfold lesspoll_def)
   190 apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
   191             intro!: eqpollI elim: notE 
   192             elim!: eqpollE lepoll_trans)
   193 done
   194 
   195 lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
   196 apply (unfold Finite_def) 
   197 apply (blast intro: eqpoll_trans eqpoll_sym) 
   198 done
   199 
   200 
   201 (*** Cardinal addition ***)
   202 
   203 (** Cardinal addition is commutative **)
   204 
   205 lemma sum_commute_eqpoll: "A+B \<approx> B+A"
   206 apply (unfold eqpoll_def)
   207 apply (rule exI)
   208 apply (rule_tac c = "case(Inr,Inl)" and d = "case(Inr,Inl)" in lam_bijective)
   209 apply auto
   210 done
   211 
   212 lemma cadd_commute: "i |+| j = j |+| i"
   213 apply (unfold cadd_def)
   214 apply (rule sum_commute_eqpoll [THEN cardinal_cong])
   215 done
   216 
   217 (** Cardinal addition is associative **)
   218 
   219 lemma sum_assoc_eqpoll: "(A+B)+C \<approx> A+(B+C)"
   220 apply (unfold eqpoll_def)
   221 apply (rule exI)
   222 apply (rule sum_assoc_bij)
   223 done
   224 
   225 (*Unconditional version requires AC*)
   226 lemma well_ord_cadd_assoc: 
   227     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
   228      ==> (i |+| j) |+| k = i |+| (j |+| k)"
   229 apply (unfold cadd_def)
   230 apply (rule cardinal_cong)
   231 apply (rule eqpoll_trans)
   232  apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
   233  apply (blast intro: well_ord_radd elim:) 
   234 apply (rule sum_assoc_eqpoll [THEN eqpoll_trans])
   235 apply (rule eqpoll_sym)
   236 apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
   237 apply (blast intro: well_ord_radd elim:) 
   238 done
   239 
   240 (** 0 is the identity for addition **)
   241 
   242 lemma sum_0_eqpoll: "0+A \<approx> A"
   243 apply (unfold eqpoll_def)
   244 apply (rule exI)
   245 apply (rule bij_0_sum)
   246 done
   247 
   248 lemma cadd_0 [simp]: "Card(K) ==> 0 |+| K = K"
   249 apply (unfold cadd_def)
   250 apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
   251 done
   252 
   253 (** Addition by another cardinal **)
   254 
   255 lemma sum_lepoll_self: "A \<lesssim> A+B"
   256 apply (unfold lepoll_def inj_def)
   257 apply (rule_tac x = "lam x:A. Inl (x) " in exI)
   258 apply (simp (no_asm_simp))
   259 done
   260 
   261 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
   262 
   263 lemma cadd_le_self: 
   264     "[| Card(K);  Ord(L) |] ==> K le (K |+| L)"
   265 apply (unfold cadd_def)
   266 apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
   267 apply assumption; 
   268 apply (rule_tac [2] sum_lepoll_self)
   269 apply (blast intro: well_ord_radd well_ord_Memrel Card_is_Ord)
   270 done
   271 
   272 (** Monotonicity of addition **)
   273 
   274 lemma sum_lepoll_mono: 
   275      "[| A \<lesssim> C;  B \<lesssim> D |] ==> A + B  \<lesssim>  C + D"
   276 apply (unfold lepoll_def)
   277 apply (elim exE);
   278 apply (rule_tac x = "lam z:A+B. case (%w. Inl(f`w), %y. Inr(fa`y), z)" in exI)
   279 apply (rule_tac d = "case (%w. Inl(converse(f) `w), %y. Inr(converse(fa) `y))"
   280        in lam_injective)
   281 apply (typecheck add: inj_is_fun)
   282 apply auto
   283 done
   284 
   285 lemma cadd_le_mono:
   286     "[| K' le K;  L' le L |] ==> (K' |+| L') le (K |+| L)"
   287 apply (unfold cadd_def)
   288 apply (safe dest!: le_subset_iff [THEN iffD1])
   289 apply (rule well_ord_lepoll_imp_Card_le)
   290 apply (blast intro: well_ord_radd well_ord_Memrel)
   291 apply (blast intro: sum_lepoll_mono subset_imp_lepoll)
   292 done
   293 
   294 (** Addition of finite cardinals is "ordinary" addition **)
   295 
   296 (*????????????????upair.ML*)
   297 lemma eq_imp_not_mem: "a=A ==> a ~: A"
   298 apply (blast intro: elim: mem_irrefl); 
   299 done
   300 
   301 lemma sum_succ_eqpoll: "succ(A)+B \<approx> succ(A+B)"
   302 apply (unfold eqpoll_def)
   303 apply (rule exI)
   304 apply (rule_tac c = "%z. if z=Inl (A) then A+B else z" 
   305             and d = "%z. if z=A+B then Inl (A) else z" in lam_bijective)
   306    apply (simp_all)
   307 apply (blast dest: sym [THEN eq_imp_not_mem] elim: mem_irrefl)+
   308 done
   309 
   310 (*Pulling the  succ(...)  outside the |...| requires m, n: nat  *)
   311 (*Unconditional version requires AC*)
   312 lemma cadd_succ_lemma:
   313     "[| Ord(m);  Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"
   314 apply (unfold cadd_def)
   315 apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans])
   316 apply (rule succ_eqpoll_cong [THEN cardinal_cong])
   317 apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym])
   318 apply (blast intro: well_ord_radd well_ord_Memrel)
   319 done
   320 
   321 lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m |+| n = m#+n"
   322 apply (induct_tac "m")
   323 apply (simp add: nat_into_Card [THEN cadd_0])
   324 apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq])
   325 done
   326 
   327 
   328 (*** Cardinal multiplication ***)
   329 
   330 (** Cardinal multiplication is commutative **)
   331 
   332 (*Easier to prove the two directions separately*)
   333 lemma prod_commute_eqpoll: "A*B \<approx> B*A"
   334 apply (unfold eqpoll_def)
   335 apply (rule exI)
   336 apply (rule_tac c = "%<x,y>.<y,x>" and d = "%<x,y>.<y,x>" in lam_bijective)
   337 apply (auto ); 
   338 done
   339 
   340 lemma cmult_commute: "i |*| j = j |*| i"
   341 apply (unfold cmult_def)
   342 apply (rule prod_commute_eqpoll [THEN cardinal_cong])
   343 done
   344 
   345 (** Cardinal multiplication is associative **)
   346 
   347 lemma prod_assoc_eqpoll: "(A*B)*C \<approx> A*(B*C)"
   348 apply (unfold eqpoll_def)
   349 apply (rule exI)
   350 apply (rule prod_assoc_bij)
   351 done
   352 
   353 (*Unconditional version requires AC*)
   354 lemma well_ord_cmult_assoc:
   355     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
   356      ==> (i |*| j) |*| k = i |*| (j |*| k)"
   357 apply (unfold cmult_def)
   358 apply (rule cardinal_cong)
   359 apply (rule eqpoll_trans); 
   360  apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
   361  apply (blast intro: well_ord_rmult)
   362 apply (rule prod_assoc_eqpoll [THEN eqpoll_trans])
   363 apply (rule eqpoll_sym); 
   364 apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
   365 apply (blast intro: well_ord_rmult)
   366 done
   367 
   368 (** Cardinal multiplication distributes over addition **)
   369 
   370 lemma sum_prod_distrib_eqpoll: "(A+B)*C \<approx> (A*C)+(B*C)"
   371 apply (unfold eqpoll_def)
   372 apply (rule exI)
   373 apply (rule sum_prod_distrib_bij)
   374 done
   375 
   376 lemma well_ord_cadd_cmult_distrib:
   377     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
   378      ==> (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
   379 apply (unfold cadd_def cmult_def)
   380 apply (rule cardinal_cong)
   381 apply (rule eqpoll_trans); 
   382  apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])
   383 apply (blast intro: well_ord_radd)
   384 apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans])
   385 apply (rule eqpoll_sym); 
   386 apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll 
   387                                 well_ord_cardinal_eqpoll])
   388 apply (blast intro: well_ord_rmult)+
   389 done
   390 
   391 (** Multiplication by 0 yields 0 **)
   392 
   393 lemma prod_0_eqpoll: "0*A \<approx> 0"
   394 apply (unfold eqpoll_def)
   395 apply (rule exI)
   396 apply (rule lam_bijective)
   397 apply safe
   398 done
   399 
   400 lemma cmult_0 [simp]: "0 |*| i = 0"
   401 apply (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])
   402 done
   403 
   404 (** 1 is the identity for multiplication **)
   405 
   406 lemma prod_singleton_eqpoll: "{x}*A \<approx> A"
   407 apply (unfold eqpoll_def)
   408 apply (rule exI)
   409 apply (rule singleton_prod_bij [THEN bij_converse_bij])
   410 done
   411 
   412 lemma cmult_1 [simp]: "Card(K) ==> 1 |*| K = K"
   413 apply (unfold cmult_def succ_def)
   414 apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
   415 done
   416 
   417 (*** Some inequalities for multiplication ***)
   418 
   419 lemma prod_square_lepoll: "A \<lesssim> A*A"
   420 apply (unfold lepoll_def inj_def)
   421 apply (rule_tac x = "lam x:A. <x,x>" in exI)
   422 apply (simp (no_asm))
   423 done
   424 
   425 (*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
   426 lemma cmult_square_le: "Card(K) ==> K le K |*| K"
   427 apply (unfold cmult_def)
   428 apply (rule le_trans)
   429 apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
   430 apply (rule_tac [3] prod_square_lepoll)
   431 apply (simp (no_asm_simp) add: le_refl Card_is_Ord Card_cardinal_eq)
   432 apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord);
   433 done
   434 
   435 (** Multiplication by a non-zero cardinal **)
   436 
   437 lemma prod_lepoll_self: "b: B ==> A \<lesssim> A*B"
   438 apply (unfold lepoll_def inj_def)
   439 apply (rule_tac x = "lam x:A. <x,b>" in exI)
   440 apply (simp (no_asm_simp))
   441 done
   442 
   443 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
   444 lemma cmult_le_self:
   445     "[| Card(K);  Ord(L);  0<L |] ==> K le (K |*| L)"
   446 apply (unfold cmult_def)
   447 apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
   448   apply assumption; 
   449  apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
   450 apply (blast intro: prod_lepoll_self ltD)
   451 done
   452 
   453 (** Monotonicity of multiplication **)
   454 
   455 lemma prod_lepoll_mono:
   456      "[| A \<lesssim> C;  B \<lesssim> D |] ==> A * B  \<lesssim>  C * D"
   457 apply (unfold lepoll_def)
   458 apply (elim exE);
   459 apply (rule_tac x = "lam <w,y>:A*B. <f`w, fa`y>" in exI)
   460 apply (rule_tac d = "%<w,y>. <converse (f) `w, converse (fa) `y>" 
   461        in lam_injective)
   462 apply (typecheck add: inj_is_fun)
   463 apply auto
   464 done
   465 
   466 lemma cmult_le_mono:
   467     "[| K' le K;  L' le L |] ==> (K' |*| L') le (K |*| L)"
   468 apply (unfold cmult_def)
   469 apply (safe dest!: le_subset_iff [THEN iffD1])
   470 apply (rule well_ord_lepoll_imp_Card_le)
   471  apply (blast intro: well_ord_rmult well_ord_Memrel)
   472 apply (blast intro: prod_lepoll_mono subset_imp_lepoll)
   473 done
   474 
   475 (*** Multiplication of finite cardinals is "ordinary" multiplication ***)
   476 
   477 lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B"
   478 apply (unfold eqpoll_def)
   479 apply (rule exI);
   480 apply (rule_tac c = "%<x,y>. if x=A then Inl (y) else Inr (<x,y>)"
   481             and d = "case (%y. <A,y>, %z. z)" in lam_bijective)
   482 apply safe
   483 apply (simp_all add: succI2 if_type mem_imp_not_eq)
   484 done
   485 
   486 (*Unconditional version requires AC*)
   487 lemma cmult_succ_lemma:
   488     "[| Ord(m);  Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"
   489 apply (unfold cmult_def cadd_def)
   490 apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])
   491 apply (rule cardinal_cong [symmetric])
   492 apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
   493 apply (blast intro: well_ord_rmult well_ord_Memrel)
   494 done
   495 
   496 lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m |*| n = m#*n"
   497 apply (induct_tac "m")
   498 apply (simp (no_asm_simp))
   499 apply (simp (no_asm_simp) add: cmult_succ_lemma nat_cadd_eq_add)
   500 done
   501 
   502 lemma cmult_2: "Card(n) ==> 2 |*| n = n |+| n"
   503 apply (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
   504 done
   505 
   506 lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
   507 apply (rule lepoll_trans); 
   508 apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll]) 
   509 apply (erule prod_lepoll_mono) 
   510 apply (rule lepoll_refl); 
   511 done
   512 
   513 lemma lepoll_imp_sum_lepoll_prod: "[| A \<lesssim> B; 2 \<lesssim> A |] ==> A+B \<lesssim> A*B"
   514 apply (blast intro: sum_lepoll_mono sum_lepoll_prod lepoll_trans lepoll_refl)
   515 done
   516 
   517 
   518 (*** Infinite Cardinals are Limit Ordinals ***)
   519 
   520 (*This proof is modelled upon one assuming nat<=A, with injection
   521   lam z:cons(u,A). if z=u then 0 else if z : nat then succ(z) else z
   522   and inverse %y. if y:nat then nat_case(u, %z. z, y) else y.  \
   523   If f: inj(nat,A) then range(f) behaves like the natural numbers.*)
   524 lemma nat_cons_lepoll: "nat \<lesssim> A ==> cons(u,A) \<lesssim> A"
   525 apply (unfold lepoll_def)
   526 apply (erule exE)
   527 apply (rule_tac x = 
   528           "lam z:cons (u,A).
   529              if z=u then f`0 
   530              else if z: range (f) then f`succ (converse (f) `z) else z" 
   531        in exI)
   532 apply (rule_tac d =
   533           "%y. if y: range(f) then nat_case (u, %z. f`z, converse(f) `y) 
   534                               else y" 
   535        in lam_injective)
   536 apply (fast intro!: if_type apply_type intro: inj_is_fun inj_converse_fun)
   537 apply (simp add: inj_is_fun [THEN apply_rangeI]
   538                  inj_converse_fun [THEN apply_rangeI]
   539                  inj_converse_fun [THEN apply_funtype])
   540 done
   541 
   542 lemma nat_cons_eqpoll: "nat \<lesssim> A ==> cons(u,A) \<approx> A"
   543 apply (erule nat_cons_lepoll [THEN eqpollI])
   544 apply (rule subset_consI [THEN subset_imp_lepoll])
   545 done
   546 
   547 (*Specialized version required below*)
   548 lemma nat_succ_eqpoll: "nat <= A ==> succ(A) \<approx> A"
   549 apply (unfold succ_def)
   550 apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll])
   551 done
   552 
   553 lemma InfCard_nat: "InfCard(nat)"
   554 apply (unfold InfCard_def)
   555 apply (blast intro: Card_nat le_refl Card_is_Ord)
   556 done
   557 
   558 lemma InfCard_is_Card: "InfCard(K) ==> Card(K)"
   559 apply (unfold InfCard_def)
   560 apply (erule conjunct1)
   561 done
   562 
   563 lemma InfCard_Un:
   564     "[| InfCard(K);  Card(L) |] ==> InfCard(K Un L)"
   565 apply (unfold InfCard_def)
   566 apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans]  Card_is_Ord)
   567 done
   568 
   569 (*Kunen's Lemma 10.11*)
   570 lemma InfCard_is_Limit: "InfCard(K) ==> Limit(K)"
   571 apply (unfold InfCard_def)
   572 apply (erule conjE)
   573 apply (frule Card_is_Ord)
   574 apply (rule ltI [THEN non_succ_LimitI])
   575 apply (erule le_imp_subset [THEN subsetD])
   576 apply (safe dest!: Limit_nat [THEN Limit_le_succD])
   577 apply (unfold Card_def)
   578 apply (drule trans)
   579 apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong])
   580 apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl])
   581 apply (rule le_eqI) 
   582 apply assumption; 
   583 apply (rule Ord_cardinal)
   584 done
   585 
   586 
   587 (*** An infinite cardinal equals its square (Kunen, Thm 10.12, page 29) ***)
   588 
   589 (*A general fact about ordermap*)
   590 lemma ordermap_eqpoll_pred:
   591     "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> pred(A,x,r)"
   592 apply (unfold eqpoll_def)
   593 apply (rule exI)
   594 apply (simp (no_asm_simp) add: ordermap_eq_image well_ord_is_wf)
   595 apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij, THEN bij_converse_bij])
   596 apply (rule pred_subset)
   597 done
   598 
   599 (** Establishing the well-ordering **)
   600 
   601 lemma csquare_lam_inj:
   602      "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)"
   603 apply (unfold inj_def)
   604 apply (force intro: lam_type Un_least_lt [THEN ltD] ltI)
   605 done
   606 
   607 lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))"
   608 apply (unfold csquare_rel_def)
   609 apply (rule csquare_lam_inj [THEN well_ord_rvimage])
   610 apply assumption; 
   611 apply (blast intro: well_ord_rmult well_ord_Memrel)
   612 done
   613 
   614 (** Characterising initial segments of the well-ordering **)
   615 
   616 lemma csquareD:
   617  "[| <<x,y>, <z,z>> : csquare_rel(K);  x<K;  y<K;  z<K |] ==> x le z & y le z"
   618 apply (unfold csquare_rel_def)
   619 apply (erule rev_mp)
   620 apply (elim ltE)
   621 apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
   622 apply (safe elim!: mem_irrefl intro!: Un_upper1_le Un_upper2_le)
   623 apply (simp_all (no_asm_simp) add: lt_def succI2)
   624 done
   625 
   626 lemma pred_csquare_subset: 
   627     "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
   628 apply (unfold Order.pred_def)
   629 apply (safe del: SigmaI succCI)
   630 apply (erule csquareD [THEN conjE])
   631 apply (unfold lt_def)
   632 apply (auto ); 
   633 done
   634 
   635 lemma csquare_ltI:
   636  "[| x<z;  y<z;  z<K |] ==>  <<x,y>, <z,z>> : csquare_rel(K)"
   637 apply (unfold csquare_rel_def)
   638 apply (subgoal_tac "x<K & y<K")
   639  prefer 2 apply (blast intro: lt_trans) 
   640 apply (elim ltE)
   641 apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
   642 done
   643 
   644 (*Part of the traditional proof.  UNUSED since it's harder to prove & apply *)
   645 lemma csquare_or_eqI:
   646  "[| x le z;  y le z;  z<K |] ==> <<x,y>, <z,z>> : csquare_rel(K) | x=z & y=z"
   647 apply (unfold csquare_rel_def)
   648 apply (subgoal_tac "x<K & y<K")
   649  prefer 2 apply (blast intro: lt_trans1) 
   650 apply (elim ltE)
   651 apply (simp (no_asm_simp) add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
   652 apply (elim succE)
   653 apply (simp_all (no_asm_simp) add: subset_Un_iff [THEN iff_sym] subset_Un_iff2 [THEN iff_sym] OrdmemD)
   654 done
   655 
   656 (** The cardinality of initial segments **)
   657 
   658 lemma ordermap_z_lt:
   659       "[| Limit(K);  x<K;  y<K;  z=succ(x Un y) |] ==>
   660           ordermap(K*K, csquare_rel(K)) ` <x,y> <
   661           ordermap(K*K, csquare_rel(K)) ` <z,z>"
   662 apply (subgoal_tac "z<K & well_ord (K*K, csquare_rel (K))")
   663 prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ
   664                               Limit_is_Ord [THEN well_ord_csquare])
   665 apply (clarify ); 
   666 apply (rule csquare_ltI [THEN ordermap_mono, THEN ltI])
   667 apply (erule_tac [4] well_ord_is_wf)
   668 apply (blast intro!: Un_upper1_le Un_upper2_le Ord_ordermap elim!: ltE)+
   669 done
   670 
   671 (*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
   672 lemma ordermap_csquare_le:
   673   "[| Limit(K);  x<K;  y<K;  z=succ(x Un y) |] ==>
   674         | ordermap(K*K, csquare_rel(K)) ` <x,y> | le  |succ(z)| |*| |succ(z)|"
   675 apply (unfold cmult_def)
   676 apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
   677 apply (rule Ord_cardinal [THEN well_ord_Memrel])+
   678 apply (subgoal_tac "z<K")
   679  prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ)
   680 apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans])
   681 apply assumption +
   682 apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
   683 apply (erule Limit_is_Ord [THEN well_ord_csquare])
   684 apply (blast intro: ltD)
   685 apply (rule pred_csquare_subset [THEN subset_imp_lepoll, THEN lepoll_trans],
   686             assumption)
   687 apply (elim ltE)
   688 apply (rule prod_eqpoll_cong [THEN eqpoll_sym, THEN eqpoll_imp_lepoll])
   689 apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+
   690 done
   691 
   692 (*Kunen: "... so the order type <= K" *)
   693 lemma ordertype_csquare_le:
   694      "[| InfCard(K);  ALL y:K. InfCard(y) --> y |*| y = y |] 
   695       ==> ordertype(K*K, csquare_rel(K)) le K"
   696 apply (frule InfCard_is_Card [THEN Card_is_Ord])
   697 apply (rule all_lt_imp_le)
   698 apply assumption
   699 apply (erule well_ord_csquare [THEN Ord_ordertype])
   700 apply (rule Card_lt_imp_lt)
   701 apply (erule_tac [3] InfCard_is_Card)
   702 apply (erule_tac [2] ltE)
   703 apply (simp add: ordertype_unfold)
   704 apply (safe elim!: ltE)
   705 apply (subgoal_tac "Ord (xa) & Ord (ya)")
   706  prefer 2 apply (blast intro: Ord_in_Ord)
   707 apply (clarify );
   708 (*??WHAT A MESS!*)  
   709 apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
   710        (assumption | rule refl | erule ltI)+) 
   711 apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2,
   712        simp_all add: Ord_Un Ord_nat)
   713 prefer 2 (*case nat le (xa Un ya) *)
   714  apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] 
   715                   le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un
   716                 ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD])
   717 (*the finite case: xa Un ya < nat *)
   718 apply (rule_tac j = "nat" in lt_trans2)
   719  apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
   720                   nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
   721 apply (simp add: InfCard_def)
   722 done
   723 
   724 (*Main result: Kunen's Theorem 10.12*)
   725 lemma InfCard_csquare_eq: "InfCard(K) ==> K |*| K = K"
   726 apply (frule InfCard_is_Card [THEN Card_is_Ord])
   727 apply (erule rev_mp)
   728 apply (erule_tac i=K in trans_induct) 
   729 apply (rule impI)
   730 apply (rule le_anti_sym)
   731 apply (erule_tac [2] InfCard_is_Card [THEN cmult_square_le])
   732 apply (rule ordertype_csquare_le [THEN [2] le_trans])
   733 prefer 2 apply (assumption)
   734 prefer 2 apply (assumption)
   735 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])
   736 done
   737 
   738 (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
   739 lemma well_ord_InfCard_square_eq:
   740      "[| well_ord(A,r);  InfCard(|A|) |] ==> A*A \<approx> A"
   741 apply (rule prod_eqpoll_cong [THEN eqpoll_trans])
   742 apply (erule well_ord_cardinal_eqpoll [THEN eqpoll_sym])+
   743 apply (rule well_ord_cardinal_eqE)
   744 apply (blast intro: Ord_cardinal well_ord_rmult well_ord_Memrel)
   745 apply assumption; 
   746 apply (simp (no_asm_simp) add: cmult_def [symmetric] InfCard_csquare_eq)
   747 done
   748 
   749 (** Toward's Kunen's Corollary 10.13 (1) **)
   750 
   751 lemma InfCard_le_cmult_eq: "[| InfCard(K);  L le K;  0<L |] ==> K |*| L = K"
   752 apply (rule le_anti_sym)
   753  prefer 2
   754  apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card)
   755 apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl])
   756 apply (rule cmult_le_mono [THEN le_trans], assumption+)
   757 apply (simp add: InfCard_csquare_eq)
   758 done
   759 
   760 (*Corollary 10.13 (1), for cardinal multiplication*)
   761 lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K Un L"
   762 apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
   763 apply (typecheck add: InfCard_is_Card Card_is_Ord)
   764 apply (rule cmult_commute [THEN ssubst])
   765 apply (rule Un_commute [THEN ssubst])
   766 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)
   767 done
   768 
   769 lemma InfCard_cdouble_eq: "InfCard(K) ==> K |+| K = K"
   770 apply (simp (no_asm_simp) add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)
   771 apply (simp (no_asm_simp) add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)
   772 done
   773 
   774 (*Corollary 10.13 (1), for cardinal addition*)
   775 lemma InfCard_le_cadd_eq: "[| InfCard(K);  L le K |] ==> K |+| L = K"
   776 apply (rule le_anti_sym)
   777  prefer 2
   778  apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card)
   779 apply (frule InfCard_is_Card [THEN Card_is_Ord, THEN le_refl])
   780 apply (rule cadd_le_mono [THEN le_trans], assumption+)
   781 apply (simp add: InfCard_cdouble_eq)
   782 done
   783 
   784 lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L"
   785 apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
   786 apply (typecheck add: InfCard_is_Card Card_is_Ord)
   787 apply (rule cadd_commute [THEN ssubst])
   788 apply (rule Un_commute [THEN ssubst])
   789 apply (simp_all (no_asm_simp) add: InfCard_le_cadd_eq subset_Un_iff2 [THEN iffD1] le_imp_subset)
   790 done
   791 
   792 (*The other part, Corollary 10.13 (2), refers to the cardinality of the set
   793   of all n-tuples of elements of K.  A better version for the Isabelle theory
   794   might be  InfCard(K) ==> |list(K)| = K.
   795 *)
   796 
   797 (*** For every cardinal number there exists a greater one
   798      [Kunen's Theorem 10.16, which would be trivial using AC] ***)
   799 
   800 lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))"
   801 apply (unfold jump_cardinal_def)
   802 apply (rule Ord_is_Transset [THEN [2] OrdI])
   803  prefer 2 apply (blast intro!: Ord_ordertype)
   804 apply (unfold Transset_def)
   805 apply (safe del: subsetI)
   806 apply (simp add: ordertype_pred_unfold)
   807 apply safe
   808 apply (rule UN_I)
   809 apply (rule_tac [2] ReplaceI)
   810    prefer 4 apply (blast intro: well_ord_subset elim!: predE)+
   811 done
   812 
   813 (*Allows selective unfolding.  Less work than deriving intro/elim rules*)
   814 lemma jump_cardinal_iff:
   815      "i : jump_cardinal(K) <->
   816       (EX r X. r <= K*K & X <= K & well_ord(X,r) & i = ordertype(X,r))"
   817 apply (unfold jump_cardinal_def)
   818 apply (blast del: subsetI) 
   819 done
   820 
   821 (*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*)
   822 lemma K_lt_jump_cardinal: "Ord(K) ==> K < jump_cardinal(K)"
   823 apply (rule Ord_jump_cardinal [THEN [2] ltI])
   824 apply (rule jump_cardinal_iff [THEN iffD2])
   825 apply (rule_tac x="Memrel(K)" in exI)
   826 apply (rule_tac x=K in exI)  
   827 apply (simp add: ordertype_Memrel well_ord_Memrel)
   828 apply (simp add: Memrel_def subset_iff)
   829 done
   830 
   831 (*The proof by contradiction: the bijection f yields a wellordering of X
   832   whose ordertype is jump_cardinal(K).  *)
   833 lemma Card_jump_cardinal_lemma:
   834      "[| well_ord(X,r);  r <= K * K;  X <= K;
   835          f : bij(ordertype(X,r), jump_cardinal(K)) |]
   836       ==> jump_cardinal(K) : jump_cardinal(K)"
   837 apply (subgoal_tac "f O ordermap (X,r) : bij (X, jump_cardinal (K))")
   838  prefer 2 apply (blast intro: comp_bij ordermap_bij)
   839 apply (rule jump_cardinal_iff [THEN iffD2])
   840 apply (intro exI conjI)
   841 apply (rule subset_trans [OF rvimage_type Sigma_mono])
   842 apply assumption+
   843 apply (erule bij_is_inj [THEN well_ord_rvimage])
   844 apply (rule Ord_jump_cardinal [THEN well_ord_Memrel])
   845 apply (simp add: well_ord_Memrel [THEN [2] bij_ordertype_vimage]
   846                  ordertype_Memrel Ord_jump_cardinal)
   847 done
   848 
   849 (*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*)
   850 lemma Card_jump_cardinal: "Card(jump_cardinal(K))"
   851 apply (rule Ord_jump_cardinal [THEN CardI])
   852 apply (unfold eqpoll_def)
   853 apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1])
   854 apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl])
   855 done
   856 
   857 (*** Basic properties of successor cardinals ***)
   858 
   859 lemma csucc_basic: "Ord(K) ==> Card(csucc(K)) & K < csucc(K)"
   860 apply (unfold csucc_def)
   861 apply (rule LeastI)
   862 apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+
   863 done
   864 
   865 lemmas Card_csucc = csucc_basic [THEN conjunct1, standard]
   866 
   867 lemmas lt_csucc = csucc_basic [THEN conjunct2, standard]
   868 
   869 lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)"
   870 apply (blast intro: Ord_0_le lt_csucc lt_trans1)
   871 done
   872 
   873 lemma csucc_le: "[| Card(L);  K<L |] ==> csucc(K) le L"
   874 apply (unfold csucc_def)
   875 apply (rule Least_le)
   876 apply (blast intro: Card_is_Ord)+
   877 done
   878 
   879 lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K"
   880 apply (rule iffI)
   881 apply (rule_tac [2] Card_lt_imp_lt)
   882 apply (erule_tac [2] lt_trans1)
   883 apply (simp_all add: lt_csucc Card_csucc Card_is_Ord)
   884 apply (rule notI [THEN not_lt_imp_le])
   885 apply (rule Card_cardinal [THEN csucc_le, THEN lt_trans1, THEN lt_irrefl])
   886 apply assumption
   887 apply (rule Ord_cardinal_le [THEN lt_trans1])
   888 apply (simp_all add: Ord_cardinal Card_is_Ord) 
   889 done
   890 
   891 lemma Card_lt_csucc_iff:
   892      "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"
   893 by (simp (no_asm_simp) add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
   894 
   895 lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))"
   896 by (simp add: InfCard_def Card_csucc Card_is_Ord 
   897               lt_csucc [THEN leI, THEN [2] le_trans])
   898 
   899 
   900 (*** Finite sets ***)
   901 
   902 lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
   903 apply (induct_tac "n")
   904 apply (simp (no_asm) add: eqpoll_0_iff)
   905 apply clarify
   906 apply (subgoal_tac "EX u. u:A")
   907 apply (erule exE)
   908 apply (rule Diff_sing_eqpoll [THEN revcut_rl])
   909 prefer 2 apply (assumption)
   910 apply assumption
   911 apply (rule_tac b = "A" in cons_Diff [THEN subst])
   912 apply assumption
   913 apply (rule Fin.consI)
   914 apply blast
   915 apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
   916 (*Now for the lemma assumed above*)
   917 apply (unfold eqpoll_def)
   918 apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
   919 done
   920 
   921 lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)"
   922 apply (unfold Finite_def)
   923 apply (blast intro: Fin_lemma)
   924 done
   925 
   926 lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
   927 apply (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
   928 done
   929 
   930 lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
   931 apply (blast intro: Finite_into_Fin Fin_into_Finite)
   932 done
   933 
   934 lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
   935 by (blast intro!: Fin_into_Finite Fin_UnI 
   936           dest!: Finite_into_Fin
   937           intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 
   938                  Un_upper2 [THEN Fin_mono, THEN subsetD])
   939 
   940 lemma Finite_Union: "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))"
   941 apply (simp add: Finite_Fin_iff)
   942 apply (rule Fin_UnionI)
   943 apply (erule Fin_induct)
   944 apply (simp (no_asm))
   945 apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
   946 done
   947 
   948 (* Induction principle for Finite(A), by Sidi Ehmety *)
   949 lemma Finite_induct:
   950 "[| Finite(A); P(0);
   951     !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
   952  ==> P(A)"
   953 apply (erule Finite_into_Fin [THEN Fin_induct]) 
   954 apply (blast intro: Fin_into_Finite)+
   955 done
   956 
   957 
   958 (** Removing elements from a finite set decreases its cardinality **)
   959 
   960 lemma Fin_imp_not_cons_lepoll: "A: Fin(U) ==> x~:A --> ~ cons(x,A) \<lesssim> A"
   961 apply (erule Fin_induct)
   962 apply (simp (no_asm) add: lepoll_0_iff)
   963 apply (subgoal_tac "cons (x,cons (xa,y)) = cons (xa,cons (x,y))")
   964 apply (simp (no_asm_simp))
   965 apply (blast dest!: cons_lepoll_consD)
   966 apply blast
   967 done
   968 
   969 lemma Finite_imp_cardinal_cons: "[| Finite(A);  a~:A |] ==> |cons(a,A)| = succ(|A|)"
   970 apply (unfold cardinal_def)
   971 apply (rule Least_equality)
   972 apply (fold cardinal_def)
   973 apply (simp (no_asm) add: succ_def)
   974 apply (blast intro: cons_eqpoll_cong well_ord_cardinal_eqpoll
   975              elim!: mem_irrefl  dest!: Finite_imp_well_ord)
   976 apply (blast intro: Card_cardinal Card_is_Ord)
   977 apply (rule notI)
   978 apply (rule Finite_into_Fin [THEN Fin_imp_not_cons_lepoll, THEN mp, THEN notE])
   979 apply assumption
   980 apply assumption
   981 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
   982 apply (erule le_imp_lepoll [THEN lepoll_trans])
   983 apply (blast intro: well_ord_cardinal_eqpoll [THEN eqpoll_imp_lepoll]
   984              dest!: Finite_imp_well_ord)
   985 done
   986 
   987 
   988 lemma Finite_imp_succ_cardinal_Diff: "[| Finite(A);  a:A |] ==> succ(|A-{a}|) = |A|"
   989 apply (rule_tac b = "A" in cons_Diff [THEN subst])
   990 apply assumption
   991 apply (simp (no_asm_simp) add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
   992 apply (simp (no_asm_simp) add: cons_Diff)
   993 done
   994 
   995 lemma Finite_imp_cardinal_Diff: "[| Finite(A);  a:A |] ==> |A-{a}| < |A|"
   996 apply (rule succ_leE)
   997 apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff)
   998 done
   999 
  1000 
  1001 (** Theorems by Krzysztof Grabczewski, proofs by lcp **)
  1002 
  1003 lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard]
  1004 
  1005 lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n"
  1006 apply (rule eqpoll_trans)
  1007 apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
  1008 apply (erule nat_implies_well_ord)+
  1009 apply (simp (no_asm_simp) add: nat_cadd_eq_add [symmetric] cadd_def eqpoll_refl)
  1010 done
  1011 
  1012 
  1013 (*** Theorems by Sidi Ehmety ***)
  1014 
  1015 (*The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
  1016 lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
  1017 apply (unfold Finite_def)
  1018 apply (case_tac "a:A")
  1019 apply (subgoal_tac [2] "A-{a}=A")
  1020 apply auto
  1021 apply (rule_tac x = "succ (n) " in bexI)
  1022 apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
  1023 apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
  1024 apply (auto dest: mem_irrefl)
  1025 done
  1026 
  1027 (*And the contrapositive of this says
  1028    [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
  1029 lemma Diff_Finite [rule_format (no_asm)]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
  1030 apply (erule Finite_induct)
  1031 apply auto
  1032 apply (case_tac "x:A")
  1033  apply (subgoal_tac [2] "A-cons (x, B) = A - B")
  1034 apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
  1035 apply (rotate_tac -1)
  1036 apply simp
  1037 apply (drule Diff_sing_Finite)
  1038 apply auto
  1039 done
  1040 
  1041 lemma Ord_subset_natD [rule_format (no_asm)]: "Ord(i) ==> i <= nat --> i : nat | i=nat"
  1042 apply (erule trans_induct3)
  1043 apply auto
  1044 apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
  1045 done
  1046 
  1047 lemma Ord_nat_subset_into_Card: "[| Ord(i); i <= nat |] ==> Card(i)"
  1048 apply (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
  1049 done
  1050 
  1051 lemma Finite_cardinal_in_nat [simp]: "Finite(A) ==> |A| : nat"
  1052 apply (erule Finite_induct)
  1053 apply (auto simp add: cardinal_0 Finite_imp_cardinal_cons)
  1054 done
  1055 
  1056 lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1"
  1057 apply (rule succ_inject)
  1058 apply (rule_tac b = "|A|" in trans)
  1059 apply (simp (no_asm_simp) add: Finite_imp_succ_cardinal_Diff)
  1060 apply (subgoal_tac "1 \<lesssim> A")
  1061 prefer 2 apply (blast intro: not_0_is_lepoll_1)
  1062 apply (frule Finite_imp_well_ord)
  1063 apply clarify
  1064 apply (rotate_tac -1)
  1065 apply (drule well_ord_lepoll_imp_Card_le)
  1066 apply (auto simp add: cardinal_1)
  1067 apply (rule trans)
  1068 apply (rule_tac [2] diff_succ)
  1069 apply (auto simp add: Finite_cardinal_in_nat)
  1070 done
  1071 
  1072 lemma cardinal_lt_imp_Diff_not_0 [rule_format (no_asm)]: "Finite(B) ==> ALL A. |B|<|A| --> A - B ~= 0"
  1073 apply (erule Finite_induct)
  1074 apply auto
  1075 apply (simp_all add: Finite_imp_cardinal_cons)
  1076 apply (case_tac "Finite (A) ")
  1077 apply (subgoal_tac [2] "Finite (cons (x, B))")
  1078 apply (drule_tac [2] B = "cons (x, B) " in Diff_Finite)
  1079 apply (auto simp add: Finite_0 Finite_cons)
  1080 apply (subgoal_tac "|B|<|A|")
  1081 prefer 2 apply (blast intro: lt_trans Ord_cardinal)
  1082 apply (case_tac "x:A")
  1083 apply (subgoal_tac [2] "A - cons (x, B) = A - B")
  1084 apply auto
  1085 apply (subgoal_tac "|A| le |cons (x, B) |")
  1086 prefer 2
  1087  apply (blast dest: Finite_cons [THEN Finite_imp_well_ord] 
  1088               intro: well_ord_lepoll_imp_Card_le subset_imp_lepoll)
  1089 apply (auto simp add: Finite_imp_cardinal_cons)
  1090 apply (auto dest!: Finite_cardinal_in_nat simp add: le_iff)
  1091 apply (blast intro: lt_trans)
  1092 done
  1093 
  1094 
  1095 ML{*
  1096 val InfCard_def = thm "InfCard_def"
  1097 val cmult_def = thm "cmult_def"
  1098 val cadd_def = thm "cadd_def"
  1099 val jump_cardinal_def = thm "jump_cardinal_def"
  1100 val csucc_def = thm "csucc_def"
  1101 
  1102 val sum_commute_eqpoll = thm "sum_commute_eqpoll";
  1103 val cadd_commute = thm "cadd_commute";
  1104 val sum_assoc_eqpoll = thm "sum_assoc_eqpoll";
  1105 val well_ord_cadd_assoc = thm "well_ord_cadd_assoc";
  1106 val sum_0_eqpoll = thm "sum_0_eqpoll";
  1107 val cadd_0 = thm "cadd_0";
  1108 val sum_lepoll_self = thm "sum_lepoll_self";
  1109 val cadd_le_self = thm "cadd_le_self";
  1110 val sum_lepoll_mono = thm "sum_lepoll_mono";
  1111 val cadd_le_mono = thm "cadd_le_mono";
  1112 val eq_imp_not_mem = thm "eq_imp_not_mem";
  1113 val sum_succ_eqpoll = thm "sum_succ_eqpoll";
  1114 val nat_cadd_eq_add = thm "nat_cadd_eq_add";
  1115 val prod_commute_eqpoll = thm "prod_commute_eqpoll";
  1116 val cmult_commute = thm "cmult_commute";
  1117 val prod_assoc_eqpoll = thm "prod_assoc_eqpoll";
  1118 val well_ord_cmult_assoc = thm "well_ord_cmult_assoc";
  1119 val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll";
  1120 val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib";
  1121 val prod_0_eqpoll = thm "prod_0_eqpoll";
  1122 val cmult_0 = thm "cmult_0";
  1123 val prod_singleton_eqpoll = thm "prod_singleton_eqpoll";
  1124 val cmult_1 = thm "cmult_1";
  1125 val prod_lepoll_self = thm "prod_lepoll_self";
  1126 val cmult_le_self = thm "cmult_le_self";
  1127 val prod_lepoll_mono = thm "prod_lepoll_mono";
  1128 val cmult_le_mono = thm "cmult_le_mono";
  1129 val prod_succ_eqpoll = thm "prod_succ_eqpoll";
  1130 val nat_cmult_eq_mult = thm "nat_cmult_eq_mult";
  1131 val cmult_2 = thm "cmult_2";
  1132 val sum_lepoll_prod = thm "sum_lepoll_prod";
  1133 val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod";
  1134 val nat_cons_lepoll = thm "nat_cons_lepoll";
  1135 val nat_cons_eqpoll = thm "nat_cons_eqpoll";
  1136 val nat_succ_eqpoll = thm "nat_succ_eqpoll";
  1137 val InfCard_nat = thm "InfCard_nat";
  1138 val InfCard_is_Card = thm "InfCard_is_Card";
  1139 val InfCard_Un = thm "InfCard_Un";
  1140 val InfCard_is_Limit = thm "InfCard_is_Limit";
  1141 val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred";
  1142 val ordermap_z_lt = thm "ordermap_z_lt";
  1143 val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq";
  1144 val InfCard_cmult_eq = thm "InfCard_cmult_eq";
  1145 val InfCard_cdouble_eq = thm "InfCard_cdouble_eq";
  1146 val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq";
  1147 val InfCard_cadd_eq = thm "InfCard_cadd_eq";
  1148 val Ord_jump_cardinal = thm "Ord_jump_cardinal";
  1149 val jump_cardinal_iff = thm "jump_cardinal_iff";
  1150 val K_lt_jump_cardinal = thm "K_lt_jump_cardinal";
  1151 val Card_jump_cardinal = thm "Card_jump_cardinal";
  1152 val csucc_basic = thm "csucc_basic";
  1153 val Card_csucc = thm "Card_csucc";
  1154 val lt_csucc = thm "lt_csucc";
  1155 val Ord_0_lt_csucc = thm "Ord_0_lt_csucc";
  1156 val csucc_le = thm "csucc_le";
  1157 val lt_csucc_iff = thm "lt_csucc_iff";
  1158 val Card_lt_csucc_iff = thm "Card_lt_csucc_iff";
  1159 val InfCard_csucc = thm "InfCard_csucc";
  1160 val Finite_into_Fin = thm "Finite_into_Fin";
  1161 val Fin_into_Finite = thm "Fin_into_Finite";
  1162 val Finite_Fin_iff = thm "Finite_Fin_iff";
  1163 val Finite_Un = thm "Finite_Un";
  1164 val Finite_Union = thm "Finite_Union";
  1165 val Finite_induct = thm "Finite_induct";
  1166 val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll";
  1167 val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons";
  1168 val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff";
  1169 val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff";
  1170 val nat_implies_well_ord = thm "nat_implies_well_ord";
  1171 val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum";
  1172 val Diff_sing_Finite = thm "Diff_sing_Finite";
  1173 val Diff_Finite = thm "Diff_Finite";
  1174 val Ord_subset_natD = thm "Ord_subset_natD";
  1175 val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card";
  1176 val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat";
  1177 val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1";
  1178 val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0";
  1179 *}
  1180 
  1181 end