modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
authorimmler
Fri Mar 10 23:16:40 2017 +0100 (2017-03-10)
changeset 65204d23eded35a33
parent 65203 314246c6eeaa
child 65205 f435640193b6
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
src/HOL/Analysis/Bounded_Continuous_Function.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Uniform_Limit.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Limits.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Sun Mar 12 19:06:10 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Mar 10 23:16:40 2017 +0100
     1.3 @@ -1,7 +1,8 @@
     1.4  section \<open>Bounded Continuous Functions\<close>
     1.5  
     1.6  theory Bounded_Continuous_Function
     1.7 -imports Henstock_Kurzweil_Integration
     1.8 +  imports
     1.9 +    Henstock_Kurzweil_Integration
    1.10  begin
    1.11  
    1.12  subsection \<open>Definition\<close>
    1.13 @@ -9,162 +10,163 @@
    1.14  definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
    1.15    where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
    1.16  
    1.17 -typedef (overloaded) ('a, 'b) bcontfun =
    1.18 -    "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
    1.19 -  by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
    1.20 +typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
    1.21 +    "{f::'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}"
    1.22 +  morphisms apply_bcontfun Bcontfun
    1.23 +  by (auto intro: continuous_intros simp: bounded_def)
    1.24 +
    1.25 +declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
    1.26 +
    1.27 +setup_lifting type_definition_bcontfun
    1.28 +
    1.29 +lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
    1.30 +  and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
    1.31 +  using apply_bcontfun[of x]
    1.32 +  by (auto simp: intro: continuous_on_subset)
    1.33 +
    1.34 +lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
    1.35 +  by transfer auto
    1.36  
    1.37  lemma bcontfunE:
    1.38 -  assumes "f \<in> bcontfun"
    1.39 -  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y"
    1.40 -  using assms unfolding bcontfun_def
    1.41 -  by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI)
    1.42 -
    1.43 -lemma bcontfunE':
    1.44 -  assumes "f \<in> bcontfun"
    1.45 -  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
    1.46 -  using assms bcontfunE
    1.47 -  by metis
    1.48 +  assumes "continuous_on UNIV f" "bounded (range f)"
    1.49 +  obtains g where "f = apply_bcontfun g"
    1.50 +  by (blast intro: apply_bcontfun_cases assms)
    1.51  
    1.52 -lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
    1.53 -  unfolding bcontfun_def
    1.54 -  by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)
    1.55 -
    1.56 -lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun"
    1.57 -  using bcontfunI by metis
    1.58 -
    1.59 -lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)"
    1.60 -  using Rep_bcontfun[of x]
    1.61 -  by (auto simp: bcontfun_def intro: continuous_on_subset)
    1.62 +lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
    1.63 +  by (auto intro!: continuous_intros simp: image_def)
    1.64  
    1.65  (* TODO: Generalize to uniform spaces? *)
    1.66  instantiation bcontfun :: (topological_space, metric_space) metric_space
    1.67  begin
    1.68  
    1.69 -definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
    1.70 -  where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
    1.71 +lift_definition dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
    1.72 +  is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
    1.73  
    1.74 -definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
    1.75 +definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
    1.76    where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.77  
    1.78 -definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
    1.79 +definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
    1.80    where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    1.81  
    1.82 +lemma bounded_dist_le_SUP_dist:
    1.83 +  "bounded (range f) \<Longrightarrow> bounded (range g) \<Longrightarrow> dist (f x) (g x) \<le> (SUP x. dist (f x) (g x))"
    1.84 +  by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp)
    1.85 +
    1.86  lemma dist_bounded:
    1.87 -  fixes f :: "('a, 'b) bcontfun"
    1.88 -  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
    1.89 -proof -
    1.90 -  have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun)
    1.91 -  from bcontfunE'[OF this] obtain y where y:
    1.92 -    "continuous_on UNIV (Rep_bcontfun f)"
    1.93 -    "\<And>x. dist (Rep_bcontfun f x) undefined \<le> y"
    1.94 -    by auto
    1.95 -  have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun)
    1.96 -  from bcontfunE'[OF this] obtain z where z:
    1.97 -    "continuous_on UNIV (Rep_bcontfun g)"
    1.98 -    "\<And>x. dist (Rep_bcontfun g x) undefined \<le> z"
    1.99 -    by auto
   1.100 -  show ?thesis
   1.101 -    unfolding dist_bcontfun_def
   1.102 -  proof (intro cSUP_upper bdd_aboveI2)
   1.103 -    fix x
   1.104 -    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
   1.105 -      dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
   1.106 -      by (rule dist_triangle2)
   1.107 -    also have "\<dots> \<le> y + z"
   1.108 -      using y(2)[of x] z(2)[of x] by (rule add_mono)
   1.109 -    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" .
   1.110 -  qed simp
   1.111 -qed
   1.112 +  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
   1.113 +  shows "dist (f x) (g x) \<le> dist f g"
   1.114 +  by transfer (auto intro!: bounded_dist_le_SUP_dist)
   1.115  
   1.116  lemma dist_bound:
   1.117 -  fixes f :: "('a, 'b) bcontfun"
   1.118 -  assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b"
   1.119 +  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
   1.120 +  assumes "\<And>x. dist (f x) (g x) \<le> b"
   1.121    shows "dist f g \<le> b"
   1.122 -  using assms by (auto simp: dist_bcontfun_def intro: cSUP_least)
   1.123 -
   1.124 -lemma dist_bounded_Abs:
   1.125 -  fixes f g :: "'a \<Rightarrow> 'b"
   1.126 -  assumes "f \<in> bcontfun" "g \<in> bcontfun"
   1.127 -  shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)"
   1.128 -  by (metis Abs_bcontfun_inverse assms dist_bounded)
   1.129 -
   1.130 -lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun"
   1.131 -  by (auto intro: bcontfunI continuous_on_const)
   1.132 +  using assms
   1.133 +  by transfer (auto intro!: cSUP_least)
   1.134  
   1.135  lemma dist_fun_lt_imp_dist_val_lt:
   1.136 +  fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
   1.137    assumes "dist f g < e"
   1.138 -  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
   1.139 +  shows "dist (f x) (g x) < e"
   1.140    using dist_bounded assms by (rule le_less_trans)
   1.141  
   1.142 -lemma dist_val_lt_imp_dist_fun_le:
   1.143 -  assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
   1.144 -  shows "dist f g \<le> e"
   1.145 -  unfolding dist_bcontfun_def
   1.146 -proof (intro cSUP_least)
   1.147 -  fix x
   1.148 -  show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e"
   1.149 -    using assms[THEN spec[where x=x]] by (simp add: dist_norm)
   1.150 -qed simp
   1.151 -
   1.152  instance
   1.153  proof
   1.154 -  fix f g h :: "('a, 'b) bcontfun"
   1.155 +  fix f g h :: "'a \<Rightarrow>\<^sub>C 'b"
   1.156    show "dist f g = 0 \<longleftrightarrow> f = g"
   1.157    proof
   1.158 -    have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
   1.159 +    have "\<And>x. dist (f x) (g x) \<le> dist f g"
   1.160        by (rule dist_bounded)
   1.161      also assume "dist f g = 0"
   1.162      finally show "f = g"
   1.163 -      by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
   1.164 +      by (auto simp: apply_bcontfun_inject[symmetric])
   1.165    qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
   1.166    show "dist f g \<le> dist f h + dist g h"
   1.167 -  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
   1.168 +  proof (rule dist_bound)
   1.169      fix x
   1.170 -    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
   1.171 -      dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)"
   1.172 +    have "dist (f x) (g x) \<le> dist (f x) (h x) + dist (g x) (h x)"
   1.173        by (rule dist_triangle2)
   1.174 -    also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h"
   1.175 +    also have "dist (f x) (h x) \<le> dist f h"
   1.176        by (rule dist_bounded)
   1.177 -    also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h"
   1.178 +    also have "dist (g x) (h x) \<le> dist g h"
   1.179        by (rule dist_bounded)
   1.180 -    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
   1.181 +    finally show "dist (f x) (g x) \<le> dist f h + dist g h"
   1.182        by simp
   1.183    qed
   1.184  qed (rule open_bcontfun_def uniformity_bcontfun_def)+
   1.185  
   1.186  end
   1.187  
   1.188 -lemma closed_Pi_bcontfun:
   1.189 +lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set"
   1.190 +  is "\<lambda>I X. Pi I X \<inter> {f. continuous_on UNIV f \<and> bounded (range f)}"
   1.191 +  by auto
   1.192 +
   1.193 +lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X"
   1.194 +  by transfer simp
   1.195 +
   1.196 +lemmas mem_PiCD = mem_PiC_iff[THEN iffD1]
   1.197 +  and mem_PiCI = mem_PiC_iff[THEN iffD2]
   1.198 +
   1.199 +lemma tendsto_bcontfun_uniform_limit:
   1.200 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   1.201 +  assumes "(f \<longlongrightarrow> l) F"
   1.202 +  shows "uniform_limit UNIV f l F"
   1.203 +proof (rule uniform_limitI)
   1.204 +  fix e::real assume "e > 0"
   1.205 +  from tendstoD[OF assms this] have "\<forall>\<^sub>F x in F. dist (f x) l < e" .
   1.206 +  then show "\<forall>\<^sub>F n in F. \<forall>x\<in>UNIV. dist ((f n) x) (l x) < e"
   1.207 +    by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt)
   1.208 +qed
   1.209 +
   1.210 +lemma uniform_limit_tendsto_bcontfun:
   1.211 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   1.212 +    and l::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   1.213 +  assumes "uniform_limit UNIV f l F"
   1.214 +  shows "(f \<longlongrightarrow> l) F"
   1.215 +proof (rule tendstoI)
   1.216 +  fix e::real assume "e > 0"
   1.217 +  then have "e / 2 > 0" by simp
   1.218 +  from uniform_limitD[OF assms this]
   1.219 +  have "\<forall>\<^sub>F i in F. \<forall>x. dist (f i x) (l x) < e / 2" by simp
   1.220 +  then have "\<forall>\<^sub>F x in F. dist (f x) l \<le> e / 2"
   1.221 +    by eventually_elim (blast intro: dist_bound less_imp_le)
   1.222 +  then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
   1.223 +    by eventually_elim (use \<open>0 < e\<close> in auto)
   1.224 +qed
   1.225 +
   1.226 +lemma uniform_limit_bcontfunE:
   1.227 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   1.228 +    and l::"'a::topological_space \<Rightarrow> 'b::metric_space"
   1.229 +  assumes "uniform_limit UNIV f l F" "F \<noteq> bot"
   1.230 +  obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   1.231 +  where "l = l'" "(f \<longlongrightarrow> l') F"
   1.232 +  by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
   1.233 +      mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun uniform_limit_theorem)
   1.234 +
   1.235 +lemma closed_PiC:
   1.236    fixes I :: "'a::metric_space set"
   1.237      and X :: "'a \<Rightarrow> 'b::complete_space set"
   1.238    assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
   1.239 -  shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))"
   1.240 +  shows "closed (PiC I X)"
   1.241    unfolding closed_sequential_limits
   1.242  proof safe
   1.243    fix f l
   1.244 -  assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l"
   1.245 -  have lim_fun: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (Rep_bcontfun l x) < e"
   1.246 -    using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
   1.247 -    by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
   1.248 -      (metis dist_fun_lt_imp_dist_val_lt)+
   1.249 -  show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)"
   1.250 -  proof (rule, safe)
   1.251 +  assume seq: "\<forall>n. f n \<in> PiC I X" and lim: "f \<longlonglongrightarrow> l"
   1.252 +  show "l \<in> PiC I X"
   1.253 +  proof (safe intro!: mem_PiCI)
   1.254      fix x assume "x \<in> I"
   1.255      then have "closed (X x)"
   1.256        using assms by simp
   1.257 -    moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially"
   1.258 -    proof (rule always_eventually, safe)
   1.259 -      fix i
   1.260 -      from seq[THEN spec, of i] \<open>x \<in> I\<close>
   1.261 -      show "Rep_bcontfun (f i) x \<in> X x"
   1.262 -        by (auto simp: Abs_bcontfun_inverse)
   1.263 -    qed
   1.264 +    moreover have "eventually (\<lambda>i. f i x \<in> X x) sequentially"
   1.265 +      using seq \<open>x \<in> I\<close>
   1.266 +      by (auto intro!: eventuallyI dest!: mem_PiCD simp: Pi_iff)
   1.267      moreover note sequentially_bot
   1.268 -    moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x"
   1.269 -      using lim_fun by (blast intro!: metric_LIMSEQ_I)
   1.270 -    ultimately show "Rep_bcontfun l x \<in> X x"
   1.271 +    moreover have "(\<lambda>n. (f n) x) \<longlonglongrightarrow> l x"
   1.272 +      using tendsto_bcontfun_uniform_limit[OF lim]
   1.273 +      by (rule tendsto_uniform_limitI) simp
   1.274 +    ultimately show "l x \<in> X x"
   1.275        by (rule Lim_in_closed_set)
   1.276 -  qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse)
   1.277 +  qed
   1.278  qed
   1.279  
   1.280  
   1.281 @@ -174,53 +176,15 @@
   1.282  proof
   1.283    fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
   1.284    assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
   1.285 -  then obtain g where limit_function:
   1.286 -    "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e"
   1.287 -    using uniformly_convergent_eq_cauchy[of "\<lambda>_. True"
   1.288 -      "\<lambda>n. Rep_bcontfun (f n)"]
   1.289 -    unfolding Cauchy_def
   1.290 +  then obtain g where "uniform_limit UNIV f g sequentially"
   1.291 +    using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" f]
   1.292 +    unfolding Cauchy_def uniform_limit_sequentially_iff
   1.293      by (metis dist_fun_lt_imp_dist_val_lt)
   1.294  
   1.295 -  then obtain N where fg_dist:  \<comment> \<open>for an upper bound on @{term g}\<close>
   1.296 -    "\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1"
   1.297 -    by (force simp add: dist_commute)
   1.298 -  from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where
   1.299 -    f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b"
   1.300 -    by force
   1.301 -  have "g \<in> bcontfun"  \<comment> \<open>The limit function is bounded and continuous\<close>
   1.302 -  proof (intro bcontfunI)
   1.303 -    show "continuous_on UNIV g"
   1.304 -      apply (rule bcontfunE[OF Rep_bcontfun])
   1.305 -      using limit_function
   1.306 -      by (auto simp add: uniform_limit_sequentially_iff intro: uniform_limit_theorem[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
   1.307 -  next
   1.308 -    fix x
   1.309 -    from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
   1.310 -      by (simp add: dist_norm norm_minus_commute)
   1.311 -    with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"]
   1.312 -    show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x]
   1.313 -      by simp
   1.314 -  qed
   1.315 -  show "convergent f"
   1.316 -  proof (rule convergentI, subst lim_sequentially, safe)
   1.317 -    \<comment> \<open>The limit function converges according to its norm\<close>
   1.318 -    fix e :: real
   1.319 -    assume "e > 0"
   1.320 -    then have "e/2 > 0" by simp
   1.321 -    with limit_function[THEN spec, of"e/2"]
   1.322 -    have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2"
   1.323 -      by simp
   1.324 -    then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto
   1.325 -    show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e"
   1.326 -    proof (rule, safe)
   1.327 -      fix n
   1.328 -      assume "N \<le> n"
   1.329 -      with N show "dist (f n) (Abs_bcontfun g) < e"
   1.330 -        using dist_val_lt_imp_dist_fun_le[of
   1.331 -          "f n" "Abs_bcontfun g" "e/2"]
   1.332 -          Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp
   1.333 -    qed
   1.334 -  qed
   1.335 +  from uniform_limit_bcontfunE[OF this sequentially_bot]
   1.336 +  obtain l' where "g = apply_bcontfun l'" "(f \<longlonglongrightarrow> l')" by metis
   1.337 +  then show "convergent f"
   1.338 +    by (intro convergentI)
   1.339  qed
   1.340  
   1.341  
   1.342 @@ -229,104 +193,42 @@
   1.343  instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
   1.344  begin
   1.345  
   1.346 -definition "-f = Abs_bcontfun (\<lambda>x. -(Rep_bcontfun f x))"
   1.347 -
   1.348 -definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)"
   1.349 +lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x"
   1.350 +  by (auto intro!: continuous_intros)
   1.351  
   1.352 -definition "f - g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x - Rep_bcontfun g x)"
   1.353 -
   1.354 -definition "0 = Abs_bcontfun (\<lambda>x. 0)"
   1.355 -
   1.356 -definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)"
   1.357 +lift_definition plus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x + g x"
   1.358 +  by (auto simp: intro!: continuous_intros bounded_plus_comp)
   1.359  
   1.360 -lemma plus_cont:
   1.361 -  fixes f g :: "'a \<Rightarrow> 'b"
   1.362 -  assumes f: "f \<in> bcontfun"
   1.363 -    and g: "g \<in> bcontfun"
   1.364 -  shows "(\<lambda>x. f x + g x) \<in> bcontfun"
   1.365 -proof -
   1.366 -  from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
   1.367 -    by auto
   1.368 -  moreover
   1.369 -  from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z"
   1.370 -    by auto
   1.371 -  ultimately show ?thesis
   1.372 -  proof (intro bcontfunI)
   1.373 -    fix x
   1.374 -    have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)"
   1.375 -      by simp
   1.376 -    also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0"
   1.377 -      by (rule dist_triangle_add)
   1.378 -    also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
   1.379 -      unfolding zero_bcontfun_def using assms
   1.380 -      by (metis add_mono const_bcontfun dist_bounded_Abs)
   1.381 -    finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
   1.382 -  qed (simp add: continuous_on_add)
   1.383 -qed
   1.384 +lift_definition minus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x - g x"
   1.385 +  by (auto simp: intro!: continuous_intros bounded_minus_comp)
   1.386  
   1.387 -lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x"
   1.388 -  by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun)
   1.389 +lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0"
   1.390 +  by (auto intro!: continuous_intros simp: image_def)
   1.391  
   1.392 -lemma uminus_cont:
   1.393 -  fixes f :: "'a \<Rightarrow> 'b"
   1.394 -  assumes "f \<in> bcontfun"
   1.395 -  shows "(\<lambda>x. - f x) \<in> bcontfun"
   1.396 -proof -
   1.397 -  from bcontfunE[OF assms, of 0] obtain y
   1.398 -    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
   1.399 -    by auto
   1.400 -  then show ?thesis
   1.401 -  proof (intro bcontfunI)
   1.402 -    fix x
   1.403 -    assume "\<And>x. dist (f x) 0 \<le> y"
   1.404 -    then show "dist (- f x) 0 \<le> y"
   1.405 -      by (subst dist_minus[symmetric]) simp
   1.406 -  qed (simp add: continuous_on_minus)
   1.407 -qed
   1.408 +lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
   1.409 +  by transfer simp
   1.410  
   1.411 -lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
   1.412 -  by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)
   1.413 +lift_definition scaleR_bcontfun::"real \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>r g x. r *\<^sub>R g x"
   1.414 +  by (auto simp: intro!: continuous_intros bounded_scaleR_comp)
   1.415  
   1.416 -lemma minus_cont:
   1.417 -  fixes f g :: "'a \<Rightarrow> 'b"
   1.418 -  assumes f: "f \<in> bcontfun"
   1.419 -    and g: "g \<in> bcontfun"
   1.420 -  shows "(\<lambda>x. f x - g x) \<in> bcontfun"
   1.421 -  using plus_cont [of f "- g"] assms
   1.422 -  by (simp add: uminus_cont fun_Compl_def)
   1.423 -
   1.424 -lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
   1.425 -  by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)
   1.426 +lemmas [simp] =
   1.427 +  const_bcontfun.rep_eq
   1.428 +  uminus_bcontfun.rep_eq
   1.429 +  plus_bcontfun.rep_eq
   1.430 +  minus_bcontfun.rep_eq
   1.431 +  zero_bcontfun.rep_eq
   1.432 +  scaleR_bcontfun.rep_eq
   1.433  
   1.434 -lemma scaleR_cont:
   1.435 -  fixes a :: real
   1.436 -    and f :: "'a \<Rightarrow> 'b"
   1.437 -  assumes "f \<in> bcontfun"
   1.438 -  shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun"
   1.439 -proof -
   1.440 -  from bcontfunE[OF assms, of 0] obtain y
   1.441 -    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
   1.442 -    by auto
   1.443 -  then show ?thesis
   1.444 -  proof (intro bcontfunI)
   1.445 -    fix x
   1.446 -    assume "\<And>x. dist (f x) 0 \<le> y"
   1.447 -    then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
   1.448 -      by (metis norm_cmul_rule_thm norm_conv_dist)
   1.449 -  qed (simp add: continuous_intros)
   1.450 -qed
   1.451 -
   1.452 -lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
   1.453 -  by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
   1.454  
   1.455  instance
   1.456 -  by standard
   1.457 -    (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
   1.458 -      Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
   1.459 -      plus_cont const_bcontfun minus_cont scaleR_cont)
   1.460 +  by standard (auto intro!: bcontfun_eqI simp: algebra_simps)
   1.461  
   1.462  end
   1.463  
   1.464 +lemma bounded_norm_le_SUP_norm:
   1.465 +  "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
   1.466 +  by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
   1.467 +
   1.468  instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
   1.469  begin
   1.470  
   1.471 @@ -340,179 +242,68 @@
   1.472    fix a :: real
   1.473    fix f g :: "('a, 'b) bcontfun"
   1.474    show "dist f g = norm (f - g)"
   1.475 -    by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
   1.476 -      Abs_bcontfun_inverse const_bcontfun dist_norm)
   1.477 +    unfolding norm_bcontfun_def
   1.478 +    by transfer (simp add: dist_norm)
   1.479    show "norm (f + g) \<le> norm f + norm g"
   1.480      unfolding norm_bcontfun_def
   1.481 -  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
   1.482 -    fix x
   1.483 -    have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le>
   1.484 -      dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0"
   1.485 -      by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm
   1.486 -        le_less_linear less_irrefl norm_triangle_lt)
   1.487 -    also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0"
   1.488 -      using dist_bounded[of f x 0]
   1.489 -      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
   1.490 -    also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0]
   1.491 -      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
   1.492 -    finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp
   1.493 -  qed
   1.494 +    by transfer
   1.495 +      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm simp: dist_norm)
   1.496    show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   1.497 -  proof -
   1.498 -    have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) =
   1.499 -      (SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)"
   1.500 -    proof (intro continuous_at_Sup_mono bdd_aboveI2)
   1.501 -      fix x
   1.502 -      show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0]
   1.503 -        by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
   1.504 -          const_bcontfun)
   1.505 -    qed (auto intro!: monoI mult_left_mono continuous_intros)
   1.506 -    moreover
   1.507 -    have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
   1.508 -      (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
   1.509 -      by auto
   1.510 -    ultimately
   1.511 -    show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   1.512 -      by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse
   1.513 -        zero_bcontfun_def const_bcontfun image_image)
   1.514 -  qed
   1.515 +    unfolding norm_bcontfun_def
   1.516 +    apply transfer
   1.517 +    by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
   1.518 +      (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
   1.519 +        simp: bounded_norm_comp)
   1.520  qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
   1.521  
   1.522  end
   1.523  
   1.524 -lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
   1.525 -  by (metis bcontfunI dist_0_norm dist_commute)
   1.526 -
   1.527  lemma norm_bounded:
   1.528    fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   1.529 -  shows "norm (Rep_bcontfun f x) \<le> norm f"
   1.530 +  shows "norm (apply_bcontfun f x) \<le> norm f"
   1.531    using dist_bounded[of f x 0]
   1.532 -  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
   1.533 -    const_bcontfun)
   1.534 +  by (simp add: dist_norm)
   1.535  
   1.536  lemma norm_bound:
   1.537    fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   1.538 -  assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
   1.539 +  assumes "\<And>x. norm (apply_bcontfun f x) \<le> b"
   1.540    shows "norm f \<le> b"
   1.541    using dist_bound[of f 0 b] assms
   1.542 -  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun)
   1.543 -
   1.544 -
   1.545 -subsection \<open>Continuously Extended Functions\<close>
   1.546 -
   1.547 -definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.548 -  "clamp a b x = (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)"
   1.549 -
   1.550 -definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
   1.551 -  where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))"
   1.552 -
   1.553 -lemma ext_cont_def':
   1.554 -  "ext_cont f a b = Abs_bcontfun (\<lambda>x.
   1.555 -    f (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i))"
   1.556 -  unfolding ext_cont_def clamp_def ..
   1.557 -
   1.558 -lemma clamp_in_interval:
   1.559 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.560 -  shows "clamp a b x \<in> cbox a b"
   1.561 -  unfolding clamp_def
   1.562 -  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
   1.563 -
   1.564 -lemma dist_clamps_le_dist_args:
   1.565 -  fixes x :: "'a::euclidean_space"
   1.566 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.567 -  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
   1.568 -proof -
   1.569 -  from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   1.570 -    by (simp add: cbox_def)
   1.571 -  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
   1.572 -    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
   1.573 -    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
   1.574 -  then show ?thesis
   1.575 -    by (auto intro: real_sqrt_le_mono
   1.576 -      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
   1.577 -qed
   1.578 +  by (simp add: dist_norm)
   1.579  
   1.580 -lemma clamp_continuous_at:
   1.581 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   1.582 -    and x :: 'a
   1.583 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.584 -    and f_cont: "continuous_on (cbox a b) f"
   1.585 -  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
   1.586 -  unfolding continuous_at_eps_delta
   1.587 -proof safe
   1.588 -  fix x :: 'a
   1.589 -  fix e :: real
   1.590 -  assume "e > 0"
   1.591 -  moreover have "clamp a b x \<in> cbox a b"
   1.592 -    by (simp add: clamp_in_interval assms)
   1.593 -  moreover note f_cont[simplified continuous_on_iff]
   1.594 -  ultimately
   1.595 -  obtain d where d: "0 < d"
   1.596 -    "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
   1.597 -    by force
   1.598 -  show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
   1.599 -    dist (f (clamp a b x')) (f (clamp a b x)) < e"
   1.600 -    by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans])
   1.601 -qed
   1.602 -
   1.603 -lemma clamp_continuous_on:
   1.604 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   1.605 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.606 -    and f_cont: "continuous_on (cbox a b) f"
   1.607 -  shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))"
   1.608 -  using assms
   1.609 -  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
   1.610 -
   1.611 -lemma clamp_bcontfun:
   1.612 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   1.613 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   1.614 -    and continuous: "continuous_on (cbox a b) f"
   1.615 -  shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
   1.616 -proof -
   1.617 -  have "bounded (f ` (cbox a b))"
   1.618 -    by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
   1.619 -  then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c"
   1.620 -    by (auto simp add: bounded_pos)
   1.621 -  show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
   1.622 -  proof (intro bcontfun_normI)
   1.623 -    fix x
   1.624 -    show "norm (f (clamp a b x)) \<le> c"
   1.625 -      using clamp_in_interval[OF assms(1), of x] f_bound
   1.626 -      by (simp add: ext_cont_def)
   1.627 -  qed (simp add: clamp_continuous_on assms)
   1.628 -qed
   1.629 +subsection \<open>(bounded) continuous extenstion\<close>
   1.630  
   1.631  lemma integral_clamp:
   1.632    "integral {t0::real..clamp t0 t1 x} f =
   1.633      (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
   1.634    by (auto simp: clamp_def)
   1.635  
   1.636 -
   1.637 -declare [[coercion Rep_bcontfun]]
   1.638 +lemma continuous_on_interval_bcontfunE:
   1.639 +  fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::metric_space"
   1.640 +  assumes "continuous_on {a .. b} f"
   1.641 +  obtains g::"'a \<Rightarrow>\<^sub>C 'b" where
   1.642 +    "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> g x = f x"
   1.643 +    "\<And>x. g x = f (clamp a b x)"
   1.644 +proof -
   1.645 +  define g where "g \<equiv> ext_cont f a b"
   1.646 +  have "continuous_on UNIV g"
   1.647 +    using assms
   1.648 +    by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval)
   1.649 +  moreover
   1.650 +  have "bounded (range g)"
   1.651 +    by (auto simp: g_def ext_cont_def cbox_interval
   1.652 +        intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
   1.653 +  ultimately
   1.654 +  obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
   1.655 +  then have "h x = f x" if "a \<le> x" "x \<le> b" for x
   1.656 +    by (auto simp: h[symmetric] g_def cbox_interval that)
   1.657 +  moreover
   1.658 +  have "h x = f (clamp a b x)" for x
   1.659 +    by (auto simp: h[symmetric] g_def ext_cont_def)
   1.660 +  ultimately show ?thesis ..
   1.661 +qed
   1.662  
   1.663 -lemma ext_cont_cancel[simp]:
   1.664 -  fixes x a b :: "'a::euclidean_space"
   1.665 -  assumes x: "x \<in> cbox a b"
   1.666 -    and "continuous_on (cbox a b) f"
   1.667 -  shows "ext_cont f a b x = f x"
   1.668 -  using assms
   1.669 -  unfolding ext_cont_def
   1.670 -proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun])
   1.671 -  show "f (clamp a b x) = f x"
   1.672 -    using x unfolding clamp_def mem_box
   1.673 -    by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less)
   1.674 -qed (auto simp: cbox_def)
   1.675 -
   1.676 -lemma ext_cont_cong:
   1.677 -  assumes "t0 = s0"
   1.678 -    and "t1 = s1"
   1.679 -    and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
   1.680 -    and "continuous_on (cbox t0 t1) f"
   1.681 -    and "continuous_on (cbox s0 s1) g"
   1.682 -    and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
   1.683 -  shows "ext_cont f t0 t1 = ext_cont g s0 s1"
   1.684 -  unfolding assms ext_cont_def
   1.685 -  using assms clamp_in_interval[OF ord]
   1.686 -  by (subst Rep_bcontfun_inject[symmetric]) simp
   1.687 +lifting_update bcontfun.lifting
   1.688 +lifting_forget bcontfun.lifting
   1.689  
   1.690  end
     2.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Mar 12 19:06:10 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Mar 10 23:16:40 2017 +0100
     2.3 @@ -2543,4 +2543,69 @@
     2.4      by simp
     2.5  qed
     2.6  
     2.7 +lemma has_integral_0_closure_imp_0:
     2.8 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
     2.9 +  assumes f: "continuous_on (closure S) f"
    2.10 +    and nonneg_interior: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
    2.11 +    and pos: "0 < emeasure lborel S"
    2.12 +    and finite: "emeasure lborel S < \<infinity>"
    2.13 +    and regular: "emeasure lborel (closure S) = emeasure lborel S"
    2.14 +    and opn: "open S"
    2.15 +  assumes int: "(f has_integral 0) (closure S)"
    2.16 +  assumes x: "x \<in> closure S"
    2.17 +  shows "f x = 0"
    2.18 +proof -
    2.19 +  have zero: "emeasure lborel (frontier S) = 0"
    2.20 +    using finite closure_subset regular
    2.21 +    unfolding frontier_def
    2.22 +    by (subst emeasure_Diff) (auto simp: frontier_def interior_open \<open>open S\<close> )
    2.23 +  have nonneg: "0 \<le> f x" if "x \<in> closure S" for x
    2.24 +    using continuous_ge_on_closure[OF f that nonneg_interior] by simp
    2.25 +  have "0 = integral (closure S) f"
    2.26 +    by (blast intro: int sym)
    2.27 +  also
    2.28 +  note intl = has_integral_integrable[OF int]
    2.29 +  have af: "f absolutely_integrable_on (closure S)"
    2.30 +    using nonneg
    2.31 +    by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
    2.32 +  then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
    2.33 +    by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
    2.34 +  also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
    2.35 +    by (rule integral_nonneg_eq_0_iff_AE[OF af]) (use nonneg in \<open>auto simp: indicator_def\<close>)
    2.36 +  also have "\<dots> \<longleftrightarrow> (AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})"
    2.37 +    by (auto simp: indicator_def)
    2.38 +  finally have "(AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})" by simp
    2.39 +  moreover have "(AE x in lebesgue. x \<in> - frontier S)"
    2.40 +    using zero
    2.41 +    by (auto simp: eventually_ae_filter null_sets_def intro!: exI[where x="frontier S"])
    2.42 +  ultimately have ae: "AE x \<in> S in lebesgue. x \<in> {x \<in> closure S. f x = 0}" (is ?th)
    2.43 +    by eventually_elim (use closure_subset in \<open>auto simp: \<close>)
    2.44 +  have "closed {0::real}" by simp
    2.45 +  with continuous_on_closed_vimage[OF closed_closure, of S f] f
    2.46 +  have "closed (f -` {0} \<inter> closure S)" by blast
    2.47 +  then have "closed {x \<in> closure S. f x = 0}" by (auto simp: vimage_def Int_def conj_commute)
    2.48 +  with \<open>open S\<close> have "x \<in> {x \<in> closure S. f x = 0}" if "x \<in> S" for x using ae that
    2.49 +    by (rule mem_closed_if_AE_lebesgue_open)
    2.50 +  then have "f x = 0" if "x \<in> S" for x using that by auto
    2.51 +  from continuous_constant_on_closure[OF f this \<open>x \<in> closure S\<close>]
    2.52 +  show "f x = 0" .
    2.53 +qed
    2.54 +
    2.55 +lemma has_integral_0_cbox_imp_0:
    2.56 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
    2.57 +  assumes f: "continuous_on (cbox a b) f"
    2.58 +    and nonneg_interior: "\<And>x. x \<in> box a b \<Longrightarrow> 0 \<le> f x"
    2.59 +  assumes int: "(f has_integral 0) (cbox a b)"
    2.60 +  assumes ne: "box a b \<noteq> {}"
    2.61 +  assumes x: "x \<in> cbox a b"
    2.62 +  shows "f x = 0"
    2.63 +proof -
    2.64 +  have "0 < emeasure lborel (box a b)"
    2.65 +    using ne x unfolding emeasure_lborel_box_eq
    2.66 +    by (force intro!: prod_pos simp: mem_box algebra_simps)
    2.67 +  then show ?thesis using assms
    2.68 +    by (intro has_integral_0_closure_imp_0[of "box a b" f x])
    2.69 +      (auto simp: emeasure_lborel_box_eq emeasure_lborel_cbox_eq algebra_simps mem_box)
    2.70 +qed
    2.71 +
    2.72  end
     3.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Mar 12 19:06:10 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Mar 10 23:16:40 2017 +0100
     3.3 @@ -268,6 +268,9 @@
     3.4  
     3.5  subsection \<open>Basic theorems about integrals.\<close>
     3.6  
     3.7 +lemma has_integral_eq_rhs: "(f has_integral j) S \<Longrightarrow> i = j \<Longrightarrow> (f has_integral i) S"
     3.8 +  by (rule forw_subst)
     3.9 +
    3.10  lemma has_integral_unique:
    3.11    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
    3.12    assumes "(f has_integral k1) i"
    3.13 @@ -499,6 +502,9 @@
    3.14  lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) s"
    3.15    by (drule_tac c="-1" in has_integral_cmul) auto
    3.16  
    3.17 +lemma has_integral_neg_iff: "((\<lambda>x. - f x) has_integral k) s \<longleftrightarrow> (f has_integral - k) s"
    3.18 +  using has_integral_neg[of f "- k"] has_integral_neg[of "\<lambda>x. - f x" k] by auto
    3.19 +
    3.20  lemma has_integral_add:
    3.21    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
    3.22    assumes "(f has_integral k) s"
    3.23 @@ -2604,11 +2610,14 @@
    3.24      by auto
    3.25  qed
    3.26  
    3.27 -lemma integrable_continuous_real:
    3.28 -  fixes f :: "real \<Rightarrow> 'a::banach"
    3.29 +lemma integrable_continuous_interval:
    3.30 +  fixes f :: "'b::ordered_euclidean_space \<Rightarrow> 'a::banach"
    3.31    assumes "continuous_on {a .. b} f"
    3.32    shows "f integrable_on {a .. b}"
    3.33 -  by (metis assms box_real(2) integrable_continuous)
    3.34 +  by (metis assms integrable_continuous interval_cbox)
    3.35 +
    3.36 +lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
    3.37 +
    3.38  
    3.39  subsection \<open>Specialization of additivity to one dimension.\<close>
    3.40  
    3.41 @@ -4566,6 +4575,18 @@
    3.42    qed
    3.43  qed
    3.44  
    3.45 +lemma indefinite_integral_continuous':
    3.46 +  fixes f::"real \<Rightarrow> 'a::banach"
    3.47 +  assumes "f integrable_on {a..b}"
    3.48 +  shows "continuous_on {a..b} (\<lambda>x. integral {x..b} f)"
    3.49 +proof -
    3.50 +  have "integral {a .. b} f - integral {a .. x} f = integral {x .. b} f" if "x \<in> {a .. b}" for x
    3.51 +    using integral_combine[OF _ _ assms, of x] that
    3.52 +    by (auto simp: algebra_simps)
    3.53 +  with _ show ?thesis
    3.54 +    by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous assms)
    3.55 +qed
    3.56 +
    3.57  
    3.58  subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
    3.59  
    3.60 @@ -7282,7 +7303,7 @@
    3.61  
    3.62  subsection \<open>Exchange uniform limit and integral\<close>
    3.63  
    3.64 -lemma uniform_limit_integral:
    3.65 +lemma uniform_limit_integral_cbox:
    3.66    fixes f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
    3.67    assumes u: "uniform_limit (cbox a b) f g F"
    3.68    assumes c: "\<And>n. continuous_on (cbox a b) (f n)"
    3.69 @@ -7344,6 +7365,17 @@
    3.70    ultimately show ?thesis ..
    3.71  qed
    3.72  
    3.73 +lemma uniform_limit_integral:
    3.74 +  fixes f::"'a \<Rightarrow> 'b::ordered_euclidean_space \<Rightarrow> 'c::banach"
    3.75 +  assumes u: "uniform_limit {a .. b} f g F"
    3.76 +  assumes c: "\<And>n. continuous_on {a .. b} (f n)"
    3.77 +  assumes [simp]: "F \<noteq> bot"
    3.78 +  obtains I J where
    3.79 +    "\<And>n. (f n has_integral I n) {a .. b}"
    3.80 +    "(g has_integral J) {a .. b}"
    3.81 +    "(I \<longlongrightarrow> J) F"
    3.82 +  by (metis interval_cbox assms uniform_limit_integral_cbox)
    3.83 +
    3.84  
    3.85  subsection \<open>Integration by parts\<close>
    3.86  
    3.87 @@ -7428,15 +7460,15 @@
    3.88  subsection \<open>Integration by substitution\<close>
    3.89  
    3.90  
    3.91 -lemma has_integral_substitution_strong:
    3.92 +lemma has_integral_substitution_general:
    3.93    fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
    3.94 -  assumes s: "finite s" and le: "a \<le> b" "c \<le> d" "g a \<le> g b"
    3.95 +  assumes s: "finite s" and le: "a \<le> b"
    3.96        and subset: "g ` {a..b} \<subseteq> {c..d}"
    3.97        and f [continuous_intros]: "continuous_on {c..d} f"
    3.98        and g [continuous_intros]: "continuous_on {a..b} g"
    3.99        and deriv [derivative_intros]:
   3.100                "\<And>x. x \<in> {a..b} - s \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
   3.101 -    shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
   3.102 +    shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}"
   3.103  proof -
   3.104    let ?F = "\<lambda>x. integral {c..g x} f"
   3.105    have cont_int: "continuous_on {a..b} ?F"
   3.106 @@ -7461,22 +7493,48 @@
   3.107    have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
   3.108      using le cont_int s deriv cont_int
   3.109      by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
   3.110 -  also from subset have "g x \<in> {c..d}" if "x \<in> {a..b}" for x using that by blast
   3.111 -  from this[of a] this[of b] le have "c \<le> g a" "g b \<le> d" by auto
   3.112 -  hence "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
   3.113 -    by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
   3.114 -  hence "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f"
   3.115 -    by (simp add: algebra_simps)
   3.116 +  also
   3.117 +  from subset have "g x \<in> {c..d}" if "x \<in> {a..b}" for x using that by blast
   3.118 +  from this[of a] this[of b] le have cd: "c \<le> g a" "g b \<le> d" "c \<le> g b" "g a \<le> d" by auto
   3.119 +  have "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f"
   3.120 +  proof cases
   3.121 +    assume "g a \<le> g b"
   3.122 +    note le = le this
   3.123 +    from cd have "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
   3.124 +      by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
   3.125 +    with le show ?thesis
   3.126 +      by (cases "g a = g b") (simp_all add: algebra_simps)
   3.127 +  next
   3.128 +    assume less: "\<not>g a \<le> g b"
   3.129 +    then have "g a \<ge> g b" by simp
   3.130 +    note le = le this
   3.131 +    from cd have "integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f"
   3.132 +      by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
   3.133 +    with less show ?thesis
   3.134 +      by (simp_all add: algebra_simps)
   3.135 +  qed
   3.136    finally show ?thesis .
   3.137  qed
   3.138  
   3.139 +lemma has_integral_substitution_strong:
   3.140 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
   3.141 +  assumes s: "finite s" and le: "a \<le> b" "g a \<le> g b"
   3.142 +    and subset: "g ` {a..b} \<subseteq> {c..d}"
   3.143 +    and f [continuous_intros]: "continuous_on {c..d} f"
   3.144 +    and g [continuous_intros]: "continuous_on {a..b} g"
   3.145 +    and deriv [derivative_intros]:
   3.146 +    "\<And>x. x \<in> {a..b} - s \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
   3.147 +  shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
   3.148 +  using has_integral_substitution_general[OF s le(1) subset f g deriv] le(2)
   3.149 +  by (cases "g a = g b") auto
   3.150 +
   3.151  lemma has_integral_substitution:
   3.152    fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
   3.153 -  assumes "a \<le> b" "c \<le> d" "g a \<le> g b" "g ` {a..b} \<subseteq> {c..d}"
   3.154 +  assumes "a \<le> b" "g a \<le> g b" "g ` {a..b} \<subseteq> {c..d}"
   3.155        and "continuous_on {c..d} f"
   3.156        and "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
   3.157      shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
   3.158 -  by (intro has_integral_substitution_strong[of "{}" a b c d] assms)
   3.159 +  by (intro has_integral_substitution_strong[of "{}" a b g c d] assms)
   3.160       (auto intro: DERIV_continuous_on assms)
   3.161  
   3.162  
     4.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Mar 12 19:06:10 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Mar 10 23:16:40 2017 +0100
     4.3 @@ -586,6 +586,33 @@
     4.4    ultimately show False by contradiction
     4.5  qed
     4.6  
     4.7 +lemma mem_closed_if_AE_lebesgue_open:
     4.8 +  assumes "open S" "closed C"
     4.9 +  assumes "AE x \<in> S in lebesgue. x \<in> C"
    4.10 +  assumes "x \<in> S"
    4.11 +  shows "x \<in> C"
    4.12 +proof (rule ccontr)
    4.13 +  assume xC: "x \<notin> C"
    4.14 +  with openE[of "S - C"] assms
    4.15 +  obtain e where e: "0 < e" "ball x e \<subseteq> S - C"
    4.16 +    by blast
    4.17 +  then obtain a b where box: "x \<in> box a b" "box a b \<subseteq> S - C"
    4.18 +    by (metis rational_boxes order_trans)
    4.19 +  then have "0 < emeasure lebesgue (box a b)"
    4.20 +    by (auto simp: emeasure_lborel_box_eq mem_box algebra_simps intro!: prod_pos)
    4.21 +  also have "\<dots> \<le> emeasure lebesgue (S - C)"
    4.22 +    using assms box
    4.23 +    by (auto intro!: emeasure_mono)
    4.24 +  also have "\<dots> = 0"
    4.25 +    using assms
    4.26 +    by (auto simp: eventually_ae_filter completion.complete2 set_diff_eq null_setsD1)
    4.27 +  finally show False by simp
    4.28 +qed
    4.29 +
    4.30 +lemma mem_closed_if_AE_lebesgue: "closed C \<Longrightarrow> (AE x in lebesgue. x \<in> C) \<Longrightarrow> x \<in> C"
    4.31 +  using mem_closed_if_AE_lebesgue_open[OF open_UNIV] by simp
    4.32 +
    4.33 +
    4.34  subsection \<open>Affine transformation on the Lebesgue-Borel\<close>
    4.35  
    4.36  lemma lborel_eqI:
     5.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Mar 12 19:06:10 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Mar 10 23:16:40 2017 +0100
     5.3 @@ -3940,6 +3940,9 @@
     5.4  lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
     5.5    by (simp add: bounded_iff bdd_above_def)
     5.6  
     5.7 +lemma bounded_norm_comp: "bounded ((\<lambda>x. norm (f x)) ` S) = bounded (f ` S)"
     5.8 +  by (simp add: bounded_iff)
     5.9 +
    5.10  lemma boundedI:
    5.11    assumes "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
    5.12    shows "bounded S"
    5.13 @@ -4056,6 +4059,19 @@
    5.14      shows "bounded (- S) \<Longrightarrow> ~ (bounded S)"
    5.15    using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
    5.16  
    5.17 +lemma bounded_dist_comp:
    5.18 +  assumes "bounded (f ` S)" "bounded (g ` S)"
    5.19 +  shows "bounded ((\<lambda>x. dist (f x) (g x)) ` S)"
    5.20 +proof -
    5.21 +  from assms obtain M1 M2 where *: "dist (f x) undefined \<le> M1" "dist undefined (g x) \<le> M2" if "x \<in> S" for x
    5.22 +    by (auto simp: bounded_any_center[of _ undefined] dist_commute)
    5.23 +  have "dist (f x) (g x) \<le> M1 + M2" if "x \<in> S" for x
    5.24 +    using *[OF that]
    5.25 +    by (rule order_trans[OF dist_triangle add_mono])
    5.26 +  then show ?thesis
    5.27 +    by (auto intro!: boundedI)
    5.28 +qed
    5.29 +
    5.30  lemma bounded_linear_image:
    5.31    assumes "bounded S"
    5.32      and "bounded_linear f"
    5.33 @@ -4090,6 +4106,13 @@
    5.34    apply (rule bounded_linear_scaleR_right)
    5.35    done
    5.36  
    5.37 +lemma bounded_scaleR_comp:
    5.38 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.39 +  assumes "bounded (f ` S)"
    5.40 +  shows "bounded ((\<lambda>x. r *\<^sub>R f x) ` S)"
    5.41 +  using bounded_scaling[of "f ` S" r] assms
    5.42 +  by (auto simp: image_image)
    5.43 +
    5.44  lemma bounded_translation:
    5.45    fixes S :: "'a::real_normed_vector set"
    5.46    assumes "bounded S"
    5.47 @@ -4119,6 +4142,33 @@
    5.48    shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
    5.49  by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
    5.50  
    5.51 +lemma uminus_bounded_comp [simp]:
    5.52 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.53 +  shows "bounded ((\<lambda>x. - f x) ` S) \<longleftrightarrow> bounded (f ` S)"
    5.54 +  using bounded_uminus[of "f ` S"]
    5.55 +  by (auto simp: image_image)
    5.56 +
    5.57 +lemma bounded_plus_comp:
    5.58 +  fixes f g::"'a \<Rightarrow> 'b::real_normed_vector"
    5.59 +  assumes "bounded (f ` S)"
    5.60 +  assumes "bounded (g ` S)"
    5.61 +  shows "bounded ((\<lambda>x. f x + g x) ` S)"
    5.62 +proof -
    5.63 +  {
    5.64 +    fix B C
    5.65 +    assume "\<And>x. x\<in>S \<Longrightarrow> norm (f x) \<le> B" "\<And>x. x\<in>S \<Longrightarrow> norm (g x) \<le> C"
    5.66 +    then have "\<And>x. x \<in> S \<Longrightarrow> norm (f x + g x) \<le> B + C"
    5.67 +      by (auto intro!: norm_triangle_le add_mono)
    5.68 +  } then show ?thesis
    5.69 +    using assms by (fastforce simp: bounded_iff)
    5.70 +qed
    5.71 +
    5.72 +lemma bounded_minus_comp:
    5.73 +  "bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
    5.74 +  for f g::"'a \<Rightarrow> 'b::real_normed_vector"
    5.75 +  using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
    5.76 +  by (auto simp: )
    5.77 +
    5.78  
    5.79  subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
    5.80  
    5.81 @@ -5915,89 +5965,6 @@
    5.82    then show ?thesis ..
    5.83  qed
    5.84  
    5.85 -text\<open>Cauchy-type criteria for uniform convergence.\<close>
    5.86 -
    5.87 -lemma uniformly_convergent_eq_cauchy:
    5.88 -  fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
    5.89 -  shows
    5.90 -    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
    5.91 -      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  \<longrightarrow> dist (s m x) (s n x) < e)"
    5.92 -  (is "?lhs = ?rhs")
    5.93 -proof
    5.94 -  assume ?lhs
    5.95 -  then obtain l where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e"
    5.96 -    by auto
    5.97 -  {
    5.98 -    fix e :: real
    5.99 -    assume "e > 0"
   5.100 -    then obtain N :: nat where N: "\<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e / 2"
   5.101 -      using l[THEN spec[where x="e/2"]] by auto
   5.102 -    {
   5.103 -      fix n m :: nat and x :: "'b"
   5.104 -      assume "N \<le> m \<and> N \<le> n \<and> P x"
   5.105 -      then have "dist (s m x) (s n x) < e"
   5.106 -        using N[THEN spec[where x=m], THEN spec[where x=x]]
   5.107 -        using N[THEN spec[where x=n], THEN spec[where x=x]]
   5.108 -        using dist_triangle_half_l[of "s m x" "l x" e "s n x"] by auto
   5.109 -    }
   5.110 -    then have "\<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  --> dist (s m x) (s n x) < e"  by auto
   5.111 -  }
   5.112 -  then show ?rhs by auto
   5.113 -next
   5.114 -  assume ?rhs
   5.115 -  then have "\<forall>x. P x \<longrightarrow> Cauchy (\<lambda>n. s n x)"
   5.116 -    unfolding cauchy_def
   5.117 -    apply auto
   5.118 -    apply (erule_tac x=e in allE)
   5.119 -    apply auto
   5.120 -    done
   5.121 -  then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l x) sequentially"
   5.122 -    unfolding convergent_eq_Cauchy[symmetric]
   5.123 -    using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l) sequentially"]
   5.124 -    by auto
   5.125 -  {
   5.126 -    fix e :: real
   5.127 -    assume "e > 0"
   5.128 -    then obtain N where N:"\<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x \<longrightarrow> dist (s m x) (s n x) < e/2"
   5.129 -      using \<open>?rhs\<close>[THEN spec[where x="e/2"]] by auto
   5.130 -    {
   5.131 -      fix x
   5.132 -      assume "P x"
   5.133 -      then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2"
   5.134 -        using l[THEN spec[where x=x], unfolded lim_sequentially] and \<open>e > 0\<close>
   5.135 -        by (auto elim!: allE[where x="e/2"])
   5.136 -      fix n :: nat
   5.137 -      assume "n \<ge> N"
   5.138 -      then have "dist(s n x)(l x) < e"
   5.139 -        using \<open>P x\<close>and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]]
   5.140 -        using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"]
   5.141 -        by (auto simp add: dist_commute)
   5.142 -    }
   5.143 -    then have "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
   5.144 -      by auto
   5.145 -  }
   5.146 -  then show ?lhs by auto
   5.147 -qed
   5.148 -
   5.149 -lemma uniformly_cauchy_imp_uniformly_convergent:
   5.150 -  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
   5.151 -  assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
   5.152 -    and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
   5.153 -  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
   5.154 -proof -
   5.155 -  obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
   5.156 -    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
   5.157 -  moreover
   5.158 -  {
   5.159 -    fix x
   5.160 -    assume "P x"
   5.161 -    then have "l x = l' x"
   5.162 -      using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
   5.163 -      using l and assms(2) unfolding lim_sequentially by blast
   5.164 -  }
   5.165 -  ultimately show ?thesis by auto
   5.166 -qed
   5.167 -
   5.168  
   5.169  subsection \<open>Continuity\<close>
   5.170  
   5.171 @@ -10960,6 +10927,109 @@
   5.172    by blast
   5.173  
   5.174  
   5.175 +
   5.176 +subsection \<open>Continuous Extension\<close>
   5.177 +
   5.178 +definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   5.179 +  "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
   5.180 +    then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
   5.181 +    else a)"
   5.182 +
   5.183 +lemma clamp_in_interval[simp]:
   5.184 +  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
   5.185 +  shows "clamp a b x \<in> cbox a b"
   5.186 +  unfolding clamp_def
   5.187 +  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
   5.188 +
   5.189 +lemma clamp_cancel_cbox[simp]:
   5.190 +  fixes x a b :: "'a::euclidean_space"
   5.191 +  assumes x: "x \<in> cbox a b"
   5.192 +  shows "clamp a b x = x"
   5.193 +  using assms
   5.194 +  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
   5.195 +
   5.196 +lemma clamp_empty_interval:
   5.197 +  assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
   5.198 +  shows "clamp a b = (\<lambda>_. a)"
   5.199 +  using assms
   5.200 +  by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
   5.201 +
   5.202 +lemma dist_clamps_le_dist_args:
   5.203 +  fixes x :: "'a::euclidean_space"
   5.204 +  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
   5.205 +proof cases
   5.206 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   5.207 +  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
   5.208 +    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
   5.209 +    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
   5.210 +  then show ?thesis
   5.211 +    by (auto intro: real_sqrt_le_mono
   5.212 +      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
   5.213 +qed (auto simp: clamp_def)
   5.214 +
   5.215 +lemma clamp_continuous_at:
   5.216 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   5.217 +    and x :: 'a
   5.218 +  assumes f_cont: "continuous_on (cbox a b) f"
   5.219 +  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
   5.220 +proof cases
   5.221 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   5.222 +  show ?thesis
   5.223 +    unfolding continuous_at_eps_delta
   5.224 +  proof safe
   5.225 +    fix x :: 'a
   5.226 +    fix e :: real
   5.227 +    assume "e > 0"
   5.228 +    moreover have "clamp a b x \<in> cbox a b"
   5.229 +      by (simp add: clamp_in_interval le)
   5.230 +    moreover note f_cont[simplified continuous_on_iff]
   5.231 +    ultimately
   5.232 +    obtain d where d: "0 < d"
   5.233 +      "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
   5.234 +      by force
   5.235 +    show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
   5.236 +      dist (f (clamp a b x')) (f (clamp a b x)) < e"
   5.237 +      using le
   5.238 +      by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
   5.239 +  qed
   5.240 +qed (auto simp: clamp_empty_interval)
   5.241 +
   5.242 +lemma clamp_continuous_on:
   5.243 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   5.244 +  assumes f_cont: "continuous_on (cbox a b) f"
   5.245 +  shows "continuous_on S (\<lambda>x. f (clamp a b x))"
   5.246 +  using assms
   5.247 +  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
   5.248 +
   5.249 +lemma clamp_bounded:
   5.250 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
   5.251 +  assumes bounded: "bounded (f ` (cbox a b))"
   5.252 +  shows "bounded (range (\<lambda>x. f (clamp a b x)))"
   5.253 +proof cases
   5.254 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
   5.255 +  from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
   5.256 +    by (auto simp add: bounded_any_center[where a=undefined])
   5.257 +  then show ?thesis
   5.258 +    by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
   5.259 +        simp: bounded_any_center[where a=undefined])
   5.260 +qed (auto simp: clamp_empty_interval image_def)
   5.261 +
   5.262 +
   5.263 +definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
   5.264 +  where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
   5.265 +
   5.266 +lemma ext_cont_cancel_cbox[simp]:
   5.267 +  fixes x a b :: "'a::euclidean_space"
   5.268 +  assumes x: "x \<in> cbox a b"
   5.269 +  shows "ext_cont f a b x = f x"
   5.270 +  using assms
   5.271 +  unfolding ext_cont_def
   5.272 +  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
   5.273 +
   5.274 +lemma continuous_on_ext_cont[continuous_intros]:
   5.275 +  "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
   5.276 +  by (auto intro!: clamp_continuous_on simp: ext_cont_def)
   5.277 +
   5.278  no_notation
   5.279    eucl_less (infix "<e" 50)
   5.280  
     6.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Mar 12 19:06:10 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Fri Mar 10 23:16:40 2017 +0100
     6.3 @@ -203,6 +203,8 @@
     6.4  lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
     6.5    by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
     6.6  
     6.7 +text\<open>Cauchy-type criteria for uniform convergence.\<close>
     6.8 +
     6.9  lemma Cauchy_uniformly_convergent:
    6.10    fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
    6.11    assumes "uniformly_Cauchy_on X f"
    6.12 @@ -235,6 +237,62 @@
    6.13    qed
    6.14  qed
    6.15  
    6.16 +lemma uniformly_convergent_Cauchy:
    6.17 +  assumes "uniformly_convergent_on X f"
    6.18 +  shows "uniformly_Cauchy_on X f"
    6.19 +proof (rule uniformly_Cauchy_onI)
    6.20 +  fix e::real assume "e > 0"
    6.21 +  then have "0 < e / 2" by simp
    6.22 +  with assms[unfolded uniformly_convergent_on_def uniform_limit_sequentially_iff]
    6.23 +  obtain l N where l:"x \<in> X \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f n x) (l x) < e / 2" for n x
    6.24 +    by metis
    6.25 +  from l l have "x \<in> X \<Longrightarrow> n \<ge> N \<Longrightarrow> m \<ge> N \<Longrightarrow> dist (f n x) (f m x) < e" for n m x
    6.26 +    by (rule dist_triangle_half_l)
    6.27 +  then show "\<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" by blast
    6.28 +qed
    6.29 +
    6.30 +lemma uniformly_convergent_eq_Cauchy:
    6.31 +  "uniformly_convergent_on X f = uniformly_Cauchy_on X f" for f::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
    6.32 +  using Cauchy_uniformly_convergent uniformly_convergent_Cauchy by blast
    6.33 +
    6.34 +lemma uniformly_convergent_eq_cauchy:
    6.35 +  fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
    6.36 +  shows
    6.37 +    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
    6.38 +      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  \<longrightarrow> dist (s m x) (s n x) < e)"
    6.39 +proof -
    6.40 +  have *: "(\<forall>n\<ge>N. \<forall>x. Q x \<longrightarrow> R n x) \<longleftrightarrow> (\<forall>n x. N \<le> n \<and> Q x \<longrightarrow> R n x)"
    6.41 +    "(\<forall>x. Q x \<longrightarrow> (\<forall>m\<ge>N. \<forall>n\<ge>N. S n m x)) \<longleftrightarrow> (\<forall>m n x. N \<le> m \<and> N \<le> n \<and> Q x \<longrightarrow> S n m x)"
    6.42 +    for N::nat and Q::"'b \<Rightarrow> bool" and R S
    6.43 +    by blast+
    6.44 +  show ?thesis
    6.45 +    using uniformly_convergent_eq_Cauchy[of "Collect P" s]
    6.46 +    unfolding uniformly_convergent_on_def uniformly_Cauchy_on_def uniform_limit_sequentially_iff
    6.47 +    by (simp add: *)
    6.48 +qed
    6.49 +
    6.50 +lemma uniformly_cauchy_imp_uniformly_convergent:
    6.51 +  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
    6.52 +  assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
    6.53 +    and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
    6.54 +  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
    6.55 +proof -
    6.56 +  obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
    6.57 +    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
    6.58 +  moreover
    6.59 +  {
    6.60 +    fix x
    6.61 +    assume "P x"
    6.62 +    then have "l x = l' x"
    6.63 +      using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
    6.64 +      using l and assms(2) unfolding lim_sequentially by blast
    6.65 +  }
    6.66 +  ultimately show ?thesis by auto
    6.67 +qed
    6.68 +
    6.69 +text \<open>TODO: remove explicit formulations
    6.70 +  @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
    6.71 +
    6.72  lemma uniformly_convergent_imp_convergent:
    6.73    "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
    6.74    unfolding uniformly_convergent_on_def convergent_def
    6.75 @@ -363,7 +421,7 @@
    6.76  lemmas uniform_limit_uminus[uniform_limit_intros] =
    6.77    bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
    6.78  
    6.79 -lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x y. c) (\<lambda>x. c) f"
    6.80 +lemma uniform_limit_const[uniform_limit_intros]: "uniform_limit S (\<lambda>x. c) c f"
    6.81    by (auto intro!: uniform_limitI)
    6.82  
    6.83  lemma uniform_limit_add[uniform_limit_intros]:
    6.84 @@ -574,6 +632,24 @@
    6.85    "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
    6.86    by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
    6.87  
    6.88 +lemma uniform_limit_bounded:
    6.89 +  fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::metric_space"
    6.90 +  assumes l: "uniform_limit S f l F"
    6.91 +  assumes bnd: "\<forall>\<^sub>F i in F. bounded (f i ` S)"
    6.92 +  assumes "F \<noteq> bot"
    6.93 +  shows "bounded (l ` S)"
    6.94 +proof -
    6.95 +  from l have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (l x) (f n x) < 1"
    6.96 +    by (auto simp: uniform_limit_iff dist_commute dest!: spec[where x=1])
    6.97 +  with bnd
    6.98 +  have "\<forall>\<^sub>F n in F. \<exists>M. \<forall>x\<in>S. dist undefined (l x) \<le> M + 1"
    6.99 +    by eventually_elim
   6.100 +      (auto intro!: order_trans[OF dist_triangle2 add_mono] intro: less_imp_le
   6.101 +        simp: bounded_any_center[where a=undefined])
   6.102 +  then show ?thesis using assms
   6.103 +    by (auto simp: bounded_any_center[where a=undefined] dest!: eventually_happens)
   6.104 +qed
   6.105 +
   6.106  lemma uniformly_convergent_add:
   6.107    "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
   6.108        uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
     7.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Sun Mar 12 19:06:10 2017 +0100
     7.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Fri Mar 10 23:16:40 2017 +0100
     7.3 @@ -1140,6 +1140,29 @@
     7.4      done
     7.5  qed
     7.6  
     7.7 +lemma Stone_Weierstrass_uniform_limit:
     7.8 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
     7.9 +  assumes S: "compact S"
    7.10 +    and f: "continuous_on S f"
    7.11 +  obtains g where "uniform_limit S g f sequentially" "\<And>n. polynomial_function (g n)"
    7.12 +proof -
    7.13 +  have pos: "inverse (Suc n) > 0" for n by auto
    7.14 +  obtain g where g: "\<And>n. polynomial_function (g n)" "\<And>x n. x \<in> S \<Longrightarrow> norm(f x - g n x) < inverse (Suc n)"
    7.15 +    using Stone_Weierstrass_polynomial_function[OF S f pos]
    7.16 +    by metis
    7.17 +  have "uniform_limit S g f sequentially"
    7.18 +  proof (rule uniform_limitI)
    7.19 +    fix e::real assume "0 < e"
    7.20 +    with LIMSEQ_inverse_real_of_nat have "\<forall>\<^sub>F n in sequentially. inverse (Suc n) < e"
    7.21 +      by (rule order_tendstoD)
    7.22 +    moreover have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < inverse (Suc n)"
    7.23 +      using g by (simp add: dist_norm norm_minus_commute)
    7.24 +    ultimately show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < e"
    7.25 +      by (eventually_elim) auto
    7.26 +  qed
    7.27 +  then show ?thesis using g(1) ..
    7.28 +qed
    7.29 +
    7.30  
    7.31  subsection\<open>Polynomial functions as paths\<close>
    7.32  
     8.1 --- a/src/HOL/Limits.thy	Sun Mar 12 19:06:10 2017 +0100
     8.2 +++ b/src/HOL/Limits.thy	Fri Mar 10 23:16:40 2017 +0100
     8.3 @@ -729,7 +729,7 @@
     8.4      by (intro Zfun_minus) (simp add: tendsto_Zfun_iff)
     8.5  qed
     8.6  
     8.7 -lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
     8.8 +lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real]
     8.9  
    8.10  
    8.11  subsubsection \<open>Linear operators and multiplication\<close>
     9.1 --- a/src/HOL/Topological_Spaces.thy	Sun Mar 12 19:06:10 2017 +0100
     9.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 10 23:16:40 2017 +0100
     9.3 @@ -150,12 +150,12 @@
     9.4  instance t1_space \<subseteq> t0_space
     9.5    by standard (fast dest: t1_space)
     9.6  
     9.7 +context t1_space begin
     9.8 +
     9.9  lemma separation_t1: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
    9.10 -  for x y :: "'a::t1_space"
    9.11    using t1_space[of x y] by blast
    9.12  
    9.13  lemma closed_singleton [iff]: "closed {a}"
    9.14 -  for a :: "'a::t1_space"
    9.15  proof -
    9.16    let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
    9.17    have "open ?T"
    9.18 @@ -167,7 +167,6 @@
    9.19  qed
    9.20  
    9.21  lemma closed_insert [continuous_intros, simp]:
    9.22 -  fixes a :: "'a::t1_space"
    9.23    assumes "closed S"
    9.24    shows "closed (insert a S)"
    9.25  proof -
    9.26 @@ -178,9 +177,9 @@
    9.27  qed
    9.28  
    9.29  lemma finite_imp_closed: "finite S \<Longrightarrow> closed S"
    9.30 -  for S :: "'a::t1_space set"
    9.31    by (induct pred: finite) simp_all
    9.32  
    9.33 +end
    9.34  
    9.35  text \<open>T2 spaces are also known as Hausdorff spaces.\<close>
    9.36  
    9.37 @@ -190,12 +189,10 @@
    9.38  instance t2_space \<subseteq> t1_space
    9.39    by standard (fast dest: hausdorff)
    9.40  
    9.41 -lemma separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
    9.42 -  for x y :: "'a::t2_space"
    9.43 +lemma (in t2_space) separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
    9.44    using hausdorff [of x y] by blast
    9.45  
    9.46 -lemma separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
    9.47 -  for x y :: "'a::t0_space"
    9.48 +lemma (in t0_space) separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
    9.49    using t0_space [of x y] by blast
    9.50  
    9.51  
    9.52 @@ -204,9 +201,9 @@
    9.53  class perfect_space = topological_space +
    9.54    assumes not_open_singleton: "\<not> open {x}"
    9.55  
    9.56 -lemma UNIV_not_singleton: "UNIV \<noteq> {x}"
    9.57 -  for x :: "'a::perfect_space"
    9.58 -  by (metis open_UNIV not_open_singleton)
    9.59 +lemma (in perfect_space) UNIV_not_singleton: "UNIV \<noteq> {x}"
    9.60 +  for x::'a
    9.61 +  by (metis (no_types) open_UNIV not_open_singleton)
    9.62  
    9.63  
    9.64  subsection \<open>Generators for toplogies\<close>
    9.65 @@ -476,10 +473,10 @@
    9.66    "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
    9.67    by (subst eventually_nhds) blast
    9.68  
    9.69 -lemma eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
    9.70 +lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
    9.71    by (subst (asm) eventually_nhds) blast
    9.72  
    9.73 -lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
    9.74 +lemma (in topological_space) nhds_neq_bot [simp]: "nhds a \<noteq> bot"
    9.75    by (simp add: trivial_limit_def eventually_nhds)
    9.76  
    9.77  lemma (in t1_space) t1_space_nhds: "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
    9.78 @@ -494,28 +491,34 @@
    9.79  lemma (in discrete_topology) at_discrete: "at x within S = bot"
    9.80    unfolding at_within_def nhds_discrete by simp
    9.81  
    9.82 -lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
    9.83 +lemma (in topological_space) at_within_eq:
    9.84 +  "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
    9.85    unfolding nhds_def at_within_def
    9.86    by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)
    9.87  
    9.88 -lemma eventually_at_filter:
    9.89 +lemma (in topological_space) eventually_at_filter:
    9.90    "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
    9.91    by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute)
    9.92  
    9.93 -lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
    9.94 +lemma (in topological_space) at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
    9.95    unfolding at_within_def by (intro inf_mono) auto
    9.96  
    9.97 -lemma eventually_at_topological:
    9.98 +lemma (in topological_space) eventually_at_topological:
    9.99    "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.100    by (simp add: eventually_nhds eventually_at_filter)
   9.101  
   9.102 -lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   9.103 +lemma (in topological_space) at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   9.104    unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
   9.105  
   9.106 -lemma at_within_open_NO_MATCH: "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
   9.107 +lemma (in topological_space) at_within_open_NO_MATCH:
   9.108 +  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
   9.109    by (simp only: at_within_open)
   9.110  
   9.111 -lemma at_within_nhd:
   9.112 +lemma (in topological_space) at_within_open_subset:
   9.113 +  "a \<in> S \<Longrightarrow> open S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> at a within T = at a"
   9.114 +  by (metis at_le at_within_open dual_order.antisym subset_UNIV)
   9.115 +
   9.116 +lemma (in topological_space) at_within_nhd:
   9.117    assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
   9.118    shows "at x within T = at x within U"
   9.119    unfolding filter_eq_iff eventually_at_filter
   9.120 @@ -526,14 +529,15 @@
   9.121      by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
   9.122  qed
   9.123  
   9.124 -lemma at_within_empty [simp]: "at a within {} = bot"
   9.125 +lemma (in topological_space) at_within_empty [simp]: "at a within {} = bot"
   9.126    unfolding at_within_def by simp
   9.127  
   9.128 -lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
   9.129 +lemma (in topological_space) at_within_union:
   9.130 +  "at x within (S \<union> T) = sup (at x within S) (at x within T)"
   9.131    unfolding filter_eq_iff eventually_sup eventually_at_filter
   9.132    by (auto elim!: eventually_rev_mp)
   9.133  
   9.134 -lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   9.135 +lemma (in topological_space) at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
   9.136    unfolding trivial_limit_def eventually_at_topological
   9.137    apply safe
   9.138     apply (case_tac "S = {a}")
   9.139 @@ -542,8 +546,7 @@
   9.140    apply fast
   9.141    done
   9.142  
   9.143 -lemma at_neq_bot [simp]: "at a \<noteq> bot"
   9.144 -  for a :: "'a::perfect_space"
   9.145 +lemma (in perfect_space) at_neq_bot [simp]: "at a \<noteq> bot"
   9.146    by (simp add: at_eq_bot_iff not_open_singleton)
   9.147  
   9.148  lemma (in order_topology) nhds_order:
   9.149 @@ -556,7 +559,7 @@
   9.150      by (simp only: nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def)
   9.151  qed
   9.152  
   9.153 -lemma filterlim_at_within_If:
   9.154 +lemma (in topological_space) filterlim_at_within_If:
   9.155    assumes "filterlim f G (at x within (A \<inter> {x. P x}))"
   9.156      and "filterlim g G (at x within (A \<inter> {x. \<not>P x}))"
   9.157    shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x within A)"
   9.158 @@ -580,7 +583,7 @@
   9.159    finally show "filterlim g G (inf (at x within A) (principal {x. \<not> P x}))" .
   9.160  qed
   9.161  
   9.162 -lemma filterlim_at_If:
   9.163 +lemma (in topological_space) filterlim_at_If:
   9.164    assumes "filterlim f G (at x within {x. P x})"
   9.165      and "filterlim g G (at x within {x. \<not>P x})"
   9.166    shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
   9.167 @@ -641,22 +644,20 @@
   9.168    using gt_ex[of x]
   9.169    by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
   9.170  
   9.171 -lemma at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
   9.172 -  for x :: "'a::linorder_topology"
   9.173 +lemma (in linorder_topology) at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
   9.174    by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
   9.175        elim: eventually_elim2 eventually_mono)
   9.176  
   9.177 -lemma eventually_at_split:
   9.178 +lemma (in linorder_topology) eventually_at_split:
   9.179    "eventually P (at x) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
   9.180 -  for x :: "'a::linorder_topology"
   9.181    by (subst at_eq_sup_left_right) (simp add: eventually_sup)
   9.182  
   9.183 -lemma eventually_at_leftI:
   9.184 +lemma (in order_topology) eventually_at_leftI:
   9.185    assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
   9.186    shows   "eventually P (at_left b)"
   9.187    using assms unfolding eventually_at_topological by (intro exI[of _ "{a<..}"]) auto
   9.188  
   9.189 -lemma eventually_at_rightI:
   9.190 +lemma (in order_topology) eventually_at_rightI:
   9.191    assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> P x" "a < b"
   9.192    shows   "eventually P (at_right a)"
   9.193    using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto
   9.194 @@ -671,7 +672,7 @@
   9.195  definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a"
   9.196    where "Lim A f = (THE l. (f \<longlongrightarrow> l) A)"
   9.197  
   9.198 -lemma tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
   9.199 +lemma (in topological_space) tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
   9.200    by simp
   9.201  
   9.202  named_theorems tendsto_intros "introduction rules for tendsto"
   9.203 @@ -682,7 +683,9 @@
   9.204        |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
   9.205  \<close>
   9.206  
   9.207 -lemma (in topological_space) tendsto_def:
   9.208 +context topological_space begin
   9.209 +
   9.210 +lemma tendsto_def:
   9.211     "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   9.212     unfolding nhds_def filterlim_INF filterlim_principal by auto
   9.213  
   9.214 @@ -692,14 +695,17 @@
   9.215  lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f \<longlongrightarrow> l) F' \<Longrightarrow> (f \<longlongrightarrow> l) F"
   9.216    unfolding tendsto_def le_filter_def by fast
   9.217  
   9.218 -lemma tendsto_within_subset: "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
   9.219 -  by (blast intro: tendsto_mono at_le)
   9.220 -
   9.221 -lemma filterlim_at:
   9.222 +lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
   9.223 +  by (auto simp: tendsto_def eventually_at_topological)
   9.224 +
   9.225 +lemma tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
   9.226 +  by (simp add: tendsto_def)
   9.227 +
   9.228 +lemma  filterlim_at:
   9.229    "(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 \<longlongrightarrow> b) F"
   9.230    by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
   9.231  
   9.232 -lemma filterlim_at_withinI:
   9.233 +lemma  filterlim_at_withinI:
   9.234    assumes "filterlim f (nhds c) F"
   9.235    assumes "eventually (\<lambda>x. f x \<in> A - {c}) F"
   9.236    shows   "filterlim f (at c within A) F"
   9.237 @@ -711,14 +717,23 @@
   9.238    shows   "filterlim f (at c) F"
   9.239    using assms by (intro filterlim_at_withinI) simp_all
   9.240  
   9.241 -lemma (in topological_space) topological_tendstoI:
   9.242 +lemma topological_tendstoI:
   9.243    "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
   9.244    by (auto simp: tendsto_def)
   9.245  
   9.246 -lemma (in topological_space) topological_tendstoD:
   9.247 +lemma topological_tendstoD:
   9.248    "(f \<longlongrightarrow> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
   9.249    by (auto simp: tendsto_def)
   9.250  
   9.251 +lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
   9.252 +  by (simp add: tendsto_def)
   9.253 +
   9.254 +end
   9.255 +
   9.256 +lemma tendsto_within_subset:
   9.257 +  "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
   9.258 +  by (blast intro: tendsto_mono at_le)
   9.259 +
   9.260  lemma (in order_topology) order_tendsto_iff:
   9.261    "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
   9.262    by (auto simp: nhds_order filterlim_inf filterlim_INF filterlim_principal)
   9.263 @@ -734,9 +749,6 @@
   9.264      and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
   9.265    using assms by (auto simp: order_tendsto_iff)
   9.266  
   9.267 -lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
   9.268 -  by (simp add: tendsto_def)
   9.269 -
   9.270  lemma (in linorder_topology) tendsto_max:
   9.271    assumes X: "(X \<longlongrightarrow> x) net"
   9.272      and Y: "(Y \<longlongrightarrow> y) net"
   9.273 @@ -773,11 +785,18 @@
   9.274      by (auto simp: min_less_iff_disj elim: eventually_mono)
   9.275  qed
   9.276  
   9.277 -lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
   9.278 -  by (auto simp: tendsto_def eventually_at_topological)
   9.279 -
   9.280 -lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
   9.281 -  by (simp add: tendsto_def)
   9.282 +lemma (in order_topology)
   9.283 +  assumes "a < b"
   9.284 +  shows at_within_Icc_at_right: "at a within {a..b} = at_right a"
   9.285 +    and at_within_Icc_at_left:  "at b within {a..b} = at_left b"
   9.286 +  using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"]
   9.287 +  using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"]
   9.288 +  by (auto intro!: order_class.antisym filter_leI
   9.289 +      simp: eventually_at_filter less_le
   9.290 +      elim: eventually_elim2)
   9.291 +
   9.292 +lemma (in order_topology) at_within_Icc_at: "a < x \<Longrightarrow> x < b \<Longrightarrow> at x within {a..b} = at x"
   9.293 +  by (rule at_within_open_subset[where S="{a<..<b}"]) auto
   9.294  
   9.295  lemma (in t2_space) tendsto_unique:
   9.296    assumes "F \<noteq> bot"
   9.297 @@ -810,22 +829,19 @@
   9.298    shows "((\<lambda>x. a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
   9.299    by (auto intro!: tendsto_unique [OF assms tendsto_const])
   9.300  
   9.301 -lemma increasing_tendsto:
   9.302 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   9.303 +lemma (in order_topology) increasing_tendsto:
   9.304    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
   9.305      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   9.306    shows "(f \<longlongrightarrow> l) F"
   9.307    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   9.308  
   9.309 -lemma decreasing_tendsto:
   9.310 -  fixes f :: "_ \<Rightarrow> 'a::order_topology"
   9.311 +lemma (in order_topology) decreasing_tendsto:
   9.312    assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
   9.313      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
   9.314    shows "(f \<longlongrightarrow> l) F"
   9.315    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   9.316  
   9.317 -lemma tendsto_sandwich:
   9.318 -  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
   9.319 +lemma (in order_topology) tendsto_sandwich:
   9.320    assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
   9.321    assumes lim: "(f \<longlongrightarrow> c) net" "(h \<longlongrightarrow> c) net"
   9.322    shows "(g \<longlongrightarrow> c) net"
   9.323 @@ -839,8 +855,7 @@
   9.324      using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
   9.325  qed
   9.326  
   9.327 -lemma limit_frequently_eq:
   9.328 -  fixes c d :: "'a::t1_space"
   9.329 +lemma (in t1_space) limit_frequently_eq:
   9.330    assumes "F \<noteq> bot"
   9.331      and "frequently (\<lambda>x. f x = c) F"
   9.332      and "(f \<longlongrightarrow> d) F"
   9.333 @@ -857,8 +872,7 @@
   9.334      unfolding frequently_def by contradiction
   9.335  qed
   9.336  
   9.337 -lemma tendsto_imp_eventually_ne:
   9.338 -  fixes c :: "'a::t1_space"
   9.339 +lemma (in t1_space) tendsto_imp_eventually_ne:
   9.340    assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
   9.341    shows "eventually (\<lambda>z. f z \<noteq> c') F"
   9.342  proof (cases "F=bot")
   9.343 @@ -876,8 +890,7 @@
   9.344    qed
   9.345  qed
   9.346  
   9.347 -lemma tendsto_le:
   9.348 -  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
   9.349 +lemma (in linorder_topology) tendsto_le:
   9.350    assumes F: "\<not> trivial_limit F"
   9.351      and x: "(f \<longlongrightarrow> x) F"
   9.352      and y: "(g \<longlongrightarrow> y) F"
   9.353 @@ -895,16 +908,14 @@
   9.354      by (simp add: eventually_False)
   9.355  qed
   9.356  
   9.357 -lemma tendsto_lowerbound:
   9.358 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   9.359 +lemma (in linorder_topology) tendsto_lowerbound:
   9.360    assumes x: "(f \<longlongrightarrow> x) F"
   9.361        and ev: "eventually (\<lambda>i. a \<le> f i) F"
   9.362        and F: "\<not> trivial_limit F"
   9.363    shows "a \<le> x"
   9.364    using F x tendsto_const ev by (rule tendsto_le)
   9.365  
   9.366 -lemma tendsto_upperbound:
   9.367 -  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   9.368 +lemma (in linorder_topology) tendsto_upperbound:
   9.369    assumes x: "(f \<longlongrightarrow> x) F"
   9.370        and ev: "eventually (\<lambda>i. a \<ge> f i) F"
   9.371        and F: "\<not> trivial_limit F"
   9.372 @@ -1840,7 +1851,8 @@
   9.373    unfolding continuous_on_def by auto
   9.374  
   9.375  lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
   9.376 -  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
   9.377 +  unfolding continuous_on_def
   9.378 +  by (metis subset_eq tendsto_within_subset)
   9.379  
   9.380  lemma continuous_on_compose[continuous_intros]:
   9.381    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g \<circ> f)"
   9.382 @@ -1912,6 +1924,25 @@
   9.383         (auto intro: less_le_trans[OF _ mono] less_imp_le)
   9.384  qed
   9.385  
   9.386 +lemma continuous_on_IccI:
   9.387 +  "\<lbrakk>(f \<longlongrightarrow> f a) (at_right a);
   9.388 +    (f \<longlongrightarrow> f b) (at_left b);
   9.389 +    (\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> f \<midarrow>x\<rightarrow> f x); a < b\<rbrakk> \<Longrightarrow>
   9.390 +    continuous_on {a .. b} f"
   9.391 +  for a::"'a::linorder_topology"
   9.392 +  using at_within_open[of _ "{a<..<b}"]
   9.393 +  by (auto simp: continuous_on_def at_within_Icc_at_right at_within_Icc_at_left le_less
   9.394 +      at_within_Icc_at)
   9.395 +
   9.396 +lemma
   9.397 +  fixes a b::"'a::linorder_topology"
   9.398 +  assumes "continuous_on {a .. b} f" "a < b"
   9.399 +  shows continuous_on_Icc_at_rightD: "(f \<longlongrightarrow> f a) (at_right a)"
   9.400 +    and continuous_on_Icc_at_leftD: "(f \<longlongrightarrow> f b) (at_left b)"
   9.401 +  using assms
   9.402 +  by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
   9.403 +      dest: bspec[where x=a] bspec[where x=b])
   9.404 +
   9.405  
   9.406  subsubsection \<open>Continuity at a point\<close>
   9.407  
    10.1 --- a/src/HOL/Transcendental.thy	Sun Mar 12 19:06:10 2017 +0100
    10.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 10 23:16:40 2017 +0100
    10.3 @@ -1493,6 +1493,8 @@
    10.4    apply (simp add: scaleR_conv_of_real)
    10.5    done
    10.6  
    10.7 +lemmas of_real_exp = exp_of_real[symmetric]
    10.8 +
    10.9  corollary exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
   10.10    by (metis Reals_cases Reals_of_real exp_of_real)
   10.11  
   10.12 @@ -1795,6 +1797,10 @@
   10.13    for x :: real
   10.14    using ln_less_cancel_iff [of x 1] by simp
   10.15  
   10.16 +lemma ln_le_zero_iff [simp]: "0 < x \<Longrightarrow> ln x \<le> 0 \<longleftrightarrow> x \<le> 1"
   10.17 +  for x :: real
   10.18 +  by (metis less_numeral_extra(1) ln_le_cancel_iff ln_one)
   10.19 +
   10.20  lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
   10.21    for x :: real
   10.22    using ln_less_cancel_iff [of 1 x] by simp
   10.23 @@ -2347,6 +2353,10 @@
   10.24    by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
   10.25       (auto simp: eventually_at_top_dense)
   10.26  
   10.27 +lemma filtermap_ln_at_right: "filtermap ln (at_right (0::real)) = at_bot"
   10.28 +  by (auto intro!: filtermap_fun_inverse[where g="\<lambda>x. exp x"] ln_at_0
   10.29 +      simp: filterlim_at exp_at_bot)
   10.30 +
   10.31  lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) \<longlongrightarrow> (0::real)) at_top"
   10.32  proof (induct k)
   10.33    case 0