--- 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)"
--- 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:
--- 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
--- 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:
--- 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
--- 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:
--- 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"
--- 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
--- 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>
--- 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
--- 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"
--- 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]:
--- 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
--- 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
--- 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>
--- 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
--- 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
--- 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 =
--- 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]:
--- 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)
--- 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
--- 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"
--- 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
--- 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
--- 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