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