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