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
```