sorted out eventually_mono
authorpaulson <lp15@cam.ac.uk>
Wed Dec 09 17:35:22 2015 +0000 (2015-12-09)
changeset 618103c5040d5694a
parent 61809 81d34cf268d8
child 61817 6dde8fcd7f95
sorted out eventually_mono
src/HOL/Deriv.thy
src/HOL/Filter.thy
src/HOL/Finite_Set.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Uniform_Limit.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/Star.thy
src/HOL/NSA/StarDef.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Stream_Space.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Dec 08 20:21:59 2015 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Wed Dec 09 17:35:22 2015 +0000
     1.3 @@ -218,7 +218,7 @@
     1.4  
     1.5  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))"
     1.6    unfolding tendsto_def eventually_inf_principal eventually_at_filter
     1.7 -  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
     1.8 +  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
     1.9  
    1.10  lemma has_derivative_in_compose:
    1.11    assumes f: "(f has_derivative f') (at x within s)"
    1.12 @@ -903,7 +903,7 @@
    1.13    moreover from * have "f x = g x" by (auto simp: eventually_nhds)
    1.14    moreover assume "x = y" "u = v"
    1.15    ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
    1.16 -    by (auto simp: eventually_at_filter elim: eventually_elim1)
    1.17 +    by (auto simp: eventually_at_filter elim: eventually_mono)
    1.18  qed simp_all
    1.19  
    1.20  lemma DERIV_shift:
    1.21 @@ -1679,12 +1679,12 @@
    1.22    then have "(\<zeta> ---> 0) (at_right 0)"
    1.23      by (rule tendsto_norm_zero_cancel)
    1.24    with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
    1.25 -    by (auto elim!: eventually_elim1 simp: filterlim_at)
    1.26 +    by (auto elim!: eventually_mono simp: filterlim_at)
    1.27    from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
    1.28      by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
    1.29    ultimately have "((\<lambda>t. f t / g t) ---> x) (at_right 0)" (is ?P)
    1.30      by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
    1.31 -       (auto elim: eventually_elim1)
    1.32 +       (auto elim: eventually_mono)
    1.33    also have "?P \<longleftrightarrow> ?thesis"
    1.34      by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter)
    1.35    finally show ?thesis .
    1.36 @@ -1753,7 +1753,7 @@
    1.37  
    1.38    moreover
    1.39    have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"
    1.40 -    using g_0 by (auto elim: eventually_elim1 simp: filterlim_at_top_dense)
    1.41 +    using g_0 by (auto elim: eventually_mono simp: filterlim_at_top_dense)
    1.42  
    1.43    moreover
    1.44    have inv_g: "((\<lambda>x. inverse (g x)) ---> 0) (at_right 0)"
    1.45 @@ -1765,7 +1765,7 @@
    1.46      by (simp add: inverse_eq_divide)
    1.47    from this[unfolded tendsto_iff, rule_format, of 1]
    1.48    have "eventually (\<lambda>x. norm (1 - g a / g x) < 2) (at_right 0)"
    1.49 -    by (auto elim!: eventually_elim1 simp: dist_real_def)
    1.50 +    by (auto elim!: eventually_mono simp: dist_real_def)
    1.51  
    1.52    moreover
    1.53    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)"
     2.1 --- a/src/HOL/Filter.thy	Tue Dec 08 20:21:59 2015 +0100
     2.2 +++ b/src/HOL/Filter.thy	Wed Dec 09 17:35:22 2015 +0000
     2.3 @@ -67,11 +67,6 @@
     2.4    by (auto intro: always_eventually)
     2.5  
     2.6  lemma eventually_mono:
     2.7 -  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
     2.8 -  unfolding eventually_def
     2.9 -  by (rule is_filter.mono [OF is_filter_Rep_filter])
    2.10 -
    2.11 -lemma eventually_mono':
    2.12    "\<lbrakk>eventually P F; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> eventually Q F"
    2.13    unfolding eventually_def
    2.14    by (blast intro: is_filter.mono [OF is_filter_Rep_filter])
    2.15 @@ -91,7 +86,7 @@
    2.16    have "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"
    2.17      using assms by (rule eventually_conj)
    2.18    then show ?thesis
    2.19 -    by (blast intro: eventually_mono')
    2.20 +    by (blast intro: eventually_mono)
    2.21  qed
    2.22  
    2.23  lemma eventually_rev_mp:
    2.24 @@ -104,12 +99,6 @@
    2.25    "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"
    2.26    by (auto intro: eventually_conj elim: eventually_rev_mp)
    2.27  
    2.28 -lemma eventually_elim1:
    2.29 -  assumes "eventually (\<lambda>i. P i) F"
    2.30 -  assumes "\<And>i. P i \<Longrightarrow> Q i"
    2.31 -  shows "eventually (\<lambda>i. Q i) F"
    2.32 -  using assms by (auto elim!: eventually_rev_mp)
    2.33 -
    2.34  lemma eventually_elim2:
    2.35    assumes "eventually (\<lambda>i. P i) F"
    2.36    assumes "eventually (\<lambda>i. Q i) F"
    2.37 @@ -135,10 +124,10 @@
    2.38  proof
    2.39    assume "\<forall>\<^sub>Fx in F. \<exists>y. P x y"
    2.40    then have "\<forall>\<^sub>Fx in F. P x (SOME y. P x y)"
    2.41 -    by (auto intro: someI_ex eventually_elim1)
    2.42 +    by (auto intro: someI_ex eventually_mono)
    2.43    then show "\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x)"
    2.44      by auto
    2.45 -qed (auto intro: eventually_elim1)
    2.46 +qed (auto intro: eventually_mono)
    2.47  
    2.48  lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    2.49    by (auto intro: eventually_mp)
    2.50 @@ -152,7 +141,7 @@
    2.51  proof -
    2.52    from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    2.53        and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
    2.54 -    by (auto elim: eventually_elim1)
    2.55 +    by (auto elim: eventually_mono)
    2.56    then show ?thesis by (auto elim: eventually_elim2)
    2.57  qed
    2.58  
    2.59 @@ -346,7 +335,7 @@
    2.60      unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
    2.61    { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
    2.62      unfolding le_filter_def eventually_inf
    2.63 -    by (auto intro: eventually_mono' [OF eventually_conj]) }
    2.64 +    by (auto intro: eventually_mono [OF eventually_conj]) }
    2.65    { show "F \<le> sup F F'" and "F' \<le> sup F F'"
    2.66      unfolding le_filter_def eventually_sup by simp_all }
    2.67    { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
    2.68 @@ -434,7 +423,7 @@
    2.69        assume "?F P" then guess X ..
    2.70        moreover assume "\<forall>x. P x \<longrightarrow> Q x"
    2.71        ultimately show "?F Q"
    2.72 -        by (intro exI[of _ X]) (auto elim: eventually_elim1)
    2.73 +        by (intro exI[of _ X]) (auto elim: eventually_mono)
    2.74      qed }
    2.75    note eventually_F = this
    2.76  
    2.77 @@ -553,7 +542,7 @@
    2.78    by (rule eventually_Abs_filter, rule is_filter.intro) auto
    2.79  
    2.80  lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
    2.81 -  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
    2.82 +  unfolding eventually_inf eventually_principal by (auto elim: eventually_mono)
    2.83  
    2.84  lemma principal_UNIV[simp]: "principal UNIV = top"
    2.85    by (auto simp: filter_eq_iff eventually_principal)
    2.86 @@ -571,7 +560,7 @@
    2.87    unfolding le_filter_def eventually_principal
    2.88    apply safe
    2.89    apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
    2.90 -  apply (auto elim: eventually_elim1)
    2.91 +  apply (auto elim: eventually_mono)
    2.92    done
    2.93  
    2.94  lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
    2.95 @@ -877,7 +866,7 @@
    2.96  lemma filterlim_at_top:
    2.97    fixes f :: "'a \<Rightarrow> ('b::linorder)"
    2.98    shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z \<le> f x) F)"
    2.99 -  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_elim1)
   2.100 +  by (auto simp: filterlim_iff eventually_at_top_linorder elim!: eventually_mono)
   2.101  
   2.102  lemma filterlim_at_top_mono:
   2.103    "LIM x F. f x :> at_top \<Longrightarrow> eventually (\<lambda>x. f x \<le> (g x::'a::linorder)) F \<Longrightarrow>
   2.104 @@ -887,7 +876,7 @@
   2.105  lemma filterlim_at_top_dense:
   2.106    fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)"
   2.107    shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
   2.108 -  by (metis eventually_elim1[of _ F] eventually_gt_at_top order_less_imp_le
   2.109 +  by (metis eventually_mono[of _ F] eventually_gt_at_top order_less_imp_le
   2.110              filterlim_at_top[of f F] filterlim_iff[of f at_top F])
   2.111  
   2.112  lemma filterlim_at_top_ge:
   2.113 @@ -924,7 +913,7 @@
   2.114  lemma filterlim_at_bot:
   2.115    fixes f :: "'a \<Rightarrow> ('b::linorder)"
   2.116    shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F)"
   2.117 -  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_elim1)
   2.118 +  by (auto simp: filterlim_iff eventually_at_bot_linorder elim!: eventually_mono)
   2.119  
   2.120  lemma filterlim_at_bot_dense:
   2.121    fixes f :: "'a \<Rightarrow> ('b::{dense_linorder, no_bot})"
   2.122 @@ -935,12 +924,12 @@
   2.123    assume "\<forall>Z. eventually (\<lambda>x. f x \<le> Z) F"
   2.124    hence "eventually (\<lambda>x. f x \<le> Z') F" by auto
   2.125    thus "eventually (\<lambda>x. f x < Z) F"
   2.126 -    apply (rule eventually_mono')
   2.127 +    apply (rule eventually_mono)
   2.128      using 1 by auto
   2.129    next
   2.130      fix Z :: 'b
   2.131      show "\<forall>Z. eventually (\<lambda>x. f x < Z) F \<Longrightarrow> eventually (\<lambda>x. f x \<le> Z) F"
   2.132 -      by (drule spec [of _ Z], erule eventually_mono', auto simp add: less_imp_le)
   2.133 +      by (drule spec [of _ Z], erule eventually_mono, auto simp add: less_imp_le)
   2.134  qed
   2.135  
   2.136  lemma filterlim_at_bot_le:
   2.137 @@ -950,7 +939,7 @@
   2.138  proof safe
   2.139    fix Z assume *: "\<forall>Z\<le>c. eventually (\<lambda>x. Z \<ge> f x) F"
   2.140    with *[THEN spec, of "min Z c"] show "eventually (\<lambda>x. Z \<ge> f x) F"
   2.141 -    by (auto elim!: eventually_elim1)
   2.142 +    by (auto elim!: eventually_mono)
   2.143  qed simp
   2.144  
   2.145  lemma filterlim_at_bot_lt:
     3.1 --- a/src/HOL/Finite_Set.thy	Tue Dec 08 20:21:59 2015 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Wed Dec 09 17:35:22 2015 +0000
     3.3 @@ -1787,4 +1787,118 @@
     3.4  
     3.5  hide_const (open) Finite_Set.fold
     3.6  
     3.7 +
     3.8 +subsection "Infinite Sets"
     3.9 +
    3.10 +text \<open>
    3.11 +  Some elementary facts about infinite sets, mostly by Stephan Merz.
    3.12 +  Beware! Because "infinite" merely abbreviates a negation, these
    3.13 +  lemmas may not work well with \<open>blast\<close>.
    3.14 +\<close>
    3.15 +
    3.16 +abbreviation infinite :: "'a set \<Rightarrow> bool"
    3.17 +  where "infinite S \<equiv> \<not> finite S"
    3.18 +
    3.19 +text \<open>
    3.20 +  Infinite sets are non-empty, and if we remove some elements from an
    3.21 +  infinite set, the result is still infinite.
    3.22 +\<close>
    3.23 +
    3.24 +lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
    3.25 +  by auto
    3.26 +
    3.27 +lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})"
    3.28 +  by simp
    3.29 +
    3.30 +lemma Diff_infinite_finite:
    3.31 +  assumes T: "finite T" and S: "infinite S"
    3.32 +  shows "infinite (S - T)"
    3.33 +  using T
    3.34 +proof induct
    3.35 +  from S
    3.36 +  show "infinite (S - {})" by auto
    3.37 +next
    3.38 +  fix T x
    3.39 +  assume ih: "infinite (S - T)"
    3.40 +  have "S - (insert x T) = (S - T) - {x}"
    3.41 +    by (rule Diff_insert)
    3.42 +  with ih
    3.43 +  show "infinite (S - (insert x T))"
    3.44 +    by (simp add: infinite_remove)
    3.45 +qed
    3.46 +
    3.47 +lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
    3.48 +  by simp
    3.49 +
    3.50 +lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
    3.51 +  by simp
    3.52 +
    3.53 +lemma infinite_super:
    3.54 +  assumes T: "S \<subseteq> T" and S: "infinite S"
    3.55 +  shows "infinite T"
    3.56 +proof
    3.57 +  assume "finite T"
    3.58 +  with T have "finite S" by (simp add: finite_subset)
    3.59 +  with S show False by simp
    3.60 +qed
    3.61 +
    3.62 +proposition infinite_coinduct [consumes 1, case_names infinite]:
    3.63 +  assumes "X A"
    3.64 +  and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
    3.65 +  shows "infinite A"
    3.66 +proof
    3.67 +  assume "finite A"
    3.68 +  then show False using \<open>X A\<close>
    3.69 +  proof (induction rule: finite_psubset_induct)
    3.70 +    case (psubset A)
    3.71 +    then obtain x where "x \<in> A" "X (A - {x}) \<or> infinite (A - {x})"
    3.72 +      using local.step psubset.prems by blast
    3.73 +    then have "X (A - {x})"
    3.74 +      using psubset.hyps by blast
    3.75 +    show False
    3.76 +      apply (rule psubset.IH [where B = "A - {x}"])
    3.77 +      using \<open>x \<in> A\<close> apply blast
    3.78 +      by (simp add: \<open>X (A - {x})\<close>)
    3.79 +  qed
    3.80 +qed
    3.81 +
    3.82 +text \<open>
    3.83 +  For any function with infinite domain and finite range there is some
    3.84 +  element that is the image of infinitely many domain elements.  In
    3.85 +  particular, any infinite sequence of elements from a finite set
    3.86 +  contains some element that occurs infinitely often.
    3.87 +\<close>
    3.88 +
    3.89 +lemma inf_img_fin_dom':
    3.90 +  assumes img: "finite (f ` A)" and dom: "infinite A"
    3.91 +  shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
    3.92 +proof (rule ccontr)
    3.93 +  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
    3.94 +  moreover
    3.95 +  assume "\<not> ?thesis"
    3.96 +  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
    3.97 +  ultimately have "finite A" by(rule finite_subset)
    3.98 +  with dom show False by contradiction
    3.99 +qed
   3.100 +
   3.101 +lemma inf_img_fin_domE':
   3.102 +  assumes "finite (f ` A)" and "infinite A"
   3.103 +  obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
   3.104 +  using assms by (blast dest: inf_img_fin_dom')
   3.105 +
   3.106 +lemma inf_img_fin_dom:
   3.107 +  assumes img: "finite (f`A)" and dom: "infinite A"
   3.108 +  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   3.109 +using inf_img_fin_dom'[OF assms] by auto
   3.110 +
   3.111 +lemma inf_img_fin_domE:
   3.112 +  assumes "finite (f`A)" and "infinite A"
   3.113 +  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   3.114 +  using assms by (blast dest: inf_img_fin_dom)
   3.115 +
   3.116 +proposition finite_image_absD:
   3.117 +    fixes S :: "'a::linordered_ring set"
   3.118 +    shows "finite (abs ` S) \<Longrightarrow> finite S"
   3.119 +  by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
   3.120 +
   3.121  end
     4.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Dec 08 20:21:59 2015 +0100
     4.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Dec 09 17:35:22 2015 +0000
     4.3 @@ -2444,7 +2444,7 @@
     4.4    then have S: "open S" "ereal x \<in> ereal ` S"
     4.5      by (simp_all add: inj_image_mem_iff)
     4.6    show "eventually (\<lambda>x. real_of_ereal (f x) \<in> S) net"
     4.7 -    by (auto intro: eventually_mono' [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]])
     4.8 +    by (auto intro: eventually_mono [OF lim[THEN topological_tendstoD, OF open_ereal, OF S]])
     4.9  qed
    4.10  
    4.11  lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
    4.12 @@ -2456,7 +2456,7 @@
    4.13      fix l :: ereal
    4.14      assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
    4.15      from this[THEN spec, of "real_of_ereal l"] have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
    4.16 -      by (cases l) (auto elim: eventually_elim1)
    4.17 +      by (cases l) (auto elim: eventually_mono)
    4.18    }
    4.19    then show ?thesis
    4.20      by (auto simp: order_tendsto_iff)
    4.21 @@ -2477,7 +2477,7 @@
    4.22    then have "eventually (\<lambda>z. f z \<in> {..< B}) F"
    4.23      by auto
    4.24    ultimately show "eventually (\<lambda>z. f z \<in> S) F"
    4.25 -    by (auto elim!: eventually_elim1)
    4.26 +    by (auto elim!: eventually_mono)
    4.27  next
    4.28    fix x
    4.29    assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
    4.30 @@ -2571,7 +2571,7 @@
    4.31      by auto
    4.32    from tendsto[THEN topological_tendstoD, OF this]
    4.33    show "eventually (\<lambda>x. ereal (real_of_ereal (f x)) \<in> S) net"
    4.34 -    by (elim eventually_elim1) (auto simp: ereal_real)
    4.35 +    by (elim eventually_mono) (auto simp: ereal_real)
    4.36  qed
    4.37  
    4.38  lemma ereal_mult_cancel_left:
     5.1 --- a/src/HOL/Library/Infinite_Set.thy	Tue Dec 08 20:21:59 2015 +0100
     5.2 +++ b/src/HOL/Library/Infinite_Set.thy	Wed Dec 09 17:35:22 2015 +0000
     5.3 @@ -8,71 +8,7 @@
     5.4  imports Main
     5.5  begin
     5.6  
     5.7 -subsection "Infinite Sets"
     5.8 -
     5.9 -text \<open>
    5.10 -  Some elementary facts about infinite sets, mostly by Stephan Merz.
    5.11 -  Beware! Because "infinite" merely abbreviates a negation, these
    5.12 -  lemmas may not work well with \<open>blast\<close>.
    5.13 -\<close>
    5.14 -
    5.15 -abbreviation infinite :: "'a set \<Rightarrow> bool"
    5.16 -  where "infinite S \<equiv> \<not> finite S"
    5.17 -
    5.18 -text \<open>
    5.19 -  Infinite sets are non-empty, and if we remove some elements from an
    5.20 -  infinite set, the result is still infinite.
    5.21 -\<close>
    5.22 -
    5.23 -lemma infinite_imp_nonempty: "infinite S \<Longrightarrow> S \<noteq> {}"
    5.24 -  by auto
    5.25 -
    5.26 -lemma infinite_remove: "infinite S \<Longrightarrow> infinite (S - {a})"
    5.27 -  by simp
    5.28 -
    5.29 -lemma Diff_infinite_finite:
    5.30 -  assumes T: "finite T" and S: "infinite S"
    5.31 -  shows "infinite (S - T)"
    5.32 -  using T
    5.33 -proof induct
    5.34 -  from S
    5.35 -  show "infinite (S - {})" by auto
    5.36 -next
    5.37 -  fix T x
    5.38 -  assume ih: "infinite (S - T)"
    5.39 -  have "S - (insert x T) = (S - T) - {x}"
    5.40 -    by (rule Diff_insert)
    5.41 -  with ih
    5.42 -  show "infinite (S - (insert x T))"
    5.43 -    by (simp add: infinite_remove)
    5.44 -qed
    5.45 -
    5.46 -lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
    5.47 -  by simp
    5.48 -
    5.49 -lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
    5.50 -  by simp
    5.51 -
    5.52 -lemma infinite_super:
    5.53 -  assumes T: "S \<subseteq> T" and S: "infinite S"
    5.54 -  shows "infinite T"
    5.55 -proof
    5.56 -  assume "finite T"
    5.57 -  with T have "finite S" by (simp add: finite_subset)
    5.58 -  with S show False by simp
    5.59 -qed
    5.60 -
    5.61 -lemma infinite_coinduct [consumes 1, case_names infinite]:
    5.62 -  assumes "X A"
    5.63 -  and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"
    5.64 -  shows "infinite A"
    5.65 -proof
    5.66 -  assume "finite A"
    5.67 -  then show False using \<open>X A\<close>
    5.68 -    by(induction rule: finite_psubset_induct)(meson Diff_subset card_Diff1_less card_psubset finite_Diff step)
    5.69 -qed    
    5.70 -
    5.71 -text \<open>As a concrete example, we prove that the set of natural numbers is infinite.\<close>
    5.72 +text \<open>The set of natural numbers is infinite.\<close>
    5.73  
    5.74  lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
    5.75    using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    5.76 @@ -99,8 +35,9 @@
    5.77  \<close>
    5.78  
    5.79  lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
    5.80 -  by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
    5.81 -            not_less_iff_gr_or_eq sup.bounded_iff)
    5.82 +apply (clarsimp simp add: finite_nat_set_iff_bounded)
    5.83 +apply (drule_tac x="Suc (max m k)" in spec)
    5.84 +using less_Suc_eq by fastforce
    5.85  
    5.86  lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    5.87    by simp
    5.88 @@ -114,45 +51,6 @@
    5.89    then show False by simp
    5.90  qed
    5.91  
    5.92 -text \<open>
    5.93 -  For any function with infinite domain and finite range there is some
    5.94 -  element that is the image of infinitely many domain elements.  In
    5.95 -  particular, any infinite sequence of elements from a finite set
    5.96 -  contains some element that occurs infinitely often.
    5.97 -\<close>
    5.98 -
    5.99 -lemma inf_img_fin_dom':
   5.100 -  assumes img: "finite (f ` A)" and dom: "infinite A"
   5.101 -  shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
   5.102 -proof (rule ccontr)
   5.103 -  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
   5.104 -  moreover
   5.105 -  assume "\<not> ?thesis"
   5.106 -  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
   5.107 -  ultimately have "finite A" by(rule finite_subset)
   5.108 -  with dom show False by contradiction
   5.109 -qed
   5.110 -
   5.111 -lemma inf_img_fin_domE':
   5.112 -  assumes "finite (f ` A)" and "infinite A"
   5.113 -  obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
   5.114 -  using assms by (blast dest: inf_img_fin_dom')
   5.115 -
   5.116 -lemma inf_img_fin_dom:
   5.117 -  assumes img: "finite (f`A)" and dom: "infinite A"
   5.118 -  shows "\<exists>y \<in> f`A. infinite (f -` {y})"
   5.119 -using inf_img_fin_dom'[OF assms] by auto
   5.120 -
   5.121 -lemma inf_img_fin_domE:
   5.122 -  assumes "finite (f`A)" and "infinite A"
   5.123 -  obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   5.124 -  using assms by (blast dest: inf_img_fin_dom)
   5.125 -
   5.126 -proposition finite_image_absD:
   5.127 -    fixes S :: "'a::linordered_ring set"
   5.128 -    shows "finite (abs ` S) \<Longrightarrow> finite S"
   5.129 -  by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
   5.130 -
   5.131  text \<open>The set of integers is also infinite.\<close>
   5.132  
   5.133  lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
   5.134 @@ -196,10 +94,10 @@
   5.135    by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
   5.136  
   5.137  lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   5.138 -  by (auto intro: eventually_rev_mp eventually_elim1)
   5.139 +  by (auto intro: eventually_rev_mp eventually_mono)
   5.140  
   5.141  lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   5.142 -  by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
   5.143 +  by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono)
   5.144  
   5.145  text \<open>Properties of quantifiers with injective functions.\<close>
   5.146  
   5.147 @@ -272,7 +170,7 @@
   5.148  lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
   5.149  lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
   5.150  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)
   5.151 -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)
   5.152 +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)
   5.153  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)
   5.154  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)
   5.155  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)
   5.156 @@ -331,7 +229,7 @@
   5.157  lemma le_enumerate:
   5.158    assumes S: "infinite S"
   5.159    shows "n \<le> enumerate S n"
   5.160 -  using S 
   5.161 +  using S
   5.162  proof (induct n)
   5.163    case 0
   5.164    then show ?case by simp
     6.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Dec 08 20:21:59 2015 +0100
     6.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Dec 09 17:35:22 2015 +0000
     6.3 @@ -100,7 +100,7 @@
     6.4  lemma Liminf_eq:
     6.5    assumes "eventually (\<lambda>x. f x = g x) F"
     6.6    shows "Liminf F f = Liminf F g"
     6.7 -  by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
     6.8 +  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
     6.9  
    6.10  lemma Limsup_mono:
    6.11    assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
    6.12 @@ -116,7 +116,7 @@
    6.13  lemma Limsup_eq:
    6.14    assumes "eventually (\<lambda>x. f x = g x) net"
    6.15    shows "Limsup net f = Limsup net g"
    6.16 -  by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
    6.17 +  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
    6.18  
    6.19  lemma Liminf_le_Limsup:
    6.20    assumes ntriv: "\<not> trivial_limit F"
    6.21 @@ -167,7 +167,7 @@
    6.22  proof -
    6.23    have "eventually (\<lambda>x. y < X x) F"
    6.24      if "eventually P F" "y < INFIMUM (Collect P) X" for y P
    6.25 -    using that by (auto elim!: eventually_elim1 dest: less_INF_D)
    6.26 +    using that by (auto elim!: eventually_mono dest: less_INF_D)
    6.27    moreover
    6.28    have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
    6.29      if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
    6.30 @@ -218,7 +218,7 @@
    6.31        then have "eventually (\<lambda>x. y < f x) F"
    6.32          using lim[THEN topological_tendstoD, of "{y <..}"] by auto
    6.33        then have "eventually (\<lambda>x. f0 \<le> f x) F"
    6.34 -        using discrete by (auto elim!: eventually_elim1)
    6.35 +        using discrete by (auto elim!: eventually_mono)
    6.36        then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
    6.37          by (rule upper)
    6.38        moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
    6.39 @@ -257,7 +257,7 @@
    6.40        then have "eventually (\<lambda>x. f x < y) F"
    6.41          using lim[THEN topological_tendstoD, of "{..< y}"] by auto
    6.42        then have "eventually (\<lambda>x. f x \<le> f0) F"
    6.43 -        using False by (auto elim!: eventually_elim1 simp: not_less)
    6.44 +        using False by (auto elim!: eventually_mono simp: not_less)
    6.45        then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
    6.46          by (rule lower)
    6.47        moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
    6.48 @@ -278,14 +278,14 @@
    6.49    then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
    6.50      unfolding Limsup_def INF_less_iff by auto
    6.51    then show "eventually (\<lambda>x. f x < a) F"
    6.52 -    by (auto elim!: eventually_elim1 dest: SUP_lessD)
    6.53 +    by (auto elim!: eventually_mono dest: SUP_lessD)
    6.54  next
    6.55    fix a assume "a < f0"
    6.56    with assms have "a < Liminf F f" by simp
    6.57    then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
    6.58      unfolding Liminf_def less_SUP_iff by auto
    6.59    then show "eventually (\<lambda>x. a < f x) F"
    6.60 -    by (auto elim!: eventually_elim1 dest: less_INF_D)
    6.61 +    by (auto elim!: eventually_mono dest: less_INF_D)
    6.62  qed
    6.63  
    6.64  lemma tendsto_iff_Liminf_eq_Limsup:
     7.1 --- a/src/HOL/Limits.thy	Tue Dec 08 20:21:59 2015 +0100
     7.2 +++ b/src/HOL/Limits.thy	Wed Dec 09 17:35:22 2015 +0000
     7.3 @@ -83,7 +83,7 @@
     7.4    show "0 < max K 1" by simp
     7.5  next
     7.6    show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F"
     7.7 -    using K by (rule eventually_elim1, simp)
     7.8 +    using K by (rule eventually_mono, simp)
     7.9  qed
    7.10  
    7.11  lemma BfunE:
    7.12 @@ -897,10 +897,10 @@
    7.13    with f have "eventually (\<lambda>x. dist (f x) a < norm a) F"
    7.14      by (rule tendstoD)
    7.15    then have "eventually (\<lambda>x. f x \<noteq> 0) F"
    7.16 -    unfolding dist_norm by (auto elim!: eventually_elim1)
    7.17 +    unfolding dist_norm by (auto elim!: eventually_mono)
    7.18    with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
    7.19      - (inverse (f x) * (f x - a) * inverse a)) F"
    7.20 -    by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
    7.21 +    by (auto elim!: eventually_mono simp: inverse_diff_inverse)
    7.22    moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
    7.23      by (intro Zfun_minus Zfun_mult_left
    7.24        bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
    7.25 @@ -1149,7 +1149,7 @@
    7.26    then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
    7.27      by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
    7.28    then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
    7.29 -    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
    7.30 +    by (auto elim!: eventually_mono simp: inverse_eq_divide field_simps)
    7.31  qed
    7.32  
    7.33  lemma tendsto_inverse_0:
    7.34 @@ -1202,7 +1202,7 @@
    7.35  lemma filterlim_inverse_at_top:
    7.36    "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
    7.37    by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
    7.38 -     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
    7.39 +     (simp add: filterlim_def eventually_filtermap eventually_mono at_within_def le_principal)
    7.40  
    7.41  lemma filterlim_inverse_at_bot_neg:
    7.42    "LIM x (at_left (0::real)). inverse x :> at_bot"
    7.43 @@ -1335,7 +1335,7 @@
    7.44  proof safe
    7.45    fix Z :: real assume "0 < Z"
    7.46    from f \<open>0 < c\<close> have "eventually (\<lambda>x. c / 2 < f x) F"
    7.47 -    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1
    7.48 +    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono
    7.49               simp: dist_real_def abs_real_def split: split_if_asm)
    7.50    moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F"
    7.51      unfolding filterlim_at_top by auto
    7.52 @@ -1409,7 +1409,7 @@
    7.53  proof safe
    7.54    fix Z :: real assume "0 < Z"
    7.55    from f have "eventually (\<lambda>x. c - 1 < f x) F"
    7.56 -    by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def)
    7.57 +    by (auto dest!: tendstoD[where e=1] elim!: eventually_mono simp: dist_real_def)
    7.58    moreover from g have "eventually (\<lambda>x. Z - (c - 1) \<le> g x) F"
    7.59      unfolding filterlim_at_top by auto
    7.60    ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F"
     8.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Dec 08 20:21:59 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Dec 09 17:35:22 2015 +0000
     8.3 @@ -886,7 +886,7 @@
     8.4        finally have "dist (f (r n)) l < e" by simp
     8.5      }
     8.6      ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
     8.7 -      by (rule eventually_elim1)
     8.8 +      by (rule eventually_mono)
     8.9    }
    8.10    hence "((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
    8.11    with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
     9.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 08 20:21:59 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 09 17:35:22 2015 +0000
     9.3 @@ -3336,7 +3336,6 @@
     9.4  
     9.5  subsection\<open>Winding Numbers\<close>
     9.6  
     9.7 -text\<open>The result is an integer, but it doesn't have type @{typ int}!\<close>
     9.8  definition winding_number:: "[real \<Rightarrow> complex, complex] \<Rightarrow> complex" where
     9.9    "winding_number \<gamma> z \<equiv>
    9.10      @n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and>
    10.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 08 20:21:59 2015 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Dec 09 17:35:22 2015 +0000
    10.3 @@ -290,13 +290,13 @@
    10.4    unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto)
    10.5  
    10.6  lemma le_nhds: "F \<le> nhds a \<longleftrightarrow> (\<forall>S. open S \<and> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F)"
    10.7 -  unfolding le_filter_def eventually_nhds by (fast elim: eventually_elim1)
    10.8 +  unfolding le_filter_def eventually_nhds by (fast elim: eventually_mono)
    10.9  
   10.10  lemma le_nhds_metric: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a < e) F)"
   10.11 -  unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_elim1)
   10.12 +  unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_mono)
   10.13  
   10.14  lemma le_nhds_metric_le: "F \<le> nhds a \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist x a \<le> e) F)"
   10.15 -  unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_elim1)
   10.16 +  unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_mono)
   10.17  
   10.18  text \<open>Several results are easier using a "multiplied-out" variant.
   10.19  (I got this idea from Dieudonne's proof of the chain rule).\<close>
   10.20 @@ -2016,15 +2016,15 @@
   10.21          case True
   10.22          have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e * norm u) sequentially"
   10.23            using assms(3)[folded eventually_sequentially] and \<open>0 < e\<close> and \<open>x \<in> s\<close>
   10.24 -          by (fast elim: eventually_elim1)
   10.25 +          by (fast elim: eventually_mono)
   10.26          then show ?thesis
   10.27 -          using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_elim1)
   10.28 +          using \<open>u = 0\<close> and \<open>0 < e\<close> by (auto elim: eventually_mono)
   10.29        next
   10.30          case False
   10.31          with \<open>0 < e\<close> have "0 < e / norm u" by simp
   10.32          then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
   10.33            using assms(3)[folded eventually_sequentially] and \<open>x \<in> s\<close>
   10.34 -          by (fast elim: eventually_elim1)
   10.35 +          by (fast elim: eventually_mono)
   10.36          then show ?thesis
   10.37            using \<open>u \<noteq> 0\<close> by simp
   10.38        qed
   10.39 @@ -2250,7 +2250,7 @@
   10.40    also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
   10.41                  ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
   10.42      using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
   10.43 -    by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff)
   10.44 +    by (intro DERIV_cong_ev) (auto elim!: eventually_mono simp: sums_iff)
   10.45    finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
   10.46  qed
   10.47  
    11.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Dec 08 20:21:59 2015 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Dec 09 17:35:22 2015 +0000
    11.3 @@ -431,7 +431,7 @@
    11.4        by (simp add: mono_set)
    11.5    }
    11.6    with P show "eventually (\<lambda>x. f x \<in> S) net"
    11.7 -    by (auto elim: eventually_elim1)
    11.8 +    by (auto elim: eventually_mono)
    11.9  next
   11.10    fix y l
   11.11    assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   11.12 @@ -470,7 +470,7 @@
   11.13      have "f x \<in> S"
   11.14        by (simp add: inj_image_mem_iff) }
   11.15    with P show "eventually (\<lambda>x. f x \<in> S) net"
   11.16 -    by (auto elim: eventually_elim1)
   11.17 +    by (auto elim: eventually_mono)
   11.18  next
   11.19    fix y l
   11.20    assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
    12.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Dec 08 20:21:59 2015 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 09 17:35:22 2015 +0000
    12.3 @@ -224,7 +224,7 @@
    12.4    hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net"
    12.5      by (rule eventually_all_finite)
    12.6    thus "eventually (\<lambda>x. f x \<in> S) net"
    12.7 -    by (rule eventually_elim1, simp add: S)
    12.8 +    by (rule eventually_mono, simp add: S)
    12.9  qed
   12.10  
   12.11  lemma tendsto_vec_lambda [tendsto_intros]:
    13.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 08 20:21:59 2015 +0100
    13.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 09 17:35:22 2015 +0000
    13.3 @@ -73,8 +73,6 @@
    13.4    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
    13.5    by (metis cInf_eq_Min Min_le_iff)
    13.6  
    13.7 -(*declare not_less[simp] not_le[simp]*)
    13.8 -
    13.9  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   13.10    scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   13.11    scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
    14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 08 20:21:59 2015 +0100
    14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 09 17:35:22 2015 +0000
    14.3 @@ -2310,7 +2310,7 @@
    14.4    by (auto simp add: tendsto_iff eventually_at_infinity)
    14.5  
    14.6  lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
    14.7 -  by (rule topological_tendstoI, auto elim: eventually_mono')
    14.8 +  by (rule topological_tendstoI, auto elim: eventually_mono)
    14.9  
   14.10  text\<open>The expected monotonicity property.\<close>
   14.11  
   14.12 @@ -2348,7 +2348,7 @@
   14.13    next
   14.14      assume "?rhs"
   14.15      then show "?lhs"
   14.16 -      by (auto elim: eventually_elim1 simp: eventually_at_filter)
   14.17 +      by (auto elim: eventually_mono simp: eventually_at_filter)
   14.18    }
   14.19  qed
   14.20  
   14.21 @@ -2429,7 +2429,7 @@
   14.22      assume "open S" "x \<in> S"
   14.23      from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
   14.24      show "eventually (\<lambda>x. f x \<in> S) sequentially"
   14.25 -      by (auto elim!: eventually_elim1)
   14.26 +      by (auto elim!: eventually_mono)
   14.27    qed
   14.28    ultimately show ?rhs by fast
   14.29  next
   14.30 @@ -2459,7 +2459,7 @@
   14.31    using assms(2)
   14.32  proof (rule metric_tendsto_imp_tendsto)
   14.33    show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
   14.34 -    using assms(1) by (rule eventually_elim1) (simp add: dist_norm)
   14.35 +    using assms(1) by (rule eventually_mono) (simp add: dist_norm)
   14.36  qed
   14.37  
   14.38  lemma Lim_transform_bound:
   14.39 @@ -3206,7 +3206,7 @@
   14.40        unfolding closure_sequential by auto
   14.41      have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
   14.42      then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
   14.43 -      by (rule eventually_mono, simp add: f(1))
   14.44 +      by (simp add: f(1))
   14.45      have "dist x y \<le> a"
   14.46        apply (rule Lim_dist_ubound [of sequentially f])
   14.47        apply (rule trivial_limit_sequentially)
   14.48 @@ -3808,7 +3808,7 @@
   14.49      by auto
   14.50    moreover
   14.51    have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
   14.52 -    unfolding Z_def by (auto elim: eventually_elim1 intro: set_mp[OF closure_subset])
   14.53 +    unfolding Z_def by (auto elim: eventually_mono intro: set_mp[OF closure_subset])
   14.54    have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   14.55    proof (intro allI impI)
   14.56      fix B assume "finite B" "B \<subseteq> Z"
   14.57 @@ -4485,7 +4485,7 @@
   14.58          by auto
   14.59      }
   14.60      ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
   14.61 -      by (rule eventually_elim1)
   14.62 +      by (rule eventually_mono)
   14.63    }
   14.64    then have *: "((f \<circ> r) ---> l) sequentially"
   14.65      unfolding o_def tendsto_iff by simp
   14.66 @@ -5559,7 +5559,7 @@
   14.67    then have "eventually (\<lambda>n. x n \<in> T) sequentially"
   14.68      using assms T_def by (auto simp: tendsto_def)
   14.69    then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
   14.70 -    using T_def by (auto elim!: eventually_elim1)
   14.71 +    using T_def by (auto elim!: eventually_mono)
   14.72  qed
   14.73  
   14.74  lemma continuous_on_open:
   14.75 @@ -5734,7 +5734,7 @@
   14.76      using \<open>open U\<close> and \<open>f x \<in> U\<close>
   14.77      unfolding tendsto_def by fast
   14.78    then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
   14.79 -    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono')
   14.80 +    using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
   14.81    then show ?thesis
   14.82      using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
   14.83  qed
    15.1 --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Tue Dec 08 20:21:59 2015 +0100
    15.2 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Wed Dec 09 17:35:22 2015 +0000
    15.3 @@ -28,7 +28,7 @@
    15.4      (fastforce
    15.5        simp: eventually_principal uniformly_on_def
    15.6        intro: bexI[where x="min a b" for a b]
    15.7 -      elim: eventually_elim1)+
    15.8 +      elim: eventually_mono)+
    15.9  
   15.10  lemma uniform_limitD:
   15.11    "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"
   15.12 @@ -103,7 +103,7 @@
   15.13    assumes "x \<in> S"
   15.14    shows "((\<lambda>y. f y x) ---> l x) F"
   15.15    using assms
   15.16 -  by (auto intro!: tendstoI simp: eventually_elim1 dest!: uniform_limitD)
   15.17 +  by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)
   15.18  
   15.19  lemma uniform_limit_theorem:
   15.20    assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)"
   15.21 @@ -115,7 +115,7 @@
   15.22    fix x assume "x \<in> A"
   15.23    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"
   15.24      using c ul
   15.25 -    by (auto simp: continuous_on_def eventually_elim1 tendsto_uniform_limitI)
   15.26 +    by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI)
   15.27    then show "(l ---> l x) (at x within A)"
   15.28      by (rule swap_uniform_limit) fact+
   15.29  qed
   15.30 @@ -451,7 +451,7 @@
   15.31    using assms(2)
   15.32  proof (rule metric_uniform_limit_imp_uniform_limit)
   15.33    show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (f x y) 0 \<le> dist (g x y) 0"
   15.34 -    using assms(1) by (rule eventually_elim1) (force simp add: dist_norm)
   15.35 +    using assms(1) by (rule eventually_mono) (force simp add: dist_norm)
   15.36  qed
   15.37  
   15.38  lemma uniform_limit_on_union:
   15.39 @@ -477,7 +477,7 @@
   15.40  
   15.41  lemma uniform_limit_on_subset:
   15.42    "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
   15.43 -  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono')
   15.44 +  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
   15.45  
   15.46  lemma uniformly_convergent_add:
   15.47    "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
    16.1 --- a/src/HOL/NSA/HyperDef.thy	Tue Dec 08 20:21:59 2015 +0100
    16.2 +++ b/src/HOL/NSA/HyperDef.thy	Wed Dec 09 17:35:22 2015 +0000
    16.3 @@ -243,7 +243,7 @@
    16.4  apply (simp add: omega_def star_of_def star_n_eq_iff)
    16.5  apply clarify
    16.6  apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
    16.7 -apply (erule eventually_mono')
    16.8 +apply (erule eventually_mono)
    16.9  apply auto
   16.10  done
   16.11  
    17.1 --- a/src/HOL/NSA/NSA.thy	Tue Dec 08 20:21:59 2015 +0100
    17.2 +++ b/src/HOL/NSA/NSA.thy	Wed Dec 09 17:35:22 2015 +0000
    17.3 @@ -1960,7 +1960,7 @@
    17.4       "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \<in> HFinite"
    17.5  apply (rule FreeUltrafilterNat_HFinite)
    17.6  apply (rule_tac x = "u + 1" in exI)
    17.7 -apply (auto elim: eventually_elim1)
    17.8 +apply (auto elim: eventually_mono)
    17.9  done
   17.10  
   17.11  lemma HInfinite_FreeUltrafilterNat:
   17.12 @@ -1969,7 +1969,7 @@
   17.13  apply (simp add: HFinite_FreeUltrafilterNat_iff)
   17.14  apply (rule allI, drule_tac x="u + 1" in spec)
   17.15  apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
   17.16 -apply (auto elim: eventually_elim1)
   17.17 +apply (auto elim: eventually_mono)
   17.18  done
   17.19  
   17.20  lemma lemma_Int_HI:
   17.21 @@ -2106,7 +2106,7 @@
   17.22  apply (simp add: omega_def)
   17.23  apply (rule FreeUltrafilterNat_HInfinite)
   17.24  apply clarify
   17.25 -apply (rule_tac u1 = "u-1" in eventually_mono' [OF FreeUltrafilterNat_nat_gt_real])
   17.26 +apply (rule_tac u1 = "u-1" in eventually_mono [OF FreeUltrafilterNat_nat_gt_real])
   17.27  apply auto
   17.28  done
   17.29  
   17.30 @@ -2200,7 +2200,7 @@
   17.31       ==> star_n X - star_of x \<in> Infinitesimal"
   17.32  unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
   17.33  by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
   17.34 -         intro: order_less_trans elim!: eventually_elim1)
   17.35 +         intro: order_less_trans elim!: eventually_mono)
   17.36  
   17.37  lemma real_seq_to_hypreal_approx:
   17.38       "\<forall>n. norm(X n - x) < inverse(real(Suc n))
   17.39 @@ -2217,6 +2217,6 @@
   17.40        ==> star_n X - star_n Y \<in> Infinitesimal"
   17.41  unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
   17.42  by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
   17.43 -         intro: order_less_trans elim!: eventually_elim1)
   17.44 +         intro: order_less_trans elim!: eventually_mono)
   17.45  
   17.46  end
    18.1 --- a/src/HOL/NSA/Star.thy	Tue Dec 08 20:21:59 2015 +0100
    18.2 +++ b/src/HOL/NSA/Star.thy	Wed Dec 09 17:35:22 2015 +0000
    18.3 @@ -316,7 +316,7 @@
    18.4        HNatInfinite_FreeUltrafilterNat_iff
    18.5        Infinitesimal_FreeUltrafilterNat_iff2)
    18.6  apply (drule_tac x="Suc m" in spec)
    18.7 -apply (auto elim!: eventually_elim1)
    18.8 +apply (auto elim!: eventually_mono)
    18.9  done
   18.10  
   18.11  lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
    19.1 --- a/src/HOL/NSA/StarDef.thy	Tue Dec 08 20:21:59 2015 +0100
    19.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Dec 09 17:35:22 2015 +0000
    19.3 @@ -136,7 +136,7 @@
    19.4    "\<lbrakk>p \<equiv> eventually (\<lambda>n. P n) \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
    19.5      \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
    19.6  apply (rule eq_reflection)
    19.7 -apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1)
    19.8 +apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_mono)
    19.9  done
   19.10  
   19.11  lemma transfer_fun_eq [transfer_intro]:
    20.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Tue Dec 08 20:21:59 2015 +0100
    20.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Wed Dec 09 17:35:22 2015 +0000
    20.3 @@ -727,7 +727,7 @@
    20.4      lim_0: "(\<lambda>i. \<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) ----> 0"
    20.5    from order_tendstoD[OF lim_0, of "\<infinity>"]
    20.6    obtain i where f_s_fin: "(\<integral>\<^sup>+ x. ereal (norm (f x - s i x)) \<partial>M) < \<infinity>"
    20.7 -    by (metis (mono_tags, lifting) eventually_False_sequentially eventually_elim1
    20.8 +    by (metis (mono_tags, lifting) eventually_False_sequentially eventually_mono
    20.9                less_ereal.simps(4) zero_ereal_def)
   20.10  
   20.11    have [measurable]: "\<And>i. s i \<in> borel_measurable M"
   20.12 @@ -2417,7 +2417,7 @@
   20.13        have "eventually (\<lambda>n. x \<le> X n) sequentially"
   20.14          unfolding filterlim_at_top_ge[where c=x] by auto
   20.15        then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) ----> f x"
   20.16 -        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_elim1)
   20.17 +        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
   20.18      qed
   20.19      fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
   20.20        by (auto split: split_indicator)
    21.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Dec 08 20:21:59 2015 +0100
    21.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Wed Dec 09 17:35:22 2015 +0000
    21.3 @@ -221,7 +221,7 @@
    21.4        using \<open>x \<in> I\<close> \<open>open I\<close> X(2)
    21.5        apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff
    21.6                  integrable_const X q)
    21.7 -      apply (elim eventually_elim1)
    21.8 +      apply (elim eventually_mono)
    21.9        apply (intro convex_le_Inf_differential)
   21.10        apply (auto simp: interior_open q)
   21.11        done
    22.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Dec 08 20:21:59 2015 +0100
    22.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 09 17:35:22 2015 +0000
    22.3 @@ -750,7 +750,7 @@
    22.4      with borel have "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> h x \<le> 0"
    22.5        by (auto simp add: null_sets_density_iff)
    22.6      with pos sets.sets_into_space have "AE x in M. x \<notin> A"
    22.7 -      by (elim eventually_elim1) (auto simp: not_le[symmetric])
    22.8 +      by (elim eventually_mono) (auto simp: not_le[symmetric])
    22.9      then have "A \<in> null_sets M"
   22.10        using \<open>A \<in> sets M\<close> by (simp add: AE_iff_null_sets)
   22.11      with ac show "A \<in> null_sets N"
    23.1 --- a/src/HOL/Probability/Stream_Space.thy	Tue Dec 08 20:21:59 2015 +0100
    23.2 +++ b/src/HOL/Probability/Stream_Space.thy	Wed Dec 09 17:35:22 2015 +0000
    23.3 @@ -238,7 +238,7 @@
    23.4    { fix n have "AE x in stream_space M. P (x !! n)"
    23.5      proof (induct n)
    23.6        case 0 with P show ?case
    23.7 -        by (subst AE_stream_space) (auto elim!: eventually_elim1)
    23.8 +        by (subst AE_stream_space) (auto elim!: eventually_mono)
    23.9      next
   23.10        case (Suc n) then show ?case
   23.11          by (subst AE_stream_space) auto
    24.1 --- a/src/HOL/Topological_Spaces.thy	Tue Dec 08 20:21:59 2015 +0100
    24.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Dec 09 17:35:22 2015 +0000
    24.3 @@ -471,7 +471,7 @@
    24.4  
    24.5  lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
    24.6    by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
    24.7 -           elim: eventually_elim2 eventually_elim1)
    24.8 +           elim: eventually_elim2 eventually_mono)
    24.9  
   24.10  lemma eventually_at_split:
   24.11    "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   24.12 @@ -551,7 +551,7 @@
   24.13    fix a assume "a < max x y"
   24.14    then show "eventually (\<lambda>x. a < max (X x) (Y x)) net"
   24.15      using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
   24.16 -    by (auto simp: less_max_iff_disj elim: eventually_elim1)
   24.17 +    by (auto simp: less_max_iff_disj elim: eventually_mono)
   24.18  next
   24.19    fix a assume "max x y < a"
   24.20    then show "eventually (\<lambda>x. max (X x) (Y x) < a) net"
   24.21 @@ -572,7 +572,7 @@
   24.22    fix a assume "min x y < a"
   24.23    then show "eventually (\<lambda>x. min (X x) (Y x) < a) net"
   24.24      using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
   24.25 -    by (auto simp: min_less_iff_disj elim: eventually_elim1)
   24.26 +    by (auto simp: min_less_iff_disj elim: eventually_mono)
   24.27  qed
   24.28  
   24.29  lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
   24.30 @@ -613,14 +613,14 @@
   24.31    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
   24.32        and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   24.33    shows "(f ---> l) F"
   24.34 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
   24.35 +  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   24.36  
   24.37  lemma decreasing_tendsto:
   24.38    fixes f :: "_ \<Rightarrow> 'a::order_topology"
   24.39    assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
   24.40        and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
   24.41    shows "(f ---> l) F"
   24.42 -  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
   24.43 +  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   24.44  
   24.45  lemma tendsto_sandwich:
   24.46    fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
   24.47 @@ -773,7 +773,7 @@
   24.48  lemma tendsto_at_within_iff_tendsto_nhds:
   24.49    "(g ---> g l) (at l within S) \<longleftrightarrow> (g ---> g l) (inf (nhds l) (principal S))"
   24.50    unfolding tendsto_def eventually_at_filter eventually_inf_principal
   24.51 -  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
   24.52 +  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
   24.53  
   24.54  subsection \<open>Limits on sequences\<close>
   24.55  
   24.56 @@ -1152,7 +1152,7 @@
   24.57    {
   24.58      fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
   24.59      with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
   24.60 -      by (auto elim: eventually_elim1 simp: subset_eq)
   24.61 +      by (auto elim: eventually_mono simp: subset_eq)
   24.62    }
   24.63    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)"
   24.64      by (intro exI[of _ A]) (auto simp: tendsto_def)
   24.65 @@ -1187,7 +1187,7 @@
   24.66      by (auto simp: eventually_inf_principal eventually_nhds)
   24.67    moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
   24.68    ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
   24.69 -    by (auto dest!: topological_tendstoD elim: eventually_elim1)
   24.70 +    by (auto dest!: topological_tendstoD elim: eventually_mono)
   24.71  qed
   24.72  
   24.73  lemma (in first_countable_topology) eventually_nhds_iff_sequentially:
   24.74 @@ -1243,7 +1243,7 @@
   24.75  lemma tendsto_at_iff_tendsto_nhds:
   24.76    "g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
   24.77    unfolding tendsto_def eventually_at_filter
   24.78 -  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
   24.79 +  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
   24.80  
   24.81  lemma tendsto_compose:
   24.82    "g -- l --> g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
   24.83 @@ -1758,7 +1758,7 @@
   24.84    with \<open>finite D\<close> have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
   24.85      by (simp add: eventually_ball_finite)
   24.86    with \<open>s \<subseteq> \<Union>D\<close> have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
   24.87 -    by (auto elim!: eventually_mono')
   24.88 +    by (auto elim!: eventually_mono)
   24.89    thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
   24.90      by (simp add: eventually_nhds subset_eq)
   24.91  qed
    25.1 --- a/src/HOL/Transcendental.thy	Tue Dec 08 20:21:59 2015 +0100
    25.2 +++ b/src/HOL/Transcendental.thy	Wed Dec 09 17:35:22 2015 +0000
    25.3 @@ -2510,7 +2510,7 @@
    25.4    unfolding powr_def
    25.5  proof (rule filterlim_If)
    25.6    from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
    25.7 -    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
    25.8 +    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
    25.9  qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
   25.10  
   25.11  lemma continuous_powr:
   25.12 @@ -2544,12 +2544,12 @@
   25.13    unfolding powr_def
   25.14  proof (rule filterlim_If)
   25.15    from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
   25.16 -    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
   25.17 +    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
   25.18  next
   25.19    { assume "a = 0"
   25.20      with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0"
   25.21        by (auto simp add: filterlim_at eventually_inf_principal le_less
   25.22 -               elim: eventually_elim1 intro: tendsto_mono inf_le1)
   25.23 +               elim: eventually_mono intro: tendsto_mono inf_le1)
   25.24      then have "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))"
   25.25        by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
   25.26                         filterlim_tendsto_pos_mult_at_bot[OF _ \<open>0 < b\<close>]
   25.27 @@ -2571,7 +2571,7 @@
   25.28      from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
   25.29        unfolding isCont_def by (rule order_tendstoD(1))
   25.30      with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
   25.31 -      by (auto simp: eventually_at_filter powr_def elim: eventually_elim1)
   25.32 +      by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
   25.33    qed
   25.34  qed
   25.35  
   25.36 @@ -2610,7 +2610,7 @@
   25.37                       filterlim_tendsto_neg_mult_at_bot assms)
   25.38    also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) ---> (0::real)) F"
   25.39      using f filterlim_at_top_dense[of f F]
   25.40 -    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_elim1)
   25.41 +    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_mono)
   25.42    finally show ?thesis .
   25.43  qed
   25.44  
   25.45 @@ -2657,7 +2657,7 @@
   25.46      apply (auto simp add: field_simps)
   25.47      done
   25.48    then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
   25.49 -    by (rule eventually_elim1) (erule powr_realpow)
   25.50 +    by (rule eventually_mono) (erule powr_realpow)
   25.51    show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
   25.52      by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
   25.53  qed auto