remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
--- a/src/HOL/Deriv.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Deriv.thy Tue Apr 09 14:04:41 2013 +0200
@@ -1043,7 +1043,7 @@
moreover then 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_within at_def elim: eventually_elim1)
+ by (auto simp: eventually_at_filter elim: eventually_elim1)
qed simp_all
lemma DERIV_shift:
@@ -1055,6 +1055,17 @@
by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
tendsto_minus_cancel_left field_simps conj_commute)
+lemma isCont_If_ge:
+ fixes a :: "'a :: linorder_topology"
+ shows "continuous (at_left a) g \<Longrightarrow> (f ---> g a) (at_right a) \<Longrightarrow> isCont (\<lambda>x. if x \<le> a then g x else f x) a"
+ unfolding isCont_def continuous_within
+ apply (intro filterlim_split_at)
+ apply (subst filterlim_cong[OF refl refl, where g=g])
+ apply (simp_all add: eventually_at_filter less_le)
+ apply (subst filterlim_cong[OF refl refl, where g=f])
+ apply (simp_all add: eventually_at_filter less_le)
+ done
+
lemma lhopital_right_0:
fixes f0 g0 :: "real \<Rightarrow> real"
assumes f_0: "(f0 ---> 0) (at_right 0)"
@@ -1081,7 +1092,7 @@
and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0"
and f0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f0 x :> (f' x)"
and g0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g0 x :> (g' x)"
- unfolding eventually_within eventually_at by (auto simp: dist_real_def)
+ unfolding eventually_at eventually_at by (auto simp: dist_real_def)
have g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0"
using g0_neq_0 by (simp add: g_def)
@@ -1097,18 +1108,10 @@
note g = this
have "isCont f 0"
- using tendsto_const[of "0::real" "at 0"] f_0
- unfolding isCont_def f_def
- by (intro filterlim_split_at_real)
- (auto elim: eventually_elim1
- simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
-
+ unfolding f_def by (intro isCont_If_ge f_0 continuous_const)
+
have "isCont g 0"
- using tendsto_const[of "0::real" "at 0"] g_0
- unfolding isCont_def g_def
- by (intro filterlim_split_at_real)
- (auto elim: eventually_elim1
- simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
+ unfolding g_def by (intro isCont_If_ge g_0 continuous_const)
have "\<exists>\<zeta>. \<forall>x\<in>{0 <..< a}. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)"
proof (rule bchoice, rule)
@@ -1131,24 +1134,24 @@
qed
then guess \<zeta> ..
then have \<zeta>: "eventually (\<lambda>x. 0 < \<zeta> x \<and> \<zeta> x < x \<and> f x / g x = f' (\<zeta> x) / g' (\<zeta> x)) (at_right 0)"
- unfolding eventually_within eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
+ unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
moreover
from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
by eventually_elim auto
then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"])
- (auto intro: tendsto_const tendsto_ident_at_within)
+ (auto intro: tendsto_const tendsto_ident_at)
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_within filterlim_at)
+ by (auto elim!: eventually_elim1 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)
also have "?P \<longleftrightarrow> ?thesis"
- by (rule filterlim_cong) (auto simp: f_def g_def eventually_within)
+ by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter)
finally show ?thesis .
qed
@@ -1206,11 +1209,12 @@
and f0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV f x :> (f' x)"
and g0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV g x :> (g' x)"
and Df: "\<And>t. 0 < t \<Longrightarrow> t < a \<Longrightarrow> dist (f' t / g' t) x < e / 4"
- unfolding eventually_within_le by (auto simp: dist_real_def)
+ unfolding eventually_at_le by (auto simp: dist_real_def)
+
from Df have
"eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
- unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
+ unfolding eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
moreover
have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"
--- a/src/HOL/Limits.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Limits.thy Tue Apr 09 14:04:41 2013 +0200
@@ -12,10 +12,6 @@
imports Real_Vector_Spaces
begin
-(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
- Hence it was references as Limits.eventually_within, but now it is Basic_Topology.eventually_within *)
-lemmas eventually_within = eventually_within
-
subsection {* Filter going to infinity norm *}
definition at_infinity :: "'a::real_normed_vector filter" where
@@ -910,25 +906,36 @@
lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
-lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
- unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
- by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
+lemma filtermap_homeomorph:
+ assumes f: "continuous (at a) f"
+ assumes g: "continuous (at (f a)) g"
+ assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
+ shows "filtermap f (nhds a) = nhds (f a)"
+ unfolding filter_eq_iff eventually_filtermap eventually_nhds
+proof safe
+ fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
+ from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
+ show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
+next
+ fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
+ with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
+ obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
+ by (metis UNIV_I)
+ with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
+ by (force intro!: exI[of _ A])
+qed
-lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
- unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
- apply (intro allI ex_cong)
- apply (auto simp: dist_real_def field_simps)
- apply (erule_tac x="-x" in allE)
- apply simp
- done
+lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
+ by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
-lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
- unfolding at_def filtermap_nhds_shift[symmetric]
- by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
+ by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
+
+lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
- unfolding filtermap_at_shift[symmetric]
- by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
using filtermap_at_right_shift[of "-a" 0] by simp
@@ -941,15 +948,14 @@
"eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
-lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
- unfolding at_def filtermap_nhds_minus[symmetric]
- by (simp add: filter_eq_iff eventually_filtermap eventually_within)
+lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::'a::real_normed_vector)"
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
- by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
- by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
+ by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
lemma filterlim_at_left_to_right:
"filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
@@ -989,19 +995,19 @@
unfolding filterlim_uminus_at_top by simp
lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
- unfolding filterlim_at_top_gt[where c=0] eventually_within at_def
+ unfolding filterlim_at_top_gt[where c=0] eventually_at_filter
proof safe
fix Z :: real assume [arith]: "0 < Z"
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 \<in> - {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
+ 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)
qed
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 le_within_iff at_def eventually_elim1)
+ (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
lemma filterlim_inverse_at_bot_neg:
"LIM x (at_left (0::real)). inverse x :> at_bot"
@@ -1033,8 +1039,7 @@
have "(inverse ---> (0::real)) at_top"
by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
then show "filtermap inverse at_top \<le> at_right (0::real)"
- unfolding at_within_eq
- by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def)
+ by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
next
have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
@@ -1082,9 +1087,9 @@
then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity"
by (rule filtermap_mono)
also have "\<dots> \<le> at 0"
- using tendsto_inverse_0
- by (auto intro!: le_withinI exI[of _ 1]
- simp: eventually_filtermap eventually_at_infinity filterlim_def at_def)
+ using tendsto_inverse_0[where 'a='b]
+ by (auto intro!: exI[of _ 1]
+ simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity)
finally show "filtermap inverse (filtermap g F) \<le> at 0" .
next
assume "filtermap inverse (filtermap g F) \<le> at 0"
@@ -1094,9 +1099,8 @@
by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
qed
-lemma tendsto_inverse_0_at_top:
- "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
- by (metis at_top_le_at_infinity filterlim_at filterlim_inverse_at_iff filterlim_mono order_refl)
+lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
+ by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
text {*
@@ -1516,13 +1520,7 @@
lemma LIM_offset:
fixes a :: "'a::real_normed_vector"
shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
-apply (rule topological_tendstoI)
-apply (drule (2) topological_tendstoD)
-apply (simp only: eventually_at dist_norm)
-apply (clarify, rule_tac x=d in exI, safe)
-apply (drule_tac x="x + k" in spec)
-apply (simp add: algebra_simps)
-done
+ unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
lemma LIM_offset_zero:
fixes a :: "'a::real_normed_vector"
@@ -1717,7 +1715,7 @@
show "(f ---> f x) (at_left x)"
using `isCont f x` by (simp add: filterlim_at_split isCont_def)
show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
- using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
+ using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"])
qed simp
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Apr 09 14:04:41 2013 +0200
@@ -1167,7 +1167,7 @@
lemma differentiable_at_imp_differentiable_on:
"(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
- unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
+ by (metis differentiable_at_withinI differentiable_on_def)
definition "jacobian f net = matrix(frechet_derivative f net)"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Apr 09 14:04:41 2013 +0200
@@ -40,7 +40,7 @@
apply (simp add: norm_sgn sgn_zero_iff x)
done
thus ?thesis
- by (rule netlimit_within [of a UNIV, unfolded within_UNIV])
+ by (rule netlimit_within [of a UNIV])
qed simp
lemma FDERIV_conv_has_derivative:
@@ -80,7 +80,7 @@
using has_derivative_within' [of f f' x UNIV] by simp
lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
- unfolding has_derivative_within' has_derivative_at' by meson
+ unfolding has_derivative_within' has_derivative_at' by blast
lemma has_derivative_within_open:
"a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
@@ -252,7 +252,7 @@
lemma differentiable_on_eq_differentiable_at:
"open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
unfolding differentiable_on_def
- by (auto simp add: at_within_interior interior_open)
+ by (metis at_within_interior interior_open)
lemma differentiable_transform_within:
assumes "0 < d" and "x \<in> s" and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
@@ -317,7 +317,7 @@
lemma differentiable_imp_continuous_at:
"f differentiable at x \<Longrightarrow> continuous (at x) f"
- by(rule differentiable_imp_continuous_within[of _ x UNIV, unfolded within_UNIV])
+ by(rule differentiable_imp_continuous_within[of _ x UNIV])
lemma differentiable_imp_continuous_on:
"f differentiable_on s \<Longrightarrow> continuous_on s f"
@@ -326,7 +326,7 @@
lemma has_derivative_within_subset:
"(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
- unfolding has_derivative_within using Lim_within_subset by blast
+ unfolding has_derivative_within using tendsto_within_subset by blast
lemma differentiable_within_subset:
"f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable (at x within s)"
@@ -621,7 +621,7 @@
shows "f' = f''"
proof -
from assms(1) have *: "at x within {a<..<b} = at x"
- by (simp add: at_within_interior interior_open open_interval)
+ by (metis at_within_interior interior_open open_interval)
from assms(2,3) [unfolded *] show "f' = f''"
by (rule frechet_derivative_unique_at)
qed
@@ -1805,7 +1805,7 @@
assumes "(g has_vector_derivative g') (at x)"
assumes "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
- using has_vector_derivative_bilinear_within[where s=UNIV] assms by simp
+ using has_vector_derivative_bilinear_within[OF assms] .
lemma has_vector_derivative_at_within:
"(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Apr 09 14:04:41 2013 +0200
@@ -890,16 +890,16 @@
lemma Liminf_within:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
- unfolding Liminf_def eventually_within_less
+ unfolding Liminf_def eventually_at
proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
- fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
by (auto simp: zero_less_dist_iff dist_commute)
then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
next
fix d :: real assume "0 < d"
- then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
(auto intro!: INF_mono exI[of _ d] simp: dist_commute)
@@ -908,16 +908,16 @@
lemma Limsup_within:
fixes f :: "'a::metric_space => 'b::complete_lattice"
shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
- unfolding Limsup_def eventually_within_less
+ unfolding Limsup_def eventually_at
proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
- fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+ fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
by (auto simp: zero_less_dist_iff dist_commute)
then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
next
fix d :: real assume "0 < d"
- then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+ then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
(auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Apr 09 14:04:41 2013 +0200
@@ -39,9 +39,6 @@
shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
by (fact tendsto_within_open)
-lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
- by (fact tendsto_within_subset)
-
lemma continuous_on_union:
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
by (fact continuous_on_closed_Un)
@@ -1205,7 +1202,7 @@
definition
indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
(infixr "indirection" 70) where
- "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
+ "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
@@ -1215,7 +1212,7 @@
assume "trivial_limit (at a within S)"
thus "\<not> a islimpt S"
unfolding trivial_limit_def
- unfolding eventually_within eventually_at_topological
+ unfolding eventually_at_topological
unfolding islimpt_def
apply (clarsimp simp add: set_eq_iff)
apply (rename_tac T, rule_tac x=T in exI)
@@ -1225,7 +1222,7 @@
assume "\<not> a islimpt S"
thus "trivial_limit (at a within S)"
unfolding trivial_limit_def
- unfolding eventually_within eventually_at_topological
+ unfolding eventually_at_topological
unfolding islimpt_def
apply clarsimp
apply (rule_tac x=T in exI)
@@ -1292,11 +1289,11 @@
lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_iff eventually_within_le)
+ by (auto simp add: tendsto_iff eventually_at_le dist_nz)
lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_iff eventually_within_less)
+ by (auto simp add: tendsto_iff eventually_at dist_nz)
lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
@@ -1311,12 +1308,12 @@
text{* The expected monotonicity property. *}
-lemma Lim_within_empty: "(f ---> l) (net within {})"
- unfolding tendsto_def Limits.eventually_within by simp
-
-lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
- shows "(f ---> l) (net within (S \<union> T))"
- using assms unfolding tendsto_def Limits.eventually_within
+lemma Lim_within_empty: "(f ---> l) (at x within {})"
+ unfolding tendsto_def eventually_at_filter by simp
+
+lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
+ shows "(f ---> l) (at x within (S \<union> T))"
+ using assms unfolding tendsto_def eventually_at_filter
apply clarify
apply (drule spec, drule (1) mp, drule (1) mp)
apply (drule spec, drule (1) mp, drule (1) mp)
@@ -1324,17 +1321,16 @@
done
lemma Lim_Un_univ:
- "(f ---> l) (net within S) \<Longrightarrow> (f ---> l) (net within T) \<Longrightarrow> S \<union> T = UNIV
- ==> (f ---> l) net"
- by (metis Lim_Un within_UNIV)
+ "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow> S \<union> T = UNIV
+ ==> (f ---> l) (at x)"
+ by (metis Lim_Un)
text{* Interrelations between restricted and unrestricted limits. *}
-lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
- (* FIXME: rename *)
- unfolding tendsto_def Limits.eventually_within
- apply (clarify, drule spec, drule (1) mp, drule (1) mp)
- by (auto elim!: eventually_elim1)
+
+lemma Lim_at_within: (* FIXME: rename *)
+ "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
+ by (metis order_refl filterlim_mono subset_UNIV at_le)
lemma eventually_within_interior:
assumes "x \<in> interior S"
@@ -1343,7 +1339,7 @@
from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
{ assume "?lhs"
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
- unfolding Limits.eventually_within eventually_at_topological
+ unfolding eventually_at_topological
by auto
with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
by auto
@@ -1351,15 +1347,14 @@
unfolding eventually_at_topological by auto
} moreover
{ assume "?rhs" hence "?lhs"
- unfolding Limits.eventually_within
- by (auto elim: eventually_elim1)
+ by (auto elim: eventually_elim1 simp: eventually_at_filter)
} ultimately
show "?thesis" ..
qed
lemma at_within_interior:
"x \<in> interior S \<Longrightarrow> at x within S = at x"
- by (simp add: filter_eq_iff eventually_within_interior)
+ unfolding filter_eq_iff by (intro allI eventually_within_interior)
lemma Lim_within_LIMSEQ:
fixes a :: "'a::metric_space"
@@ -1386,17 +1381,14 @@
by (auto intro: cInf_lower)
with a have "a < f y" by (blast intro: less_le_trans) }
then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
- by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
+ by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
next
fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
- show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
- unfolding within_within_eq[symmetric]
- Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
- proof (safe intro!: exI[of _ y] y)
- fix z assume "x < z" "z \<in> I" "z < y"
- with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
- qed
+ then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
+ unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
+ then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
+ unfolding eventually_at_filter by eventually_elim simp
qed
qed
@@ -1540,7 +1532,7 @@
text{* These are special for limits out of the same vector space. *}
lemma Lim_within_id: "(id ---> a) (at a within s)"
- unfolding id_def by (rule tendsto_ident_at_within)
+ unfolding id_def by (rule tendsto_ident_at)
lemma Lim_at_id: "(id ---> a) (at a)"
unfolding id_def by (rule tendsto_ident_at)
@@ -1567,13 +1559,13 @@
lemma lim_within_interior:
"x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
- by (simp add: at_within_interior)
+ by (metis at_within_interior)
lemma netlimit_within_interior:
fixes x :: "'a::{t2_space,perfect_space}"
assumes "x \<in> interior S"
shows "netlimit (at x within S) = x"
-using assms by (simp add: at_within_interior netlimit_at)
+using assms by (metis at_within_interior netlimit_at)
text{* Transformation of limit. *}
@@ -1596,8 +1588,7 @@
shows "(g ---> l) (at x within S)"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>x. f x = g x) (at x within S)"
- unfolding eventually_within_less
- using assms(1,2) by auto
+ using assms(1,2) by (auto simp: dist_nz eventually_at)
show "(f ---> l) (at x within S)" by fact
qed
@@ -1622,7 +1613,7 @@
proof (rule Lim_transform_eventually)
show "(f ---> l) (at a within S)" by fact
show "eventually (\<lambda>x. f x = g x) (at a within S)"
- unfolding Limits.eventually_within eventually_at_topological
+ unfolding eventually_at_topological
by (rule exI [where x="- {b}"], simp add: open_Compl assms)
qed
@@ -1655,7 +1646,7 @@
assumes "a = b" "x = y" "S = T"
assumes "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
- unfolding tendsto_def Limits.eventually_within eventually_at_topological
+ unfolding tendsto_def eventually_at_topological
using assms by simp
lemma Lim_cong_at(*[cong add]*):
@@ -3759,7 +3750,7 @@
lemma continuous_within_subset:
"continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
==> continuous (at x within t) f"
- unfolding continuous_within by(metis Lim_within_subset)
+ unfolding continuous_within by(metis tendsto_within_subset)
lemma continuous_on_interior:
shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
@@ -3768,7 +3759,7 @@
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
- unfolding continuous_on_def tendsto_def Limits.eventually_within
+ unfolding continuous_on_def tendsto_def eventually_at_topological
by simp
text {* Characterization of various kinds of continuity in terms of sequences. *}
@@ -3783,7 +3774,7 @@
{ fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
fix T::"'b set" assume "open T" and "f a \<in> T"
with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
- unfolding continuous_within tendsto_def eventually_within_less by auto
+ unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
using x(2) `d>0` by simp
hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
@@ -4015,7 +4006,7 @@
lemma continuous_at_open:
shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
-unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
+unfolding continuous_within_topological [of x UNIV f]
unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
lemma continuous_imp_tendsto:
@@ -4181,7 +4172,7 @@
hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
using `a \<notin> U` by (fast elim: eventually_mono [rotated])
thus ?thesis
- using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
+ using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_at)
qed
lemma continuous_at_avoid:
@@ -4514,7 +4505,7 @@
proof (rule continuous_attains_sup [OF assms])
{ fix x assume "x\<in>s"
have "(dist a ---> dist a x) (at x within s)"
- by (intro tendsto_dist tendsto_const Lim_at_within tendsto_ident_at)
+ by (intro tendsto_dist tendsto_const tendsto_ident_at)
}
thus "continuous_on s (dist a)"
unfolding continuous_on ..
@@ -5350,7 +5341,7 @@
assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
proof -
from assms(1) have "continuous_on UNIV f"
- unfolding isCont_def continuous_on_def within_UNIV by simp
+ unfolding isCont_def continuous_on_def by simp
hence "open {x \<in> UNIV. f x \<in> s}"
using open_UNIV `open s` by (rule continuous_open_preimage)
thus "open (f -` s)"
@@ -5508,14 +5499,13 @@
text{* Limits relative to a union. *}
lemma eventually_within_Un:
- "eventually P (net within (s \<union> t)) \<longleftrightarrow>
- eventually P (net within s) \<and> eventually P (net within t)"
- unfolding Limits.eventually_within
+ "eventually P (at x within (s \<union> t)) \<longleftrightarrow> eventually P (at x within s) \<and> eventually P (at x within t)"
+ unfolding eventually_at_filter
by (auto elim!: eventually_rev_mp)
lemma Lim_within_union:
- "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
- (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
+ "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow>
+ (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
unfolding tendsto_def
by (auto simp add: eventually_within_Un)
--- a/src/HOL/Probability/Fin_Map.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Tue Apr 09 14:04:41 2013 +0200
@@ -206,8 +206,7 @@
lemma continuous_proj:
shows "continuous_on s (\<lambda>x. (x)\<^isub>F i)"
- unfolding continuous_on_def
- by (safe intro!: tendsto_proj tendsto_ident_at_within)
+ unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at)
instance finmap :: (type, first_countable_topology) first_countable_topology
proof
--- a/src/HOL/Real_Vector_Spaces.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Apr 09 14:04:41 2013 +0200
@@ -1117,19 +1117,18 @@
done
lemma eventually_at:
- fixes a :: "'a::metric_space"
- shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding at_def eventually_within eventually_nhds_metric by auto
+ fixes a :: "'a :: metric_space"
+ shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
+ unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz)
-lemma eventually_within_less:
- fixes a :: "'a :: metric_space"
- shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
- unfolding eventually_within eventually_at dist_nz by auto
-
-lemma eventually_within_le:
- fixes a :: "'a :: metric_space"
- shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> P x)"
- unfolding eventually_within_less by auto (metis dense order_le_less_trans)
+lemma eventually_at_le:
+ fixes a :: "'a::metric_space"
+ shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a \<le> d \<longrightarrow> P x)"
+ unfolding eventually_at_filter eventually_nhds_metric
+ apply auto
+ apply (rule_tac x="d / 2" in exI)
+ apply auto
+ done
lemma tendstoI:
fixes l :: "'a :: metric_space"
@@ -1200,7 +1199,7 @@
lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
--> dist (f x) L < r)"
-unfolding tendsto_iff eventually_at ..
+ unfolding tendsto_iff eventually_at by simp
lemma metric_LIM_I:
"(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
@@ -1235,8 +1234,8 @@
assumes g: "g -- b --> c"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
shows "(\<lambda>x. g (f x)) -- a --> c"
- using g f inj [folded eventually_at]
- by (rule tendsto_compose_eventually)
+ using inj
+ by (intro tendsto_compose_eventually[OF g f]) (auto simp: eventually_at)
lemma metric_isCont_LIM_compose2:
fixes f :: "'a :: metric_space \<Rightarrow> _"
--- a/src/HOL/Topological_Spaces.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Apr 09 14:04:41 2013 +0200
@@ -658,40 +658,58 @@
subsubsection {* Standard filters *}
-definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
- where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
+definition principal :: "'a set \<Rightarrow> 'a filter" where
+ "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
+
+lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
+ unfolding principal_def
+ by (rule eventually_Abs_filter, rule is_filter.intro) auto
-lemma eventually_within:
- "eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F"
- unfolding within_def
- by (rule eventually_Abs_filter, rule is_filter.intro)
- (auto elim!: eventually_rev_mp)
+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)
+
+lemma principal_UNIV[simp]: "principal UNIV = top"
+ by (auto simp: filter_eq_iff eventually_principal)
-lemma within_UNIV [simp]: "F within UNIV = F"
- unfolding filter_eq_iff eventually_within by simp
+lemma principal_empty[simp]: "principal {} = bot"
+ by (auto simp: filter_eq_iff eventually_principal)
+
+lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
+ by (auto simp: le_filter_def eventually_principal)
-lemma within_empty [simp]: "F within {} = bot"
- unfolding filter_eq_iff eventually_within by simp
+lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
+ unfolding le_filter_def eventually_principal
+ apply safe
+ apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
+ apply (auto elim: eventually_elim1)
+ done
-lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
- by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
+lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
+ unfolding eq_iff by simp
-lemma within_le: "F within S \<le> F"
- unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
+lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
+ unfolding filter_eq_iff eventually_sup eventually_principal by auto
-lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
- unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
+lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
+ unfolding filter_eq_iff eventually_inf eventually_principal
+ by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
-lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
- by (blast intro: within_le le_withinI order_trans)
+lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
+ unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
+
+lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
+ unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
subsubsection {* Topological filters *}
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
-definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
- where "at a = nhds a within - {a}"
+definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
+ where "at a within s = inf (nhds a) (principal (s - {a}))"
+
+abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where
+ "at x \<equiv> at x within (CONST UNIV)"
abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter" where
"at_right x \<equiv> at x within {x <..}"
@@ -720,12 +738,19 @@
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
unfolding trivial_limit_def eventually_nhds by simp
+lemma eventually_at_filter:
+ "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
+ unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute)
+
+lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
+ unfolding at_within_def by (intro inf_mono) auto
+
lemma eventually_at_topological:
- "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
-unfolding at_def eventually_within eventually_nhds by simp
+ "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
+ unfolding eventually_nhds eventually_at_filter by simp
lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
- unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
+ unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
unfolding trivial_limit_def eventually_at_topological
@@ -737,33 +762,33 @@
lemma eventually_at_right:
fixes x :: "'a :: {no_top, linorder_topology}"
shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
- unfolding eventually_nhds eventually_within at_def
+ unfolding eventually_at_topological
proof safe
from gt_ex[of x] guess y ..
moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
moreover note gt_ex[of x]
- moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
+ moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
by (auto simp: subset_eq Ball_def)
next
fix b assume "x < b" "\<forall>z. x < z \<and> z < b \<longrightarrow> P z"
- then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in> - {x} \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)"
+ then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)"
by (intro exI[of _ "{..< b}"]) auto
qed
lemma eventually_at_left:
fixes x :: "'a :: {no_bot, linorder_topology}"
shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
- unfolding eventually_nhds eventually_within at_def
+ unfolding eventually_at_topological
proof safe
from lt_ex[of x] guess y ..
moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
- moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
+ moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
by (auto simp: subset_eq Ball_def)
next
fix b assume "b < x" "\<forall>z. b < z \<and> z < x \<longrightarrow> P z"
- then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<in> - {x} \<longrightarrow> xa \<in> {..<x} \<longrightarrow> P xa)"
+ then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s)"
by (intro exI[of _ "{b <..}"]) auto
qed
@@ -775,11 +800,8 @@
"\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
-lemma at_within_eq: "at x within T = nhds x within (T - {x})"
- unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
-
lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
- by (auto simp: eventually_within at_def filter_eq_iff eventually_sup
+ by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
elim: eventually_elim2 eventually_elim1)
lemma eventually_at_split:
@@ -816,13 +838,13 @@
"F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
-lemma filterlim_within:
- "(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))"
- unfolding filterlim_def
-proof safe
- assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1"
- by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
-qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
+lemma filterlim_principal:
+ "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
+ unfolding filterlim_def eventually_filtermap le_principal ..
+
+lemma filterlim_inf:
+ "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
+ unfolding filterlim_def by simp
lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
unfolding filterlim_def filtermap_filtermap ..
@@ -859,7 +881,7 @@
setup {*
Tendsto_Intros.setup #>
Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
- map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
+ map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of);
*}
lemma (in topological_space) tendsto_def:
@@ -872,19 +894,18 @@
by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
-lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
- by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
-
-lemma filterlim_at:
- "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
- by (simp add: at_def filterlim_within)
-
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
unfolding tendsto_def le_filter_def by fast
+lemma tendsto_within_subset: "(f ---> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at x within T)"
+ by (blast intro: tendsto_mono at_le)
+
+lemma filterlim_at:
+ "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f ---> b) F)"
+ by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
+
lemma (in topological_space) topological_tendstoI:
- "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F)
- \<Longrightarrow> (f ---> l) F"
+ "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f ---> l) F"
unfolding tendsto_def by auto
lemma (in topological_space) topological_tendstoD:
@@ -923,13 +944,9 @@
lemma tendsto_bot [simp]: "(f ---> a) bot"
unfolding tendsto_def by simp
-lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
+lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
unfolding tendsto_def eventually_at_topological by auto
-lemma tendsto_ident_at_within [tendsto_intros]:
- "((\<lambda>x. x) ---> a) (at a within S)"
- unfolding tendsto_def eventually_within eventually_at_topological by auto
-
lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
by (simp add: tendsto_def)
@@ -1018,12 +1035,9 @@
"\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
unfolding Lim_def using tendsto_unique[of net f] by auto
-lemma Lim_ident_at: "\<not> trivial_limit (at x) \<Longrightarrow> Lim (at x) (\<lambda>x. x) = x"
+lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
-lemma Lim_ident_at_within: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
- by (rule tendsto_Lim[OF _ tendsto_ident_at_within]) auto
-
subsection {* Limits to @{const at_top} and @{const at_bot} *}
lemma filterlim_at_top:
@@ -1508,12 +1522,12 @@
lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within:
assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
- shows "eventually P (nhds a within s)"
+ shows "eventually P (inf (nhds a) (principal s))"
proof (rule ccontr)
from countable_basis[of a] guess A . note A = this
- assume "\<not> eventually P (nhds a within s)"
+ assume "\<not> eventually P (inf (nhds a) (principal s))"
with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
- unfolding eventually_within eventually_nhds by (intro choice) fastforce
+ unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
then guess F ..
hence F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
by fast+
@@ -1524,12 +1538,12 @@
qed
lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially:
- "eventually P (nhds a within s) \<longleftrightarrow>
+ "eventually P (inf (nhds a) (principal s)) \<longleftrightarrow>
(\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
proof (safe intro!: sequentially_imp_eventually_nhds_within)
- assume "eventually P (nhds a within s)"
+ assume "eventually P (inf (nhds a) (principal s))"
then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x"
- by (auto simp: eventually_within eventually_nhds)
+ 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)
@@ -1547,7 +1561,7 @@
"f -- a --> L \<equiv> (f ---> L) (at a)"
lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
- unfolding tendsto_def by (simp add: at_within_open)
+ unfolding tendsto_def by (simp add: at_within_open[where S=S])
lemma LIM_const_not_eq[tendsto_intros]:
fixes a :: "'a::perfect_space"
@@ -1581,7 +1595,7 @@
lemma tendsto_at_iff_tendsto_nhds:
"g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
- unfolding tendsto_def at_def eventually_within
+ unfolding tendsto_def eventually_at_filter
by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
lemma tendsto_compose:
@@ -1607,7 +1621,7 @@
lemma (in first_countable_topology) sequentially_imp_eventually_within:
"(\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow>
eventually P (at a within s)"
- unfolding at_def within_within_eq
+ unfolding at_within_def
by (intro sequentially_imp_eventually_nhds_within) auto
lemma (in first_countable_topology) sequentially_imp_eventually_at:
@@ -1640,12 +1654,12 @@
lemma continuous_on_cong [cong]:
"s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
- unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
+ unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
lemma continuous_on_topological:
"continuous_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
- unfolding continuous_on_def tendsto_def eventually_within eventually_at_topological by metis
+ unfolding continuous_on_def tendsto_def eventually_at_topological by metis
lemma continuous_on_open_invariant:
"continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> (\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s))"
@@ -1689,7 +1703,7 @@
lemma continuous_on_open_Union:
"(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
- unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
+ unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)
lemma continuous_on_open_UN:
"(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
@@ -1725,7 +1739,7 @@
setup Continuous_On_Intros.setup
lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
- unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
+ unfolding continuous_on_def by (fast intro: tendsto_ident_at)
lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
unfolding continuous_on_def by (auto intro: tendsto_const)
@@ -1762,12 +1776,12 @@
by simp
lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f x) (at x within s)"
- by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at_within continuous_def)
+ by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at continuous_def)
lemma continuous_within_topological:
"continuous (at x within s) f \<longleftrightarrow>
(\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
- unfolding continuous_within tendsto_def eventually_within eventually_at_topological by metis
+ unfolding continuous_within tendsto_def eventually_at_topological by metis
lemma continuous_within_compose[continuous_intros]:
"continuous (at x within s) f \<Longrightarrow> continuous (at (f x) within f ` s) g \<Longrightarrow>
@@ -1783,7 +1797,7 @@
using continuous_within[of x UNIV f] by simp
lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
- unfolding continuous_within by (rule tendsto_ident_at_within)
+ unfolding continuous_within by (rule tendsto_ident_at)
lemma continuous_const[continuous_intros, simp]: "continuous F (\<lambda>x. c)"
unfolding continuous_def by (rule tendsto_const)
@@ -1799,10 +1813,10 @@
by (rule continuous_at)
lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
- by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
+ by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
- by (simp add: continuous_on_def continuous_at tendsto_within_open)
+ by (simp add: continuous_on_def continuous_at at_within_open[of _ s])
lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
--- a/src/HOL/Transcendental.thy Mon Apr 08 21:01:59 2013 +0200
+++ b/src/HOL/Transcendental.thy Tue Apr 09 14:04:41 2013 +0200
@@ -1578,7 +1578,7 @@
lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
- (auto simp: eventually_within)
+ (auto simp: eventually_at_filter)
lemma ln_at_top: "LIM x at_top. ln x :> at_top"
by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
@@ -3190,12 +3190,12 @@
lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
- (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
+ (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
intro!: tan_monotone exI[of _ "pi/2"])
lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
- (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
+ (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
intro!: tan_monotone exI[of _ "pi/2"])
lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"