# HG changeset patch # User paulson # Date 1449682522 0 # Node ID 3c5040d5694a35c1980b31bf3d263b7042566b29 # Parent 81d34cf268d8e599ebc99e6b3ac9ac5f3af891d0 sorted out eventually_mono diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Deriv.thy Wed Dec 09 17:35:22 2015 +0000 @@ -218,7 +218,7 @@ lemma tendsto_at_iff_tendsto_nhds_within: "f x = y \ (f ---> y) (at x within s) \ (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 (\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 "(\ ---> 0) (at_right 0)" by (rule tendsto_norm_zero_cancel) with \ have "filterlim \ (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 "((\t. f' (\ t) / g' (\ t)) ---> x) (at_right 0)" by (rule_tac filterlim_compose[of _ _ _ \]) ultimately have "((\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 \ ?thesis" by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter) finally show ?thesis . @@ -1753,7 +1753,7 @@ moreover have "eventually (\t. 0 < g t) (at_right 0)" "eventually (\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: "((\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 (\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 "((\t. norm ((f a - x * g a) * inverse (g t))) ---> norm ((f a - x * g a) * 0)) (at_right 0)" diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Filter.thy --- a/src/HOL/Filter.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Filter.thy Wed Dec 09 17:35:22 2015 +0000 @@ -67,11 +67,6 @@ by (auto intro: always_eventually) lemma eventually_mono: - "(\x. P x \ Q x) \ eventually P F \ eventually Q F" - unfolding eventually_def - by (rule is_filter.mono [OF is_filter_Rep_filter]) - -lemma eventually_mono': "\eventually P F; \x. P x \ Q x\ \ eventually Q F" unfolding eventually_def by (blast intro: is_filter.mono [OF is_filter_Rep_filter]) @@ -91,7 +86,7 @@ have "eventually (\x. (P x \ Q x) \ 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 (\x. P x \ Q x) F \ eventually P F \ eventually Q F" by (auto intro: eventually_conj elim: eventually_rev_mp) -lemma eventually_elim1: - assumes "eventually (\i. P i) F" - assumes "\i. P i \ Q i" - shows "eventually (\i. Q i) F" - using assms by (auto elim!: eventually_rev_mp) - lemma eventually_elim2: assumes "eventually (\i. P i) F" assumes "eventually (\i. Q i) F" @@ -135,10 +124,10 @@ proof assume "\\<^sub>Fx in F. \y. P x y" then have "\\<^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 "\Y. \\<^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 \ \ eventually Q F \ \ eventually (\x. P x \ Q x) F" by (auto intro: eventually_mp) @@ -152,7 +141,7 @@ proof - from assms have "eventually (\x. P x \ Q x) F" and "eventually (\x. Q x \ 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 \ F'" and "F \ F''" thus "F \ 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 \ sup F F'" and "F' \ sup F F'" unfolding le_filter_def eventually_sup by simp_all } { assume "F \ F''" and "F' \ F''" thus "sup F F' \ F''" @@ -434,7 +423,7 @@ assume "?F P" then guess X .. moreover assume "\x. P x \ 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)) \ eventually (\x. x \ s \ 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="\x. x \ A" in allE) - apply (auto elim: eventually_elim1) + apply (auto elim: eventually_mono) done lemma principal_inject[iff]: "principal A = principal B \ A = B" @@ -877,7 +866,7 @@ lemma filterlim_at_top: fixes f :: "'a \ ('b::linorder)" shows "(LIM x F. f x :> at_top) \ (\Z. eventually (\x. Z \ 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 \ eventually (\x. f x \ (g x::'a::linorder)) F \ @@ -887,7 +876,7 @@ lemma filterlim_at_top_dense: fixes f :: "'a \ ('b::unbounded_dense_linorder)" shows "(LIM x F. f x :> at_top) \ (\Z. eventually (\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 \ ('b::linorder)" shows "(LIM x F. f x :> at_bot) \ (\Z. eventually (\x. f x \ 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 \ ('b::{dense_linorder, no_bot})" @@ -935,12 +924,12 @@ assume "\Z. eventually (\x. f x \ Z) F" hence "eventually (\x. f x \ Z') F" by auto thus "eventually (\x. f x < Z) F" - apply (rule eventually_mono') + apply (rule eventually_mono) using 1 by auto next fix Z :: 'b show "\Z. eventually (\x. f x < Z) F \ eventually (\x. f x \ 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 *: "\Z\c. eventually (\x. Z \ f x) F" with *[THEN spec, of "min Z c"] show "eventually (\x. Z \ f x) F" - by (auto elim!: eventually_elim1) + by (auto elim!: eventually_mono) qed simp lemma filterlim_at_bot_lt: diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Finite_Set.thy Wed Dec 09 17:35:22 2015 +0000 @@ -1787,4 +1787,118 @@ hide_const (open) Finite_Set.fold + +subsection "Infinite Sets" + +text \ + Some elementary facts about infinite sets, mostly by Stephan Merz. + Beware! Because "infinite" merely abbreviates a negation, these + lemmas may not work well with \blast\. +\ + +abbreviation infinite :: "'a set \ bool" + where "infinite S \ \ finite S" + +text \ + Infinite sets are non-empty, and if we remove some elements from an + infinite set, the result is still infinite. +\ + +lemma infinite_imp_nonempty: "infinite S \ S \ {}" + by auto + +lemma infinite_remove: "infinite S \ 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 \ infinite (S \ T)" + by simp + +lemma infinite_Un: "infinite (S \ T) \ infinite S \ infinite T" + by simp + +lemma infinite_super: + assumes T: "S \ 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: "\A. X A \ \x\A. X (A - {x}) \ infinite (A - {x})" + shows "infinite A" +proof + assume "finite A" + then show False using \X A\ + proof (induction rule: finite_psubset_induct) + case (psubset A) + then obtain x where "x \ A" "X (A - {x}) \ 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 \x \ A\ apply blast + by (simp add: \X (A - {x})\) + qed +qed + +text \ + For any function with infinite domain and finite range there is some + element that is the image of infinitely many domain elements. In + particular, any infinite sequence of elements from a finite set + contains some element that occurs infinitely often. +\ + +lemma inf_img_fin_dom': + assumes img: "finite (f ` A)" and dom: "infinite A" + shows "\y \ f ` A. infinite (f -` {y} \ A)" +proof (rule ccontr) + have "A \ (\y\f ` A. f -` {y} \ A)" by auto + moreover + assume "\ ?thesis" + with img have "finite (\y\f ` A. f -` {y} \ 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 \ f`A" and "infinite (f -` {y} \ 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 "\y \ 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 \ 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) \ finite S" + by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom) + end diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Library/Extended_Real.thy Wed Dec 09 17:35:22 2015 +0000 @@ -2444,7 +2444,7 @@ then have S: "open S" "ereal x \ ereal ` S" by (simp_all add: inj_image_mem_iff) show "eventually (\x. real_of_ereal (f x) \ 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]: "((\n. ereal (f n)) ---> ereal x) net \ (f ---> x) net" @@ -2456,7 +2456,7 @@ fix l :: ereal assume "\r. eventually (\x. ereal r < f x) F" from this[THEN spec, of "real_of_ereal l"] have "l \ \ \ eventually (\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 (\z. f z \ {..< B}) F" by auto ultimately show "eventually (\z. f z \ S) F" - by (auto elim!: eventually_elim1) + by (auto elim!: eventually_mono) next fix x assume "\S. open S \ -\ \ S \ eventually (\x. f x \ S) F" @@ -2571,7 +2571,7 @@ by auto from tendsto[THEN topological_tendstoD, OF this] show "eventually (\x. ereal (real_of_ereal (f x)) \ S) net" - by (elim eventually_elim1) (auto simp: ereal_real) + by (elim eventually_mono) (auto simp: ereal_real) qed lemma ereal_mult_cancel_left: diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Wed Dec 09 17:35:22 2015 +0000 @@ -8,71 +8,7 @@ imports Main begin -subsection "Infinite Sets" - -text \ - Some elementary facts about infinite sets, mostly by Stephan Merz. - Beware! Because "infinite" merely abbreviates a negation, these - lemmas may not work well with \blast\. -\ - -abbreviation infinite :: "'a set \ bool" - where "infinite S \ \ finite S" - -text \ - Infinite sets are non-empty, and if we remove some elements from an - infinite set, the result is still infinite. -\ - -lemma infinite_imp_nonempty: "infinite S \ S \ {}" - by auto - -lemma infinite_remove: "infinite S \ 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 \ infinite (S \ T)" - by simp - -lemma infinite_Un: "infinite (S \ T) \ infinite S \ infinite T" - by simp - -lemma infinite_super: - assumes T: "S \ 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: "\A. X A \ \x\A. X (A - {x}) \ infinite (A - {x})" - shows "infinite A" -proof - assume "finite A" - then show False using \X A\ - by(induction rule: finite_psubset_induct)(meson Diff_subset card_Diff1_less card_psubset finite_Diff step) -qed - -text \As a concrete example, we prove that the set of natural numbers is infinite.\ +text \The set of natural numbers is infinite.\ lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \ (\m. \n\m. n \ S)" using frequently_cofinite[of "\x. x \ S"] @@ -99,8 +35,9 @@ \ lemma unbounded_k_infinite: "\m>k. \n>m. n \ S \ 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) \ R" by simp @@ -114,45 +51,6 @@ then show False by simp qed -text \ - For any function with infinite domain and finite range there is some - element that is the image of infinitely many domain elements. In - particular, any infinite sequence of elements from a finite set - contains some element that occurs infinitely often. -\ - -lemma inf_img_fin_dom': - assumes img: "finite (f ` A)" and dom: "infinite A" - shows "\y \ f ` A. infinite (f -` {y} \ A)" -proof (rule ccontr) - have "A \ (\y\f ` A. f -` {y} \ A)" by auto - moreover - assume "\ ?thesis" - with img have "finite (\y\f ` A. f -` {y} \ 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 \ f`A" and "infinite (f -` {y} \ 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 "\y \ 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 \ 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) \ finite S" - by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom) - text \The set of integers is also infinite.\ lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \ 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 \ (MOST x. P x \ Q x) \ (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 \ MOST x. Q x \ INFM x. P x \ 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 \Properties of quantifiers with injective functions.\ @@ -272,7 +170,7 @@ lemma INFM_EX: "(\\<^sub>\x. P x) \ (\x. P x)" by (fact frequently_ex) lemma ALL_MOST: "\x. P x \ \\<^sub>\x. P x" by (fact always_eventually) lemma INFM_mono: "\\<^sub>\x. P x \ (\x. P x \ Q x) \ \\<^sub>\x. Q x" by (fact frequently_elim1) -lemma MOST_mono: "\\<^sub>\x. P x \ (\x. P x \ Q x) \ \\<^sub>\x. Q x" by (fact eventually_elim1) +lemma MOST_mono: "\\<^sub>\x. P x \ (\x. P x \ Q x) \ \\<^sub>\x. Q x" by (fact eventually_mono) lemma INFM_disj_distrib: "(\\<^sub>\x. P x \ Q x) \ (\\<^sub>\x. P x) \ (\\<^sub>\x. Q x)" by (fact frequently_disj_iff) lemma MOST_rev_mp: "\\<^sub>\x. P x \ \\<^sub>\x. P x \ Q x \ \\<^sub>\x. Q x" by (fact eventually_rev_mp) lemma MOST_conj_distrib: "(\\<^sub>\x. P x \ Q x) \ (\\<^sub>\x. P x) \ (\\<^sub>\x. Q x)" by (fact eventually_conj_iff) @@ -331,7 +229,7 @@ lemma le_enumerate: assumes S: "infinite S" shows "n \ enumerate S n" - using S + using S proof (induct n) case 0 then show ?case by simp diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Library/Liminf_Limsup.thy Wed Dec 09 17:35:22 2015 +0000 @@ -100,7 +100,7 @@ lemma Liminf_eq: assumes "eventually (\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 (\x. f x \ g x) F" @@ -116,7 +116,7 @@ lemma Limsup_eq: assumes "eventually (\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: "\ trivial_limit F" @@ -167,7 +167,7 @@ proof - have "eventually (\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 "\P. eventually P F \ y < INFIMUM (Collect P) X" if "y < C" and y: "\yx. y < X x) F" for y P @@ -218,7 +218,7 @@ then have "eventually (\x. y < f x) F" using lim[THEN topological_tendstoD, of "{y <..}"] by auto then have "eventually (\x. f0 \ f x) F" - using discrete by (auto elim!: eventually_elim1) + using discrete by (auto elim!: eventually_mono) then have "INFIMUM {x. f0 \ f x} f \ y" by (rule upper) moreover have "f0 \ INFIMUM {x. f0 \ f x} f" @@ -257,7 +257,7 @@ then have "eventually (\x. f x < y) F" using lim[THEN topological_tendstoD, of "{..< y}"] by auto then have "eventually (\x. f x \ 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 \ SUPREMUM {x. f x \ f0} f" by (rule lower) moreover have "SUPREMUM {x. f x \ f0} f \ 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 (\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 (\x. a < f x) F" - by (auto elim!: eventually_elim1 dest: less_INF_D) + by (auto elim!: eventually_mono dest: less_INF_D) qed lemma tendsto_iff_Liminf_eq_Limsup: diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Limits.thy Wed Dec 09 17:35:22 2015 +0000 @@ -83,7 +83,7 @@ show "0 < max K 1" by simp next show "eventually (\x. norm (f x) \ 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 (\x. dist (f x) a < norm a) F" by (rule tendstoD) then have "eventually (\x. f x \ 0) F" - unfolding dist_norm by (auto elim!: eventually_elim1) + unfolding dist_norm by (auto elim!: eventually_mono) with a have "eventually (\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 (\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 (\x. x < inverse Z) (nhds 0)" by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\inverse Z\"]) then show "eventually (\x. x \ 0 \ x \ {0<..} \ Z \ 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 \ eventually (\x. 0 < f x) F \ 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 \0 < c\ have "eventually (\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 (\x. (Z / c * 2) \ 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 (\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 (\x. Z - (c - 1) \ g x) F" unfolding filterlim_at_top by auto ultimately show "eventually (\x. Z \ f x + g x) F" diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Dec 09 17:35:22 2015 +0000 @@ -886,7 +886,7 @@ finally have "dist (f (r n)) l < e" by simp } ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" - by (rule eventually_elim1) + by (rule eventually_mono) } hence "((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" by auto diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Dec 09 17:35:22 2015 +0000 @@ -3336,7 +3336,6 @@ subsection\Winding Numbers\ -text\The result is an integer, but it doesn't have type @{typ int}!\ definition winding_number:: "[real \ complex, complex] \ complex" where "winding_number \ z \ @n. \e > 0. \p. valid_path p \ z \ path_image p \ diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Dec 09 17:35:22 2015 +0000 @@ -290,13 +290,13 @@ unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto) lemma le_nhds: "F \ nhds a \ (\S. open S \ a \ S \ eventually (\x. x \ 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 \ nhds a \ (\e>0. eventually (\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 \ nhds a \ (\e>0. eventually (\x. dist x a \ 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 \Several results are easier using a "multiplied-out" variant. (I got this idea from Dieudonne's proof of the chain rule).\ @@ -2016,15 +2016,15 @@ case True have "eventually (\n. norm (f' n x u - g' x u) \ e * norm u) sequentially" using assms(3)[folded eventually_sequentially] and \0 < e\ and \x \ s\ - by (fast elim: eventually_elim1) + by (fast elim: eventually_mono) then show ?thesis - using \u = 0\ and \0 < e\ by (auto elim: eventually_elim1) + using \u = 0\ and \0 < e\ by (auto elim: eventually_mono) next case False with \0 < e\ have "0 < e / norm u" by simp then have "eventually (\n. norm (f' n x u - g' x u) \ e / norm u * norm u) sequentially" using assms(3)[folded eventually_sequentially] and \x \ s\ - by (fast elim: eventually_elim1) + by (fast elim: eventually_mono) then show ?thesis using \u \ 0\ by simp qed @@ -2250,7 +2250,7 @@ also have "(g has_field_derivative g' x) (at x) \ ((\x. \n. f n x) has_field_derivative g' x) (at x)" using eventually_nhds_in_nhd[OF \x \ interior s\] 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 "((\x. \n. f n x) has_field_derivative g' x) (at x)" . qed diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Wed Dec 09 17:35:22 2015 +0000 @@ -431,7 +431,7 @@ by (simp add: mono_set) } with P show "eventually (\x. f x \ S) net" - by (auto elim: eventually_elim1) + by (auto elim: eventually_mono) next fix y l assume S: "\S. open S \ mono_set S \ l \ S \ eventually (\x. f x \ S) net" @@ -470,7 +470,7 @@ have "f x \ S" by (simp add: inj_image_mem_iff) } with P show "eventually (\x. f x \ S) net" - by (auto elim: eventually_elim1) + by (auto elim: eventually_mono) next fix y l assume S: "\S. open S \ mono_set (uminus ` S) \ l \ S \ eventually (\x. f x \ S) net" diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Dec 09 17:35:22 2015 +0000 @@ -224,7 +224,7 @@ hence "eventually (\x. \i. f x $ i \ A i) net" by (rule eventually_all_finite) thus "eventually (\x. f x \ S) net" - by (rule eventually_elim1, simp add: S) + by (rule eventually_mono, simp add: S) qed lemma tendsto_vec_lambda [tendsto_intros]: diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Dec 09 17:35:22 2015 +0000 @@ -73,8 +73,6 @@ shows "finite S \ S \ {} \ a \ Inf S \ (\x\S. a \ x)" by (metis cInf_eq_Min Min_le_iff) -(*declare not_less[simp] not_le[simp]*) - lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Dec 09 17:35:22 2015 +0000 @@ -2310,7 +2310,7 @@ by (auto simp add: tendsto_iff eventually_at_infinity) lemma Lim_eventually: "eventually (\x. f x = l) net \ (f ---> l) net" - by (rule topological_tendstoI, auto elim: eventually_mono') + by (rule topological_tendstoI, auto elim: eventually_mono) text\The expected monotonicity property.\ @@ -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 \ S" from A(3)[OF this] \\n. f n \ A n\ show "eventually (\x. f x \ 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 (\x. dist (f x) 0 \ 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 "\n. f n \ S \ dist x (f n) \ a" using a by simp then have "eventually (\n. dist x (f n) \ a) sequentially" - by (rule eventually_mono, simp add: f(1)) + by (simp add: f(1)) have "dist x y \ a" apply (rule Lim_dist_ubound [of sequentially f]) apply (rule trivial_limit_sequentially) @@ -3808,7 +3808,7 @@ by auto moreover have ev_Z: "\z. z \ Z \ eventually (\x. x \ 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 "(\B \ Z. finite B \ U \ \B \ {})" proof (intro allI impI) fix B assume "finite B" "B \ Z" @@ -4485,7 +4485,7 @@ by auto } ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" - by (rule eventually_elim1) + by (rule eventually_mono) } then have *: "((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp @@ -5559,7 +5559,7 @@ then have "eventually (\n. x n \ T) sequentially" using assms T_def by (auto simp: tendsto_def) then show "eventually (\n. (f \ x) n \ 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 U\ and \f x \ U\ unfolding tendsto_def by fast then have "eventually (\y. f y \ a) (at x within s)" - using \a \ U\ by (fast elim: eventually_mono') + using \a \ U\ by (fast elim: eventually_mono) then show ?thesis using \f x \ a\ by (auto simp: dist_commute zero_less_dist_iff eventually_at) qed diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Multivariate_Analysis/Uniform_Limit.thy --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Wed Dec 09 17:35:22 2015 +0000 @@ -28,7 +28,7 @@ (fastforce simp: eventually_principal uniformly_on_def intro: bexI[where x="min a b" for a b] - elim: eventually_elim1)+ + elim: eventually_mono)+ lemma uniform_limitD: "uniform_limit S f l F \ e > 0 \ \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e" @@ -103,7 +103,7 @@ assumes "x \ S" shows "((\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: "\\<^sub>F n in F. continuous_on A (f n)" @@ -115,7 +115,7 @@ fix x assume "x \ A" then have "\\<^sub>F n in F. (f n ---> f n x) (at x within A)" "((\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 "\\<^sub>F x in F. \y\S. dist (f x y) 0 \ 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 \ I \ J \ 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 \ uniformly_convergent_on A g\ diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/HyperDef.thy --- a/src/HOL/NSA/HyperDef.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/NSA/HyperDef.thy Wed Dec 09 17:35:22 2015 +0000 @@ -243,7 +243,7 @@ apply (simp add: omega_def star_of_def star_n_eq_iff) apply clarify apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE]) -apply (erule eventually_mono') +apply (erule eventually_mono) apply auto done diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/NSA/NSA.thy Wed Dec 09 17:35:22 2015 +0000 @@ -1960,7 +1960,7 @@ "eventually (\n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \ 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 \ 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: "\n. norm(X n - x) < inverse(real(Suc n)) @@ -2217,6 +2217,6 @@ ==> star_n X - star_n Y \ Infinitesimal" unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat - intro: order_less_trans elim!: eventually_elim1) + intro: order_less_trans elim!: eventually_mono) end diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/Star.thy --- a/src/HOL/NSA/Star.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/NSA/Star.thy Wed Dec 09 17:35:22 2015 +0000 @@ -316,7 +316,7 @@ HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2) apply (drule_tac x="Suc m" in spec) -apply (auto elim!: eventually_elim1) +apply (auto elim!: eventually_mono) done lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y = diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/NSA/StarDef.thy Wed Dec 09 17:35:22 2015 +0000 @@ -136,7 +136,7 @@ "\p \ eventually (\n. P n) \; x \ star_n X; y \ star_n Y\ \ (if p then x else y) \ star_n (\n. if P n then X n else Y n)" apply (rule eq_reflection) -apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_elim1) +apply (auto simp add: star_n_eq_iff transfer_not elim!: eventually_mono) done lemma transfer_fun_eq [transfer_intro]: diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Probability/Bochner_Integration.thy Wed Dec 09 17:35:22 2015 +0000 @@ -727,7 +727,7 @@ lim_0: "(\i. \\<^sup>+ x. ereal (norm (f x - s i x)) \M) ----> 0" from order_tendstoD[OF lim_0, of "\"] obtain i where f_s_fin: "(\\<^sup>+ x. ereal (norm (f x - s i x)) \M) < \" - 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]: "\i. s i \ borel_measurable M" @@ -2417,7 +2417,7 @@ have "eventually (\n. x \ X n) sequentially" unfolding filterlim_at_top_ge[where c=x] by auto then show "(\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) \ norm (f x)" by (auto split: split_indicator) diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Wed Dec 09 17:35:22 2015 +0000 @@ -221,7 +221,7 @@ using \x \ I\ \open I\ X(2) apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff integrable_const X q) - apply (elim eventually_elim1) + apply (elim eventually_mono) apply (intro convex_le_Inf_differential) apply (auto simp: interior_open q) done diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 09 17:35:22 2015 +0000 @@ -750,7 +750,7 @@ with borel have "A \ sets M" "AE x in M. x \ A \ h x \ 0" by (auto simp add: null_sets_density_iff) with pos sets.sets_into_space have "AE x in M. x \ A" - by (elim eventually_elim1) (auto simp: not_le[symmetric]) + by (elim eventually_mono) (auto simp: not_le[symmetric]) then have "A \ null_sets M" using \A \ sets M\ by (simp add: AE_iff_null_sets) with ac show "A \ null_sets N" diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Probability/Stream_Space.thy --- a/src/HOL/Probability/Stream_Space.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Probability/Stream_Space.thy Wed Dec 09 17:35:22 2015 +0000 @@ -238,7 +238,7 @@ { fix n have "AE x in stream_space M. P (x !! n)" proof (induct n) case 0 with P show ?case - by (subst AE_stream_space) (auto elim!: eventually_elim1) + by (subst AE_stream_space) (auto elim!: eventually_mono) next case (Suc n) then show ?case by (subst AE_stream_space) auto diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Topological_Spaces.thy Wed Dec 09 17:35:22 2015 +0000 @@ -471,7 +471,7 @@ lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)" by (auto simp: eventually_at_filter filter_eq_iff eventually_sup - elim: eventually_elim2 eventually_elim1) + elim: eventually_elim2 eventually_mono) lemma eventually_at_split: "eventually P (at (x::'a::linorder_topology)) \ eventually P (at_left x) \ eventually P (at_right x)" @@ -551,7 +551,7 @@ fix a assume "a < max x y" then show "eventually (\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 (\x. max (X x) (Y x) < a) net" @@ -572,7 +572,7 @@ fix a assume "min x y < a" then show "eventually (\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]: "((\x. x) ---> a) (at a within s)" @@ -613,14 +613,14 @@ assumes bdd: "eventually (\n. f n \ l) F" and en: "\x. x < l \ eventually (\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 :: "_ \ 'a::order_topology" assumes bdd: "eventually (\n. l \ f n) F" and en: "\x. l < x \ eventually (\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 \ 'b::order_topology" @@ -773,7 +773,7 @@ lemma tendsto_at_within_iff_tendsto_nhds: "(g ---> g l) (at l within S) \ (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 \Limits on sequences\ @@ -1152,7 +1152,7 @@ { fix F S assume "\n. F n \ A n" "open S" "x \ S" with A(3)[of S] have "eventually (\n. F n \ S) sequentially" - by (auto elim: eventually_elim1 simp: subset_eq) + by (auto elim: eventually_mono simp: subset_eq) } with A show "\A. (\i. open (A i)) \ (\i. x \ A i) \ (\F. (\n. F n \ A n) \ 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 "\n. f n \ s" "f ----> a" ultimately show "eventually (\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 \ (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 \ (f ---> l) F \ ((\x. g (f x)) ---> g l) F" @@ -1758,7 +1758,7 @@ with \finite D\ have "eventually (\y. y \ \D) (nhds y)" by (simp add: eventually_ball_finite) with \s \ \D\ have "eventually (\y. y \ s) (nhds y)" - by (auto elim!: eventually_mono') + by (auto elim!: eventually_mono) thus "\t. open t \ y \ t \ t \ - s" by (simp add: eventually_nhds subset_eq) qed diff -r 81d34cf268d8 -r 3c5040d5694a src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Dec 08 20:21:59 2015 +0100 +++ b/src/HOL/Transcendental.thy Wed Dec 09 17:35:22 2015 +0000 @@ -2510,7 +2510,7 @@ unfolding powr_def proof (rule filterlim_If) from f show "((\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 "((\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 \ 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 "((\x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \ 0}))" by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0] filterlim_tendsto_pos_mult_at_bot[OF _ \0 < b\] @@ -2571,7 +2571,7 @@ from DERIV_isCont[OF g] pos have "\\<^sub>F x in at x. 0 < g x" unfolding isCont_def by (rule order_tendstoD(1)) with pos show "\\<^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 \ ((\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 (\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 "(\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