diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -8,71 +8,7 @@
 imports Main
 begin
 
-subsection "Infinite Sets"
-
-text \<open>
-  Some elementary facts about infinite sets, mostly by Stephan Merz.
-  Beware! Because "infinite" merely abbreviates a negation, these
-  lemmas may not work well with \<open>blast\<close>.
-\<close>
-
-abbreviation infinite :: "'a set \<Rightarrow> bool"
-  where "infinite S \<equiv> \<not> finite S"
-
-text \<open>
-  Infinite sets are non-empty, and if we remove some elements from an
-  infinite set, the result is still infinite.
-\<close>
-
-lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
-  by auto
-
-lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})"
-  by simp
-
-lemma Diff_infinite_finite:
-  assumes T: "finite T" and S: "infinite S"
-  shows "infinite (S - T)"
-  using T
-proof induct
-  from S
-  show "infinite (S - {})" by auto
-next
-  fix T x
-  assume ih: "infinite (S - T)"
-  have "S - (insert x T) = (S - T) - {x}"
-    by (rule Diff_insert)
-  with ih
-  show "infinite (S - (insert x T))"
-    by (simp add: infinite_remove)
-qed
-
-lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
-  by simp
-
-lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
-lemma infinite_super:
-  assumes T: "S \<subseteq> T" and S: "infinite S"
-  shows "infinite T"
-proof
-  assume "finite T"
-  with T have "finite S" by (simp add: finite_subset)
-  with S show False by simp
-qed
-
-lemma infinite_coinduct [consumes 1, case_names infinite]:
-  assumes "X A"
-  and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
-  shows "infinite A"
-proof
-  assume "finite A"
-  then show False using \<open>X A\<close>
-    by(induction rule: finite_psubset_induct)(meson Diff_subset card_Diff1_less card_psubset finite_Diff step)
-qed    
-
-text \<open>As a concrete example, we prove that the set of natural numbers is infinite.\<close>
+text \<open>The set of natural numbers is infinite.\<close>
 
 lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
   using frequently_cofinite[of "\<lambda>x. x \<in> S"]
@@ -99,8 +35,9 @@
 \<close>
 
 lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
-  by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
-            not_less_iff_gr_or_eq sup.bounded_iff)
+apply (clarsimp simp add: finite_nat_set_iff_bounded)
+apply (drule_tac x="Suc (max m k)" in spec)
+using less_Suc_eq by fastforce
 
 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   by simp
@@ -114,45 +51,6 @@
   then show False by simp
 qed
 
-text \<open>
-  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
-  contains some element that occurs infinitely often.
-\<close>
-
-lemma inf_img_fin_dom':
-  assumes img: "finite (f ` A)" and dom: "infinite A"
-  shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
-proof (rule ccontr)
-  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
-  moreover
-  assume "\<not> ?thesis"
-  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
-  ultimately have "finite A" by(rule finite_subset)
-  with dom show False by contradiction
-qed
-
-lemma inf_img_fin_domE':
-  assumes "finite (f ` A)" and "infinite A"
-  obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
-  using assms by (blast dest: inf_img_fin_dom')
-
-lemma inf_img_fin_dom:
-  assumes img: "finite (f`A)" and dom: "infinite A"
-  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
-using inf_img_fin_dom'[OF assms] by auto
-
-lemma inf_img_fin_domE:
-  assumes "finite (f`A)" and "infinite A"
-  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
-  using assms by (blast dest: inf_img_fin_dom)
-
-proposition finite_image_absD:
-    fixes S :: "'a::linordered_ring set"
-    shows "finite (abs ` S) \<Longrightarrow> finite S"
-  by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
-
 text \<open>The set of integers is also infinite.\<close>
 
 lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
@@ -196,10 +94,10 @@
   by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
 
 lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
-  by (auto intro: eventually_rev_mp eventually_elim1)
+  by (auto intro: eventually_rev_mp eventually_mono)
 
 lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
-  by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
+  by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono)
 
 text \<open>Properties of quantifiers with injective functions.\<close>
 
@@ -272,7 +170,7 @@
 lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
 lemma INFM_mono: "\<exists>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<exists>\<^sub>\<infinity>x. Q x" by (fact frequently_elim1)
-lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_elim1)
+lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_mono)
 lemma INFM_disj_distrib: "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)" by (fact frequently_disj_iff)
 lemma MOST_rev_mp: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_rev_mp)
 lemma MOST_conj_distrib: "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)" by (fact eventually_conj_iff)
@@ -331,7 +229,7 @@
 lemma le_enumerate:
   assumes S: "infinite S"
   shows "n \<le> enumerate S n"
-  using S 
+  using S
 proof (induct n)
   case 0
   then show ?case by simp