src/ZF/Cardinal.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 14153 76a6ba67bd15
child 14883 ca000a495448
permissions -rw-r--r--
use more symbols in HTML output
     1 (*  Title:      ZF/Cardinal.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 Numbers Without the Axiom of Choice*}
     9 
    10 theory Cardinal = OrderType + Finite + Nat + Sum:
    11 
    12 constdefs
    13 
    14   (*least ordinal operator*)
    15    Least    :: "(i=>o) => i"    (binder "LEAST " 10)
    16      "Least(P) == THE i. Ord(i) & P(i) & (ALL j. j<i --> ~P(j))"
    17 
    18   eqpoll   :: "[i,i] => o"     (infixl "eqpoll" 50)
    19     "A eqpoll B == EX f. f: bij(A,B)"
    20 
    21   lepoll   :: "[i,i] => o"     (infixl "lepoll" 50)
    22     "A lepoll B == EX f. f: inj(A,B)"
    23 
    24   lesspoll :: "[i,i] => o"     (infixl "lesspoll" 50)
    25     "A lesspoll B == A lepoll B & ~(A eqpoll B)"
    26 
    27   cardinal :: "i=>i"           ("|_|")
    28     "|A| == LEAST i. i eqpoll A"
    29 
    30   Finite   :: "i=>o"
    31     "Finite(A) == EX n:nat. A eqpoll n"
    32 
    33   Card     :: "i=>o"
    34     "Card(i) == (i = |i|)"
    35 
    36 syntax (xsymbols)
    37   "eqpoll"      :: "[i,i] => o"       (infixl "\<approx>" 50)
    38   "lepoll"      :: "[i,i] => o"       (infixl "\<lesssim>" 50)
    39   "lesspoll"    :: "[i,i] => o"       (infixl "\<prec>" 50)
    40   "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
    41 
    42 syntax (HTML output)
    43   "eqpoll"      :: "[i,i] => o"       (infixl "\<approx>" 50)
    44   "LEAST "         :: "[pttrn, o] => i"  ("(3\<mu>_./ _)" [0, 10] 10)
    45 
    46 subsection{*The Schroeder-Bernstein Theorem*}
    47 text{*See Davey and Priestly, page 106*}
    48 
    49 (** Lemma: Banach's Decomposition Theorem **)
    50 
    51 lemma decomp_bnd_mono: "bnd_mono(X, %W. X - g``(Y - f``W))"
    52 by (rule bnd_monoI, blast+)
    53 
    54 lemma Banach_last_equation:
    55     "g: Y->X
    56      ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =        
    57 	 X - lfp(X, %W. X - g``(Y - f``W))" 
    58 apply (rule_tac P = "%u. ?v = X-u" 
    59        in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
    60 apply (simp add: double_complement  fun_is_rel [THEN image_subset])
    61 done
    62 
    63 lemma decomposition:
    64      "[| f: X->Y;  g: Y->X |] ==>    
    65       EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) &     
    66                       (YA Int YB = 0) & (YA Un YB = Y) &     
    67                       f``XA=YA & g``YB=XB"
    68 apply (intro exI conjI)
    69 apply (rule_tac [6] Banach_last_equation)
    70 apply (rule_tac [5] refl)
    71 apply (assumption | 
    72        rule  Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
    73 done
    74 
    75 lemma schroeder_bernstein:
    76     "[| f: inj(X,Y);  g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"
    77 apply (insert decomposition [of f X Y g]) 
    78 apply (simp add: inj_is_fun)
    79 apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
    80 (* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))"
    81    is forced by the context!! *)
    82 done
    83 
    84 
    85 (** Equipollence is an equivalence relation **)
    86 
    87 lemma bij_imp_eqpoll: "f: bij(A,B) ==> A \<approx> B"
    88 apply (unfold eqpoll_def)
    89 apply (erule exI)
    90 done
    91 
    92 (*A eqpoll A*)
    93 lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, standard, simp]
    94 
    95 lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
    96 apply (unfold eqpoll_def)
    97 apply (blast intro: bij_converse_bij)
    98 done
    99 
   100 lemma eqpoll_trans: 
   101     "[| X \<approx> Y;  Y \<approx> Z |] ==> X \<approx> Z"
   102 apply (unfold eqpoll_def)
   103 apply (blast intro: comp_bij)
   104 done
   105 
   106 (** Le-pollence is a partial ordering **)
   107 
   108 lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y"
   109 apply (unfold lepoll_def)
   110 apply (rule exI)
   111 apply (erule id_subset_inj)
   112 done
   113 
   114 lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, standard, simp]
   115 
   116 lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll, standard]
   117 
   118 lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
   119 by (unfold eqpoll_def bij_def lepoll_def, blast)
   120 
   121 lemma lepoll_trans: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
   122 apply (unfold lepoll_def)
   123 apply (blast intro: comp_inj)
   124 done
   125 
   126 (*Asymmetry law*)
   127 lemma eqpollI: "[| X \<lesssim> Y;  Y \<lesssim> X |] ==> X \<approx> Y"
   128 apply (unfold lepoll_def eqpoll_def)
   129 apply (elim exE)
   130 apply (rule schroeder_bernstein, assumption+)
   131 done
   132 
   133 lemma eqpollE:
   134     "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
   135 by (blast intro: eqpoll_imp_lepoll eqpoll_sym) 
   136 
   137 lemma eqpoll_iff: "X \<approx> Y <-> X \<lesssim> Y & Y \<lesssim> X"
   138 by (blast intro: eqpollI elim!: eqpollE)
   139 
   140 lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
   141 apply (unfold lepoll_def inj_def)
   142 apply (blast dest: apply_type)
   143 done
   144 
   145 (*0 \<lesssim> Y*)
   146 lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard]
   147 
   148 lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
   149 by (blast intro: lepoll_0_is_0 lepoll_refl)
   150 
   151 lemma Un_lepoll_Un: 
   152     "[| A \<lesssim> B; C \<lesssim> D; B Int D = 0 |] ==> A Un C \<lesssim> B Un D"
   153 apply (unfold lepoll_def)
   154 apply (blast intro: inj_disjoint_Un)
   155 done
   156 
   157 (*A eqpoll 0 ==> A=0*)
   158 lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0, standard]
   159 
   160 lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
   161 by (blast intro: eqpoll_0_is_0 eqpoll_refl)
   162 
   163 lemma eqpoll_disjoint_Un: 
   164     "[| A \<approx> B;  C \<approx> D;  A Int C = 0;  B Int D = 0 |]   
   165      ==> A Un C \<approx> B Un D"
   166 apply (unfold eqpoll_def)
   167 apply (blast intro: bij_disjoint_Un)
   168 done
   169 
   170 
   171 subsection{*lesspoll: contributions by Krzysztof Grabczewski *}
   172 
   173 lemma lesspoll_not_refl: "~ (i \<prec> i)"
   174 by (simp add: lesspoll_def) 
   175 
   176 lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P"
   177 by (simp add: lesspoll_def) 
   178 
   179 lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
   180 by (unfold lesspoll_def, blast)
   181 
   182 lemma lepoll_well_ord: "[| A \<lesssim> B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"
   183 apply (unfold lepoll_def)
   184 apply (blast intro: well_ord_rvimage)
   185 done
   186 
   187 lemma lepoll_iff_leqpoll: "A \<lesssim> B <-> A \<prec> B | A \<approx> B"
   188 apply (unfold lesspoll_def)
   189 apply (blast intro!: eqpollI elim!: eqpollE)
   190 done
   191 
   192 lemma inj_not_surj_succ: 
   193   "[| f : inj(A, succ(m)); f ~: surj(A, succ(m)) |] ==> EX f. f:inj(A,m)"
   194 apply (unfold inj_def surj_def) 
   195 apply (safe del: succE) 
   196 apply (erule swap, rule exI) 
   197 apply (rule_tac a = "lam z:A. if f`z=m then y else f`z" in CollectI)
   198 txt{*the typing condition*}
   199  apply (best intro!: if_type [THEN lam_type] elim: apply_funtype [THEN succE])
   200 txt{*Proving it's injective*}
   201 apply simp
   202 apply blast 
   203 done
   204 
   205 (** Variations on transitivity **)
   206 
   207 lemma lesspoll_trans: 
   208       "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
   209 apply (unfold lesspoll_def)
   210 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
   211 done
   212 
   213 lemma lesspoll_trans1: 
   214       "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
   215 apply (unfold lesspoll_def)
   216 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
   217 done
   218 
   219 lemma lesspoll_trans2: 
   220       "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
   221 apply (unfold lesspoll_def)
   222 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
   223 done
   224 
   225 
   226 (** LEAST -- the least number operator [from HOL/Univ.ML] **)
   227 
   228 lemma Least_equality: 
   229     "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i"
   230 apply (unfold Least_def) 
   231 apply (rule the_equality, blast)
   232 apply (elim conjE)
   233 apply (erule Ord_linear_lt, assumption, blast+)
   234 done
   235 
   236 lemma LeastI: "[| P(i);  Ord(i) |] ==> P(LEAST x. P(x))"
   237 apply (erule rev_mp)
   238 apply (erule_tac i=i in trans_induct) 
   239 apply (rule impI)
   240 apply (rule classical)
   241 apply (blast intro: Least_equality [THEN ssubst]  elim!: ltE)
   242 done
   243 
   244 (*Proof is almost identical to the one above!*)
   245 lemma Least_le: "[| P(i);  Ord(i) |] ==> (LEAST x. P(x)) le i"
   246 apply (erule rev_mp)
   247 apply (erule_tac i=i in trans_induct) 
   248 apply (rule impI)
   249 apply (rule classical)
   250 apply (subst Least_equality, assumption+)
   251 apply (erule_tac [2] le_refl)
   252 apply (blast elim: ltE intro: leI ltI lt_trans1)
   253 done
   254 
   255 (*LEAST really is the smallest*)
   256 lemma less_LeastE: "[| P(i);  i < (LEAST x. P(x)) |] ==> Q"
   257 apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
   258 apply (simp add: lt_Ord) 
   259 done
   260 
   261 (*Easier to apply than LeastI: conclusion has only one occurrence of P*)
   262 lemma LeastI2:
   263     "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
   264 by (blast intro: LeastI ) 
   265 
   266 (*If there is no such P then LEAST is vacuously 0*)
   267 lemma Least_0: 
   268     "[| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0"
   269 apply (unfold Least_def)
   270 apply (rule the_0, blast)
   271 done
   272 
   273 lemma Ord_Least [intro,simp,TC]: "Ord(LEAST x. P(x))"
   274 apply (case_tac "\<exists>i. Ord(i) & P(i)")  
   275 apply safe
   276 apply (rule Least_le [THEN ltE])
   277 prefer 3 apply assumption+
   278 apply (erule Least_0 [THEN ssubst])
   279 apply (rule Ord_0)
   280 done
   281 
   282 
   283 (** Basic properties of cardinals **)
   284 
   285 (*Not needed for simplification, but helpful below*)
   286 lemma Least_cong:
   287      "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
   288 by simp
   289 
   290 (*Need AC to get X \<lesssim> Y ==> |X| le |Y|;  see well_ord_lepoll_imp_Card_le
   291   Converse also requires AC, but see well_ord_cardinal_eqE*)
   292 lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
   293 apply (unfold eqpoll_def cardinal_def)
   294 apply (rule Least_cong)
   295 apply (blast intro: comp_bij bij_converse_bij)
   296 done
   297 
   298 (*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
   299 lemma well_ord_cardinal_eqpoll: 
   300     "well_ord(A,r) ==> |A| \<approx> A"
   301 apply (unfold cardinal_def)
   302 apply (rule LeastI)
   303 apply (erule_tac [2] Ord_ordertype)
   304 apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_imp_eqpoll])
   305 done
   306 
   307 (* Ord(A) ==> |A| \<approx> A *)
   308 lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
   309 
   310 lemma well_ord_cardinal_eqE:
   311      "[| well_ord(X,r);  well_ord(Y,s);  |X| = |Y| |] ==> X \<approx> Y"
   312 apply (rule eqpoll_sym [THEN eqpoll_trans])
   313 apply (erule well_ord_cardinal_eqpoll)
   314 apply (simp (no_asm_simp) add: well_ord_cardinal_eqpoll)
   315 done
   316 
   317 lemma well_ord_cardinal_eqpoll_iff:
   318      "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X \<approx> Y"
   319 by (blast intro: cardinal_cong well_ord_cardinal_eqE)
   320 
   321 
   322 (** Observations from Kunen, page 28 **)
   323 
   324 lemma Ord_cardinal_le: "Ord(i) ==> |i| le i"
   325 apply (unfold cardinal_def)
   326 apply (erule eqpoll_refl [THEN Least_le])
   327 done
   328 
   329 lemma Card_cardinal_eq: "Card(K) ==> |K| = K"
   330 apply (unfold Card_def)
   331 apply (erule sym)
   332 done
   333 
   334 (* Could replace the  ~(j \<approx> i)  by  ~(i \<lesssim> j) *)
   335 lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
   336 apply (unfold Card_def cardinal_def) 
   337 apply (subst Least_equality)
   338 apply (blast intro: eqpoll_refl )+
   339 done
   340 
   341 lemma Card_is_Ord: "Card(i) ==> Ord(i)"
   342 apply (unfold Card_def cardinal_def)
   343 apply (erule ssubst)
   344 apply (rule Ord_Least)
   345 done
   346 
   347 lemma Card_cardinal_le: "Card(K) ==> K le |K|"
   348 apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
   349 done
   350 
   351 lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
   352 apply (unfold cardinal_def)
   353 apply (rule Ord_Least)
   354 done
   355 
   356 (*The cardinals are the initial ordinals*)
   357 lemma Card_iff_initial: "Card(K) <-> Ord(K) & (ALL j. j<K --> ~ j \<approx> K)"
   358 apply (safe intro!: CardI Card_is_Ord)
   359  prefer 2 apply blast
   360 apply (unfold Card_def cardinal_def)
   361 apply (rule less_LeastE)
   362 apply (erule_tac [2] subst, assumption+)
   363 done
   364 
   365 lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
   366 apply (unfold lesspoll_def)
   367 apply (drule Card_iff_initial [THEN iffD1])
   368 apply (blast intro!: leI [THEN le_imp_lepoll])
   369 done
   370 
   371 lemma Card_0: "Card(0)"
   372 apply (rule Ord_0 [THEN CardI])
   373 apply (blast elim!: ltE)
   374 done
   375 
   376 lemma Card_Un: "[| Card(K);  Card(L) |] ==> Card(K Un L)"
   377 apply (rule Ord_linear_le [of K L])
   378 apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_is_Ord le_imp_subset
   379                      subset_Un_iff2 [THEN iffD1])
   380 done
   381 
   382 (*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)
   383 
   384 lemma Card_cardinal: "Card(|A|)"
   385 apply (unfold cardinal_def)
   386 apply (case_tac "EX i. Ord (i) & i \<approx> A")
   387  txt{*degenerate case*}
   388  prefer 2 apply (erule Least_0 [THEN ssubst], rule Card_0)
   389 txt{*real case: A is isomorphic to some ordinal*}
   390 apply (rule Ord_Least [THEN CardI], safe)
   391 apply (rule less_LeastE)
   392 prefer 2 apply assumption
   393 apply (erule eqpoll_trans)
   394 apply (best intro: LeastI ) 
   395 done
   396 
   397 (*Kunen's Lemma 10.5*)
   398 lemma cardinal_eq_lemma: "[| |i| le j;  j le i |] ==> |j| = |i|"
   399 apply (rule eqpollI [THEN cardinal_cong])
   400 apply (erule le_imp_lepoll)
   401 apply (rule lepoll_trans)
   402 apply (erule_tac [2] le_imp_lepoll)
   403 apply (rule eqpoll_sym [THEN eqpoll_imp_lepoll])
   404 apply (rule Ord_cardinal_eqpoll)
   405 apply (elim ltE Ord_succD)
   406 done
   407 
   408 lemma cardinal_mono: "i le j ==> |i| le |j|"
   409 apply (rule_tac i = "|i|" and j = "|j|" in Ord_linear_le)
   410 apply (safe intro!: Ord_cardinal le_eqI)
   411 apply (rule cardinal_eq_lemma)
   412 prefer 2 apply assumption
   413 apply (erule le_trans)
   414 apply (erule ltE)
   415 apply (erule Ord_cardinal_le)
   416 done
   417 
   418 (*Since we have |succ(nat)| le |nat|, the converse of cardinal_mono fails!*)
   419 lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
   420 apply (rule Ord_linear2 [of i j], assumption+)
   421 apply (erule lt_trans2 [THEN lt_irrefl])
   422 apply (erule cardinal_mono)
   423 done
   424 
   425 lemma Card_lt_imp_lt: "[| |i| < K;  Ord(i);  Card(K) |] ==> i < K"
   426 apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
   427 done
   428 
   429 lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) <-> (i < K)"
   430 by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
   431 
   432 lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K le |i|) <-> (K le i)"
   433 by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
   434 
   435 (*Can use AC or finiteness to discharge first premise*)
   436 lemma well_ord_lepoll_imp_Card_le:
   437      "[| well_ord(B,r);  A \<lesssim> B |] ==> |A| le |B|"
   438 apply (rule_tac i = "|A|" and j = "|B|" in Ord_linear_le)
   439 apply (safe intro!: Ord_cardinal le_eqI)
   440 apply (rule eqpollI [THEN cardinal_cong], assumption)
   441 apply (rule lepoll_trans)
   442 apply (rule well_ord_cardinal_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll], assumption)
   443 apply (erule le_imp_lepoll [THEN lepoll_trans])
   444 apply (rule eqpoll_imp_lepoll)
   445 apply (unfold lepoll_def)
   446 apply (erule exE)
   447 apply (rule well_ord_cardinal_eqpoll)
   448 apply (erule well_ord_rvimage, assumption)
   449 done
   450 
   451 lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| le i"
   452 apply (rule le_trans)
   453 apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
   454 apply (erule Ord_cardinal_le)
   455 done
   456 
   457 lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
   458 by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
   459 
   460 lemma lesspoll_imp_eqpoll: "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
   461 apply (unfold lesspoll_def)
   462 apply (blast intro: lepoll_Ord_imp_eqpoll)
   463 done
   464 
   465 lemma cardinal_subset_Ord: "[|A<=i; Ord(i)|] ==> |A| <= i"
   466 apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le])
   467 apply (auto simp add: lt_def)
   468 apply (blast intro: Ord_trans)
   469 done
   470 
   471 subsection{*The finite cardinals *}
   472 
   473 lemma cons_lepoll_consD: 
   474  "[| cons(u,A) \<lesssim> cons(v,B);  u~:A;  v~:B |] ==> A \<lesssim> B"
   475 apply (unfold lepoll_def inj_def, safe)
   476 apply (rule_tac x = "lam x:A. if f`x=v then f`u else f`x" in exI)
   477 apply (rule CollectI)
   478 (*Proving it's in the function space A->B*)
   479 apply (rule if_type [THEN lam_type])
   480 apply (blast dest: apply_funtype)
   481 apply (blast elim!: mem_irrefl dest: apply_funtype)
   482 (*Proving it's injective*)
   483 apply (simp (no_asm_simp))
   484 apply blast
   485 done
   486 
   487 lemma cons_eqpoll_consD: "[| cons(u,A) \<approx> cons(v,B);  u~:A;  v~:B |] ==> A \<approx> B"
   488 apply (simp add: eqpoll_iff)
   489 apply (blast intro: cons_lepoll_consD)
   490 done
   491 
   492 (*Lemma suggested by Mike Fourman*)
   493 lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n"
   494 apply (unfold succ_def)
   495 apply (erule cons_lepoll_consD)
   496 apply (rule mem_not_refl)+
   497 done
   498 
   499 lemma nat_lepoll_imp_le [rule_format]:
   500      "m:nat ==> ALL n: nat. m \<lesssim> n --> m le n"
   501 apply (induct_tac m)
   502 apply (blast intro!: nat_0_le)
   503 apply (rule ballI)
   504 apply (erule_tac n = n in natE)
   505 apply (simp (no_asm_simp) add: lepoll_def inj_def)
   506 apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
   507 done
   508 
   509 lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"
   510 apply (rule iffI)
   511 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
   512 apply (simp add: eqpoll_refl)
   513 done
   514 
   515 (*The object of all this work: every natural number is a (finite) cardinal*)
   516 lemma nat_into_Card: 
   517     "n: nat ==> Card(n)"
   518 apply (unfold Card_def cardinal_def)
   519 apply (subst Least_equality)
   520 apply (rule eqpoll_refl)
   521 apply (erule nat_into_Ord) 
   522 apply (simp (no_asm_simp) add: lt_nat_in_nat [THEN nat_eqpoll_iff])
   523 apply (blast elim!: lt_irrefl)+
   524 done
   525 
   526 lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
   527 lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
   528 
   529 
   530 (*Part of Kunen's Lemma 10.6*)
   531 lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n:nat |] ==> P"
   532 by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
   533 
   534 lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
   535 apply (unfold lesspoll_def)
   536 apply (fast elim!: Ord_nat [THEN [2] ltI [THEN leI, THEN le_imp_lepoll]]
   537                    eqpoll_sym [THEN eqpoll_imp_lepoll] 
   538     intro: Ord_nat [THEN [2] nat_succI [THEN ltI], THEN leI, 
   539                  THEN le_imp_lepoll, THEN lepoll_trans, THEN succ_lepoll_natE])
   540 done
   541 
   542 lemma nat_lepoll_imp_ex_eqpoll_n: 
   543      "[| n \<in> nat;  nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
   544 apply (unfold lepoll_def eqpoll_def)
   545 apply (fast del: subsetI subsetCE
   546             intro!: subset_SIs
   547             dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
   548             elim!: restrict_bij 
   549                    inj_is_fun [THEN fun_is_rel, THEN image_subset])
   550 done
   551 
   552 
   553 (** lepoll, \<prec> and natural numbers **)
   554 
   555 lemma lepoll_imp_lesspoll_succ: 
   556      "[| A \<lesssim> m; m:nat |] ==> A \<prec> succ(m)"
   557 apply (unfold lesspoll_def)
   558 apply (rule conjI)
   559 apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
   560 apply (rule notI)
   561 apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll])
   562 apply (drule lepoll_trans, assumption)
   563 apply (erule succ_lepoll_natE, assumption)
   564 done
   565 
   566 lemma lesspoll_succ_imp_lepoll: 
   567      "[| A \<prec> succ(m); m:nat |] ==> A \<lesssim> m"
   568 apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def, clarify)
   569 apply (blast intro!: inj_not_surj_succ)
   570 done
   571 
   572 lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) <-> A \<lesssim> m"
   573 by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
   574 
   575 lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
   576 apply (rule disjCI)
   577 apply (rule lesspoll_succ_imp_lepoll)
   578 prefer 2 apply assumption
   579 apply (simp (no_asm_simp) add: lesspoll_def)
   580 done
   581 
   582 lemma lesspoll_cardinal_lt: "[| A \<prec> i; Ord(i) |] ==> |A| < i"
   583 apply (unfold lesspoll_def, clarify)
   584 apply (frule lepoll_cardinal_le, assumption)
   585 apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
   586              dest: lepoll_well_ord  elim!: leE)
   587 done
   588 
   589 
   590 subsection{*The first infinite cardinal: Omega, or nat *}
   591 
   592 (*This implies Kunen's Lemma 10.6*)
   593 lemma lt_not_lepoll: "[| n<i;  n:nat |] ==> ~ i \<lesssim> n"
   594 apply (rule notI)
   595 apply (rule succ_lepoll_natE [of n])
   596 apply (rule lepoll_trans [of _ i])
   597 apply (erule ltE)
   598 apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
   599 done
   600 
   601 lemma Ord_nat_eqpoll_iff: "[| Ord(i);  n:nat |] ==> i \<approx> n <-> i=n"
   602 apply (rule iffI)
   603  prefer 2 apply (simp add: eqpoll_refl)
   604 apply (rule Ord_linear_lt [of i n])
   605 apply (simp_all add: nat_into_Ord)
   606 apply (erule lt_nat_in_nat [THEN nat_eqpoll_iff, THEN iffD1], assumption+)
   607 apply (rule lt_not_lepoll [THEN notE], assumption+)
   608 apply (erule eqpoll_imp_lepoll)
   609 done
   610 
   611 lemma Card_nat: "Card(nat)"
   612 apply (unfold Card_def cardinal_def)
   613 apply (subst Least_equality)
   614 apply (rule eqpoll_refl) 
   615 apply (rule Ord_nat) 
   616 apply (erule ltE)
   617 apply (simp_all add: eqpoll_iff lt_not_lepoll ltI)
   618 done
   619 
   620 (*Allows showing that |i| is a limit cardinal*)
   621 lemma nat_le_cardinal: "nat le i ==> nat le |i|"
   622 apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
   623 apply (erule cardinal_mono)
   624 done
   625 
   626 
   627 subsection{*Towards Cardinal Arithmetic *}
   628 (** Congruence laws for successor, cardinal addition and multiplication **)
   629 
   630 (*Congruence law for  cons  under equipollence*)
   631 lemma cons_lepoll_cong: 
   632     "[| A \<lesssim> B;  b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B)"
   633 apply (unfold lepoll_def, safe)
   634 apply (rule_tac x = "lam y: cons (a,A) . if y=a then b else f`y" in exI)
   635 apply (rule_tac d = "%z. if z:B then converse (f) `z else a" in lam_injective)
   636 apply (safe elim!: consE') 
   637    apply simp_all
   638 apply (blast intro: inj_is_fun [THEN apply_type])+ 
   639 done
   640 
   641 lemma cons_eqpoll_cong:
   642      "[| A \<approx> B;  a ~: A;  b ~: B |] ==> cons(a,A) \<approx> cons(b,B)"
   643 by (simp add: eqpoll_iff cons_lepoll_cong)
   644 
   645 lemma cons_lepoll_cons_iff:
   646      "[| a ~: A;  b ~: B |] ==> cons(a,A) \<lesssim> cons(b,B)  <->  A \<lesssim> B"
   647 by (blast intro: cons_lepoll_cong cons_lepoll_consD)
   648 
   649 lemma cons_eqpoll_cons_iff:
   650      "[| a ~: A;  b ~: B |] ==> cons(a,A) \<approx> cons(b,B)  <->  A \<approx> B"
   651 by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
   652 
   653 lemma singleton_eqpoll_1: "{a} \<approx> 1"
   654 apply (unfold succ_def)
   655 apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
   656 done
   657 
   658 lemma cardinal_singleton: "|{a}| = 1"
   659 apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
   660 apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
   661 done
   662 
   663 lemma not_0_is_lepoll_1: "A ~= 0 ==> 1 \<lesssim> A"
   664 apply (erule not_emptyE)
   665 apply (rule_tac a = "cons (x, A-{x}) " in subst)
   666 apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A-{x})" in subst)
   667 prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
   668 done
   669 
   670 (*Congruence law for  succ  under equipollence*)
   671 lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)"
   672 apply (unfold succ_def)
   673 apply (simp add: cons_eqpoll_cong mem_not_refl)
   674 done
   675 
   676 (*Congruence law for + under equipollence*)
   677 lemma sum_eqpoll_cong: "[| A \<approx> C;  B \<approx> D |] ==> A+B \<approx> C+D"
   678 apply (unfold eqpoll_def)
   679 apply (blast intro!: sum_bij)
   680 done
   681 
   682 (*Congruence law for * under equipollence*)
   683 lemma prod_eqpoll_cong: 
   684     "[| A \<approx> C;  B \<approx> D |] ==> A*B \<approx> C*D"
   685 apply (unfold eqpoll_def)
   686 apply (blast intro!: prod_bij)
   687 done
   688 
   689 lemma inj_disjoint_eqpoll: 
   690     "[| f: inj(A,B);  A Int B = 0 |] ==> A Un (B - range(f)) \<approx> B"
   691 apply (unfold eqpoll_def)
   692 apply (rule exI)
   693 apply (rule_tac c = "%x. if x:A then f`x else x" 
   694             and d = "%y. if y: range (f) then converse (f) `y else y" 
   695        in lam_bijective)
   696 apply (blast intro!: if_type inj_is_fun [THEN apply_type])
   697 apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
   698 apply (safe elim!: UnE') 
   699    apply (simp_all add: inj_is_fun [THEN apply_rangeI])
   700 apply (blast intro: inj_converse_fun [THEN apply_type])+ 
   701 done
   702 
   703 
   704 subsection{*Lemmas by Krzysztof Grabczewski*}
   705 
   706 (*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*)
   707 
   708 (*If A has at most n+1 elements and a:A then A-{a} has at most n.*)
   709 lemma Diff_sing_lepoll: 
   710       "[| a:A;  A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
   711 apply (unfold succ_def)
   712 apply (rule cons_lepoll_consD)
   713 apply (rule_tac [3] mem_not_refl)
   714 apply (erule cons_Diff [THEN ssubst], safe)
   715 done
   716 
   717 (*If A has at least n+1 elements then A-{a} has at least n.*)
   718 lemma lepoll_Diff_sing: 
   719       "[| succ(n) \<lesssim> A |] ==> n \<lesssim> A - {a}"
   720 apply (unfold succ_def)
   721 apply (rule cons_lepoll_consD)
   722 apply (rule_tac [2] mem_not_refl)
   723 prefer 2 apply blast
   724 apply (blast intro: subset_imp_lepoll [THEN [2] lepoll_trans])
   725 done
   726 
   727 lemma Diff_sing_eqpoll: "[| a:A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
   728 by (blast intro!: eqpollI 
   729           elim!: eqpollE 
   730           intro: Diff_sing_lepoll lepoll_Diff_sing)
   731 
   732 lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a:A |] ==> A = {a}"
   733 apply (frule Diff_sing_lepoll, assumption)
   734 apply (drule lepoll_0_is_0)
   735 apply (blast elim: equalityE)
   736 done
   737 
   738 lemma Un_lepoll_sum: "A Un B \<lesssim> A+B"
   739 apply (unfold lepoll_def)
   740 apply (rule_tac x = "lam x: A Un B. if x:A then Inl (x) else Inr (x) " in exI)
   741 apply (rule_tac d = "%z. snd (z) " in lam_injective)
   742 apply force 
   743 apply (simp add: Inl_def Inr_def)
   744 done
   745 
   746 lemma well_ord_Un:
   747      "[| well_ord(X,R); well_ord(Y,S) |] ==> EX T. well_ord(X Un Y, T)"
   748 by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]], 
   749     assumption)
   750 
   751 (*Krzysztof Grabczewski*)
   752 lemma disj_Un_eqpoll_sum: "A Int B = 0 ==> A Un B \<approx> A + B"
   753 apply (unfold eqpoll_def)
   754 apply (rule_tac x = "lam a:A Un B. if a:A then Inl (a) else Inr (a) " in exI)
   755 apply (rule_tac d = "%z. case (%x. x, %x. x, z) " in lam_bijective)
   756 apply auto
   757 done
   758 
   759 
   760 subsection {*Finite and infinite sets*}
   761 
   762 lemma Finite_0 [simp]: "Finite(0)"
   763 apply (unfold Finite_def)
   764 apply (blast intro!: eqpoll_refl nat_0I)
   765 done
   766 
   767 lemma lepoll_nat_imp_Finite: "[| A \<lesssim> n;  n:nat |] ==> Finite(A)"
   768 apply (unfold Finite_def)
   769 apply (erule rev_mp)
   770 apply (erule nat_induct)
   771 apply (blast dest!: lepoll_0_is_0 intro!: eqpoll_refl nat_0I)
   772 apply (blast dest!: lepoll_succ_disj)
   773 done
   774 
   775 lemma lesspoll_nat_is_Finite: 
   776      "A \<prec> nat ==> Finite(A)"
   777 apply (unfold Finite_def)
   778 apply (blast dest: ltD lesspoll_cardinal_lt 
   779                    lesspoll_imp_eqpoll [THEN eqpoll_sym])
   780 done
   781 
   782 lemma lepoll_Finite: 
   783      "[| Y \<lesssim> X;  Finite(X) |] ==> Finite(Y)"
   784 apply (unfold Finite_def)
   785 apply (blast elim!: eqpollE
   786              intro: lepoll_trans [THEN lepoll_nat_imp_Finite
   787                                        [unfolded Finite_def]])
   788 done
   789 
   790 lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard]
   791 
   792 lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard]
   793 
   794 lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
   795 apply (unfold Finite_def)
   796 apply (case_tac "y:x")
   797 apply (simp add: cons_absorb)
   798 apply (erule bexE)
   799 apply (rule bexI)
   800 apply (erule_tac [2] nat_succI)
   801 apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
   802 done
   803 
   804 lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
   805 apply (unfold succ_def)
   806 apply (erule Finite_cons)
   807 done
   808 
   809 lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
   810 by (blast intro: Finite_cons subset_Finite)
   811 
   812 lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
   813 by (simp add: succ_def)
   814 
   815 lemma nat_le_infinite_Ord: 
   816       "[| Ord(i);  ~ Finite(i) |] ==> nat le i"
   817 apply (unfold Finite_def)
   818 apply (erule Ord_nat [THEN [2] Ord_linear2])
   819 prefer 2 apply assumption
   820 apply (blast intro!: eqpoll_refl elim!: ltE)
   821 done
   822 
   823 lemma Finite_imp_well_ord: 
   824     "Finite(A) ==> EX r. well_ord(A,r)"
   825 apply (unfold Finite_def eqpoll_def)
   826 apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
   827 done
   828 
   829 lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
   830 by (fast dest!: lepoll_0_is_0)
   831 
   832 lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
   833 by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
   834 
   835 lemma Finite_Fin_lemma [rule_format]:
   836      "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) --> A \<in> Fin(X)"
   837 apply (induct_tac n)
   838 apply (rule allI)
   839 apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
   840 apply (rule allI)
   841 apply (rule impI)
   842 apply (erule conjE)
   843 apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
   844 apply (frule Diff_sing_eqpoll, assumption)
   845 apply (erule allE)
   846 apply (erule impE, fast)
   847 apply (drule subsetD, assumption)
   848 apply (drule Fin.consI, assumption)
   849 apply (simp add: cons_Diff)
   850 done
   851 
   852 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
   853 by (unfold Finite_def, blast intro: Finite_Fin_lemma) 
   854 
   855 lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
   856 apply (unfold Finite_def) 
   857 apply (blast intro: eqpoll_trans eqpoll_sym) 
   858 done
   859 
   860 lemma Fin_lemma [rule_format]: "n: nat ==> ALL A. A \<approx> n --> A : Fin(A)"
   861 apply (induct_tac n)
   862 apply (simp add: eqpoll_0_iff, clarify)
   863 apply (subgoal_tac "EX u. u:A")
   864 apply (erule exE)
   865 apply (rule Diff_sing_eqpoll [THEN revcut_rl])
   866 prefer 2 apply assumption
   867 apply assumption
   868 apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
   869 apply (rule Fin.consI, blast)
   870 apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
   871 (*Now for the lemma assumed above*)
   872 apply (unfold eqpoll_def)
   873 apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
   874 done
   875 
   876 lemma Finite_into_Fin: "Finite(A) ==> A : Fin(A)"
   877 apply (unfold Finite_def)
   878 apply (blast intro: Fin_lemma)
   879 done
   880 
   881 lemma Fin_into_Finite: "A : Fin(U) ==> Finite(A)"
   882 by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
   883 
   884 lemma Finite_Fin_iff: "Finite(A) <-> A : Fin(A)"
   885 by (blast intro: Finite_into_Fin Fin_into_Finite)
   886 
   887 lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A Un B)"
   888 by (blast intro!: Fin_into_Finite Fin_UnI 
   889           dest!: Finite_into_Fin
   890           intro: Un_upper1 [THEN Fin_mono, THEN subsetD] 
   891                  Un_upper2 [THEN Fin_mono, THEN subsetD])
   892 
   893 lemma Finite_Union: "[| ALL y:X. Finite(y);  Finite(X) |] ==> Finite(Union(X))"
   894 apply (simp add: Finite_Fin_iff)
   895 apply (rule Fin_UnionI)
   896 apply (erule Fin_induct, simp)
   897 apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
   898 done
   899 
   900 (* Induction principle for Finite(A), by Sidi Ehmety *)
   901 lemma Finite_induct [case_names 0 cons, induct set: Finite]:
   902 "[| Finite(A); P(0);
   903     !! x B.   [| Finite(B); x ~: B; P(B) |] ==> P(cons(x, B)) |]
   904  ==> P(A)"
   905 apply (erule Finite_into_Fin [THEN Fin_induct]) 
   906 apply (blast intro: Fin_into_Finite)+
   907 done
   908 
   909 (*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
   910 lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
   911 apply (unfold Finite_def)
   912 apply (case_tac "a:A")
   913 apply (subgoal_tac [2] "A-{a}=A", auto)
   914 apply (rule_tac x = "succ (n) " in bexI)
   915 apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
   916 apply (drule_tac a = a and b = n in cons_eqpoll_cong)
   917 apply (auto dest: mem_irrefl)
   918 done
   919 
   920 (*Sidi Ehmety.  And the contrapositive of this says
   921    [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
   922 lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) --> Finite(A)"
   923 apply (erule Finite_induct, auto)
   924 apply (case_tac "x:A")
   925  apply (subgoal_tac [2] "A-cons (x, B) = A - B")
   926 apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
   927 apply (drule Diff_sing_Finite, auto)
   928 done
   929 
   930 lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
   931 by (erule Finite_induct, simp_all)
   932 
   933 lemma Finite_RepFun_iff_lemma [rule_format]:
   934      "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] 
   935       ==> \<forall>A. x = RepFun(A,f) --> Finite(A)" 
   936 apply (erule Finite_induct)
   937  apply clarify 
   938  apply (case_tac "A=0", simp)
   939  apply (blast del: allE, clarify) 
   940 apply (subgoal_tac "\<exists>z\<in>A. x = f(z)") 
   941  prefer 2 apply (blast del: allE elim: equalityE, clarify) 
   942 apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
   943  apply (blast intro: Diff_sing_Finite) 
   944 apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)") 
   945 apply (rule equalityI) 
   946  apply (blast intro: elim: equalityE) 
   947 apply (blast intro: elim: equalityCE) 
   948 done
   949 
   950 text{*I don't know why, but if the premise is expressed using meta-connectives
   951 then  the simplifier cannot prove it automatically in conditional rewriting.*}
   952 lemma Finite_RepFun_iff:
   953      "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
   954 by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f]) 
   955 
   956 lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
   957 apply (erule Finite_induct) 
   958 apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) 
   959 done
   960 
   961 lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
   962 apply (subgoal_tac "Finite({{x} . x \<in> A})")
   963  apply (simp add: Finite_RepFun_iff ) 
   964 apply (blast intro: subset_Finite) 
   965 done
   966 
   967 lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
   968 by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
   969 
   970 
   971 
   972 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
   973   set is well-ordered.  Proofs simplified by lcp. *)
   974 
   975 lemma nat_wf_on_converse_Memrel: "n:nat ==> wf[n](converse(Memrel(n)))"
   976 apply (erule nat_induct)
   977 apply (blast intro: wf_onI)
   978 apply (rule wf_onI)
   979 apply (simp add: wf_on_def wf_def)
   980 apply (case_tac "x:Z")
   981  txt{*x:Z case*}
   982  apply (drule_tac x = x in bspec, assumption)
   983  apply (blast elim: mem_irrefl mem_asym)
   984 txt{*other case*} 
   985 apply (drule_tac x = Z in spec, blast) 
   986 done
   987 
   988 lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
   989 apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
   990 apply (unfold well_ord_def)
   991 apply (blast intro!: tot_ord_converse nat_wf_on_converse_Memrel)
   992 done
   993 
   994 lemma well_ord_converse:
   995      "[|well_ord(A,r);      
   996         well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |]
   997       ==> well_ord(A,converse(r))"
   998 apply (rule well_ord_Int_iff [THEN iffD1])
   999 apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
  1000 apply (simp add: rvimage_converse converse_Int converse_prod
  1001                  ordertype_ord_iso [THEN ord_iso_rvimage_eq])
  1002 done
  1003 
  1004 lemma ordertype_eq_n:
  1005      "[| well_ord(A,r);  A \<approx> n;  n:nat |] ==> ordertype(A,r)=n"
  1006 apply (rule Ord_ordertype [THEN Ord_nat_eqpoll_iff, THEN iffD1], assumption+)
  1007 apply (rule eqpoll_trans)
  1008  prefer 2 apply assumption
  1009 apply (unfold eqpoll_def)
  1010 apply (blast intro!: ordermap_bij [THEN bij_converse_bij])
  1011 done
  1012 
  1013 lemma Finite_well_ord_converse: 
  1014     "[| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))"
  1015 apply (unfold Finite_def)
  1016 apply (rule well_ord_converse, assumption)
  1017 apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
  1018 done
  1019 
  1020 lemma nat_into_Finite: "n:nat ==> Finite(n)"
  1021 apply (unfold Finite_def)
  1022 apply (fast intro!: eqpoll_refl)
  1023 done
  1024 
  1025 lemma nat_not_Finite: "~Finite(nat)"
  1026 apply (unfold Finite_def, clarify) 
  1027 apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp) 
  1028 apply (insert Card_nat) 
  1029 apply (simp add: Card_def)
  1030 apply (drule le_imp_subset)
  1031 apply (blast elim: mem_irrefl)
  1032 done
  1033 
  1034 ML
  1035 {*
  1036 val Least_def = thm "Least_def";
  1037 val eqpoll_def = thm "eqpoll_def";
  1038 val lepoll_def = thm "lepoll_def";
  1039 val lesspoll_def = thm "lesspoll_def";
  1040 val cardinal_def = thm "cardinal_def";
  1041 val Finite_def = thm "Finite_def";
  1042 val Card_def = thm "Card_def";
  1043 val eq_imp_not_mem = thm "eq_imp_not_mem";
  1044 val decomp_bnd_mono = thm "decomp_bnd_mono";
  1045 val Banach_last_equation = thm "Banach_last_equation";
  1046 val decomposition = thm "decomposition";
  1047 val schroeder_bernstein = thm "schroeder_bernstein";
  1048 val bij_imp_eqpoll = thm "bij_imp_eqpoll";
  1049 val eqpoll_refl = thm "eqpoll_refl";
  1050 val eqpoll_sym = thm "eqpoll_sym";
  1051 val eqpoll_trans = thm "eqpoll_trans";
  1052 val subset_imp_lepoll = thm "subset_imp_lepoll";
  1053 val lepoll_refl = thm "lepoll_refl";
  1054 val le_imp_lepoll = thm "le_imp_lepoll";
  1055 val eqpoll_imp_lepoll = thm "eqpoll_imp_lepoll";
  1056 val lepoll_trans = thm "lepoll_trans";
  1057 val eqpollI = thm "eqpollI";
  1058 val eqpollE = thm "eqpollE";
  1059 val eqpoll_iff = thm "eqpoll_iff";
  1060 val lepoll_0_is_0 = thm "lepoll_0_is_0";
  1061 val empty_lepollI = thm "empty_lepollI";
  1062 val lepoll_0_iff = thm "lepoll_0_iff";
  1063 val Un_lepoll_Un = thm "Un_lepoll_Un";
  1064 val eqpoll_0_is_0 = thm "eqpoll_0_is_0";
  1065 val eqpoll_0_iff = thm "eqpoll_0_iff";
  1066 val eqpoll_disjoint_Un = thm "eqpoll_disjoint_Un";
  1067 val lesspoll_not_refl = thm "lesspoll_not_refl";
  1068 val lesspoll_irrefl = thm "lesspoll_irrefl";
  1069 val lesspoll_imp_lepoll = thm "lesspoll_imp_lepoll";
  1070 val lepoll_well_ord = thm "lepoll_well_ord";
  1071 val lepoll_iff_leqpoll = thm "lepoll_iff_leqpoll";
  1072 val inj_not_surj_succ = thm "inj_not_surj_succ";
  1073 val lesspoll_trans = thm "lesspoll_trans";
  1074 val lesspoll_trans1 = thm "lesspoll_trans1";
  1075 val lesspoll_trans2 = thm "lesspoll_trans2";
  1076 val Least_equality = thm "Least_equality";
  1077 val LeastI = thm "LeastI";
  1078 val Least_le = thm "Least_le";
  1079 val less_LeastE = thm "less_LeastE";
  1080 val LeastI2 = thm "LeastI2";
  1081 val Least_0 = thm "Least_0";
  1082 val Ord_Least = thm "Ord_Least";
  1083 val Least_cong = thm "Least_cong";
  1084 val cardinal_cong = thm "cardinal_cong";
  1085 val well_ord_cardinal_eqpoll = thm "well_ord_cardinal_eqpoll";
  1086 val Ord_cardinal_eqpoll = thm "Ord_cardinal_eqpoll";
  1087 val well_ord_cardinal_eqE = thm "well_ord_cardinal_eqE";
  1088 val well_ord_cardinal_eqpoll_iff = thm "well_ord_cardinal_eqpoll_iff";
  1089 val Ord_cardinal_le = thm "Ord_cardinal_le";
  1090 val Card_cardinal_eq = thm "Card_cardinal_eq";
  1091 val CardI = thm "CardI";
  1092 val Card_is_Ord = thm "Card_is_Ord";
  1093 val Card_cardinal_le = thm "Card_cardinal_le";
  1094 val Ord_cardinal = thm "Ord_cardinal";
  1095 val Card_iff_initial = thm "Card_iff_initial";
  1096 val lt_Card_imp_lesspoll = thm "lt_Card_imp_lesspoll";
  1097 val Card_0 = thm "Card_0";
  1098 val Card_Un = thm "Card_Un";
  1099 val Card_cardinal = thm "Card_cardinal";
  1100 val cardinal_mono = thm "cardinal_mono";
  1101 val cardinal_lt_imp_lt = thm "cardinal_lt_imp_lt";
  1102 val Card_lt_imp_lt = thm "Card_lt_imp_lt";
  1103 val Card_lt_iff = thm "Card_lt_iff";
  1104 val Card_le_iff = thm "Card_le_iff";
  1105 val well_ord_lepoll_imp_Card_le = thm "well_ord_lepoll_imp_Card_le";
  1106 val lepoll_cardinal_le = thm "lepoll_cardinal_le";
  1107 val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll";
  1108 val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll";
  1109 val cardinal_subset_Ord = thm "cardinal_subset_Ord";
  1110 val cons_lepoll_consD = thm "cons_lepoll_consD";
  1111 val cons_eqpoll_consD = thm "cons_eqpoll_consD";
  1112 val succ_lepoll_succD = thm "succ_lepoll_succD";
  1113 val nat_lepoll_imp_le = thm "nat_lepoll_imp_le";
  1114 val nat_eqpoll_iff = thm "nat_eqpoll_iff";
  1115 val nat_into_Card = thm "nat_into_Card";
  1116 val cardinal_0 = thm "cardinal_0";
  1117 val cardinal_1 = thm "cardinal_1";
  1118 val succ_lepoll_natE = thm "succ_lepoll_natE";
  1119 val n_lesspoll_nat = thm "n_lesspoll_nat";
  1120 val nat_lepoll_imp_ex_eqpoll_n = thm "nat_lepoll_imp_ex_eqpoll_n";
  1121 val lepoll_imp_lesspoll_succ = thm "lepoll_imp_lesspoll_succ";
  1122 val lesspoll_succ_imp_lepoll = thm "lesspoll_succ_imp_lepoll";
  1123 val lesspoll_succ_iff = thm "lesspoll_succ_iff";
  1124 val lepoll_succ_disj = thm "lepoll_succ_disj";
  1125 val lesspoll_cardinal_lt = thm "lesspoll_cardinal_lt";
  1126 val lt_not_lepoll = thm "lt_not_lepoll";
  1127 val Ord_nat_eqpoll_iff = thm "Ord_nat_eqpoll_iff";
  1128 val Card_nat = thm "Card_nat";
  1129 val nat_le_cardinal = thm "nat_le_cardinal";
  1130 val cons_lepoll_cong = thm "cons_lepoll_cong";
  1131 val cons_eqpoll_cong = thm "cons_eqpoll_cong";
  1132 val cons_lepoll_cons_iff = thm "cons_lepoll_cons_iff";
  1133 val cons_eqpoll_cons_iff = thm "cons_eqpoll_cons_iff";
  1134 val singleton_eqpoll_1 = thm "singleton_eqpoll_1";
  1135 val cardinal_singleton = thm "cardinal_singleton";
  1136 val not_0_is_lepoll_1 = thm "not_0_is_lepoll_1";
  1137 val succ_eqpoll_cong = thm "succ_eqpoll_cong";
  1138 val sum_eqpoll_cong = thm "sum_eqpoll_cong";
  1139 val prod_eqpoll_cong = thm "prod_eqpoll_cong";
  1140 val inj_disjoint_eqpoll = thm "inj_disjoint_eqpoll";
  1141 val Diff_sing_lepoll = thm "Diff_sing_lepoll";
  1142 val lepoll_Diff_sing = thm "lepoll_Diff_sing";
  1143 val Diff_sing_eqpoll = thm "Diff_sing_eqpoll";
  1144 val lepoll_1_is_sing = thm "lepoll_1_is_sing";
  1145 val Un_lepoll_sum = thm "Un_lepoll_sum";
  1146 val well_ord_Un = thm "well_ord_Un";
  1147 val disj_Un_eqpoll_sum = thm "disj_Un_eqpoll_sum";
  1148 val Finite_0 = thm "Finite_0";
  1149 val lepoll_nat_imp_Finite = thm "lepoll_nat_imp_Finite";
  1150 val lesspoll_nat_is_Finite = thm "lesspoll_nat_is_Finite";
  1151 val lepoll_Finite = thm "lepoll_Finite";
  1152 val subset_Finite = thm "subset_Finite";
  1153 val Finite_Diff = thm "Finite_Diff";
  1154 val Finite_cons = thm "Finite_cons";
  1155 val Finite_succ = thm "Finite_succ";
  1156 val nat_le_infinite_Ord = thm "nat_le_infinite_Ord";
  1157 val Finite_imp_well_ord = thm "Finite_imp_well_ord";
  1158 val nat_wf_on_converse_Memrel = thm "nat_wf_on_converse_Memrel";
  1159 val nat_well_ord_converse_Memrel = thm "nat_well_ord_converse_Memrel";
  1160 val well_ord_converse = thm "well_ord_converse";
  1161 val ordertype_eq_n = thm "ordertype_eq_n";
  1162 val Finite_well_ord_converse = thm "Finite_well_ord_converse";
  1163 val nat_into_Finite = thm "nat_into_Finite";
  1164 *}
  1165 
  1166 end