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