1.1 --- a/src/HOL/Deriv.thy	Mon Apr 08 21:01:59 2013 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Tue Apr 09 14:04:41 2013 +0200
     1.3 @@ -1043,7 +1043,7 @@
     1.4    moreover then have "f x = g x" by (auto simp: eventually_nhds)
     1.5    moreover assume "x = y" "u = v"
     1.6    ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
     1.7 -    by (auto simp: eventually_within at_def elim: eventually_elim1)
     1.8 +    by (auto simp: eventually_at_filter elim: eventually_elim1)
     1.9  qed simp_all
    1.10  
    1.11  lemma DERIV_shift:
    1.12 @@ -1055,6 +1055,17 @@
    1.13    by (simp add: deriv_def filterlim_at_split filterlim_at_left_to_right
    1.14                  tendsto_minus_cancel_left field_simps conj_commute)
    1.15  
    1.16 +lemma isCont_If_ge:
    1.17 +  fixes a :: "'a :: linorder_topology"
    1.18 +  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"
    1.19 +  unfolding isCont_def continuous_within
    1.20 +  apply (intro filterlim_split_at)
    1.21 +  apply (subst filterlim_cong[OF refl refl, where g=g])
    1.22 +  apply (simp_all add: eventually_at_filter less_le)
    1.23 +  apply (subst filterlim_cong[OF refl refl, where g=f])
    1.24 +  apply (simp_all add: eventually_at_filter less_le)
    1.25 +  done
    1.26 +
    1.27  lemma lhopital_right_0:
    1.28    fixes f0 g0 :: "real \<Rightarrow> real"
    1.29    assumes f_0: "(f0 ---> 0) (at_right 0)"
    1.30 @@ -1081,7 +1092,7 @@
    1.31      and g'_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g' x \<noteq> 0"
    1.32      and f0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV f0 x :> (f' x)"
    1.33      and g0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> DERIV g0 x :> (g' x)"
    1.34 -    unfolding eventually_within eventually_at by (auto simp: dist_real_def)
    1.35 +    unfolding eventually_at eventually_at by (auto simp: dist_real_def)
    1.36  
    1.37    have g_neq_0: "\<And>x. 0 < x \<Longrightarrow> x < a \<Longrightarrow> g x \<noteq> 0"
    1.38      using g0_neq_0 by (simp add: g_def)
    1.39 @@ -1097,18 +1108,10 @@
    1.40    note g = this
    1.41  
    1.42    have "isCont f 0"
    1.43 -    using tendsto_const[of "0::real" "at 0"] f_0
    1.44 -    unfolding isCont_def f_def
    1.45 -    by (intro filterlim_split_at_real)
    1.46 -       (auto elim: eventually_elim1
    1.47 -             simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
    1.48 -    
    1.49 +    unfolding f_def by (intro isCont_If_ge f_0 continuous_const)
    1.50 +
    1.51    have "isCont g 0"
    1.52 -    using tendsto_const[of "0::real" "at 0"] g_0
    1.53 -    unfolding isCont_def g_def
    1.54 -    by (intro filterlim_split_at_real)
    1.55 -       (auto elim: eventually_elim1
    1.56 -             simp add: filterlim_def le_filter_def eventually_within eventually_filtermap)
    1.57 +    unfolding g_def by (intro isCont_If_ge g_0 continuous_const)
    1.58  
    1.59    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)"
    1.60    proof (rule bchoice, rule)
    1.61 @@ -1131,24 +1134,24 @@
    1.62    qed
    1.63    then guess \<zeta> ..
    1.64    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)"
    1.65 -    unfolding eventually_within eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
    1.66 +    unfolding eventually_at by (intro exI[of _ a]) (auto simp: dist_real_def)
    1.67    moreover
    1.68    from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
    1.69      by eventually_elim auto
    1.70    then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
    1.71      by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"])
    1.72 -       (auto intro: tendsto_const tendsto_ident_at_within)
    1.73 +       (auto intro: tendsto_const tendsto_ident_at)
    1.74    then have "(\<zeta> ---> 0) (at_right 0)"
    1.75      by (rule tendsto_norm_zero_cancel)
    1.76    with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
    1.77 -    by (auto elim!: eventually_elim1 simp: filterlim_within filterlim_at)
    1.78 +    by (auto elim!: eventually_elim1 simp: filterlim_at)
    1.79    from this lim have "((\<lambda>t. f' (\<zeta> t) / g' (\<zeta> t)) ---> x) (at_right 0)"
    1.80      by (rule_tac filterlim_compose[of _ _ _ \<zeta>])
    1.81    ultimately have "((\<lambda>t. f t / g t) ---> x) (at_right 0)" (is ?P)
    1.82      by (rule_tac filterlim_cong[THEN iffD1, OF refl refl])
    1.83         (auto elim: eventually_elim1)
    1.84    also have "?P \<longleftrightarrow> ?thesis"
    1.85 -    by (rule filterlim_cong) (auto simp: f_def g_def eventually_within)
    1.86 +    by (rule filterlim_cong) (auto simp: f_def g_def eventually_at_filter)
    1.87    finally show ?thesis .
    1.88  qed
    1.89  
    1.90 @@ -1206,11 +1209,12 @@
    1.91      and f0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV f x :> (f' x)"
    1.92      and g0: "\<And>x. 0 < x \<Longrightarrow> x \<le> a \<Longrightarrow> DERIV g x :> (g' x)"
    1.93      and Df: "\<And>t. 0 < t \<Longrightarrow> t < a \<Longrightarrow> dist (f' t / g' t) x < e / 4"
    1.94 -    unfolding eventually_within_le by (auto simp: dist_real_def)
    1.95 +    unfolding eventually_at_le by (auto simp: dist_real_def)
    1.96 +    
    1.97  
    1.98    from Df have
    1.99      "eventually (\<lambda>t. t < a) (at_right 0)" "eventually (\<lambda>t::real. 0 < t) (at_right 0)"
   1.100 -    unfolding eventually_within eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
   1.101 +    unfolding eventually_at by (auto intro!: exI[of _ a] simp: dist_real_def)
   1.102  
   1.103    moreover
   1.104    have "eventually (\<lambda>t. 0 < g t) (at_right 0)" "eventually (\<lambda>t. g a < g t) (at_right 0)"

     2.1 --- a/src/HOL/Limits.thy	Mon Apr 08 21:01:59 2013 +0200
     2.2 +++ b/src/HOL/Limits.thy	Tue Apr 09 14:04:41 2013 +0200
     2.3 @@ -12,10 +12,6 @@
     2.4  imports Real_Vector_Spaces
     2.5  begin
     2.6  
     2.7 -(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
     2.8 -   Hence it was references as Limits.eventually_within, but now it is Basic_Topology.eventually_within *)
     2.9 -lemmas eventually_within = eventually_within
    2.10 -
    2.11  subsection {* Filter going to infinity norm *}
    2.12  
    2.13  definition at_infinity :: "'a::real_normed_vector filter" where
    2.14 @@ -910,25 +906,36 @@
    2.15  
    2.16  lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
    2.17  
    2.18 -lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::real)"
    2.19 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    2.20 -  by (intro allI ex_cong) (auto simp: dist_real_def field_simps)
    2.21 +lemma filtermap_homeomorph:
    2.22 +  assumes f: "continuous (at a) f"
    2.23 +  assumes g: "continuous (at (f a)) g"
    2.24 +  assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
    2.25 +  shows "filtermap f (nhds a) = nhds (f a)"
    2.26 +  unfolding filter_eq_iff eventually_filtermap eventually_nhds
    2.27 +proof safe
    2.28 +  fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
    2.29 +  from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
    2.30 +  show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
    2.31 +next
    2.32 +  fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
    2.33 +  with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
    2.34 +  obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
    2.35 +    by (metis UNIV_I)
    2.36 +  with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
    2.37 +    by (force intro!: exI[of _ A])
    2.38 +qed
    2.39  
    2.40 -lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::real)"
    2.41 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric
    2.42 -  apply (intro allI ex_cong)
    2.43 -  apply (auto simp: dist_real_def field_simps)
    2.44 -  apply (erule_tac x="-x" in allE)
    2.45 -  apply simp
    2.46 -  done
    2.47 +lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
    2.48 +  by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
    2.49  
    2.50 -lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::real)"
    2.51 -  unfolding at_def filtermap_nhds_shift[symmetric]
    2.52 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.53 +lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
    2.54 +  by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
    2.55 +
    2.56 +lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
    2.57 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
    2.58  
    2.59  lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
    2.60 -  unfolding filtermap_at_shift[symmetric]
    2.61 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.62 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
    2.63  
    2.64  lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
    2.65    using filtermap_at_right_shift[of "-a" 0] by simp
    2.66 @@ -941,15 +948,14 @@
    2.67    "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
    2.68    unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
    2.69  
    2.70 -lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::real)"
    2.71 -  unfolding at_def filtermap_nhds_minus[symmetric]
    2.72 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within)
    2.73 +lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::'a::real_normed_vector)"
    2.74 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
    2.75  
    2.76  lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
    2.77 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
    2.78 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
    2.79  
    2.80  lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
    2.81 -  by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric])
    2.82 +  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
    2.83  
    2.84  lemma filterlim_at_left_to_right:
    2.85    "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
    2.86 @@ -989,19 +995,19 @@
    2.87    unfolding filterlim_uminus_at_top by simp
    2.88  
    2.89  lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
    2.90 -  unfolding filterlim_at_top_gt[where c=0] eventually_within at_def
    2.91 +  unfolding filterlim_at_top_gt[where c=0] eventually_at_filter
    2.92  proof safe
    2.93    fix Z :: real assume [arith]: "0 < Z"
    2.94    then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
    2.95      by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
    2.96 -  then show "eventually (\<lambda>x. x \<in> - {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
    2.97 +  then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
    2.98      by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
    2.99  qed
   2.100  
   2.101  lemma filterlim_inverse_at_top:
   2.102    "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
   2.103    by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
   2.104 -     (simp add: filterlim_def eventually_filtermap le_within_iff at_def eventually_elim1)
   2.105 +     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
   2.106  
   2.107  lemma filterlim_inverse_at_bot_neg:
   2.108    "LIM x (at_left (0::real)). inverse x :> at_bot"
   2.109 @@ -1033,8 +1039,7 @@
   2.110    have "(inverse ---> (0::real)) at_top"
   2.111      by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
   2.112    then show "filtermap inverse at_top \<le> at_right (0::real)"
   2.113 -    unfolding at_within_eq
   2.114 -    by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def)
   2.115 +    by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
   2.116  next
   2.117    have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
   2.118      using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
   2.119 @@ -1082,9 +1087,9 @@
   2.120    then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity"
   2.121      by (rule filtermap_mono)
   2.122    also have "\<dots> \<le> at 0"
   2.123 -    using tendsto_inverse_0
   2.124 -    by (auto intro!: le_withinI exI[of _ 1]
   2.125 -             simp: eventually_filtermap eventually_at_infinity filterlim_def at_def)
   2.126 +    using tendsto_inverse_0[where 'a='b]
   2.127 +    by (auto intro!: exI[of _ 1]
   2.128 +             simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity)
   2.129    finally show "filtermap inverse (filtermap g F) \<le> at 0" .
   2.130  next
   2.131    assume "filtermap inverse (filtermap g F) \<le> at 0"
   2.132 @@ -1094,9 +1099,8 @@
   2.133      by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
   2.134  qed
   2.135  
   2.136 -lemma tendsto_inverse_0_at_top:
   2.137 -  "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
   2.138 - by (metis at_top_le_at_infinity filterlim_at filterlim_inverse_at_iff filterlim_mono order_refl)
   2.139 +lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
   2.140 + by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
   2.141  
   2.142  text {*
   2.143  
   2.144 @@ -1516,13 +1520,7 @@
   2.145  lemma LIM_offset:
   2.146    fixes a :: "'a::real_normed_vector"
   2.147    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
   2.148 -apply (rule topological_tendstoI)
   2.149 -apply (drule (2) topological_tendstoD)
   2.150 -apply (simp only: eventually_at dist_norm)
   2.151 -apply (clarify, rule_tac x=d in exI, safe)
   2.152 -apply (drule_tac x="x + k" in spec)
   2.153 -apply (simp add: algebra_simps)
   2.154 -done
   2.155 +  unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
   2.156  
   2.157  lemma LIM_offset_zero:
   2.158    fixes a :: "'a::real_normed_vector"
   2.159 @@ -1717,7 +1715,7 @@
   2.160    show "(f ---> f x) (at_left x)"
   2.161      using `isCont f x` by (simp add: filterlim_at_split isCont_def)
   2.162    show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
   2.163 -    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
   2.164 +    using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"])
   2.165  qed simp
   2.166  
   2.167  

     3.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 08 21:01:59 2013 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Apr 09 14:04:41 2013 +0200
     3.3 @@ -1167,7 +1167,7 @@
     3.4  
     3.5  lemma differentiable_at_imp_differentiable_on:
     3.6    "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
     3.7 -  unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
     3.8 +  by (metis differentiable_at_withinI differentiable_on_def)
     3.9  
    3.10  definition "jacobian f net = matrix(frechet_derivative f net)"
    3.11  

     4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 08 21:01:59 2013 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Apr 09 14:04:41 2013 +0200
     4.3 @@ -40,7 +40,7 @@
     4.4      apply (simp add: norm_sgn sgn_zero_iff x)
     4.5      done
     4.6    thus ?thesis
     4.7 -    by (rule netlimit_within [of a UNIV, unfolded within_UNIV])
     4.8 +    by (rule netlimit_within [of a UNIV])
     4.9  qed simp
    4.10  
    4.11  lemma FDERIV_conv_has_derivative:
    4.12 @@ -80,7 +80,7 @@
    4.13    using has_derivative_within' [of f f' x UNIV] by simp
    4.14  
    4.15  lemma has_derivative_at_within: "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
    4.16 -  unfolding has_derivative_within' has_derivative_at' by meson
    4.17 +  unfolding has_derivative_within' has_derivative_at' by blast
    4.18  
    4.19  lemma has_derivative_within_open:
    4.20    "a \<in> s \<Longrightarrow> open s \<Longrightarrow> ((f has_derivative f') (at a within s) \<longleftrightarrow> (f has_derivative f') (at a))"
    4.21 @@ -252,7 +252,7 @@
    4.22  lemma differentiable_on_eq_differentiable_at:
    4.23    "open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
    4.24    unfolding differentiable_on_def
    4.25 -  by (auto simp add: at_within_interior interior_open)
    4.26 +  by (metis at_within_interior interior_open)
    4.27  
    4.28  lemma differentiable_transform_within:
    4.29    assumes "0 < d" and "x \<in> s" and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
    4.30 @@ -317,7 +317,7 @@
    4.31  
    4.32  lemma differentiable_imp_continuous_at:
    4.33    "f differentiable at x \<Longrightarrow> continuous (at x) f"
    4.34 - by(rule differentiable_imp_continuous_within[of _ x UNIV, unfolded within_UNIV])
    4.35 + by(rule differentiable_imp_continuous_within[of _ x UNIV])
    4.36  
    4.37  lemma differentiable_imp_continuous_on:
    4.38    "f differentiable_on s \<Longrightarrow> continuous_on s f"
    4.39 @@ -326,7 +326,7 @@
    4.40  
    4.41  lemma has_derivative_within_subset:
    4.42   "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
    4.43 -  unfolding has_derivative_within using Lim_within_subset by blast
    4.44 +  unfolding has_derivative_within using tendsto_within_subset by blast
    4.45  
    4.46  lemma differentiable_within_subset:
    4.47    "f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable (at x within s)"
    4.48 @@ -621,7 +621,7 @@
    4.49    shows "f' = f''"
    4.50  proof -
    4.51    from assms(1) have *: "at x within {a<..<b} = at x"
    4.52 -    by (simp add: at_within_interior interior_open open_interval)
    4.53 +    by (metis at_within_interior interior_open open_interval)
    4.54    from assms(2,3) [unfolded *] show "f' = f''"
    4.55      by (rule frechet_derivative_unique_at)
    4.56  qed
    4.57 @@ -1805,7 +1805,7 @@
    4.58    assumes "(g has_vector_derivative g') (at x)"
    4.59    assumes "bounded_bilinear h"
    4.60    shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
    4.61 -  using has_vector_derivative_bilinear_within[where s=UNIV] assms by simp
    4.62 +  using has_vector_derivative_bilinear_within[OF assms] .
    4.63  
    4.64  lemma has_vector_derivative_at_within:
    4.65    "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"

     5.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Apr 08 21:01:59 2013 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Apr 09 14:04:41 2013 +0200
     5.3 @@ -890,16 +890,16 @@
     5.4  lemma Liminf_within:
     5.5    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
     5.6    shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
     5.7 -  unfolding Liminf_def eventually_within_less
     5.8 +  unfolding Liminf_def eventually_at
     5.9  proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
    5.10 -  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
    5.11 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
    5.12    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
    5.13      by (auto simp: zero_less_dist_iff dist_commute)
    5.14    then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
    5.15      by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
    5.16  next
    5.17    fix d :: real assume "0 < d"
    5.18 -  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>
    5.19 +  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>
    5.20      INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
    5.21      by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
    5.22         (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
    5.23 @@ -908,16 +908,16 @@
    5.24  lemma Limsup_within:
    5.25    fixes f :: "'a::metric_space => 'b::complete_lattice"
    5.26    shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
    5.27 -  unfolding Limsup_def eventually_within_less
    5.28 +  unfolding Limsup_def eventually_at
    5.29  proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
    5.30 -  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
    5.31 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
    5.32    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
    5.33      by (auto simp: zero_less_dist_iff dist_commute)
    5.34    then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
    5.35      by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
    5.36  next
    5.37    fix d :: real assume "0 < d"
    5.38 -  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>
    5.39 +  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>
    5.40      SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
    5.41      by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
    5.42         (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)

     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 08 21:01:59 2013 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 09 14:04:41 2013 +0200
     6.3 @@ -39,9 +39,6 @@
     6.4    shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
     6.5    by (fact tendsto_within_open)
     6.6  
     6.7 -lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
     6.8 -  by (fact tendsto_within_subset)
     6.9 -
    6.10  lemma continuous_on_union:
    6.11    "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    6.12    by (fact continuous_on_closed_Un)
    6.13 @@ -1205,7 +1202,7 @@
    6.14  definition
    6.15    indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
    6.16      (infixr "indirection" 70) where
    6.17 -  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
    6.18 +  "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
    6.19  
    6.20  text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
    6.21  
    6.22 @@ -1215,7 +1212,7 @@
    6.23    assume "trivial_limit (at a within S)"
    6.24    thus "\<not> a islimpt S"
    6.25      unfolding trivial_limit_def
    6.26 -    unfolding eventually_within eventually_at_topological
    6.27 +    unfolding eventually_at_topological
    6.28      unfolding islimpt_def
    6.29      apply (clarsimp simp add: set_eq_iff)
    6.30      apply (rename_tac T, rule_tac x=T in exI)
    6.31 @@ -1225,7 +1222,7 @@
    6.32    assume "\<not> a islimpt S"
    6.33    thus "trivial_limit (at a within S)"
    6.34      unfolding trivial_limit_def
    6.35 -    unfolding eventually_within eventually_at_topological
    6.36 +    unfolding eventually_at_topological
    6.37      unfolding islimpt_def
    6.38      apply clarsimp
    6.39      apply (rule_tac x=T in exI)
    6.40 @@ -1292,11 +1289,11 @@
    6.41  
    6.42  lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
    6.43             (\<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)"
    6.44 -  by (auto simp add: tendsto_iff eventually_within_le)
    6.45 +  by (auto simp add: tendsto_iff eventually_at_le dist_nz)
    6.46  
    6.47  lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
    6.48          (\<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)"
    6.49 -  by (auto simp add: tendsto_iff eventually_within_less)
    6.50 +  by (auto simp add: tendsto_iff eventually_at dist_nz)
    6.51  
    6.52  lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
    6.53          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
    6.54 @@ -1311,12 +1308,12 @@
    6.55  
    6.56  text{* The expected monotonicity property. *}
    6.57  
    6.58 -lemma Lim_within_empty: "(f ---> l) (net within {})"
    6.59 -  unfolding tendsto_def Limits.eventually_within by simp
    6.60 -
    6.61 -lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
    6.62 -  shows "(f ---> l) (net within (S \<union> T))"
    6.63 -  using assms unfolding tendsto_def Limits.eventually_within
    6.64 +lemma Lim_within_empty: "(f ---> l) (at x within {})"
    6.65 +  unfolding tendsto_def eventually_at_filter by simp
    6.66 +
    6.67 +lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
    6.68 +  shows "(f ---> l) (at x within (S \<union> T))"
    6.69 +  using assms unfolding tendsto_def eventually_at_filter
    6.70    apply clarify
    6.71    apply (drule spec, drule (1) mp, drule (1) mp)
    6.72    apply (drule spec, drule (1) mp, drule (1) mp)
    6.73 @@ -1324,17 +1321,16 @@
    6.74    done
    6.75  
    6.76  lemma Lim_Un_univ:
    6.77 - "(f ---> l) (net within S) \<Longrightarrow> (f ---> l) (net within T) \<Longrightarrow>  S \<union> T = UNIV
    6.78 -        ==> (f ---> l) net"
    6.79 -  by (metis Lim_Un within_UNIV)
    6.80 + "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
    6.81 +        ==> (f ---> l) (at x)"
    6.82 +  by (metis Lim_Un)
    6.83  
    6.84  text{* Interrelations between restricted and unrestricted limits. *}
    6.85  
    6.86 -lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
    6.87 -  (* FIXME: rename *)
    6.88 -  unfolding tendsto_def Limits.eventually_within
    6.89 -  apply (clarify, drule spec, drule (1) mp, drule (1) mp)
    6.90 -  by (auto elim!: eventually_elim1)
    6.91 +
    6.92 +lemma Lim_at_within: (* FIXME: rename *)
    6.93 +  "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
    6.94 +  by (metis order_refl filterlim_mono subset_UNIV at_le)
    6.95  
    6.96  lemma eventually_within_interior:
    6.97    assumes "x \<in> interior S"
    6.98 @@ -1343,7 +1339,7 @@
    6.99    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
   6.100    { assume "?lhs"
   6.101      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
   6.102 -      unfolding Limits.eventually_within eventually_at_topological
   6.103 +      unfolding eventually_at_topological
   6.104        by auto
   6.105      with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
   6.106        by auto
   6.107 @@ -1351,15 +1347,14 @@
   6.108        unfolding eventually_at_topological by auto
   6.109    } moreover
   6.110    { assume "?rhs" hence "?lhs"
   6.111 -      unfolding Limits.eventually_within
   6.112 -      by (auto elim: eventually_elim1)
   6.113 +      by (auto elim: eventually_elim1 simp: eventually_at_filter)
   6.114    } ultimately
   6.115    show "?thesis" ..
   6.116  qed
   6.117  
   6.118  lemma at_within_interior:
   6.119    "x \<in> interior S \<Longrightarrow> at x within S = at x"
   6.120 -  by (simp add: filter_eq_iff eventually_within_interior)
   6.121 +  unfolding filter_eq_iff by (intro allI eventually_within_interior)
   6.122  
   6.123  lemma Lim_within_LIMSEQ:
   6.124    fixes a :: "'a::metric_space"
   6.125 @@ -1386,17 +1381,14 @@
   6.126          by (auto intro: cInf_lower)
   6.127        with a have "a < f y" by (blast intro: less_le_trans) }
   6.128      then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
   6.129 -      by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
   6.130 +      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
   6.131    next
   6.132      fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
   6.133      from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
   6.134 -    show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
   6.135 -      unfolding within_within_eq[symmetric]
   6.136 -        Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
   6.137 -    proof (safe intro!: exI[of _ y] y)
   6.138 -      fix z assume "x < z" "z \<in> I" "z < y"
   6.139 -      with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
   6.140 -    qed
   6.141 +    then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
   6.142 +      unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
   6.143 +    then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
   6.144 +      unfolding eventually_at_filter by eventually_elim simp
   6.145    qed
   6.146  qed
   6.147  
   6.148 @@ -1540,7 +1532,7 @@
   6.149  text{* These are special for limits out of the same vector space. *}
   6.150  
   6.151  lemma Lim_within_id: "(id ---> a) (at a within s)"
   6.152 -  unfolding id_def by (rule tendsto_ident_at_within)
   6.153 +  unfolding id_def by (rule tendsto_ident_at)
   6.154  
   6.155  lemma Lim_at_id: "(id ---> a) (at a)"
   6.156    unfolding id_def by (rule tendsto_ident_at)
   6.157 @@ -1567,13 +1559,13 @@
   6.158  
   6.159  lemma lim_within_interior:
   6.160    "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
   6.161 -  by (simp add: at_within_interior)
   6.162 +  by (metis at_within_interior)
   6.163  
   6.164  lemma netlimit_within_interior:
   6.165    fixes x :: "'a::{t2_space,perfect_space}"
   6.166    assumes "x \<in> interior S"
   6.167    shows "netlimit (at x within S) = x"
   6.168 -using assms by (simp add: at_within_interior netlimit_at)
   6.169 +using assms by (metis at_within_interior netlimit_at)
   6.170  
   6.171  text{* Transformation of limit. *}
   6.172  
   6.173 @@ -1596,8 +1588,7 @@
   6.174    shows "(g ---> l) (at x within S)"
   6.175  proof (rule Lim_transform_eventually)
   6.176    show "eventually (\<lambda>x. f x = g x) (at x within S)"
   6.177 -    unfolding eventually_within_less
   6.178 -    using assms(1,2) by auto
   6.179 +    using assms(1,2) by (auto simp: dist_nz eventually_at)
   6.180    show "(f ---> l) (at x within S)" by fact
   6.181  qed
   6.182  
   6.183 @@ -1622,7 +1613,7 @@
   6.184  proof (rule Lim_transform_eventually)
   6.185    show "(f ---> l) (at a within S)" by fact
   6.186    show "eventually (\<lambda>x. f x = g x) (at a within S)"
   6.187 -    unfolding Limits.eventually_within eventually_at_topological
   6.188 +    unfolding eventually_at_topological
   6.189      by (rule exI [where x="- {b}"], simp add: open_Compl assms)
   6.190  qed
   6.191  
   6.192 @@ -1655,7 +1646,7 @@
   6.193    assumes "a = b" "x = y" "S = T"
   6.194    assumes "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
   6.195    shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
   6.196 -  unfolding tendsto_def Limits.eventually_within eventually_at_topological
   6.197 +  unfolding tendsto_def eventually_at_topological
   6.198    using assms by simp
   6.199  
   6.200  lemma Lim_cong_at(*[cong add]*):
   6.201 @@ -3759,7 +3750,7 @@
   6.202  lemma continuous_within_subset:
   6.203   "continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
   6.204               ==> continuous (at x within t) f"
   6.205 -  unfolding continuous_within by(metis Lim_within_subset)
   6.206 +  unfolding continuous_within by(metis tendsto_within_subset)
   6.207  
   6.208  lemma continuous_on_interior:
   6.209    shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
   6.210 @@ -3768,7 +3759,7 @@
   6.211  
   6.212  lemma continuous_on_eq:
   6.213    "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
   6.214 -  unfolding continuous_on_def tendsto_def Limits.eventually_within
   6.215 +  unfolding continuous_on_def tendsto_def eventually_at_topological
   6.216    by simp
   6.217  
   6.218  text {* Characterization of various kinds of continuity in terms of sequences. *}
   6.219 @@ -3783,7 +3774,7 @@
   6.220    { 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"
   6.221      fix T::"'b set" assume "open T" and "f a \<in> T"
   6.222      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"
   6.223 -      unfolding continuous_within tendsto_def eventually_within_less by auto
   6.224 +      unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
   6.225      have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
   6.226        using x(2) `d>0` by simp
   6.227      hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
   6.228 @@ -4015,7 +4006,7 @@
   6.229  
   6.230  lemma continuous_at_open:
   6.231    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)))"
   6.232 -unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
   6.233 +unfolding continuous_within_topological [of x UNIV f]
   6.234  unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
   6.235  
   6.236  lemma continuous_imp_tendsto:
   6.237 @@ -4181,7 +4172,7 @@
   6.238    hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
   6.239      using `a \<notin> U` by (fast elim: eventually_mono [rotated])
   6.240    thus ?thesis
   6.241 -    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
   6.242 +    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_at)
   6.243  qed
   6.244  
   6.245  lemma continuous_at_avoid:
   6.246 @@ -4514,7 +4505,7 @@
   6.247  proof (rule continuous_attains_sup [OF assms])
   6.248    { fix x assume "x\<in>s"
   6.249      have "(dist a ---> dist a x) (at x within s)"
   6.250 -      by (intro tendsto_dist tendsto_const Lim_at_within tendsto_ident_at)
   6.251 +      by (intro tendsto_dist tendsto_const tendsto_ident_at)
   6.252    }
   6.253    thus "continuous_on s (dist a)"
   6.254      unfolding continuous_on ..
   6.255 @@ -5350,7 +5341,7 @@
   6.256    assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
   6.257  proof -
   6.258    from assms(1) have "continuous_on UNIV f"
   6.259 -    unfolding isCont_def continuous_on_def within_UNIV by simp
   6.260 +    unfolding isCont_def continuous_on_def by simp
   6.261    hence "open {x \<in> UNIV. f x \<in> s}"
   6.262      using open_UNIV `open s` by (rule continuous_open_preimage)
   6.263    thus "open (f -` s)"
   6.264 @@ -5508,14 +5499,13 @@
   6.265  text{* Limits relative to a union.                                               *}
   6.266  
   6.267  lemma eventually_within_Un:
   6.268 -  "eventually P (net within (s \<union> t)) \<longleftrightarrow>
   6.269 -    eventually P (net within s) \<and> eventually P (net within t)"
   6.270 -  unfolding Limits.eventually_within
   6.271 +  "eventually P (at x within (s \<union> t)) \<longleftrightarrow> eventually P (at x within s) \<and> eventually P (at x within t)"
   6.272 +  unfolding eventually_at_filter
   6.273    by (auto elim!: eventually_rev_mp)
   6.274  
   6.275  lemma Lim_within_union:
   6.276 - "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
   6.277 -  (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
   6.278 + "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow>
   6.279 +  (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
   6.280    unfolding tendsto_def
   6.281    by (auto simp add: eventually_within_Un)
   6.282  

     7.1 --- a/src/HOL/Probability/Fin_Map.thy	Mon Apr 08 21:01:59 2013 +0200
     7.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Apr 09 14:04:41 2013 +0200
     7.3 @@ -206,8 +206,7 @@
     7.4  
     7.5  lemma continuous_proj:
     7.6    shows "continuous_on s (\<lambda>x. (x)\<^isub>F i)"
     7.7 -  unfolding continuous_on_def
     7.8 -  by (safe intro!: tendsto_proj tendsto_ident_at_within)
     7.9 +  unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at)
    7.10  
    7.11  instance finmap :: (type, first_countable_topology) first_countable_topology
    7.12  proof

     8.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Apr 08 21:01:59 2013 +0200
     8.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Apr 09 14:04:41 2013 +0200
     8.3 @@ -1117,19 +1117,18 @@
     8.4  done
     8.5  
     8.6  lemma eventually_at:
     8.7 +  fixes a :: "'a :: metric_space"
     8.8 +  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)"
     8.9 +  unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz)
    8.10 +
    8.11 +lemma eventually_at_le:
    8.12    fixes a :: "'a::metric_space"
    8.13 -  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    8.14 -unfolding at_def eventually_within eventually_nhds_metric by auto
    8.15 -
    8.16 -lemma eventually_within_less:
    8.17 -  fixes a :: "'a :: metric_space"
    8.18 -  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)"
    8.19 -  unfolding eventually_within eventually_at dist_nz by auto
    8.20 -
    8.21 -lemma eventually_within_le:
    8.22 -  fixes a :: "'a :: metric_space"
    8.23 -  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)"
    8.24 -  unfolding eventually_within_less by auto (metis dense order_le_less_trans)
    8.25 +  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)"
    8.26 +  unfolding eventually_at_filter eventually_nhds_metric
    8.27 +  apply auto
    8.28 +  apply (rule_tac x="d / 2" in exI)
    8.29 +  apply auto
    8.30 +  done
    8.31  
    8.32  lemma tendstoI:
    8.33    fixes l :: "'a :: metric_space"
    8.34 @@ -1200,7 +1199,7 @@
    8.35  lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
    8.36       (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
    8.37          --> dist (f x) L < r)"
    8.38 -unfolding tendsto_iff eventually_at ..
    8.39 +  unfolding tendsto_iff eventually_at by simp
    8.40  
    8.41  lemma metric_LIM_I:
    8.42    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
    8.43 @@ -1235,8 +1234,8 @@
    8.44    assumes g: "g -- b --> c"
    8.45    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
    8.46    shows "(\<lambda>x. g (f x)) -- a --> c"
    8.47 -  using g f inj [folded eventually_at]
    8.48 -  by (rule tendsto_compose_eventually)
    8.49 +  using inj
    8.50 +  by (intro tendsto_compose_eventually[OF g f]) (auto simp: eventually_at)
    8.51  
    8.52  lemma metric_isCont_LIM_compose2:
    8.53    fixes f :: "'a :: metric_space \<Rightarrow> _"

     9.1 --- a/src/HOL/Topological_Spaces.thy	Mon Apr 08 21:01:59 2013 +0200
     9.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Apr 09 14:04:41 2013 +0200
     9.3 @@ -658,40 +658,58 @@
     9.4  
     9.5  subsubsection {* Standard filters *}
     9.6  
     9.7 -definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
     9.8 -  where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
     9.9 +definition principal :: "'a set \<Rightarrow> 'a filter" where
    9.10 +  "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
    9.11  
    9.12 -lemma eventually_within:
    9.13 -  "eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F"
    9.14 -  unfolding within_def
    9.15 -  by (rule eventually_Abs_filter, rule is_filter.intro)
    9.16 -     (auto elim!: eventually_rev_mp)
    9.17 +lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"
    9.18 +  unfolding principal_def
    9.19 +  by (rule eventually_Abs_filter, rule is_filter.intro) auto
    9.20  
    9.21 -lemma within_UNIV [simp]: "F within UNIV = F"
    9.22 -  unfolding filter_eq_iff eventually_within by simp
    9.23 +lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"
    9.24 +  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)
    9.25  
    9.26 -lemma within_empty [simp]: "F within {} = bot"
    9.27 -  unfolding filter_eq_iff eventually_within by simp
    9.28 +lemma principal_UNIV[simp]: "principal UNIV = top"
    9.29 +  by (auto simp: filter_eq_iff eventually_principal)
    9.30  
    9.31 -lemma within_within_eq: "(F within S) within T = F within (S \<inter> T)"
    9.32 -  by (auto simp: filter_eq_iff eventually_within elim: eventually_elim1)
    9.33 +lemma principal_empty[simp]: "principal {} = bot"
    9.34 +  by (auto simp: filter_eq_iff eventually_principal)
    9.35  
    9.36 -lemma within_le: "F within S \<le> F"
    9.37 -  unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
    9.38 +lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"
    9.39 +  by (auto simp: le_filter_def eventually_principal)
    9.40  
    9.41 -lemma le_withinI: "F \<le> F' \<Longrightarrow> eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S"
    9.42 -  unfolding le_filter_def eventually_within by (auto elim: eventually_elim2)
    9.43 +lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"
    9.44 +  unfolding le_filter_def eventually_principal
    9.45 +  apply safe
    9.46 +  apply (erule_tac x="\<lambda>x. x \<in> A" in allE)
    9.47 +  apply (auto elim: eventually_elim1)
    9.48 +  done
    9.49  
    9.50 -lemma le_within_iff: "eventually (\<lambda>x. x \<in> S) F \<Longrightarrow> F \<le> F' within S \<longleftrightarrow> F \<le> F'"
    9.51 -  by (blast intro: within_le le_withinI order_trans)
    9.52 +lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"
    9.53 +  unfolding eq_iff by simp
    9.54 +
    9.55 +lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"
    9.56 +  unfolding filter_eq_iff eventually_sup eventually_principal by auto
    9.57 +
    9.58 +lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"
    9.59 +  unfolding filter_eq_iff eventually_inf eventually_principal
    9.60 +  by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
    9.61 +
    9.62 +lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"
    9.63 +  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)
    9.64 +
    9.65 +lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
    9.66 +  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
    9.67  
    9.68  subsubsection {* Topological filters *}
    9.69  
    9.70  definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
    9.71    where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    9.72  
    9.73 -definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
    9.74 -  where "at a = nhds a within - {a}"
    9.75 +definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
    9.76 +  where "at a within s = inf (nhds a) (principal (s - {a}))"
    9.77 +
    9.78 +abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where
    9.79 +  "at x \<equiv> at x within (CONST UNIV)"
    9.80  
    9.81  abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter" where
    9.82    "at_right x \<equiv> at x within {x <..}"
    9.83 @@ -720,12 +738,19 @@
    9.84  lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
    9.85    unfolding trivial_limit_def eventually_nhds by simp
    9.86  
    9.87 +lemma eventually_at_filter:
    9.88 +  "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
    9.89 +  unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute)
    9.90 +
    9.91 +lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
    9.92 +  unfolding at_within_def by (intro inf_mono) auto
    9.93 +
    9.94  lemma eventually_at_topological:
    9.95 -  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
    9.96 -unfolding at_def eventually_within eventually_nhds by simp
    9.97 +  "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))"
    9.98 +  unfolding eventually_nhds eventually_at_filter by simp
    9.99  
   9.100  lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   9.101 -  unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
   9.102 +  unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
   9.103  
   9.104  lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   9.105    unfolding trivial_limit_def eventually_at_topological
   9.106 @@ -737,33 +762,33 @@
   9.107  lemma eventually_at_right:
   9.108    fixes x :: "'a :: {no_top, linorder_topology}"
   9.109    shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"
   9.110 -  unfolding eventually_nhds eventually_within at_def
   9.111 +  unfolding eventually_at_topological
   9.112  proof safe
   9.113    from gt_ex[of x] guess y ..
   9.114    moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]
   9.115    moreover note gt_ex[of x]
   9.116 -  moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
   9.117 +  moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"
   9.118    ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"
   9.119      by (auto simp: subset_eq Ball_def)
   9.120  next
   9.121    fix b assume "x < b" "\<forall>z. x < z \<and> z < b \<longrightarrow> P z"
   9.122 -  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)"
   9.123 +  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)"
   9.124      by (intro exI[of _ "{..< b}"]) auto
   9.125  qed
   9.126  
   9.127  lemma eventually_at_left:
   9.128    fixes x :: "'a :: {no_bot, linorder_topology}"
   9.129    shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"
   9.130 -  unfolding eventually_nhds eventually_within at_def
   9.131 +  unfolding eventually_at_topological
   9.132  proof safe
   9.133    from lt_ex[of x] guess y ..
   9.134    moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]
   9.135 -  moreover assume "\<forall>s\<in>S. s \<in> - {x} \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
   9.136 +  moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"
   9.137    ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"
   9.138      by (auto simp: subset_eq Ball_def)
   9.139  next
   9.140    fix b assume "b < x" "\<forall>z. b < z \<and> z < x \<longrightarrow> P z"
   9.141 -  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)"
   9.142 +  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)"
   9.143      by (intro exI[of _ "{b <..}"]) auto
   9.144  qed
   9.145  
   9.146 @@ -775,11 +800,8 @@
   9.147    "\<not> trivial_limit (at_right (x::'a::{no_top, dense_linorder, linorder_topology}))"
   9.148    unfolding trivial_limit_def eventually_at_right by (auto dest: dense)
   9.149  
   9.150 -lemma at_within_eq: "at x within T = nhds x within (T - {x})"
   9.151 -  unfolding at_def within_within_eq by (simp add: ac_simps Diff_eq)
   9.152 -
   9.153  lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
   9.154 -  by (auto simp: eventually_within at_def filter_eq_iff eventually_sup 
   9.155 +  by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
   9.156             elim: eventually_elim2 eventually_elim1)
   9.157  
   9.158  lemma eventually_at_split:
   9.159 @@ -816,13 +838,13 @@
   9.160    "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"
   9.161    by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)
   9.162  
   9.163 -lemma filterlim_within:
   9.164 -  "(LIM x F1. f x :> F2 within S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F1 \<and> (LIM x F1. f x :> F2))"
   9.165 -  unfolding filterlim_def
   9.166 -proof safe
   9.167 -  assume "filtermap f F1 \<le> F2 within S" then show "eventually (\<lambda>x. f x \<in> S) F1"
   9.168 -    by (auto simp: le_filter_def eventually_filtermap eventually_within elim!: allE[of _ "\<lambda>x. x \<in> S"])
   9.169 -qed (auto intro: within_le order_trans simp: le_within_iff eventually_filtermap)
   9.170 +lemma filterlim_principal:
   9.171 +  "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   9.172 +  unfolding filterlim_def eventually_filtermap le_principal ..
   9.173 +
   9.174 +lemma filterlim_inf:
   9.175 +  "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   9.176 +  unfolding filterlim_def by simp
   9.177  
   9.178  lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   9.179    unfolding filterlim_def filtermap_filtermap ..
   9.180 @@ -859,7 +881,7 @@
   9.181  setup {*
   9.182    Tendsto_Intros.setup #>
   9.183    Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
   9.184 -    map (fn thm => @{thm tendsto_eq_rhs} OF [thm]) o Tendsto_Intros.get o Context.proof_of);
   9.185 +    map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of);
   9.186  *}
   9.187  
   9.188  lemma (in topological_space) tendsto_def:
   9.189 @@ -872,19 +894,18 @@
   9.190      by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
   9.191  qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
   9.192  
   9.193 -lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
   9.194 -  by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
   9.195 -
   9.196 -lemma filterlim_at:
   9.197 -  "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
   9.198 -  by (simp add: at_def filterlim_within)
   9.199 -
   9.200  lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   9.201    unfolding tendsto_def le_filter_def by fast
   9.202  
   9.203 +lemma tendsto_within_subset: "(f ---> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at x within T)"
   9.204 +  by (blast intro: tendsto_mono at_le)
   9.205 +
   9.206 +lemma filterlim_at:
   9.207 +  "(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)"
   9.208 +  by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
   9.209 +
   9.210  lemma (in topological_space) topological_tendstoI:
   9.211 -  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F)
   9.212 -    \<Longrightarrow> (f ---> l) F"
   9.213 +  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f ---> l) F"
   9.214    unfolding tendsto_def by auto
   9.215  
   9.216  lemma (in topological_space) topological_tendstoD:
   9.217 @@ -923,13 +944,9 @@
   9.218  lemma tendsto_bot [simp]: "(f ---> a) bot"
   9.219    unfolding tendsto_def by simp
   9.220  
   9.221 -lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
   9.222 +lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
   9.223    unfolding tendsto_def eventually_at_topological by auto
   9.224  
   9.225 -lemma tendsto_ident_at_within [tendsto_intros]:
   9.226 -  "((\<lambda>x. x) ---> a) (at a within S)"
   9.227 -  unfolding tendsto_def eventually_within eventually_at_topological by auto
   9.228 -
   9.229  lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
   9.230    by (simp add: tendsto_def)
   9.231  
   9.232 @@ -1018,12 +1035,9 @@
   9.233    "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
   9.234    unfolding Lim_def using tendsto_unique[of net f] by auto
   9.235  
   9.236 -lemma Lim_ident_at: "\<not> trivial_limit (at x) \<Longrightarrow> Lim (at x) (\<lambda>x. x) = x"
   9.237 +lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   9.238    by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
   9.239  
   9.240 -lemma Lim_ident_at_within: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   9.241 -  by (rule tendsto_Lim[OF _ tendsto_ident_at_within]) auto
   9.242 -
   9.243  subsection {* Limits to @{const at_top} and @{const at_bot} *}
   9.244  
   9.245  lemma filterlim_at_top:
   9.246 @@ -1508,12 +1522,12 @@
   9.247  
   9.248  lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within:
   9.249    assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
   9.250 -  shows "eventually P (nhds a within s)"
   9.251 +  shows "eventually P (inf (nhds a) (principal s))"
   9.252  proof (rule ccontr)
   9.253    from countable_basis[of a] guess A . note A = this
   9.254 -  assume "\<not> eventually P (nhds a within s)"
   9.255 +  assume "\<not> eventually P (inf (nhds a) (principal s))"
   9.256    with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
   9.257 -    unfolding eventually_within eventually_nhds by (intro choice) fastforce
   9.258 +    unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
   9.259    then guess F ..
   9.260    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)"
   9.261      by fast+
   9.262 @@ -1524,12 +1538,12 @@
   9.263  qed
   9.264  
   9.265  lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially:
   9.266 -  "eventually P (nhds a within s) \<longleftrightarrow> 
   9.267 +  "eventually P (inf (nhds a) (principal s)) \<longleftrightarrow> 
   9.268      (\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
   9.269  proof (safe intro!: sequentially_imp_eventually_nhds_within)
   9.270 -  assume "eventually P (nhds a within s)" 
   9.271 +  assume "eventually P (inf (nhds a) (principal s))" 
   9.272    then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x"
   9.273 -    by (auto simp: eventually_within eventually_nhds)
   9.274 +    by (auto simp: eventually_inf_principal eventually_nhds)
   9.275    moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
   9.276    ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
   9.277      by (auto dest!: topological_tendstoD elim: eventually_elim1)
   9.278 @@ -1547,7 +1561,7 @@
   9.279    "f -- a --> L \<equiv> (f ---> L) (at a)"
   9.280  
   9.281  lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
   9.282 -  unfolding tendsto_def by (simp add: at_within_open)
   9.283 +  unfolding tendsto_def by (simp add: at_within_open[where S=S])
   9.284  
   9.285  lemma LIM_const_not_eq[tendsto_intros]:
   9.286    fixes a :: "'a::perfect_space"
   9.287 @@ -1581,7 +1595,7 @@
   9.288  
   9.289  lemma tendsto_at_iff_tendsto_nhds:
   9.290    "g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
   9.291 -  unfolding tendsto_def at_def eventually_within
   9.292 +  unfolding tendsto_def eventually_at_filter
   9.293    by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
   9.294  
   9.295  lemma tendsto_compose:
   9.296 @@ -1607,7 +1621,7 @@
   9.297  lemma (in first_countable_topology) sequentially_imp_eventually_within:
   9.298    "(\<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>
   9.299      eventually P (at a within s)"
   9.300 -  unfolding at_def within_within_eq
   9.301 +  unfolding at_within_def
   9.302    by (intro sequentially_imp_eventually_nhds_within) auto
   9.303  
   9.304  lemma (in first_countable_topology) sequentially_imp_eventually_at:
   9.305 @@ -1640,12 +1654,12 @@
   9.306  
   9.307  lemma continuous_on_cong [cong]:
   9.308    "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
   9.309 -  unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
   9.310 +  unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
   9.311  
   9.312  lemma continuous_on_topological:
   9.313    "continuous_on s f \<longleftrightarrow>
   9.314      (\<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)))"
   9.315 -  unfolding continuous_on_def tendsto_def eventually_within eventually_at_topological by metis
   9.316 +  unfolding continuous_on_def tendsto_def eventually_at_topological by metis
   9.317  
   9.318  lemma continuous_on_open_invariant:
   9.319    "continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> (\<exists>A. open A \<and> A \<inter> s = f -` B \<inter> s))"
   9.320 @@ -1689,7 +1703,7 @@
   9.321  
   9.322  lemma continuous_on_open_Union:
   9.323    "(\<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"
   9.324 -  unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
   9.325 +  unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)
   9.326  
   9.327  lemma continuous_on_open_UN:
   9.328    "(\<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"
   9.329 @@ -1725,7 +1739,7 @@
   9.330  setup Continuous_On_Intros.setup
   9.331  
   9.332  lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
   9.333 -  unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
   9.334 +  unfolding continuous_on_def by (fast intro: tendsto_ident_at)
   9.335  
   9.336  lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
   9.337    unfolding continuous_on_def by (auto intro: tendsto_const)
   9.338 @@ -1762,12 +1776,12 @@
   9.339    by simp
   9.340  
   9.341  lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f x) (at x within s)"
   9.342 -  by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at_within continuous_def)
   9.343 +  by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at continuous_def)
   9.344  
   9.345  lemma continuous_within_topological:
   9.346    "continuous (at x within s) f \<longleftrightarrow>
   9.347      (\<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)))"
   9.348 -  unfolding continuous_within tendsto_def eventually_within eventually_at_topological by metis
   9.349 +  unfolding continuous_within tendsto_def eventually_at_topological by metis
   9.350  
   9.351  lemma continuous_within_compose[continuous_intros]:
   9.352    "continuous (at x within s) f \<Longrightarrow> continuous (at (f x) within f ` s) g \<Longrightarrow>
   9.353 @@ -1783,7 +1797,7 @@
   9.354    using continuous_within[of x UNIV f] by simp
   9.355  
   9.356  lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
   9.357 -  unfolding continuous_within by (rule tendsto_ident_at_within)
   9.358 +  unfolding continuous_within by (rule tendsto_ident_at)
   9.359  
   9.360  lemma continuous_const[continuous_intros, simp]: "continuous F (\<lambda>x. c)"
   9.361    unfolding continuous_def by (rule tendsto_const)
   9.362 @@ -1799,10 +1813,10 @@
   9.363    by (rule continuous_at)
   9.364  
   9.365  lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
   9.366 -  by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
   9.367 +  by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
   9.368  
   9.369  lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
   9.370 -  by (simp add: continuous_on_def continuous_at tendsto_within_open)
   9.371 +  by (simp add: continuous_on_def continuous_at at_within_open[of _ s])
   9.372  
   9.373  lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
   9.374    unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)

    10.1 --- a/src/HOL/Transcendental.thy	Mon Apr 08 21:01:59 2013 +0200
    10.2 +++ b/src/HOL/Transcendental.thy	Tue Apr 09 14:04:41 2013 +0200
    10.3 @@ -1578,7 +1578,7 @@
    10.4  
    10.5  lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
    10.6    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
    10.7 -     (auto simp: eventually_within)
    10.8 +     (auto simp: eventually_at_filter)
    10.9  
   10.10  lemma ln_at_top: "LIM x at_top. ln x :> at_top"
   10.11    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
   10.12 @@ -3190,12 +3190,12 @@
   10.13  
   10.14  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
   10.15    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])
   10.16 -     (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
   10.17 +     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   10.18             intro!: tan_monotone exI[of _ "pi/2"])
   10.19  
   10.20  lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
   10.21    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])
   10.22 -     (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
   10.23 +     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   10.24             intro!: tan_monotone exI[of _ "pi/2"])
   10.25  
   10.26  lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"