# HG changeset patch
# User nipkow
# Date 1463807339 -7200
# Node ID 932cf444f2fe6d661d3cae3b5d7dfd342f2c88ca
# Parent  c445b0924e3ab18f6e57bac46dfac4a63bb3e1f3# Parent  412140038d3c6c309cb97bba403a670d83cb76aa
merged

diff -r 412140038d3c -r 932cf444f2fe src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat May 21 07:08:46 2016 +0200
+++ b/src/HOL/Limits.thy	Sat May 21 07:08:59 2016 +0200
@@ -2131,21 +2131,39 @@
 
 subsection \<open>Uniform Continuity\<close>
 
-definition
-  isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
-  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
+lemma uniformly_continuous_on_def:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "uniformly_continuous_on s f \<longleftrightarrow>
+    (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
+  unfolding uniformly_continuous_on_uniformity
+    uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal
+  by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric)
+
+abbreviation isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
+  "isUCont f \<equiv> uniformly_continuous_on UNIV f"
+
+lemma isUCont_def: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
+  by (auto simp: uniformly_continuous_on_def dist_commute)
 
 lemma isUCont_isCont: "isUCont f ==> isCont f x"
-by (simp add: isUCont_def isCont_def LIM_def, force)
+  by (drule uniformly_continuous_imp_continuous) (simp add: continuous_on_eq_continuous_at)
+
+lemma uniformly_continuous_on_Cauchy:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes "uniformly_continuous_on S f" "Cauchy X" "\<And>n. X n \<in> S"
+  shows "Cauchy (\<lambda>n. f (X n))"
+  using assms
+  unfolding uniformly_continuous_on_def
+  apply -
+  apply (rule metric_CauchyI)
+  apply (drule_tac x=e in spec, safe)
+  apply (drule_tac e=d in metric_CauchyD, safe)
+  apply (rule_tac x=M in exI, simp)
+  done
 
 lemma isUCont_Cauchy:
   "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
-unfolding isUCont_def
-apply (rule metric_CauchyI)
-apply (drule_tac x=e in spec, safe)
-apply (drule_tac e=s in metric_CauchyD, safe)
-apply (rule_tac x=M in exI, simp)
-done
+  by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
 
 lemma (in bounded_linear) isUCont: "isUCont f"
 unfolding isUCont_def dist_norm
diff -r 412140038d3c -r 932cf444f2fe src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 21 07:08:46 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 21 07:08:59 2016 +0200
@@ -5443,14 +5443,6 @@
 apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
 done
 
-lemma uniformly_continuous_on_def:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  shows "uniformly_continuous_on s f \<longleftrightarrow>
-    (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
-  unfolding uniformly_continuous_on_uniformity
-    uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal
-  by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric)
-
 text\<open>Some simple consequential lemmas.\<close>
 
 lemma continuous_onE:
@@ -5976,17 +5968,15 @@
   thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
   proof
     assume int: "x \<in> interior A"
-    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> A" unfolding interior_def by auto
-    then guess U .. note U = this
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
     hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
     hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
     thus ?thesis using U continuous_on_eq_continuous_at by auto
   next
     assume ext: "x \<in> interior (-A)"
-    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> -A" unfolding interior_def by auto
-    then guess U .. note U = this
-    hence "\<forall>y\<in>U. indicator A y = (0::real)" unfolding indicator_def by auto
-    hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def)
+    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
+    then have "continuous_on U (indicator A)"
+      using continuous_on_topological by (auto simp: subset_iff)
     thus ?thesis using U continuous_on_eq_continuous_at by auto
   qed
 qed
@@ -6096,6 +6086,158 @@
   qed
 qed
 
+lemma uniformly_continuous_on_extension_at_closure:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
+  assumes uc: "uniformly_continuous_on X f"
+  assumes "x \<in> closure X"
+  obtains l where "(f \<longlongrightarrow> l) (at x within X)"
+proof -
+  from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
+    by (auto simp: closure_sequential)
+
+  from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
+  obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"
+    by atomize_elim (simp only: convergent_eq_cauchy)
+
+  have "(f \<longlongrightarrow> l) (at x within X)"
+  proof (safe intro!: Lim_within_LIMSEQ)
+    fix xs'
+    assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X"
+      and xs': "xs' \<longlonglongrightarrow> x"
+    then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto
+
+    from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]
+    obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"
+      by atomize_elim (simp only: convergent_eq_cauchy)
+
+    show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
+    proof (rule tendstoI)
+      fix e::real assume "e > 0"
+      define e' where "e' \<equiv> e / 2"
+      have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
+
+      have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'"
+        by (simp add: \<open>0 < e'\<close> l tendstoD)
+      moreover
+      from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>]
+      obtain d where d: "d > 0" "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x x' < d \<Longrightarrow> dist (f x) (f x') < e'"
+        by auto
+      have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d"
+        by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs')
+      ultimately
+      show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e"
+      proof eventually_elim
+        case (elim n)
+        have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
+          by (metis dist_triangle dist_commute)
+        also have "dist (f (xs n)) (f (xs' n)) < e'"
+          by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim)
+        also note \<open>dist (f (xs n)) l < e'\<close>
+        also have "e' + e' = e" by (simp add: e'_def)
+        finally show ?case by simp
+      qed
+    qed
+  qed
+  thus ?thesis ..
+qed
+
+lemma uniformly_continuous_on_extension_on_closure:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space"
+  assumes uc: "uniformly_continuous_on X f"
+  obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
+    "\<And>Y h x. X \<subseteq> Y \<Longrightarrow> Y \<subseteq> closure X \<Longrightarrow> continuous_on Y h \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> f x = h x) \<Longrightarrow> x \<in> Y \<Longrightarrow> h x = g x"
+proof -
+  from uc have cont_f: "continuous_on X f"
+    by (simp add: uniformly_continuous_imp_continuous)
+  obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x
+    apply atomize_elim
+    apply (rule choice)
+    using uniformly_continuous_on_extension_at_closure[OF assms]
+    by metis
+  let ?g = "\<lambda>x. if x \<in> X then f x else y x"
+
+  have "uniformly_continuous_on (closure X) ?g"
+    unfolding uniformly_continuous_on_def
+  proof safe
+    fix e::real assume "e > 0"
+    define e' where "e' \<equiv> e / 3"
+    have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def)
+    from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>]
+    obtain d where "d > 0" and d: "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> dist (f x') (f x) < e'"
+      by auto
+    define d' where "d' = d / 3"
+    have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def)
+    show "\<exists>d>0. \<forall>x\<in>closure X. \<forall>x'\<in>closure X. dist x' x < d \<longrightarrow> dist (?g x') (?g x) < e"
+    proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>)
+      fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'"
+      then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
+        and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X"
+        by (auto simp: closure_sequential)
+      have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'"
+        and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'"
+        by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs')
+      moreover
+      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" if "x \<in> closure X" "x \<notin> X" "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" for xs x
+        using that not_eventuallyD
+        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at)
+      then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x"
+        using x x'
+        by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)
+      then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'"
+        "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'"
+        by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros)
+      ultimately
+      have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e"
+      proof eventually_elim
+        case (elim n)
+        have "dist (?g x') (?g x) \<le>
+          dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
+          by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
+        also
+        {
+          have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x"
+            by (metis add.commute add_le_cancel_left  dist_triangle dist_triangle_le)
+          also note \<open>dist (xs' n) x' < d'\<close>
+          also note \<open>dist x' x < d'\<close>
+          also note \<open>dist (xs n) x < d'\<close>
+          finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def)
+        }
+        with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'"
+          by (rule d)
+        also note \<open>dist (f (xs' n)) (?g x') < e'\<close>
+        also note \<open>dist (f (xs n)) (?g x) < e'\<close>
+        finally show ?case by (simp add: e'_def)
+      qed
+      then show "dist (?g x') (?g x) < e" by simp
+    qed
+  qed
+  moreover have "f x = ?g x" if "x \<in> X" for x using that by simp
+  moreover
+  {
+    fix Y h x
+    assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h"
+      and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)"
+    {
+      assume "x \<notin> X"
+      have "x \<in> closure X" using Y by auto
+      then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
+        by (auto simp: closure_sequential)
+      from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
+      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
+        by (auto simp: set_mp extension)
+      moreover
+      then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
+        using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
+        by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
+      ultimately have "h x = y x" by (rule LIMSEQ_unique)
+    } then
+    have "h x = ?g x"
+      using extension by auto
+  }
+  ultimately show ?thesis ..
+qed
+
+
 subsection\<open>Quotient maps\<close>
 
 lemma quotient_map_imp_continuous_open: