# HG changeset patch
# User hoelzl
# Date 1365509081 -7200
# Node ID cd05e9fcc63dbb7dd33198752178013791d3e3cf
# Parent  d022e8bd2375387f60ac94d023e5f27479055bc2
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Deriv.thy
--- 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)"
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Limits.thy
--- 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
 
 
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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)"
 
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Multivariate_Analysis/Derivative.thy
--- 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)"
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- 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)
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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)
 
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Probability/Fin_Map.thy
--- 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
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Real_Vector_Spaces.thy
--- 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> _"
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Topological_Spaces.thy
--- 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)
diff -r d022e8bd2375 -r cd05e9fcc63d src/HOL/Transcendental.thy
--- 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"