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