eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
authortraytel
Mon Nov 25 10:14:29 2013 +0100 (2013-11-25)
changeset 545789387251b6a46
parent 54577 627f369d505e
child 54579 9733ab5c1df6
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
src/HOL/BNF/Basic_BNFs.thy
src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy
src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy
src/HOL/Cardinals/Fun_More_FP.thy
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Infinite_Set.thy
     1.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Mon Nov 25 08:22:29 2013 +0100
     1.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Mon Nov 25 10:14:29 2013 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
     1.5  
     1.6  lemma natLeq_cinfinite: "cinfinite natLeq"
     1.7 -unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
     1.8 +unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
     1.9  
    1.10  lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
    1.11    unfolding wpull_def Grp_def by auto
     2.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Mon Nov 25 08:22:29 2013 +0100
     2.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Mon Nov 25 10:14:29 2013 +0100
     2.3 @@ -121,7 +121,7 @@
     2.4  subsection {* (In)finite cardinals *}
     2.5  
     2.6  definition cinfinite where
     2.7 -  "cinfinite r = infinite (Field r)"
     2.8 +  "cinfinite r = (\<not> finite (Field r))"
     2.9  
    2.10  abbreviation Cinfinite where
    2.11    "Cinfinite r \<equiv> cinfinite r \<and> Card_order r"
    2.12 @@ -140,7 +140,7 @@
    2.13    assumes inf: "Cinfinite r"
    2.14    shows "natLeq \<le>o r"
    2.15  proof -
    2.16 -  from inf have "natLeq \<le>o |Field r|" by (simp add: cinfinite_def infinite_iff_natLeq_ordLeq)
    2.17 +  from inf have "natLeq \<le>o |Field r|" by (metis cinfinite_def infinite_iff_natLeq_ordLeq)
    2.18    also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
    2.19    finally show ?thesis .
    2.20  qed
     3.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Nov 25 08:22:29 2013 +0100
     3.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Nov 25 10:14:29 2013 +0100
     3.3 @@ -308,18 +308,17 @@
     3.4  
     3.5  corollary Card_order_Times3:
     3.6  "Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<times> (Field r)|"
     3.7 -using card_of_Times3 card_of_Field_ordIso
     3.8 -      ordIso_ordLeq_trans ordIso_symmetric by blast
     3.9 +  by (rule card_of_Times3)
    3.10  
    3.11  lemma card_of_Times_cong1[simp]:
    3.12  assumes "|A| =o |B|"
    3.13  shows "|A \<times> C| =o |B \<times> C|"
    3.14 -using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono1)
    3.15 +using assms by (simp add: ordIso_iff_ordLeq)
    3.16  
    3.17  lemma card_of_Times_cong2[simp]:
    3.18  assumes "|A| =o |B|"
    3.19  shows "|C \<times> A| =o |C \<times> B|"
    3.20 -using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono2)
    3.21 +using assms by (simp add: ordIso_iff_ordLeq)
    3.22  
    3.23  lemma card_of_Times_mono[simp]:
    3.24  assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
    3.25 @@ -473,18 +472,18 @@
    3.26  by auto
    3.27  
    3.28  corollary Times_same_infinite_bij_betw:
    3.29 -assumes "infinite A"
    3.30 +assumes "\<not>finite A"
    3.31  shows "\<exists>f. bij_betw f (A \<times> A) A"
    3.32  using assms by (auto simp add: card_of_ordIso)
    3.33  
    3.34  corollary Times_same_infinite_bij_betw_types:
    3.35 -assumes INF: "infinite(UNIV::'a set)"
    3.36 +assumes INF: "\<not>finite(UNIV::'a set)"
    3.37  shows "\<exists>(f::('a * 'a) => 'a). bij f"
    3.38  using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
    3.39  by auto
    3.40  
    3.41  corollary Times_infinite_bij_betw:
    3.42 -assumes INF: "infinite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
    3.43 +assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
    3.44  shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
    3.45  proof-
    3.46    have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
    3.47 @@ -493,19 +492,19 @@
    3.48  qed
    3.49  
    3.50  corollary Times_infinite_bij_betw_types:
    3.51 -assumes INF: "infinite(UNIV::'a set)" and
    3.52 +assumes INF: "\<not>finite(UNIV::'a set)" and
    3.53          BIJ: "inj(g::'b \<Rightarrow> 'a)"
    3.54  shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
    3.55  using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
    3.56  by auto
    3.57  
    3.58  lemma card_of_Times_ordLeq_infinite:
    3.59 -"\<lbrakk>infinite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
    3.60 +"\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
    3.61   \<Longrightarrow> |A <*> B| \<le>o |C|"
    3.62  by(simp add: card_of_Sigma_ordLeq_infinite)
    3.63  
    3.64  corollary Plus_infinite_bij_betw:
    3.65 -assumes INF: "infinite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
    3.66 +assumes INF: "\<not>finite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
    3.67  shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
    3.68  proof-
    3.69    have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
    3.70 @@ -514,14 +513,14 @@
    3.71  qed
    3.72  
    3.73  corollary Plus_infinite_bij_betw_types:
    3.74 -assumes INF: "infinite(UNIV::'a set)" and
    3.75 +assumes INF: "\<not>finite(UNIV::'a set)" and
    3.76          BIJ: "inj(g::'b \<Rightarrow> 'a)"
    3.77  shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
    3.78  using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
    3.79  by auto
    3.80  
    3.81  lemma card_of_Un_infinite:
    3.82 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
    3.83 +assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
    3.84  shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
    3.85  proof-
    3.86    have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
    3.87 @@ -533,12 +532,12 @@
    3.88  qed
    3.89  
    3.90  lemma card_of_Un_infinite_simps[simp]:
    3.91 -"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
    3.92 -"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
    3.93 +"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
    3.94 +"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
    3.95  using card_of_Un_infinite by auto
    3.96  
    3.97  lemma card_of_Un_diff_infinite:
    3.98 -assumes INF: "infinite A" and LESS: "|B| <o |A|"
    3.99 +assumes INF: "\<not>finite A" and LESS: "|B| <o |A|"
   3.100  shows "|A - B| =o |A|"
   3.101  proof-
   3.102    obtain C where C_def: "C = A - B" by blast
   3.103 @@ -554,7 +553,7 @@
   3.104      using card_of_ordLeq_finite * by blast
   3.105      hence False using ** INF card_of_ordIso_finite 1 by blast
   3.106     }
   3.107 -   hence "infinite B" by auto
   3.108 +   hence "\<not>finite B" by auto
   3.109     ultimately have False
   3.110     using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
   3.111    }
   3.112 @@ -563,14 +562,14 @@
   3.113      hence "finite B" using card_of_ordLeq_finite 2 by blast
   3.114      hence False using * INF card_of_ordIso_finite 1 by blast
   3.115    }
   3.116 -  hence "infinite C" by auto
   3.117 +  hence "\<not>finite C" by auto
   3.118    hence "|C| =o |A|"
   3.119    using  card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
   3.120    thus ?thesis unfolding C_def .
   3.121  qed
   3.122  
   3.123  corollary Card_order_Un_infinite:
   3.124 -assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
   3.125 +assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
   3.126          LEQ: "p \<le>o r"
   3.127  shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
   3.128  proof-
   3.129 @@ -584,12 +583,12 @@
   3.130  qed
   3.131  
   3.132  corollary subset_ordLeq_diff_infinite:
   3.133 -assumes INF: "infinite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
   3.134 -shows "infinite (B - A)"
   3.135 +assumes INF: "\<not>finite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
   3.136 +shows "\<not>finite (B - A)"
   3.137  using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
   3.138  
   3.139  lemma card_of_Times_ordLess_infinite[simp]:
   3.140 -assumes INF: "infinite C" and
   3.141 +assumes INF: "\<not>finite C" and
   3.142          LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
   3.143  shows "|A \<times> B| <o |C|"
   3.144  proof(cases "A = {} \<or> B = {}")
   3.145 @@ -601,17 +600,17 @@
   3.146  next
   3.147    assume Case2: "\<not>(A = {} \<or> B = {})"
   3.148    {assume *: "|C| \<le>o |A \<times> B|"
   3.149 -   hence "infinite (A \<times> B)" using INF card_of_ordLeq_finite by blast
   3.150 -   hence 1: "infinite A \<or> infinite B" using finite_cartesian_product by blast
   3.151 +   hence "\<not>finite (A \<times> B)" using INF card_of_ordLeq_finite by blast
   3.152 +   hence 1: "\<not>finite A \<or> \<not>finite B" using finite_cartesian_product by blast
   3.153     {assume Case21: "|A| \<le>o |B|"
   3.154 -    hence "infinite B" using 1 card_of_ordLeq_finite by blast
   3.155 +    hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
   3.156      hence "|A \<times> B| =o |B|" using Case2 Case21
   3.157      by (auto simp add: card_of_Times_infinite)
   3.158      hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   3.159     }
   3.160     moreover
   3.161     {assume Case22: "|B| \<le>o |A|"
   3.162 -    hence "infinite A" using 1 card_of_ordLeq_finite by blast
   3.163 +    hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
   3.164      hence "|A \<times> B| =o |A|" using Case2 Case22
   3.165      by (auto simp add: card_of_Times_infinite)
   3.166      hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   3.167 @@ -624,7 +623,7 @@
   3.168  qed
   3.169  
   3.170  lemma card_of_Times_ordLess_infinite_Field[simp]:
   3.171 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
   3.172 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
   3.173          LESS1: "|A| <o r" and LESS2: "|B| <o r"
   3.174  shows "|A \<times> B| <o r"
   3.175  proof-
   3.176 @@ -639,14 +638,14 @@
   3.177  qed
   3.178  
   3.179  lemma card_of_Un_ordLess_infinite[simp]:
   3.180 -assumes INF: "infinite C" and
   3.181 +assumes INF: "\<not>finite C" and
   3.182          LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
   3.183  shows "|A \<union> B| <o |C|"
   3.184  using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
   3.185        ordLeq_ordLess_trans by blast
   3.186  
   3.187  lemma card_of_Un_ordLess_infinite_Field[simp]:
   3.188 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
   3.189 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
   3.190          LESS1: "|A| <o r" and LESS2: "|B| <o r"
   3.191  shows "|A Un B| <o r"
   3.192  proof-
   3.193 @@ -667,10 +666,10 @@
   3.194  "finite A = ( |A| <o |UNIV :: nat set| )"
   3.195  using infinite_iff_card_of_nat[of A]
   3.196  not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
   3.197 -by (fastforce simp: card_of_Well_order)
   3.198 +by fastforce
   3.199  
   3.200  lemma finite_ordLess_infinite2[simp]:
   3.201 -assumes "finite A" and "infinite B"
   3.202 +assumes "finite A" and "\<not>finite B"
   3.203  shows "|A| <o |B|"
   3.204  using assms
   3.205  finite_ordLess_infinite[of "|A|" "|B|"]
   3.206 @@ -678,7 +677,7 @@
   3.207  Field_card_of[of A] Field_card_of[of B] by auto
   3.208  
   3.209  lemma infinite_card_of_insert:
   3.210 -assumes "infinite A"
   3.211 +assumes "\<not>finite A"
   3.212  shows "|insert a A| =o |A|"
   3.213  proof-
   3.214    have iA: "insert a A = A \<union> {a}" by simp
   3.215 @@ -688,7 +687,7 @@
   3.216  qed
   3.217  
   3.218  lemma card_of_Un_singl_ordLess_infinite1:
   3.219 -assumes "infinite B" and "|A| <o |B|"
   3.220 +assumes "\<not>finite B" and "|A| <o |B|"
   3.221  shows "|{a} Un A| <o |B|"
   3.222  proof-
   3.223    have "|{a}| <o |B|" using assms by auto
   3.224 @@ -696,7 +695,7 @@
   3.225  qed
   3.226  
   3.227  lemma card_of_Un_singl_ordLess_infinite:
   3.228 -assumes "infinite B"
   3.229 +assumes "\<not>finite B"
   3.230  shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
   3.231  using assms card_of_Un_singl_ordLess_infinite1[of B A]
   3.232  proof(auto)
   3.233 @@ -766,11 +765,11 @@
   3.234  qed
   3.235  
   3.236  lemma card_of_nlists_infinite:
   3.237 -assumes "infinite A"
   3.238 +assumes "\<not>finite A"
   3.239  shows "|nlists A n| \<le>o |A|"
   3.240  proof(induct n)
   3.241    have "A \<noteq> {}" using assms by auto
   3.242 -  thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0 card_of_singl_ordLeq)
   3.243 +  thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0)
   3.244  next
   3.245    fix n assume IH: "|nlists A n| \<le>o |A|"
   3.246    have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
   3.247 @@ -857,18 +856,17 @@
   3.248  qed
   3.249  
   3.250  lemma card_of_lists_infinite[simp]:
   3.251 -assumes "infinite A"
   3.252 +assumes "\<not>finite A"
   3.253  shows "|lists A| =o |A|"
   3.254  proof-
   3.255 -  have "|lists A| \<le>o |A|"
   3.256 -  using assms
   3.257 -  by (auto simp add: lists_UNION_nlists card_of_UNION_ordLeq_infinite
   3.258 -                     infinite_iff_card_of_nat card_of_nlists_infinite)
   3.259 +  have "|lists A| \<le>o |A|" unfolding lists_UNION_nlists
   3.260 +  by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
   3.261 +    (metis infinite_iff_card_of_nat assms)
   3.262    thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
   3.263  qed
   3.264  
   3.265  lemma Card_order_lists_infinite:
   3.266 -assumes "Card_order r" and "infinite(Field r)"
   3.267 +assumes "Card_order r" and "\<not>finite(Field r)"
   3.268  shows "|lists(Field r)| =o r"
   3.269  using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
   3.270  
   3.271 @@ -878,12 +876,12 @@
   3.272  using assms card_of_cong card_of_lists_cong by blast
   3.273  
   3.274  corollary lists_infinite_bij_betw:
   3.275 -assumes "infinite A"
   3.276 +assumes "\<not>finite A"
   3.277  shows "\<exists>f. bij_betw f (lists A) A"
   3.278  using assms card_of_lists_infinite card_of_ordIso by blast
   3.279  
   3.280  corollary lists_infinite_bij_betw_types:
   3.281 -assumes "infinite(UNIV :: 'a set)"
   3.282 +assumes "\<not>finite(UNIV :: 'a set)"
   3.283  shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
   3.284  using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
   3.285  using lists_UNIV by auto
   3.286 @@ -991,13 +989,13 @@
   3.287  qed
   3.288  
   3.289  lemma card_of_Fpow_infinite[simp]:
   3.290 -assumes "infinite A"
   3.291 +assumes "\<not>finite A"
   3.292  shows "|Fpow A| =o |A|"
   3.293  using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
   3.294        ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
   3.295  
   3.296  corollary Fpow_infinite_bij_betw:
   3.297 -assumes "infinite A"
   3.298 +assumes "\<not>finite A"
   3.299  shows "\<exists>f. bij_betw f (Fpow A) A"
   3.300  using assms card_of_Fpow_infinite card_of_ordIso by blast
   3.301  
   3.302 @@ -1052,7 +1050,7 @@
   3.303     simp add: Field_natLeq_on, unfold rel.under_def, auto)
   3.304  
   3.305  lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
   3.306 -using Field_natLeq Field_natLeq_on[of n] nat_infinite
   3.307 +using Field_natLeq Field_natLeq_on[of n]
   3.308        finite_ordLess_infinite[of "natLeq_on n" natLeq]
   3.309        natLeq_Well_order natLeq_on_Well_order[of n] by auto
   3.310  
   3.311 @@ -1074,11 +1072,11 @@
   3.312  subsubsection {* Then as cardinals *}
   3.313  
   3.314  lemma ordIso_natLeq_infinite1:
   3.315 -"|A| =o natLeq \<Longrightarrow> infinite A"
   3.316 +"|A| =o natLeq \<Longrightarrow> \<not>finite A"
   3.317  using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
   3.318  
   3.319  lemma ordIso_natLeq_infinite2:
   3.320 -"natLeq =o |A| \<Longrightarrow> infinite A"
   3.321 +"natLeq =o |A| \<Longrightarrow> \<not>finite A"
   3.322  using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
   3.323  
   3.324  lemma ordLeq_natLeq_on_imp_finite:
   3.325 @@ -1148,11 +1146,11 @@
   3.326  qed
   3.327  
   3.328  lemma card_of_Plus_ordLeq_infinite[simp]:
   3.329 -assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
   3.330 +assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
   3.331  shows "|A <+> B| \<le>o |C|"
   3.332  proof-
   3.333    let ?r = "cardSuc |C|"
   3.334 -  have "Card_order ?r \<and> infinite (Field ?r)" using assms by simp
   3.335 +  have "Card_order ?r \<and> \<not>finite (Field ?r)" using assms by simp
   3.336    moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
   3.337    ultimately have "|A <+> B| <o ?r"
   3.338    using card_of_Plus_ordLess_infinite_Field by blast
   3.339 @@ -1160,7 +1158,7 @@
   3.340  qed
   3.341  
   3.342  lemma card_of_Un_ordLeq_infinite[simp]:
   3.343 -assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
   3.344 +assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
   3.345  shows "|A Un B| \<le>o |C|"
   3.346  using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
   3.347  ordLeq_transitive by metis
   3.348 @@ -1185,12 +1183,12 @@
   3.349  using assms unfolding relChain_def by auto
   3.350  
   3.351  lemma card_of_infinite_diff_finite:
   3.352 -assumes "infinite A" and "finite B"
   3.353 +assumes "\<not>finite A" and "finite B"
   3.354  shows "|A - B| =o |A|"
   3.355  by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
   3.356  
   3.357  lemma infinite_card_of_diff_singl:
   3.358 -assumes "infinite A"
   3.359 +assumes "\<not>finite A"
   3.360  shows "|A - {a}| =o |A|"
   3.361  by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
   3.362  
   3.363 @@ -1235,8 +1233,8 @@
   3.364  
   3.365  lemma infinite_Bpow:
   3.366  assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
   3.367 -and A: "infinite A"
   3.368 -shows "infinite (Bpow r A)"
   3.369 +and A: "\<not>finite A"
   3.370 +shows "\<not>finite (Bpow r A)"
   3.371  using ordLeq_card_Bpow[OF rc r]
   3.372  by (metis A card_of_ordLeq_infinite)
   3.373  
   3.374 @@ -1350,7 +1348,7 @@
   3.375  qed
   3.376  
   3.377  lemma Bpow_ordLeq_Func_Field:
   3.378 -assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "infinite A"
   3.379 +assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "\<not>finite A"
   3.380  shows "|Bpow r A| \<le>o |Func (Field r) A|"
   3.381  proof-
   3.382    let ?F = "\<lambda> f. {x | x a. f a = x \<and> a \<in> Field r}"
   3.383 @@ -1368,10 +1366,9 @@
   3.384    hence "|Bpow r A - {{}}| \<le>o |Func (Field r) A|"
   3.385    by (rule surj_imp_ordLeq)
   3.386    moreover
   3.387 -  {have 2: "infinite (Bpow r A)" using infinite_Bpow[OF rc r A] .
   3.388 +  {have 2: "\<not>finite (Bpow r A)" using infinite_Bpow[OF rc r A] .
   3.389     have "|Bpow r A| =o |Bpow r A - {{}}|"
   3.390 -   using card_of_infinite_diff_finite
   3.391 -   by (metis Pow_empty 2 finite_Pow_iff infinite_imp_nonempty ordIso_symmetric)
   3.392 +     by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
   3.393    }
   3.394    ultimately show ?thesis by (metis ordIso_ordLeq_trans)
   3.395  qed
   3.396 @@ -1408,8 +1405,8 @@
   3.397  qed
   3.398  
   3.399  lemma infinite_Func:
   3.400 -assumes A: "infinite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
   3.401 -shows "infinite (Func A B)"
   3.402 +assumes A: "\<not>finite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
   3.403 +shows "\<not>finite (Func A B)"
   3.404  using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
   3.405  
   3.406  end
     4.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Mon Nov 25 08:22:29 2013 +0100
     4.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Mon Nov 25 10:14:29 2013 +0100
     4.3 @@ -487,8 +487,8 @@
     4.4  
     4.5  
     4.6  lemma infinite_Pow:
     4.7 -assumes "infinite A"
     4.8 -shows "infinite (Pow A)"
     4.9 +assumes "\<not> finite A"
    4.10 +shows "\<not> finite (Pow A)"
    4.11  proof-
    4.12    have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
    4.13    thus ?thesis by (metis assms finite_Pow_iff)
    4.14 @@ -908,8 +908,8 @@
    4.15  
    4.16  
    4.17  lemma card_of_ordLeq_infinite:
    4.18 -assumes "|A| \<le>o |B|" and "infinite A"
    4.19 -shows "infinite B"
    4.20 +assumes "|A| \<le>o |B|" and "\<not> finite A"
    4.21 +shows "\<not> finite B"
    4.22  using assms card_of_ordLeq_finite by auto
    4.23  
    4.24  
    4.25 @@ -938,15 +938,14 @@
    4.26  
    4.27  
    4.28  lemma infinite_iff_card_of_nat:
    4.29 -"infinite A = ( |UNIV::nat set| \<le>o |A| )"
    4.30 -by (auto simp add: infinite_iff_countable_subset card_of_ordLeq)
    4.31 -
    4.32 +"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
    4.33 +unfolding infinite_iff_countable_subset card_of_ordLeq ..
    4.34  
    4.35  text{* The next two results correspond to the ZF fact that all infinite cardinals are
    4.36  limit ordinals: *}
    4.37  
    4.38  lemma Card_order_infinite_not_under:
    4.39 -assumes CARD: "Card_order r" and INF: "infinite (Field r)"
    4.40 +assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
    4.41  shows "\<not> (\<exists>a. Field r = rel.under r a)"
    4.42  proof(auto)
    4.43    have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
    4.44 @@ -983,7 +982,7 @@
    4.45  
    4.46  
    4.47  lemma infinite_Card_order_limit:
    4.48 -assumes r: "Card_order r" and "infinite (Field r)"
    4.49 +assumes r: "Card_order r" and "\<not>finite (Field r)"
    4.50  and a: "a : Field r"
    4.51  shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
    4.52  proof-
    4.53 @@ -1005,11 +1004,11 @@
    4.54  
    4.55  
    4.56  theorem Card_order_Times_same_infinite:
    4.57 -assumes CO: "Card_order r" and INF: "infinite(Field r)"
    4.58 +assumes CO: "Card_order r" and INF: "\<not>finite(Field r)"
    4.59  shows "|Field r \<times> Field r| \<le>o r"
    4.60  proof-
    4.61    obtain phi where phi_def:
    4.62 -  "phi = (\<lambda>r::'a rel. Card_order r \<and> infinite(Field r) \<and>
    4.63 +  "phi = (\<lambda>r::'a rel. Card_order r \<and> \<not>finite(Field r) \<and>
    4.64                        \<not> |Field r \<times> Field r| \<le>o r )" by blast
    4.65    have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
    4.66    unfolding phi_def card_order_on_def by auto
    4.67 @@ -1060,15 +1059,15 @@
    4.68      }
    4.69      ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
    4.70      (*  *)
    4.71 -    have "infinite (Field r)" using 1 unfolding phi_def by simp
    4.72 -    hence "infinite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
    4.73 -    hence "infinite A1" using 9 infinite_super finite_cartesian_product by blast
    4.74 +    have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
    4.75 +    hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
    4.76 +    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis
    4.77      moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
    4.78      using card_of_Card_order[of A1] card_of_Well_order[of A1]
    4.79      by (simp add: Field_card_of)
    4.80      moreover have "\<not> r \<le>o | A1 |"
    4.81      using temp4 11 3 using not_ordLeq_iff_ordLess by blast
    4.82 -    ultimately have "infinite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
    4.83 +    ultimately have "\<not> finite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
    4.84      by (simp add: card_of_card_order_on)
    4.85      hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
    4.86      using 2 unfolding phi_def by blast
    4.87 @@ -1081,7 +1080,7 @@
    4.88  
    4.89  
    4.90  corollary card_of_Times_same_infinite:
    4.91 -assumes "infinite A"
    4.92 +assumes "\<not>finite A"
    4.93  shows "|A \<times> A| =o |A|"
    4.94  proof-
    4.95    let ?r = "|A|"
    4.96 @@ -1094,7 +1093,7 @@
    4.97  
    4.98  
    4.99  lemma card_of_Times_infinite:
   4.100 -assumes INF: "infinite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
   4.101 +assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
   4.102  shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
   4.103  proof-
   4.104    have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
   4.105 @@ -1111,7 +1110,7 @@
   4.106  
   4.107  
   4.108  corollary Card_order_Times_infinite:
   4.109 -assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
   4.110 +assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
   4.111          NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
   4.112  shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
   4.113  proof-
   4.114 @@ -1125,7 +1124,7 @@
   4.115  
   4.116  
   4.117  lemma card_of_Sigma_ordLeq_infinite:
   4.118 -assumes INF: "infinite B" and
   4.119 +assumes INF: "\<not>finite B" and
   4.120          LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
   4.121  shows "|SIGMA i : I. A i| \<le>o |B|"
   4.122  proof(cases "I = {}", simp add: card_of_empty)
   4.123 @@ -1139,7 +1138,7 @@
   4.124  
   4.125  
   4.126  lemma card_of_Sigma_ordLeq_infinite_Field:
   4.127 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
   4.128 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
   4.129          LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
   4.130  shows "|SIGMA i : I. A i| \<le>o r"
   4.131  proof-
   4.132 @@ -1155,21 +1154,21 @@
   4.133  
   4.134  
   4.135  lemma card_of_Times_ordLeq_infinite_Field:
   4.136 -"\<lbrakk>infinite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
   4.137 +"\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
   4.138   \<Longrightarrow> |A <*> B| \<le>o r"
   4.139  by(simp add: card_of_Sigma_ordLeq_infinite_Field)
   4.140  
   4.141  
   4.142  lemma card_of_Times_infinite_simps:
   4.143 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
   4.144 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
   4.145 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
   4.146 -"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
   4.147 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
   4.148 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
   4.149 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
   4.150 +"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
   4.151  by (auto simp add: card_of_Times_infinite ordIso_symmetric)
   4.152  
   4.153  
   4.154  lemma card_of_UNION_ordLeq_infinite:
   4.155 -assumes INF: "infinite B" and
   4.156 +assumes INF: "\<not>finite B" and
   4.157          LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
   4.158  shows "|\<Union> i \<in> I. A i| \<le>o |B|"
   4.159  proof(cases "I = {}", simp add: card_of_empty)
   4.160 @@ -1183,7 +1182,7 @@
   4.161  
   4.162  
   4.163  corollary card_of_UNION_ordLeq_infinite_Field:
   4.164 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
   4.165 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
   4.166          LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
   4.167  shows "|\<Union> i \<in> I. A i| \<le>o r"
   4.168  proof-
   4.169 @@ -1199,7 +1198,7 @@
   4.170  
   4.171  
   4.172  lemma card_of_Plus_infinite1:
   4.173 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
   4.174 +assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
   4.175  shows "|A <+> B| =o |A|"
   4.176  proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
   4.177    let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b"  let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
   4.178 @@ -1210,7 +1209,7 @@
   4.179      assume Case1: "B = {b1}"
   4.180      have 2: "bij_betw ?Inl A ((?Inl ` A))"
   4.181      unfolding bij_betw_def inj_on_def by auto
   4.182 -    hence 3: "infinite (?Inl ` A)"
   4.183 +    hence 3: "\<not>finite (?Inl ` A)"
   4.184      using INF bij_betw_finite[of ?Inl A] by blast
   4.185      let ?A' = "?Inl ` A \<union> {?Inr b1}"
   4.186      obtain g where "bij_betw g (?Inl ` A) ?A'"
   4.187 @@ -1238,20 +1237,20 @@
   4.188  
   4.189  
   4.190  lemma card_of_Plus_infinite2:
   4.191 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
   4.192 +assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
   4.193  shows "|B <+> A| =o |A|"
   4.194  using assms card_of_Plus_commute card_of_Plus_infinite1
   4.195  ordIso_equivalence by blast
   4.196  
   4.197  
   4.198  lemma card_of_Plus_infinite:
   4.199 -assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
   4.200 +assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
   4.201  shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
   4.202  using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
   4.203  
   4.204  
   4.205  corollary Card_order_Plus_infinite:
   4.206 -assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
   4.207 +assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
   4.208          LEQ: "p \<le>o r"
   4.209  shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
   4.210  proof-
   4.211 @@ -1281,8 +1280,8 @@
   4.212  where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
   4.213  
   4.214  lemma infinite_cartesian_product:
   4.215 -assumes "infinite A" "infinite B"
   4.216 -shows "infinite (A \<times> B)"
   4.217 +assumes "\<not>finite A" "\<not>finite B"
   4.218 +shows "\<not>finite (A \<times> B)"
   4.219  proof
   4.220    assume "finite (A \<times> B)"
   4.221    from assms(1) have "A \<noteq> {}" by auto
   4.222 @@ -1421,7 +1420,7 @@
   4.223        Card_order_iff_Restr_underS Restr_natLeq2, simp add:  Field_natLeq)
   4.224    fix n have "finite(Field (natLeq_on n))"
   4.225    unfolding Field_natLeq_on by auto
   4.226 -  moreover have "infinite(UNIV::nat set)" by auto
   4.227 +  moreover have "\<not>finite(UNIV::nat set)" by auto
   4.228    ultimately show "natLeq_on n <o |UNIV::nat set|"
   4.229    using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
   4.230          Field_card_of[of "UNIV::nat set"]
   4.231 @@ -1441,7 +1440,7 @@
   4.232  
   4.233  
   4.234  corollary infinite_iff_natLeq_ordLeq:
   4.235 -"infinite A = ( natLeq \<le>o |A| )"
   4.236 +"\<not>finite A = ( natLeq \<le>o |A| )"
   4.237  using infinite_iff_card_of_nat[of A] card_of_nat
   4.238        ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
   4.239  
   4.240 @@ -1769,7 +1768,7 @@
   4.241  
   4.242  
   4.243  lemma card_of_Plus_ordLess_infinite:
   4.244 -assumes INF: "infinite C" and
   4.245 +assumes INF: "\<not>finite C" and
   4.246          LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
   4.247  shows "|A <+> B| <o |C|"
   4.248  proof(cases "A = {} \<or> B = {}")
   4.249 @@ -1784,17 +1783,17 @@
   4.250  next
   4.251    assume Case2: "\<not>(A = {} \<or> B = {})"
   4.252    {assume *: "|C| \<le>o |A <+> B|"
   4.253 -   hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast
   4.254 -   hence 1: "infinite A \<or> infinite B" using finite_Plus by blast
   4.255 +   hence "\<not>finite (A <+> B)" using INF card_of_ordLeq_finite by blast
   4.256 +   hence 1: "\<not>finite A \<or> \<not>finite B" using finite_Plus by blast
   4.257     {assume Case21: "|A| \<le>o |B|"
   4.258 -    hence "infinite B" using 1 card_of_ordLeq_finite by blast
   4.259 +    hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
   4.260      hence "|A <+> B| =o |B|" using Case2 Case21
   4.261      by (auto simp add: card_of_Plus_infinite)
   4.262      hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   4.263     }
   4.264     moreover
   4.265     {assume Case22: "|B| \<le>o |A|"
   4.266 -    hence "infinite A" using 1 card_of_ordLeq_finite by blast
   4.267 +    hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
   4.268      hence "|A <+> B| =o |A|" using Case2 Case22
   4.269      by (auto simp add: card_of_Plus_infinite)
   4.270      hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
   4.271 @@ -1808,7 +1807,7 @@
   4.272  
   4.273  
   4.274  lemma card_of_Plus_ordLess_infinite_Field:
   4.275 -assumes INF: "infinite (Field r)" and r: "Card_order r" and
   4.276 +assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
   4.277          LESS1: "|A| <o r" and LESS2: "|B| <o r"
   4.278  shows "|A <+> B| <o r"
   4.279  proof-
   4.280 @@ -1824,12 +1823,12 @@
   4.281  
   4.282  
   4.283  lemma card_of_Plus_ordLeq_infinite_Field:
   4.284 -assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
   4.285 +assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
   4.286  and c: "Card_order r"
   4.287  shows "|A <+> B| \<le>o r"
   4.288  proof-
   4.289    let ?r' = "cardSuc r"
   4.290 -  have "Card_order ?r' \<and> infinite (Field ?r')" using assms
   4.291 +  have "Card_order ?r' \<and> \<not>finite (Field ?r')" using assms
   4.292    by (simp add: cardSuc_Card_order cardSuc_finite)
   4.293    moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
   4.294    by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
   4.295 @@ -1841,7 +1840,7 @@
   4.296  
   4.297  
   4.298  lemma card_of_Un_ordLeq_infinite_Field:
   4.299 -assumes C: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
   4.300 +assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
   4.301  and "Card_order r"
   4.302  shows "|A Un B| \<le>o r"
   4.303  using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
   4.304 @@ -1904,7 +1903,7 @@
   4.305  
   4.306  
   4.307  lemma infinite_cardSuc_regular:
   4.308 -assumes r_inf: "infinite (Field r)" and r_card: "Card_order r"
   4.309 +assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"
   4.310  shows "regular (cardSuc r)"
   4.311  proof-
   4.312    let ?r' = "cardSuc r"
   4.313 @@ -1955,7 +1954,7 @@
   4.314  qed
   4.315  
   4.316  lemma cardSuc_UNION:
   4.317 -assumes r: "Card_order r" and "infinite (Field r)"
   4.318 +assumes r: "Card_order r" and "\<not>finite (Field r)"
   4.319  and As: "relChain (cardSuc r) As"
   4.320  and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
   4.321  and cardB: "|B| <=o r"
     5.1 --- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Mon Nov 25 08:22:29 2013 +0100
     5.2 +++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Mon Nov 25 10:14:29 2013 +0100
     5.3 @@ -861,7 +861,7 @@
     5.4  
     5.5  lemma finite_ordLess_infinite:
     5.6  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
     5.7 -        FIN: "finite(Field r)" and INF: "infinite(Field r')"
     5.8 +        FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
     5.9  shows "r <o r'"
    5.10  proof-
    5.11    {assume "r' \<le>o r"
     6.1 --- a/src/HOL/Cardinals/Fun_More_FP.thy	Mon Nov 25 08:22:29 2013 +0100
     6.2 +++ b/src/HOL/Cardinals/Fun_More_FP.thy	Mon Nov 25 10:14:29 2013 +0100
     6.3 @@ -8,12 +8,12 @@
     6.4  header {* More on Injections, Bijections and Inverses (FP) *}
     6.5  
     6.6  theory Fun_More_FP
     6.7 -imports "~~/src/HOL/Library/Infinite_Set"
     6.8 +imports Main
     6.9  begin
    6.10  
    6.11  
    6.12  text {* This section proves more facts (additional to those in @{text "Fun.thy"},
    6.13 -@{text "Hilbert_Choice.thy"}, @{text "Finite_Set.thy"} and @{text "Infinite_Set.thy"}),
    6.14 +@{text "Hilbert_Choice.thy"}, and @{text "Finite_Set.thy"}),
    6.15  mainly concerning injections, bijections, inverses and (numeric) cardinals of
    6.16  finite sets. *}
    6.17  
    6.18 @@ -97,18 +97,19 @@
    6.19  (*3*)lemma inj_on_finite:
    6.20  assumes "inj_on f A" "f ` A \<le> B" "finite B"
    6.21  shows "finite A"
    6.22 -using assms infinite_super by (fast dest: finite_imageD)
    6.23 +using assms by (metis finite_imageD finite_subset)
    6.24  
    6.25  
    6.26  (*3*)lemma infinite_imp_bij_betw:
    6.27 -assumes INF: "infinite A"
    6.28 +assumes INF: "\<not> finite A"
    6.29  shows "\<exists>h. bij_betw h A (A - {a})"
    6.30  proof(cases "a \<in> A")
    6.31    assume Case1: "a \<notin> A"  hence "A - {a} = A" by blast
    6.32    thus ?thesis using bij_betw_id[of A] by auto
    6.33  next
    6.34    assume Case2: "a \<in> A"
    6.35 -  have "infinite (A - {a})" using INF infinite_remove by auto
    6.36 +find_theorems "\<not> finite _"
    6.37 +  have "\<not> finite (A - {a})" using INF by auto
    6.38    with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
    6.39    where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
    6.40    obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
    6.41 @@ -179,7 +180,7 @@
    6.42  
    6.43  
    6.44  (*3*)lemma infinite_imp_bij_betw2:
    6.45 -assumes INF: "infinite A"
    6.46 +assumes INF: "\<not> finite A"
    6.47  shows "\<exists>h. bij_betw h A (A \<union> {a})"
    6.48  proof(cases "a \<in> A")
    6.49    assume Case1: "a \<in> A"  hence "A \<union> {a} = A" by blast
    6.50 @@ -187,7 +188,7 @@
    6.51  next
    6.52    let ?A' = "A \<union> {a}"
    6.53    assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
    6.54 -  moreover have "infinite ?A'" using INF by auto
    6.55 +  moreover have "\<not> finite ?A'" using INF by auto
    6.56    ultimately obtain f where "bij_betw f ?A' A"
    6.57    using infinite_imp_bij_betw[of ?A' a] by auto
    6.58    hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
     7.1 --- a/src/HOL/Fun.thy	Mon Nov 25 08:22:29 2013 +0100
     7.2 +++ b/src/HOL/Fun.thy	Mon Nov 25 10:14:29 2013 +0100
     7.3 @@ -308,6 +308,16 @@
     7.4    show ?thesis ..
     7.5  qed
     7.6  
     7.7 +lemma linorder_injI:
     7.8 +  assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
     7.9 +  shows "inj f"
    7.10 +  -- {* Courtesy of Stephan Merz *}
    7.11 +proof (rule inj_onI)
    7.12 +  fix x y
    7.13 +  assume f_eq: "f x = f y"
    7.14 +  show "x = y" by (rule linorder_cases) (auto dest: hyp simp: f_eq)
    7.15 +qed
    7.16 +
    7.17  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    7.18    by auto
    7.19  
     8.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Nov 25 08:22:29 2013 +0100
     8.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Nov 25 10:14:29 2013 +0100
     8.3 @@ -272,6 +272,41 @@
     8.4    ultimately show "finite (UNIV :: 'a set)" by simp
     8.5  qed
     8.6  
     8.7 +text {*
     8.8 +  Every infinite set contains a countable subset. More precisely we
     8.9 +  show that a set @{text S} is infinite if and only if there exists an
    8.10 +  injective function from the naturals into @{text S}.
    8.11 +
    8.12 +  The ``only if'' direction is harder because it requires the
    8.13 +  construction of a sequence of pairwise different elements of an
    8.14 +  infinite set @{text S}. The idea is to construct a sequence of
    8.15 +  non-empty and infinite subsets of @{text S} obtained by successively
    8.16 +  removing elements of @{text S}.
    8.17 +*}
    8.18 +
    8.19 +lemma infinite_countable_subset:
    8.20 +  assumes inf: "\<not> finite (S::'a set)"
    8.21 +  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
    8.22 +  -- {* Courtesy of Stephan Merz *}
    8.23 +proof -
    8.24 +  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
    8.25 +  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
    8.26 +  { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
    8.27 +  moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
    8.28 +  ultimately have "range pick \<subseteq> S" by auto
    8.29 +  moreover
    8.30 +  { fix n m                 
    8.31 +    have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
    8.32 +    hence "pick n \<noteq> pick (n + Suc m)" by (metis *)
    8.33 +  }
    8.34 +  then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
    8.35 +  ultimately show ?thesis by blast
    8.36 +qed
    8.37 +
    8.38 +lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
    8.39 +  -- {* Courtesy of Stephan Merz *}
    8.40 +  by (metis finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset)
    8.41 +
    8.42  lemma image_inv_into_cancel:
    8.43    assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
    8.44    shows "f `((inv_into A f)`B') = B'"
     9.1 --- a/src/HOL/Library/Infinite_Set.thy	Mon Nov 25 08:22:29 2013 +0100
     9.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Nov 25 10:14:29 2013 +0100
     9.3 @@ -200,12 +200,6 @@
     9.4  lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
     9.5    by simp
     9.6  
     9.7 -text {*
     9.8 -  Every infinite set contains a countable subset. More precisely we
     9.9 -  show that a set @{text S} is infinite if and only if there exists an
    9.10 -  injective function from the naturals into @{text S}.
    9.11 -*}
    9.12 -
    9.13  lemma range_inj_infinite:
    9.14    "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
    9.15  proof
    9.16 @@ -215,6 +209,7 @@
    9.17    then show False by simp
    9.18  qed
    9.19  
    9.20 +(* duplicates Int.infinite_UNIV_int *)
    9.21  lemma int_infinite [simp]: "infinite (UNIV::int set)"
    9.22  proof -
    9.23    from inj_int have "infinite (range int)"
    9.24 @@ -226,108 +221,6 @@
    9.25  qed
    9.26  
    9.27  text {*
    9.28 -  The ``only if'' direction is harder because it requires the
    9.29 -  construction of a sequence of pairwise different elements of an
    9.30 -  infinite set @{text S}. The idea is to construct a sequence of
    9.31 -  non-empty and infinite subsets of @{text S} obtained by successively
    9.32 -  removing elements of @{text S}.
    9.33 -*}
    9.34 -
    9.35 -lemma linorder_injI:
    9.36 -  assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
    9.37 -  shows "inj f"
    9.38 -proof (rule inj_onI)
    9.39 -  fix x y
    9.40 -  assume f_eq: "f x = f y"
    9.41 -  show "x = y"
    9.42 -  proof (rule linorder_cases)
    9.43 -    assume "x < y"
    9.44 -    with hyp have "f x \<noteq> f y" by blast
    9.45 -    with f_eq show ?thesis by simp
    9.46 -  next
    9.47 -    assume "x = y"
    9.48 -    then show ?thesis .
    9.49 -  next
    9.50 -    assume "y < x"
    9.51 -    with hyp have "f y \<noteq> f x" by blast
    9.52 -    with f_eq show ?thesis by simp
    9.53 -  qed
    9.54 -qed
    9.55 -
    9.56 -lemma infinite_countable_subset:
    9.57 -  assumes inf: "infinite (S::'a set)"
    9.58 -  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
    9.59 -proof -
    9.60 -  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
    9.61 -  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
    9.62 -  have Sseq_inf: "\<And>n. infinite (Sseq n)"
    9.63 -  proof -
    9.64 -    fix n
    9.65 -    show "infinite (Sseq n)"
    9.66 -    proof (induct n)
    9.67 -      from inf show "infinite (Sseq 0)"
    9.68 -        by (simp add: Sseq_def)
    9.69 -    next
    9.70 -      fix n
    9.71 -      assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
    9.72 -        by (simp add: Sseq_def infinite_remove)
    9.73 -    qed
    9.74 -  qed
    9.75 -  have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
    9.76 -  proof -
    9.77 -    fix n
    9.78 -    show "Sseq n \<subseteq> S"
    9.79 -      by (induct n) (auto simp add: Sseq_def)
    9.80 -  qed
    9.81 -  have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
    9.82 -  proof -
    9.83 -    fix n
    9.84 -    show "pick n \<in> Sseq n"
    9.85 -      unfolding pick_def
    9.86 -    proof (rule someI_ex)
    9.87 -      from Sseq_inf have "infinite (Sseq n)" .
    9.88 -      then have "Sseq n \<noteq> {}" by auto
    9.89 -      then show "\<exists>x. x \<in> Sseq n" by auto
    9.90 -    qed
    9.91 -  qed
    9.92 -  with Sseq_S have rng: "range pick \<subseteq> S"
    9.93 -    by auto
    9.94 -  have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
    9.95 -  proof -
    9.96 -    fix n m
    9.97 -    show "pick n \<notin> Sseq (n + Suc m)"
    9.98 -      by (induct m) (auto simp add: Sseq_def pick_def)
    9.99 -  qed
   9.100 -  have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
   9.101 -  proof -
   9.102 -    fix n m
   9.103 -    from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
   9.104 -    moreover from pick_Sseq_gt
   9.105 -    have "pick n \<notin> Sseq (n + Suc m)" .
   9.106 -    ultimately show "pick n \<noteq> pick (n + Suc m)"
   9.107 -      by auto
   9.108 -  qed
   9.109 -  have inj: "inj pick"
   9.110 -  proof (rule linorder_injI)
   9.111 -    fix i j :: nat
   9.112 -    assume "i < j"
   9.113 -    show "pick i \<noteq> pick j"
   9.114 -    proof
   9.115 -      assume eq: "pick i = pick j"
   9.116 -      from `i < j` obtain k where "j = i + Suc k"
   9.117 -        by (auto simp add: less_iff_Suc_add)
   9.118 -      with pick_pick have "pick i \<noteq> pick j" by simp
   9.119 -      with eq show False by simp
   9.120 -    qed
   9.121 -  qed
   9.122 -  from rng inj show ?thesis by auto
   9.123 -qed
   9.124 -
   9.125 -lemma infinite_iff_countable_subset:
   9.126 -    "infinite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
   9.127 -  by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
   9.128 -
   9.129 -text {*
   9.130    For any function with infinite domain and finite range there is some
   9.131    element that is the image of infinitely many domain elements.  In
   9.132    particular, any infinite sequence of elements from a finite set