# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1449682522 0
# Node ID 3c5040d5694a35c1980b31bf3d263b7042566b29
# Parent  81d34cf268d8e599ebc99e6b3ac9ac5f3af891d0
sorted out eventually_mono

diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Deriv.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -218,7 +218,7 @@
 
 lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \<Longrightarrow> (f ---> y) (at x within s) \<longleftrightarrow> (f ---> y) (inf (nhds x) (principal s))"
   unfolding tendsto_def eventually_inf_principal eventually_at_filter
-  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
 
 lemma has_derivative_in_compose:
   assumes f: "(f has_derivative f') (at x within s)"
@@ -903,7 +903,7 @@
   moreover from * have "f x = g x" by (auto simp: eventually_nhds)
   moreover assume "x = y" "u = v"
   ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
-    by (auto simp: eventually_at_filter elim: eventually_elim1)
+    by (auto simp: eventually_at_filter elim: eventually_mono)
 qed simp_all
 
 lemma DERIV_shift:
@@ -1679,12 +1679,12 @@
   then have "(\<zeta> ---> 0) (at_right 0)"
     by (rule tendsto_norm_zero_cancel)
   with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
-    by (auto elim!: eventually_elim1 simp: filterlim_at)
+    by (auto elim!: eventually_mono simp: filterlim_at)
   from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
     by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
   ultimately have "((\<lambda>t. f t / g t) ---> x) (at_right 0)" (is ?P)
     by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
-       (auto elim: eventually_elim1)
+       (auto elim: eventually_mono)
   also have "?P \<longleftrightarrow> ?thesis"
     by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter)
   finally show ?thesis .
@@ -1753,7 +1753,7 @@
 
   moreover
   have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"
-    using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top_dense)
+    using g_0 by (auto elim: eventually_mono simp: filterlim_at_top_dense)
 
   moreover
   have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"
@@ -1765,7 +1765,7 @@
     by (simp add: inverse_eq_divide)
   from this[unfolded tendsto_iff, rule_format, of 1]
   have "eventually (\<lambda>x. norm (1 - g a / g x) < 2) (at_right 0)"
-    by (auto elim!: eventually_elim1 simp: dist_real_def)
+    by (auto elim!: eventually_mono simp: dist_real_def)
 
   moreover
   from inv_g have "((\<lambda>t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)"
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Filter.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -67,11 +67,6 @@
   by (auto intro: always_eventually)
 
 lemma eventually_mono:
-  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
-  unfolding eventually_def
-  by (rule is_filter.mono [OF is_filter_Rep_filter])
-
-lemma eventually_mono':
   "\<lbrakk>eventually P F; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> eventually Q F"
   unfolding eventually_def
   by (blast intro: is_filter.mono [OF is_filter_Rep_filter])
@@ -91,7 +86,7 @@
   have "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
     using assms by (rule eventually_conj)
   then show ?thesis
-    by (blast intro: eventually_mono')
+    by (blast intro: eventually_mono)
 qed
 
 lemma eventually_rev_mp:
@@ -104,12 +99,6 @@
   "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
   by (auto intro: eventually_conj elim: eventually_rev_mp)
 
-lemma eventually_elim1:
-  assumes "eventually (\<lambda>i. P i) F"
-  assumes "\<And>i. P i \<Longrightarrow> Q i"
-  shows "eventually (\<lambda>i. Q i) F"
-  using assms by (auto elim!: eventually_rev_mp)
-
 lemma eventually_elim2:
   assumes "eventually (\<lambda>i. P i) F"
   assumes "eventually (\<lambda>i. Q i) F"
@@ -135,10 +124,10 @@
 proof
   assume "\<forall>\<^sub>Fx in F. \<exists>y. P x y"
   then have "\<forall>\<^sub>Fx in F. P x (SOME y. P x y)"
-    by (auto intro: someI_ex eventually_elim1)
+    by (auto intro: someI_ex eventually_mono)
   then show "\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x)"
     by auto
-qed (auto intro: eventually_elim1)
+qed (auto intro: eventually_mono)
 
 lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   by (auto intro: eventually_mp)
@@ -152,7 +141,7 @@
 proof -
   from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
       and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
-    by (auto elim: eventually_elim1)
+    by (auto elim: eventually_mono)
   then show ?thesis by (auto elim: eventually_elim2)
 qed
 
@@ -346,7 +335,7 @@
     unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
   { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
     unfolding le_filter_def eventually_inf
-    by (auto intro: eventually_mono' [OF eventually_conj]) }
+    by (auto intro: eventually_mono [OF eventually_conj]) }
   { show "F \<le> sup F F'" and "F' \<le> sup F F'"
     unfolding le_filter_def eventually_sup by simp_all }
   { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
@@ -434,7 +423,7 @@
       assume "?F P" then guess X ..
       moreover assume "\<forall>x. P x \<longrightarrow> Q x"
       ultimately show "?F Q"
-        by (intro exI[of _ X]) (auto elim: eventually_elim1)
+        by (intro exI[of _ X]) (auto elim: eventually_mono)
     qed }
   note eventually_F = this
 
@@ -553,7 +542,7 @@
   by (rule eventually_Abs_filter, rule is_filter.intro) auto
 
 lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
-  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
+  unfolding eventually_inf eventually_principal by (auto elim: eventually_mono)
 
 lemma principal_UNIV[simp]: "principal UNIV = top"
   by (auto simp: filter_eq_iff eventually_principal)
@@ -571,7 +560,7 @@
   unfolding le_filter_def eventually_principal
   apply safe
   apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
-  apply (auto elim: eventually_elim1)
+  apply (auto elim: eventually_mono)
   done
 
 lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
@@ -877,7 +866,7 @@
 lemma filterlim_at_top:
   fixes f :: "'a \<Rightarrow> ('b::linorder)"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
-  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
+  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_mono)
 
 lemma filterlim_at_top_mono:
   "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
@@ -887,7 +876,7 @@
 lemma filterlim_at_top_dense:
   fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
   shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
-  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
+  by (metis eventually_mono[of _ F] eventually_gt_at_top order_less_imp_le
             filterlim_at_top[of f F] filterlim_iff[of f at_top F])
 
 lemma filterlim_at_top_ge:
@@ -924,7 +913,7 @@
 lemma filterlim_at_bot:
   fixes f :: "'a \<Rightarrow> ('b::linorder)"
   shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
-  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
+  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_mono)
 
 lemma filterlim_at_bot_dense:
   fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
@@ -935,12 +924,12 @@
   assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
   hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
   thus "eventually (\<lambda>x. f x < Z) F"
-    apply (rule eventually_mono')
+    apply (rule eventually_mono)
     using 1 by auto
   next
     fix Z :: 'b
     show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
-      by (drule spec [of _ Z], erule eventually_mono', auto simp add: less_imp_le)
+      by (drule spec [of _ Z], erule eventually_mono, auto simp add: less_imp_le)
 qed
 
 lemma filterlim_at_bot_le:
@@ -950,7 +939,7 @@
 proof safe
   fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
   with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
-    by (auto elim!: eventually_elim1)
+    by (auto elim!: eventually_mono)
 qed simp
 
 lemma filterlim_at_bot_lt:
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -1787,4 +1787,118 @@
 
 hide_const (open) Finite_Set.fold
 
+
+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
+
+proposition 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>
+  proof (induction rule: finite_psubset_induct)
+    case (psubset A)
+    then obtain x where "x \<in> A" "X (A - {x}) \<or> infinite (A - {x})"
+      using local.step psubset.prems by blast
+    then have "X (A - {x})"
+      using psubset.hyps by blast
+    show False
+      apply (rule psubset.IH [where B = "A - {x}"])
+      using \<open>x \<in> A\<close> apply blast
+      by (simp add: \<open>X (A - {x})\<close>)
+  qed
+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)
+
 end
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -2444,7 +2444,7 @@
   then have S: "open S" "ereal x \<in> ereal ` S"
     by (simp_all add: inj_image_mem_iff)
   show "eventually (\<lambda>x. real_of_ereal (f x) \<in> S) net"
-    by (auto intro: eventually_mono' [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]])
+    by (auto intro: eventually_mono [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]])
 qed
 
 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
@@ -2456,7 +2456,7 @@
     fix l :: ereal
     assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
     from this[THEN spec, of "real_of_ereal l"] have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
-      by (cases l) (auto elim: eventually_elim1)
+      by (cases l) (auto elim: eventually_mono)
   }
   then show ?thesis
     by (auto simp: order_tendsto_iff)
@@ -2477,7 +2477,7 @@
   then have "eventually (\<lambda>z. f z \<in> {..< B}) F"
     by auto
   ultimately show "eventually (\<lambda>z. f z \<in> S) F"
-    by (auto elim!: eventually_elim1)
+    by (auto elim!: eventually_mono)
 next
   fix x
   assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
@@ -2571,7 +2571,7 @@
     by auto
   from tendsto[THEN topological_tendstoD, OF this]
   show "eventually (\<lambda>x. ereal (real_of_ereal (f x)) \<in> S) net"
-    by (elim eventually_elim1) (auto simp: ereal_real)
+    by (elim eventually_mono) (auto simp: ereal_real)
 qed
 
 lemma ereal_mult_cancel_left:
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
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -100,7 +100,7 @@
 lemma Liminf_eq:
   assumes "eventually (\<lambda>x. f x = g x) F"
   shows "Liminf F f = Liminf F g"
-  by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
 
 lemma Limsup_mono:
   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
@@ -116,7 +116,7 @@
 lemma Limsup_eq:
   assumes "eventually (\<lambda>x. f x = g x) net"
   shows "Limsup net f = Limsup net g"
-  by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
+  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
 
 lemma Liminf_le_Limsup:
   assumes ntriv: "\<not> trivial_limit F"
@@ -167,7 +167,7 @@
 proof -
   have "eventually (\<lambda>x. y < X x) F"
     if "eventually P F" "y < INFIMUM (Collect P) X" for y P
-    using that by (auto elim!: eventually_elim1 dest: less_INF_D)
+    using that by (auto elim!: eventually_mono dest: less_INF_D)
   moreover
   have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
     if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
@@ -218,7 +218,7 @@
       then have "eventually (\<lambda>x. y < f x) F"
         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
       then have "eventually (\<lambda>x. f0 \<le> f x) F"
-        using discrete by (auto elim!: eventually_elim1)
+        using discrete by (auto elim!: eventually_mono)
       then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
         by (rule upper)
       moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
@@ -257,7 +257,7 @@
       then have "eventually (\<lambda>x. f x < y) F"
         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
       then have "eventually (\<lambda>x. f x \<le> f0) F"
-        using False by (auto elim!: eventually_elim1 simp: not_less)
+        using False by (auto elim!: eventually_mono simp: not_less)
       then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
         by (rule lower)
       moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
@@ -278,14 +278,14 @@
   then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
     unfolding Limsup_def INF_less_iff by auto
   then show "eventually (\<lambda>x. f x < a) F"
-    by (auto elim!: eventually_elim1 dest: SUP_lessD)
+    by (auto elim!: eventually_mono dest: SUP_lessD)
 next
   fix a assume "a < f0"
   with assms have "a < Liminf F f" by simp
   then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
     unfolding Liminf_def less_SUP_iff by auto
   then show "eventually (\<lambda>x. a < f x) F"
-    by (auto elim!: eventually_elim1 dest: less_INF_D)
+    by (auto elim!: eventually_mono dest: less_INF_D)
 qed
 
 lemma tendsto_iff_Liminf_eq_Limsup:
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Limits.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -83,7 +83,7 @@
   show "0 < max K 1" by simp
 next
   show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F"
-    using K by (rule eventually_elim1, simp)
+    using K by (rule eventually_mono, simp)
 qed
 
 lemma BfunE:
@@ -897,10 +897,10 @@
   with f have "eventually (\<lambda>x. dist (f x) a < norm a) F"
     by (rule tendstoD)
   then have "eventually (\<lambda>x. f x \<noteq> 0) F"
-    unfolding dist_norm by (auto elim!: eventually_elim1)
+    unfolding dist_norm by (auto elim!: eventually_mono)
   with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
     - (inverse (f x) * (f x - a) * inverse a)) F"
-    by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
+    by (auto elim!: eventually_mono simp: inverse_diff_inverse)
   moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
     by (intro Zfun_minus Zfun_mult_left
       bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
@@ -1149,7 +1149,7 @@
   then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
     by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
   then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
-    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
+    by (auto elim!: eventually_mono simp: inverse_eq_divide field_simps)
 qed
 
 lemma tendsto_inverse_0:
@@ -1202,7 +1202,7 @@
 lemma filterlim_inverse_at_top:
   "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
   by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
-     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
+     (simp add: filterlim_def eventually_filtermap eventually_mono at_within_def le_principal)
 
 lemma filterlim_inverse_at_bot_neg:
   "LIM x (at_left (0::real)). inverse x :> at_bot"
@@ -1335,7 +1335,7 @@
 proof safe
   fix Z :: real assume "0 < Z"
   from f \<open>0 < c\<close> have "eventually (\<lambda>x. c / 2 < f x) F"
-    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1
+    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono
              simp: dist_real_def abs_real_def split: split_if_asm)
   moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F"
     unfolding filterlim_at_top by auto
@@ -1409,7 +1409,7 @@
 proof safe
   fix Z :: real assume "0 < Z"
   from f have "eventually (\<lambda>x. c - 1 < f x) F"
-    by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def)
+    by (auto dest!: tendstoD[where e=1] elim!: eventually_mono simp: dist_real_def)
   moreover from g have "eventually (\<lambda>x. Z - (c - 1) \<le> g x) F"
     unfolding filterlim_at_top by auto
   ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F"
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -886,7 +886,7 @@
       finally have "dist (f (r n)) l < e" by simp
     }
     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
-      by (rule eventually_elim1)
+      by (rule eventually_mono)
   }
   hence "((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
   with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -3336,7 +3336,6 @@
 
 subsection\<open>Winding Numbers\<close>
 
-text\<open>The result is an integer, but it doesn't have type @{typ int}!\<close>
 definition winding_number:: "[real \<Rightarrow> complex, complex] \<Rightarrow> complex" where
   "winding_number \<gamma> z \<equiv>
     @n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -290,13 +290,13 @@
   unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto)
 
 lemma le_nhds: "F \<le> nhds a \<longleftrightarrow> (\<forall>S. open S \<and> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F)"
-  unfolding le_filter_def eventually_nhds by (fast elim: eventually_elim1)
+  unfolding le_filter_def eventually_nhds by (fast elim: eventually_mono)
 
 lemma le_nhds_metric: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a < e) F)"
-  unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_elim1)
+  unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_mono)
 
 lemma le_nhds_metric_le: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a \<le> e) F)"
-  unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_elim1)
+  unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_mono)
 
 text \<open>Several results are easier using a "multiplied-out" variant.
 (I got this idea from Dieudonne's proof of the chain rule).\<close>
@@ -2016,15 +2016,15 @@
         case True
         have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
           using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> s\<close>
-          by (fast elim: eventually_elim1)
+          by (fast elim: eventually_mono)
         then show ?thesis
-          using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_elim1)
+          using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_mono)
       next
         case False
         with \<open>0 < e\<close> have "0 < e / norm u" by simp
         then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
           using assms(3)[folded eventually_sequentially] and \<open>x \<in> s\<close>
-          by (fast elim: eventually_elim1)
+          by (fast elim: eventually_mono)
         then show ?thesis
           using \<open>u \<noteq> 0\<close> by simp
       qed
@@ -2250,7 +2250,7 @@
   also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
                 ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
     using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
-    by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff)
+    by (intro DERIV_cong_ev) (auto elim!: eventually_mono simp: sums_iff)
   finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
 qed
 
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -431,7 +431,7 @@
       by (simp add: mono_set)
   }
   with P show "eventually (\<lambda>x. f x \<in> S) net"
-    by (auto elim: eventually_elim1)
+    by (auto elim: eventually_mono)
 next
   fix y l
   assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
@@ -470,7 +470,7 @@
     have "f x \<in> S"
       by (simp add: inj_image_mem_iff) }
   with P show "eventually (\<lambda>x. f x \<in> S) net"
-    by (auto elim: eventually_elim1)
+    by (auto elim: eventually_mono)
 next
   fix y l
   assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -224,7 +224,7 @@
   hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net"
     by (rule eventually_all_finite)
   thus "eventually (\<lambda>x. f x \<in> S) net"
-    by (rule eventually_elim1, simp add: S)
+    by (rule eventually_mono, simp add: S)
 qed
 
 lemma tendsto_vec_lambda [tendsto_intros]:
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -73,8 +73,6 @@
   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
   by (metis cInf_eq_Min Min_le_iff)
 
-(*declare not_less[simp] not_le[simp]*)
-
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -2310,7 +2310,7 @@
   by (auto simp add: tendsto_iff eventually_at_infinity)
 
 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
-  by (rule topological_tendstoI, auto elim: eventually_mono')
+  by (rule topological_tendstoI, auto elim: eventually_mono)
 
 text\<open>The expected monotonicity property.\<close>
 
@@ -2348,7 +2348,7 @@
   next
     assume "?rhs"
     then show "?lhs"
-      by (auto elim: eventually_elim1 simp: eventually_at_filter)
+      by (auto elim: eventually_mono simp: eventually_at_filter)
   }
 qed
 
@@ -2429,7 +2429,7 @@
     assume "open S" "x \<in> S"
     from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
     show "eventually (\<lambda>x. f x \<in> S) sequentially"
-      by (auto elim!: eventually_elim1)
+      by (auto elim!: eventually_mono)
   qed
   ultimately show ?rhs by fast
 next
@@ -2459,7 +2459,7 @@
   using assms(2)
 proof (rule metric_tendsto_imp_tendsto)
   show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
-    using assms(1) by (rule eventually_elim1) (simp add: dist_norm)
+    using assms(1) by (rule eventually_mono) (simp add: dist_norm)
 qed
 
 lemma Lim_transform_bound:
@@ -3206,7 +3206,7 @@
       unfolding closure_sequential by auto
     have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
     then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
-      by (rule eventually_mono, simp add: f(1))
+      by (simp add: f(1))
     have "dist x y \<le> a"
       apply (rule Lim_dist_ubound [of sequentially f])
       apply (rule trivial_limit_sequentially)
@@ -3808,7 +3808,7 @@
     by auto
   moreover
   have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
-    unfolding Z_def by (auto elim: eventually_elim1 intro: set_mp[OF closure_subset])
+    unfolding Z_def by (auto elim: eventually_mono intro: set_mp[OF closure_subset])
   have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   proof (intro allI impI)
     fix B assume "finite B" "B \<subseteq> Z"
@@ -4485,7 +4485,7 @@
         by auto
     }
     ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
-      by (rule eventually_elim1)
+      by (rule eventually_mono)
   }
   then have *: "((f \<circ> r) ---> l) sequentially"
     unfolding o_def tendsto_iff by simp
@@ -5559,7 +5559,7 @@
   then have "eventually (\<lambda>n. x n \<in> T) sequentially"
     using assms T_def by (auto simp: tendsto_def)
   then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
-    using T_def by (auto elim!: eventually_elim1)
+    using T_def by (auto elim!: eventually_mono)
 qed
 
 lemma continuous_on_open:
@@ -5734,7 +5734,7 @@
     using \<open>open U\<close> and \<open>f x \<in> U\<close>
     unfolding tendsto_def by fast
   then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
-    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono')
+    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
   then show ?thesis
     using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
 qed
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Uniform_Limit.thy
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -28,7 +28,7 @@
     (fastforce
       simp: eventually_principal uniformly_on_def
       intro: bexI[where x="min a b" for a b]
-      elim: eventually_elim1)+
+      elim: eventually_mono)+
 
 lemma uniform_limitD:
   "uniform_limit S f l F \<Longrightarrow> e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e"
@@ -103,7 +103,7 @@
   assumes "x \<in> S"
   shows "((\<lambda>y. f y x) ---> l x) F"
   using assms
-  by (auto intro!: tendstoI simp: eventually_elim1 dest!: uniform_limitD)
+  by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)
 
 lemma uniform_limit_theorem:
   assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)"
@@ -115,7 +115,7 @@
   fix x assume "x \<in> A"
   then have "\<forall>\<^sub>F n in F. (f n ---> f n x) (at x within A)" "((\<lambda>n. f n x) ---> l x) F"
     using c ul
-    by (auto simp: continuous_on_def eventually_elim1 tendsto_uniform_limitI)
+    by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI)
   then show "(l ---> l x) (at x within A)"
     by (rule swap_uniform_limit) fact+
 qed
@@ -451,7 +451,7 @@
   using assms(2)
 proof (rule metric_uniform_limit_imp_uniform_limit)
   show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (f x y) 0 \<le> dist (g x y) 0"
-    using assms(1) by (rule eventually_elim1) (force simp add: dist_norm)
+    using assms(1) by (rule eventually_mono) (force simp add: dist_norm)
 qed
 
 lemma uniform_limit_on_union:
@@ -477,7 +477,7 @@
 
 lemma uniform_limit_on_subset:
   "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
-  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono')
+  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
 
 lemma uniformly_convergent_add:
   "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -243,7 +243,7 @@
 apply (simp add: omega_def star_of_def star_n_eq_iff)
 apply clarify
 apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
-apply (erule eventually_mono')
+apply (erule eventually_mono)
 apply auto
 done
 
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/NSA/NSA.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -1960,7 +1960,7 @@
      "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \<in> HFinite"
 apply (rule FreeUltrafilterNat_HFinite)
 apply (rule_tac x = "u + 1" in exI)
-apply (auto elim: eventually_elim1)
+apply (auto elim: eventually_mono)
 done
 
 lemma HInfinite_FreeUltrafilterNat:
@@ -1969,7 +1969,7 @@
 apply (simp add: HFinite_FreeUltrafilterNat_iff)
 apply (rule allI, drule_tac x="u + 1" in spec)
 apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
-apply (auto elim: eventually_elim1)
+apply (auto elim: eventually_mono)
 done
 
 lemma lemma_Int_HI:
@@ -2106,7 +2106,7 @@
 apply (simp add: omega_def)
 apply (rule FreeUltrafilterNat_HInfinite)
 apply clarify
-apply (rule_tac u1 = "u-1" in eventually_mono' [OF FreeUltrafilterNat_nat_gt_real])
+apply (rule_tac u1 = "u-1" in eventually_mono [OF FreeUltrafilterNat_nat_gt_real])
 apply auto
 done
 
@@ -2200,7 +2200,7 @@
      ==> star_n X - star_of x \<in> Infinitesimal"
 unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
-         intro: order_less_trans elim!: eventually_elim1)
+         intro: order_less_trans elim!: eventually_mono)
 
 lemma real_seq_to_hypreal_approx:
      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
@@ -2217,6 +2217,6 @@
       ==> star_n X - star_n Y \<in> Infinitesimal"
 unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
-         intro: order_less_trans elim!: eventually_elim1)
+         intro: order_less_trans elim!: eventually_mono)
 
 end
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/Star.thy
--- a/src/HOL/NSA/Star.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/NSA/Star.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -316,7 +316,7 @@
       HNatInfinite_FreeUltrafilterNat_iff
       Infinitesimal_FreeUltrafilterNat_iff2)
 apply (drule_tac x="Suc m" in spec)
-apply (auto elim!: eventually_elim1)
+apply (auto elim!: eventually_mono)
 done
 
 lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -136,7 +136,7 @@
   "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
     \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
 apply (rule eq_reflection)
-apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1)
+apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_mono)
 done
 
 lemma transfer_fun_eq [transfer_intro]:
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -727,7 +727,7 @@
     lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
   from order_tendstoD[OF lim_0, of "\<infinity>"]
   obtain i where f_s_fin: "(\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) < \<infinity>"
-    by (metis (mono_tags, lifting) eventually_False_sequentially eventually_elim1
+    by (metis (mono_tags, lifting) eventually_False_sequentially eventually_mono
               less_ereal.simps(4) zero_ereal_def)
 
   have [measurable]: "\<And>i. s i \<in> borel_measurable M"
@@ -2417,7 +2417,7 @@
       have "eventually (\<lambda>n. x \<le> X n) sequentially"
         unfolding filterlim_at_top_ge[where c=x] by auto
       then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
-        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_elim1)
+        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
     qed
     fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
       by (auto split: split_indicator)
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -221,7 +221,7 @@
       using \<open>x \<in> I\<close> \<open>open I\<close> X(2)
       apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff
                 integrable_const X q)
-      apply (elim eventually_elim1)
+      apply (elim eventually_mono)
       apply (intro convex_le_Inf_differential)
       apply (auto simp: interior_open q)
       done
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -750,7 +750,7 @@
     with borel have "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> h x \<le> 0"
       by (auto simp add: null_sets_density_iff)
     with pos sets.sets_into_space have "AE x in M. x \<notin> A"
-      by (elim eventually_elim1) (auto simp: not_le[symmetric])
+      by (elim eventually_mono) (auto simp: not_le[symmetric])
     then have "A \<in> null_sets M"
       using \<open>A \<in> sets M\<close> by (simp add: AE_iff_null_sets)
     with ac show "A \<in> null_sets N"
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Probability/Stream_Space.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -238,7 +238,7 @@
   { fix n have "AE x in stream_space M. P (x !! n)"
     proof (induct n)
       case 0 with P show ?case
-        by (subst AE_stream_space) (auto elim!: eventually_elim1)
+        by (subst AE_stream_space) (auto elim!: eventually_mono)
     next
       case (Suc n) then show ?case
         by (subst AE_stream_space) auto
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -471,7 +471,7 @@
 
 lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
   by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
-           elim: eventually_elim2 eventually_elim1)
+           elim: eventually_elim2 eventually_mono)
 
 lemma eventually_at_split:
   "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
@@ -551,7 +551,7 @@
   fix a assume "a < max x y"
   then show "eventually (\<lambda>x. a < max (X x) (Y x)) net"
     using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
-    by (auto simp: less_max_iff_disj elim: eventually_elim1)
+    by (auto simp: less_max_iff_disj elim: eventually_mono)
 next
   fix a assume "max x y < a"
   then show "eventually (\<lambda>x. max (X x) (Y x) < a) net"
@@ -572,7 +572,7 @@
   fix a assume "min x y < a"
   then show "eventually (\<lambda>x. min (X x) (Y x) < a) net"
     using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
-    by (auto simp: min_less_iff_disj elim: eventually_elim1)
+    by (auto simp: min_less_iff_disj elim: eventually_mono)
 qed
 
 lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
@@ -613,14 +613,14 @@
   assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
       and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   shows "(f ---> l) F"
-  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
+  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
 
 lemma decreasing_tendsto:
   fixes f :: "_ \<Rightarrow> 'a::order_topology"
   assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
       and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
   shows "(f ---> l) F"
-  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
+  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
 
 lemma tendsto_sandwich:
   fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
@@ -773,7 +773,7 @@
 lemma tendsto_at_within_iff_tendsto_nhds:
   "(g ---> g l) (at l within S) \<longleftrightarrow> (g ---> g l) (inf (nhds l) (principal S))"
   unfolding tendsto_def eventually_at_filter eventually_inf_principal
-  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
 
 subsection \<open>Limits on sequences\<close>
 
@@ -1152,7 +1152,7 @@
   {
     fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
     with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
-      by (auto elim: eventually_elim1 simp: subset_eq)
+      by (auto elim: eventually_mono simp: subset_eq)
   }
   with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F ----> x)"
     by (intro exI[of _ A]) (auto simp: tendsto_def)
@@ -1187,7 +1187,7 @@
     by (auto simp: eventually_inf_principal eventually_nhds)
   moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
   ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
-    by (auto dest!: topological_tendstoD elim: eventually_elim1)
+    by (auto dest!: topological_tendstoD elim: eventually_mono)
 qed
 
 lemma (in first_countable_topology) eventually_nhds_iff_sequentially:
@@ -1243,7 +1243,7 @@
 lemma tendsto_at_iff_tendsto_nhds:
   "g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
   unfolding tendsto_def eventually_at_filter
-  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
+  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
 
 lemma tendsto_compose:
   "g -- l --> g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
@@ -1758,7 +1758,7 @@
   with \<open>finite D\<close> have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
     by (simp add: eventually_ball_finite)
   with \<open>s \<subseteq> \<Union>D\<close> have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
-    by (auto elim!: eventually_mono')
+    by (auto elim!: eventually_mono)
   thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
     by (simp add: eventually_nhds subset_eq)
 qed
diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Dec 08 20:21:59 2015 +0100
+++ b/src/HOL/Transcendental.thy	Wed Dec 09 17:35:22 2015 +0000
@@ -2510,7 +2510,7 @@
   unfolding powr_def
 proof (rule filterlim_If)
   from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
-    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
+    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
 qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
 
 lemma continuous_powr:
@@ -2544,12 +2544,12 @@
   unfolding powr_def
 proof (rule filterlim_If)
   from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
-    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
+    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
 next
   { assume "a = 0"
     with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0"
       by (auto simp add: filterlim_at eventually_inf_principal le_less
-               elim: eventually_elim1 intro: tendsto_mono inf_le1)
+               elim: eventually_mono intro: tendsto_mono inf_le1)
     then have "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))"
       by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
                        filterlim_tendsto_pos_mult_at_bot[OF _ \<open>0 < b\<close>]
@@ -2571,7 +2571,7 @@
     from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
       unfolding isCont_def by (rule order_tendstoD(1))
     with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
-      by (auto simp: eventually_at_filter powr_def elim: eventually_elim1)
+      by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
   qed
 qed
 
@@ -2610,7 +2610,7 @@
                      filterlim_tendsto_neg_mult_at_bot assms)
   also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) ---> (0::real)) F"
     using f filterlim_at_top_dense[of f F]
-    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_elim1)
+    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_mono)
   finally show ?thesis .
 qed
 
@@ -2657,7 +2657,7 @@
     apply (auto simp add: field_simps)
     done
   then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
-    by (rule eventually_elim1) (erule powr_realpow)
+    by (rule eventually_mono) (erule powr_realpow)
   show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
     by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
 qed auto