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