# HG changeset patch
# User traytel
# Date 1385370869 -3600
# Node ID 9387251b6a464db536084a063243fbc948deafe4
# Parent  627f369d505e049e113d009ca7ac85daff701dd1
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main

diff -r 627f369d505e -r 9387251b6a46 src/HOL/BNF/Basic_BNFs.thy
--- a/src/HOL/BNF/Basic_BNFs.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -16,7 +16,7 @@
 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
 
 lemma natLeq_cinfinite: "cinfinite natLeq"
-unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
+unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
 
 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"
   unfolding wpull_def Grp_def by auto
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -121,7 +121,7 @@
 subsection {* (In)finite cardinals *}
 
 definition cinfinite where
-  "cinfinite r = infinite (Field r)"
+  "cinfinite r = (\<not> finite (Field r))"
 
 abbreviation Cinfinite where
   "Cinfinite r \<equiv> cinfinite r \<and> Card_order r"
@@ -140,7 +140,7 @@
   assumes inf: "Cinfinite r"
   shows "natLeq \<le>o r"
 proof -
-  from inf have "natLeq \<le>o |Field r|" by (simp add: cinfinite_def infinite_iff_natLeq_ordLeq)
+  from inf have "natLeq \<le>o |Field r|" by (metis cinfinite_def infinite_iff_natLeq_ordLeq)
   also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
   finally show ?thesis .
 qed
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -308,18 +308,17 @@
 
 corollary Card_order_Times3:
 "Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<times> (Field r)|"
-using card_of_Times3 card_of_Field_ordIso
-      ordIso_ordLeq_trans ordIso_symmetric by blast
+  by (rule card_of_Times3)
 
 lemma card_of_Times_cong1[simp]:
 assumes "|A| =o |B|"
 shows "|A \<times> C| =o |B \<times> C|"
-using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono1)
+using assms by (simp add: ordIso_iff_ordLeq)
 
 lemma card_of_Times_cong2[simp]:
 assumes "|A| =o |B|"
 shows "|C \<times> A| =o |C \<times> B|"
-using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono2)
+using assms by (simp add: ordIso_iff_ordLeq)
 
 lemma card_of_Times_mono[simp]:
 assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
@@ -473,18 +472,18 @@
 by auto
 
 corollary Times_same_infinite_bij_betw:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "\<exists>f. bij_betw f (A \<times> A) A"
 using assms by (auto simp add: card_of_ordIso)
 
 corollary Times_same_infinite_bij_betw_types:
-assumes INF: "infinite(UNIV::'a set)"
+assumes INF: "\<not>finite(UNIV::'a set)"
 shows "\<exists>(f::('a * 'a) => 'a). bij f"
 using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
 by auto
 
 corollary Times_infinite_bij_betw:
-assumes INF: "infinite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
+assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
 shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
 proof-
   have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
@@ -493,19 +492,19 @@
 qed
 
 corollary Times_infinite_bij_betw_types:
-assumes INF: "infinite(UNIV::'a set)" and
+assumes INF: "\<not>finite(UNIV::'a set)" and
         BIJ: "inj(g::'b \<Rightarrow> 'a)"
 shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
 using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
 by auto
 
 lemma card_of_Times_ordLeq_infinite:
-"\<lbrakk>infinite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
+"\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
  \<Longrightarrow> |A <*> B| \<le>o |C|"
 by(simp add: card_of_Sigma_ordLeq_infinite)
 
 corollary Plus_infinite_bij_betw:
-assumes INF: "infinite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
+assumes INF: "\<not>finite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
 shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
 proof-
   have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
@@ -514,14 +513,14 @@
 qed
 
 corollary Plus_infinite_bij_betw_types:
-assumes INF: "infinite(UNIV::'a set)" and
+assumes INF: "\<not>finite(UNIV::'a set)" and
         BIJ: "inj(g::'b \<Rightarrow> 'a)"
 shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
 using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
 by auto
 
 lemma card_of_Un_infinite:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
 shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
 proof-
   have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
@@ -533,12 +532,12 @@
 qed
 
 lemma card_of_Un_infinite_simps[simp]:
-"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
-"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
+"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
+"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
 using card_of_Un_infinite by auto
 
 lemma card_of_Un_diff_infinite:
-assumes INF: "infinite A" and LESS: "|B| <o |A|"
+assumes INF: "\<not>finite A" and LESS: "|B| <o |A|"
 shows "|A - B| =o |A|"
 proof-
   obtain C where C_def: "C = A - B" by blast
@@ -554,7 +553,7 @@
     using card_of_ordLeq_finite * by blast
     hence False using ** INF card_of_ordIso_finite 1 by blast
    }
-   hence "infinite B" by auto
+   hence "\<not>finite B" by auto
    ultimately have False
    using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
   }
@@ -563,14 +562,14 @@
     hence "finite B" using card_of_ordLeq_finite 2 by blast
     hence False using * INF card_of_ordIso_finite 1 by blast
   }
-  hence "infinite C" by auto
+  hence "\<not>finite C" by auto
   hence "|C| =o |A|"
   using  card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
   thus ?thesis unfolding C_def .
 qed
 
 corollary Card_order_Un_infinite:
-assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
+assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
         LEQ: "p \<le>o r"
 shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
 proof-
@@ -584,12 +583,12 @@
 qed
 
 corollary subset_ordLeq_diff_infinite:
-assumes INF: "infinite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
-shows "infinite (B - A)"
+assumes INF: "\<not>finite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
+shows "\<not>finite (B - A)"
 using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
 
 lemma card_of_Times_ordLess_infinite[simp]:
-assumes INF: "infinite C" and
+assumes INF: "\<not>finite C" and
         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
 shows "|A \<times> B| <o |C|"
 proof(cases "A = {} \<or> B = {}")
@@ -601,17 +600,17 @@
 next
   assume Case2: "\<not>(A = {} \<or> B = {})"
   {assume *: "|C| \<le>o |A \<times> B|"
-   hence "infinite (A \<times> B)" using INF card_of_ordLeq_finite by blast
-   hence 1: "infinite A \<or> infinite B" using finite_cartesian_product by blast
+   hence "\<not>finite (A \<times> B)" using INF card_of_ordLeq_finite by blast
+   hence 1: "\<not>finite A \<or> \<not>finite B" using finite_cartesian_product by blast
    {assume Case21: "|A| \<le>o |B|"
-    hence "infinite B" using 1 card_of_ordLeq_finite by blast
+    hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
     hence "|A \<times> B| =o |B|" using Case2 Case21
     by (auto simp add: card_of_Times_infinite)
     hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
    }
    moreover
    {assume Case22: "|B| \<le>o |A|"
-    hence "infinite A" using 1 card_of_ordLeq_finite by blast
+    hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
     hence "|A \<times> B| =o |A|" using Case2 Case22
     by (auto simp add: card_of_Times_infinite)
     hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
@@ -624,7 +623,7 @@
 qed
 
 lemma card_of_Times_ordLess_infinite_Field[simp]:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
         LESS1: "|A| <o r" and LESS2: "|B| <o r"
 shows "|A \<times> B| <o r"
 proof-
@@ -639,14 +638,14 @@
 qed
 
 lemma card_of_Un_ordLess_infinite[simp]:
-assumes INF: "infinite C" and
+assumes INF: "\<not>finite C" and
         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
 shows "|A \<union> B| <o |C|"
 using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
       ordLeq_ordLess_trans by blast
 
 lemma card_of_Un_ordLess_infinite_Field[simp]:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
         LESS1: "|A| <o r" and LESS2: "|B| <o r"
 shows "|A Un B| <o r"
 proof-
@@ -667,10 +666,10 @@
 "finite A = ( |A| <o |UNIV :: nat set| )"
 using infinite_iff_card_of_nat[of A]
 not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
-by (fastforce simp: card_of_Well_order)
+by fastforce
 
 lemma finite_ordLess_infinite2[simp]:
-assumes "finite A" and "infinite B"
+assumes "finite A" and "\<not>finite B"
 shows "|A| <o |B|"
 using assms
 finite_ordLess_infinite[of "|A|" "|B|"]
@@ -678,7 +677,7 @@
 Field_card_of[of A] Field_card_of[of B] by auto
 
 lemma infinite_card_of_insert:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "|insert a A| =o |A|"
 proof-
   have iA: "insert a A = A \<union> {a}" by simp
@@ -688,7 +687,7 @@
 qed
 
 lemma card_of_Un_singl_ordLess_infinite1:
-assumes "infinite B" and "|A| <o |B|"
+assumes "\<not>finite B" and "|A| <o |B|"
 shows "|{a} Un A| <o |B|"
 proof-
   have "|{a}| <o |B|" using assms by auto
@@ -696,7 +695,7 @@
 qed
 
 lemma card_of_Un_singl_ordLess_infinite:
-assumes "infinite B"
+assumes "\<not>finite B"
 shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
 using assms card_of_Un_singl_ordLess_infinite1[of B A]
 proof(auto)
@@ -766,11 +765,11 @@
 qed
 
 lemma card_of_nlists_infinite:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "|nlists A n| \<le>o |A|"
 proof(induct n)
   have "A \<noteq> {}" using assms by auto
-  thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0 card_of_singl_ordLeq)
+  thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0)
 next
   fix n assume IH: "|nlists A n| \<le>o |A|"
   have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
@@ -857,18 +856,17 @@
 qed
 
 lemma card_of_lists_infinite[simp]:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "|lists A| =o |A|"
 proof-
-  have "|lists A| \<le>o |A|"
-  using assms
-  by (auto simp add: lists_UNION_nlists card_of_UNION_ordLeq_infinite
-                     infinite_iff_card_of_nat card_of_nlists_infinite)
+  have "|lists A| \<le>o |A|" unfolding lists_UNION_nlists
+  by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
+    (metis infinite_iff_card_of_nat assms)
   thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
 qed
 
 lemma Card_order_lists_infinite:
-assumes "Card_order r" and "infinite(Field r)"
+assumes "Card_order r" and "\<not>finite(Field r)"
 shows "|lists(Field r)| =o r"
 using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
 
@@ -878,12 +876,12 @@
 using assms card_of_cong card_of_lists_cong by blast
 
 corollary lists_infinite_bij_betw:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "\<exists>f. bij_betw f (lists A) A"
 using assms card_of_lists_infinite card_of_ordIso by blast
 
 corollary lists_infinite_bij_betw_types:
-assumes "infinite(UNIV :: 'a set)"
+assumes "\<not>finite(UNIV :: 'a set)"
 shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
 using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
 using lists_UNIV by auto
@@ -991,13 +989,13 @@
 qed
 
 lemma card_of_Fpow_infinite[simp]:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "|Fpow A| =o |A|"
 using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
       ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
 
 corollary Fpow_infinite_bij_betw:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "\<exists>f. bij_betw f (Fpow A) A"
 using assms card_of_Fpow_infinite card_of_ordIso by blast
 
@@ -1052,7 +1050,7 @@
    simp add: Field_natLeq_on, unfold rel.under_def, auto)
 
 lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
-using Field_natLeq Field_natLeq_on[of n] nat_infinite
+using Field_natLeq Field_natLeq_on[of n]
       finite_ordLess_infinite[of "natLeq_on n" natLeq]
       natLeq_Well_order natLeq_on_Well_order[of n] by auto
 
@@ -1074,11 +1072,11 @@
 subsubsection {* Then as cardinals *}
 
 lemma ordIso_natLeq_infinite1:
-"|A| =o natLeq \<Longrightarrow> infinite A"
+"|A| =o natLeq \<Longrightarrow> \<not>finite A"
 using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
 
 lemma ordIso_natLeq_infinite2:
-"natLeq =o |A| \<Longrightarrow> infinite A"
+"natLeq =o |A| \<Longrightarrow> \<not>finite A"
 using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
 
 lemma ordLeq_natLeq_on_imp_finite:
@@ -1148,11 +1146,11 @@
 qed
 
 lemma card_of_Plus_ordLeq_infinite[simp]:
-assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
+assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
 shows "|A <+> B| \<le>o |C|"
 proof-
   let ?r = "cardSuc |C|"
-  have "Card_order ?r \<and> infinite (Field ?r)" using assms by simp
+  have "Card_order ?r \<and> \<not>finite (Field ?r)" using assms by simp
   moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
   ultimately have "|A <+> B| <o ?r"
   using card_of_Plus_ordLess_infinite_Field by blast
@@ -1160,7 +1158,7 @@
 qed
 
 lemma card_of_Un_ordLeq_infinite[simp]:
-assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
+assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
 shows "|A Un B| \<le>o |C|"
 using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
 ordLeq_transitive by metis
@@ -1185,12 +1183,12 @@
 using assms unfolding relChain_def by auto
 
 lemma card_of_infinite_diff_finite:
-assumes "infinite A" and "finite B"
+assumes "\<not>finite A" and "finite B"
 shows "|A - B| =o |A|"
 by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
 
 lemma infinite_card_of_diff_singl:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "|A - {a}| =o |A|"
 by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
 
@@ -1235,8 +1233,8 @@
 
 lemma infinite_Bpow:
 assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
-and A: "infinite A"
-shows "infinite (Bpow r A)"
+and A: "\<not>finite A"
+shows "\<not>finite (Bpow r A)"
 using ordLeq_card_Bpow[OF rc r]
 by (metis A card_of_ordLeq_infinite)
 
@@ -1350,7 +1348,7 @@
 qed
 
 lemma Bpow_ordLeq_Func_Field:
-assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "infinite A"
+assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "\<not>finite A"
 shows "|Bpow r A| \<le>o |Func (Field r) A|"
 proof-
   let ?F = "\<lambda> f. {x | x a. f a = x \<and> a \<in> Field r}"
@@ -1368,10 +1366,9 @@
   hence "|Bpow r A - {{}}| \<le>o |Func (Field r) A|"
   by (rule surj_imp_ordLeq)
   moreover
-  {have 2: "infinite (Bpow r A)" using infinite_Bpow[OF rc r A] .
+  {have 2: "\<not>finite (Bpow r A)" using infinite_Bpow[OF rc r A] .
    have "|Bpow r A| =o |Bpow r A - {{}}|"
-   using card_of_infinite_diff_finite
-   by (metis Pow_empty 2 finite_Pow_iff infinite_imp_nonempty ordIso_symmetric)
+     by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
   }
   ultimately show ?thesis by (metis ordIso_ordLeq_trans)
 qed
@@ -1408,8 +1405,8 @@
 qed
 
 lemma infinite_Func:
-assumes A: "infinite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
-shows "infinite (Func A B)"
+assumes A: "\<not>finite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
+shows "\<not>finite (Func A B)"
 using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
 
 end
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -487,8 +487,8 @@
 
 
 lemma infinite_Pow:
-assumes "infinite A"
-shows "infinite (Pow A)"
+assumes "\<not> finite A"
+shows "\<not> finite (Pow A)"
 proof-
   have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
   thus ?thesis by (metis assms finite_Pow_iff)
@@ -908,8 +908,8 @@
 
 
 lemma card_of_ordLeq_infinite:
-assumes "|A| \<le>o |B|" and "infinite A"
-shows "infinite B"
+assumes "|A| \<le>o |B|" and "\<not> finite A"
+shows "\<not> finite B"
 using assms card_of_ordLeq_finite by auto
 
 
@@ -938,15 +938,14 @@
 
 
 lemma infinite_iff_card_of_nat:
-"infinite A = ( |UNIV::nat set| \<le>o |A| )"
-by (auto simp add: infinite_iff_countable_subset card_of_ordLeq)
-
+"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
+unfolding infinite_iff_countable_subset card_of_ordLeq ..
 
 text{* The next two results correspond to the ZF fact that all infinite cardinals are
 limit ordinals: *}
 
 lemma Card_order_infinite_not_under:
-assumes CARD: "Card_order r" and INF: "infinite (Field r)"
+assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
 shows "\<not> (\<exists>a. Field r = rel.under r a)"
 proof(auto)
   have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
@@ -983,7 +982,7 @@
 
 
 lemma infinite_Card_order_limit:
-assumes r: "Card_order r" and "infinite (Field r)"
+assumes r: "Card_order r" and "\<not>finite (Field r)"
 and a: "a : Field r"
 shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
 proof-
@@ -1005,11 +1004,11 @@
 
 
 theorem Card_order_Times_same_infinite:
-assumes CO: "Card_order r" and INF: "infinite(Field r)"
+assumes CO: "Card_order r" and INF: "\<not>finite(Field r)"
 shows "|Field r \<times> Field r| \<le>o r"
 proof-
   obtain phi where phi_def:
-  "phi = (\<lambda>r::'a rel. Card_order r \<and> infinite(Field r) \<and>
+  "phi = (\<lambda>r::'a rel. Card_order r \<and> \<not>finite(Field r) \<and>
                       \<not> |Field r \<times> Field r| \<le>o r )" by blast
   have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
   unfolding phi_def card_order_on_def by auto
@@ -1060,15 +1059,15 @@
     }
     ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
     (*  *)
-    have "infinite (Field r)" using 1 unfolding phi_def by simp
-    hence "infinite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
-    hence "infinite A1" using 9 infinite_super finite_cartesian_product by blast
+    have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
+    hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
+    hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis
     moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
     using card_of_Card_order[of A1] card_of_Well_order[of A1]
     by (simp add: Field_card_of)
     moreover have "\<not> r \<le>o | A1 |"
     using temp4 11 3 using not_ordLeq_iff_ordLess by blast
-    ultimately have "infinite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
+    ultimately have "\<not> finite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
     by (simp add: card_of_card_order_on)
     hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
     using 2 unfolding phi_def by blast
@@ -1081,7 +1080,7 @@
 
 
 corollary card_of_Times_same_infinite:
-assumes "infinite A"
+assumes "\<not>finite A"
 shows "|A \<times> A| =o |A|"
 proof-
   let ?r = "|A|"
@@ -1094,7 +1093,7 @@
 
 
 lemma card_of_Times_infinite:
-assumes INF: "infinite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
 shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
 proof-
   have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
@@ -1111,7 +1110,7 @@
 
 
 corollary Card_order_Times_infinite:
-assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
+assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
         NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
 shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
 proof-
@@ -1125,7 +1124,7 @@
 
 
 lemma card_of_Sigma_ordLeq_infinite:
-assumes INF: "infinite B" and
+assumes INF: "\<not>finite B" and
         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
 shows "|SIGMA i : I. A i| \<le>o |B|"
 proof(cases "I = {}", simp add: card_of_empty)
@@ -1139,7 +1138,7 @@
 
 
 lemma card_of_Sigma_ordLeq_infinite_Field:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
 shows "|SIGMA i : I. A i| \<le>o r"
 proof-
@@ -1155,21 +1154,21 @@
 
 
 lemma card_of_Times_ordLeq_infinite_Field:
-"\<lbrakk>infinite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
+"\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
  \<Longrightarrow> |A <*> B| \<le>o r"
 by(simp add: card_of_Sigma_ordLeq_infinite_Field)
 
 
 lemma card_of_Times_infinite_simps:
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
 by (auto simp add: card_of_Times_infinite ordIso_symmetric)
 
 
 lemma card_of_UNION_ordLeq_infinite:
-assumes INF: "infinite B" and
+assumes INF: "\<not>finite B" and
         LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
 shows "|\<Union> i \<in> I. A i| \<le>o |B|"
 proof(cases "I = {}", simp add: card_of_empty)
@@ -1183,7 +1182,7 @@
 
 
 corollary card_of_UNION_ordLeq_infinite_Field:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
         LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
 shows "|\<Union> i \<in> I. A i| \<le>o r"
 proof-
@@ -1199,7 +1198,7 @@
 
 
 lemma card_of_Plus_infinite1:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
 shows "|A <+> B| =o |A|"
 proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
   let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b"  let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
@@ -1210,7 +1209,7 @@
     assume Case1: "B = {b1}"
     have 2: "bij_betw ?Inl A ((?Inl ` A))"
     unfolding bij_betw_def inj_on_def by auto
-    hence 3: "infinite (?Inl ` A)"
+    hence 3: "\<not>finite (?Inl ` A)"
     using INF bij_betw_finite[of ?Inl A] by blast
     let ?A' = "?Inl ` A \<union> {?Inr b1}"
     obtain g where "bij_betw g (?Inl ` A) ?A'"
@@ -1238,20 +1237,20 @@
 
 
 lemma card_of_Plus_infinite2:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
 shows "|B <+> A| =o |A|"
 using assms card_of_Plus_commute card_of_Plus_infinite1
 ordIso_equivalence by blast
 
 
 lemma card_of_Plus_infinite:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
 shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
 using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
 
 
 corollary Card_order_Plus_infinite:
-assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
+assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
         LEQ: "p \<le>o r"
 shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
 proof-
@@ -1281,8 +1280,8 @@
 where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
 
 lemma infinite_cartesian_product:
-assumes "infinite A" "infinite B"
-shows "infinite (A \<times> B)"
+assumes "\<not>finite A" "\<not>finite B"
+shows "\<not>finite (A \<times> B)"
 proof
   assume "finite (A \<times> B)"
   from assms(1) have "A \<noteq> {}" by auto
@@ -1421,7 +1420,7 @@
       Card_order_iff_Restr_underS Restr_natLeq2, simp add:  Field_natLeq)
   fix n have "finite(Field (natLeq_on n))"
   unfolding Field_natLeq_on by auto
-  moreover have "infinite(UNIV::nat set)" by auto
+  moreover have "\<not>finite(UNIV::nat set)" by auto
   ultimately show "natLeq_on n <o |UNIV::nat set|"
   using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
         Field_card_of[of "UNIV::nat set"]
@@ -1441,7 +1440,7 @@
 
 
 corollary infinite_iff_natLeq_ordLeq:
-"infinite A = ( natLeq \<le>o |A| )"
+"\<not>finite A = ( natLeq \<le>o |A| )"
 using infinite_iff_card_of_nat[of A] card_of_nat
       ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
 
@@ -1769,7 +1768,7 @@
 
 
 lemma card_of_Plus_ordLess_infinite:
-assumes INF: "infinite C" and
+assumes INF: "\<not>finite C" and
         LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
 shows "|A <+> B| <o |C|"
 proof(cases "A = {} \<or> B = {}")
@@ -1784,17 +1783,17 @@
 next
   assume Case2: "\<not>(A = {} \<or> B = {})"
   {assume *: "|C| \<le>o |A <+> B|"
-   hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast
-   hence 1: "infinite A \<or> infinite B" using finite_Plus by blast
+   hence "\<not>finite (A <+> B)" using INF card_of_ordLeq_finite by blast
+   hence 1: "\<not>finite A \<or> \<not>finite B" using finite_Plus by blast
    {assume Case21: "|A| \<le>o |B|"
-    hence "infinite B" using 1 card_of_ordLeq_finite by blast
+    hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
     hence "|A <+> B| =o |B|" using Case2 Case21
     by (auto simp add: card_of_Plus_infinite)
     hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
    }
    moreover
    {assume Case22: "|B| \<le>o |A|"
-    hence "infinite A" using 1 card_of_ordLeq_finite by blast
+    hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
     hence "|A <+> B| =o |A|" using Case2 Case22
     by (auto simp add: card_of_Plus_infinite)
     hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
@@ -1808,7 +1807,7 @@
 
 
 lemma card_of_Plus_ordLess_infinite_Field:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
         LESS1: "|A| <o r" and LESS2: "|B| <o r"
 shows "|A <+> B| <o r"
 proof-
@@ -1824,12 +1823,12 @@
 
 
 lemma card_of_Plus_ordLeq_infinite_Field:
-assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
+assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
 and c: "Card_order r"
 shows "|A <+> B| \<le>o r"
 proof-
   let ?r' = "cardSuc r"
-  have "Card_order ?r' \<and> infinite (Field ?r')" using assms
+  have "Card_order ?r' \<and> \<not>finite (Field ?r')" using assms
   by (simp add: cardSuc_Card_order cardSuc_finite)
   moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
   by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
@@ -1841,7 +1840,7 @@
 
 
 lemma card_of_Un_ordLeq_infinite_Field:
-assumes C: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
+assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
 and "Card_order r"
 shows "|A Un B| \<le>o r"
 using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
@@ -1904,7 +1903,7 @@
 
 
 lemma infinite_cardSuc_regular:
-assumes r_inf: "infinite (Field r)" and r_card: "Card_order r"
+assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"
 shows "regular (cardSuc r)"
 proof-
   let ?r' = "cardSuc r"
@@ -1955,7 +1954,7 @@
 qed
 
 lemma cardSuc_UNION:
-assumes r: "Card_order r" and "infinite (Field r)"
+assumes r: "Card_order r" and "\<not>finite (Field r)"
 and As: "relChain (cardSuc r) As"
 and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
 and cardB: "|B| <=o r"
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -861,7 +861,7 @@
 
 lemma finite_ordLess_infinite:
 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
-        FIN: "finite(Field r)" and INF: "infinite(Field r')"
+        FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
 shows "r <o r'"
 proof-
   {assume "r' \<le>o r"
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Cardinals/Fun_More_FP.thy
--- a/src/HOL/Cardinals/Fun_More_FP.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More_FP.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -8,12 +8,12 @@
 header {* More on Injections, Bijections and Inverses (FP) *}
 
 theory Fun_More_FP
-imports "~~/src/HOL/Library/Infinite_Set"
+imports Main
 begin
 
 
 text {* This section proves more facts (additional to those in @{text "Fun.thy"},
-@{text "Hilbert_Choice.thy"}, @{text "Finite_Set.thy"} and @{text "Infinite_Set.thy"}),
+@{text "Hilbert_Choice.thy"}, and @{text "Finite_Set.thy"}),
 mainly concerning injections, bijections, inverses and (numeric) cardinals of
 finite sets. *}
 
@@ -97,18 +97,19 @@
 (*3*)lemma inj_on_finite:
 assumes "inj_on f A" "f ` A \<le> B" "finite B"
 shows "finite A"
-using assms infinite_super by (fast dest: finite_imageD)
+using assms by (metis finite_imageD finite_subset)
 
 
 (*3*)lemma infinite_imp_bij_betw:
-assumes INF: "infinite A"
+assumes INF: "\<not> finite A"
 shows "\<exists>h. bij_betw h A (A - {a})"
 proof(cases "a \<in> A")
   assume Case1: "a \<notin> A"  hence "A - {a} = A" by blast
   thus ?thesis using bij_betw_id[of A] by auto
 next
   assume Case2: "a \<in> A"
-  have "infinite (A - {a})" using INF infinite_remove by auto
+find_theorems "\<not> finite _"
+  have "\<not> finite (A - {a})" using INF by auto
   with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
   where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
   obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
@@ -179,7 +180,7 @@
 
 
 (*3*)lemma infinite_imp_bij_betw2:
-assumes INF: "infinite A"
+assumes INF: "\<not> finite A"
 shows "\<exists>h. bij_betw h A (A \<union> {a})"
 proof(cases "a \<in> A")
   assume Case1: "a \<in> A"  hence "A \<union> {a} = A" by blast
@@ -187,7 +188,7 @@
 next
   let ?A' = "A \<union> {a}"
   assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
-  moreover have "infinite ?A'" using INF by auto
+  moreover have "\<not> finite ?A'" using INF by auto
   ultimately obtain f where "bij_betw f ?A' A"
   using infinite_imp_bij_betw[of ?A' a] by auto
   hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Fun.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -308,6 +308,16 @@
   show ?thesis ..
 qed
 
+lemma linorder_injI:
+  assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
+  shows "inj f"
+  -- {* Courtesy of Stephan Merz *}
+proof (rule inj_onI)
+  fix x y
+  assume f_eq: "f x = f y"
+  show "x = y" by (rule linorder_cases) (auto dest: hyp simp: f_eq)
+qed
+
 lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
   by auto
 
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -272,6 +272,41 @@
   ultimately show "finite (UNIV :: 'a set)" by simp
 qed
 
+text {*
+  Every infinite set contains a countable subset. More precisely we
+  show that a set @{text S} is infinite if and only if there exists an
+  injective function from the naturals into @{text S}.
+
+  The ``only if'' direction is harder because it requires the
+  construction of a sequence of pairwise different elements of an
+  infinite set @{text S}. The idea is to construct a sequence of
+  non-empty and infinite subsets of @{text S} obtained by successively
+  removing elements of @{text S}.
+*}
+
+lemma infinite_countable_subset:
+  assumes inf: "\<not> finite (S::'a set)"
+  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
+  -- {* Courtesy of Stephan Merz *}
+proof -
+  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
+  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
+  { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
+  moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
+  ultimately have "range pick \<subseteq> S" by auto
+  moreover
+  { fix n m                 
+    have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
+    hence "pick n \<noteq> pick (n + Suc m)" by (metis *)
+  }
+  then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
+  ultimately show ?thesis by blast
+qed
+
+lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
+  -- {* Courtesy of Stephan Merz *}
+  by (metis finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset)
+
 lemma image_inv_into_cancel:
   assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
   shows "f `((inv_into A f)`B') = B'"
diff -r 627f369d505e -r 9387251b6a46 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Nov 25 10:14:29 2013 +0100
@@ -200,12 +200,6 @@
 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   by simp
 
-text {*
-  Every infinite set contains a countable subset. More precisely we
-  show that a set @{text S} is infinite if and only if there exists an
-  injective function from the naturals into @{text S}.
-*}
-
 lemma range_inj_infinite:
   "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
 proof
@@ -215,6 +209,7 @@
   then show False by simp
 qed
 
+(* duplicates Int.infinite_UNIV_int *)
 lemma int_infinite [simp]: "infinite (UNIV::int set)"
 proof -
   from inj_int have "infinite (range int)"
@@ -226,108 +221,6 @@
 qed
 
 text {*
-  The ``only if'' direction is harder because it requires the
-  construction of a sequence of pairwise different elements of an
-  infinite set @{text S}. The idea is to construct a sequence of
-  non-empty and infinite subsets of @{text S} obtained by successively
-  removing elements of @{text S}.
-*}
-
-lemma linorder_injI:
-  assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
-  shows "inj f"
-proof (rule inj_onI)
-  fix x y
-  assume f_eq: "f x = f y"
-  show "x = y"
-  proof (rule linorder_cases)
-    assume "x < y"
-    with hyp have "f x \<noteq> f y" by blast
-    with f_eq show ?thesis by simp
-  next
-    assume "x = y"
-    then show ?thesis .
-  next
-    assume "y < x"
-    with hyp have "f y \<noteq> f x" by blast
-    with f_eq show ?thesis by simp
-  qed
-qed
-
-lemma infinite_countable_subset:
-  assumes inf: "infinite (S::'a set)"
-  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
-proof -
-  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
-  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
-  have Sseq_inf: "\<And>n. infinite (Sseq n)"
-  proof -
-    fix n
-    show "infinite (Sseq n)"
-    proof (induct n)
-      from inf show "infinite (Sseq 0)"
-        by (simp add: Sseq_def)
-    next
-      fix n
-      assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
-        by (simp add: Sseq_def infinite_remove)
-    qed
-  qed
-  have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
-  proof -
-    fix n
-    show "Sseq n \<subseteq> S"
-      by (induct n) (auto simp add: Sseq_def)
-  qed
-  have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
-  proof -
-    fix n
-    show "pick n \<in> Sseq n"
-      unfolding pick_def
-    proof (rule someI_ex)
-      from Sseq_inf have "infinite (Sseq n)" .
-      then have "Sseq n \<noteq> {}" by auto
-      then show "\<exists>x. x \<in> Sseq n" by auto
-    qed
-  qed
-  with Sseq_S have rng: "range pick \<subseteq> S"
-    by auto
-  have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
-  proof -
-    fix n m
-    show "pick n \<notin> Sseq (n + Suc m)"
-      by (induct m) (auto simp add: Sseq_def pick_def)
-  qed
-  have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
-  proof -
-    fix n m
-    from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
-    moreover from pick_Sseq_gt
-    have "pick n \<notin> Sseq (n + Suc m)" .
-    ultimately show "pick n \<noteq> pick (n + Suc m)"
-      by auto
-  qed
-  have inj: "inj pick"
-  proof (rule linorder_injI)
-    fix i j :: nat
-    assume "i < j"
-    show "pick i \<noteq> pick j"
-    proof
-      assume eq: "pick i = pick j"
-      from `i < j` obtain k where "j = i + Suc k"
-        by (auto simp add: less_iff_Suc_add)
-      with pick_pick have "pick i \<noteq> pick j" by simp
-      with eq show False by simp
-    qed
-  qed
-  from rng inj show ?thesis by auto
-qed
-
-lemma infinite_iff_countable_subset:
-    "infinite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
-  by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
-
-text {*
   For any function with infinite domain and finite range there is some
   element that is the image of infinitely many domain elements.  In
   particular, any infinite sequence of elements from a finite set