# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1483546730 0
# Node ID 223b2ebdda791cbd506d31ec12bc644962e07426
# Parent  1ddc262514b8d5d6ccc8438fba175c340feec6bc
Many new theorems, and more tidying

diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -3271,165 +3271,6 @@
   by (force simp: L contour_integral_integral)
 qed
 
-subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
-
-text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
-
-lemma continuous_disconnected_range_constant:
-  assumes s: "connected s"
-      and conf: "continuous_on s f"
-      and fim: "f ` s \<subseteq> t"
-      and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
-    shows "\<exists>a. \<forall>x \<in> s. f x = a"
-proof (cases "s = {}")
-  case True then show ?thesis by force
-next
-  case False
-  { fix x assume "x \<in> s"
-    then have "f ` s \<subseteq> {f x}"
-    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
-  }
-  with False show ?thesis
-    by blast
-qed
-
-lemma discrete_subset_disconnected:
-  fixes s :: "'a::topological_space set"
-  fixes t :: "'b::real_normed_vector set"
-  assumes conf: "continuous_on s f"
-      and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
-   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
-proof -
-  { fix x assume x: "x \<in> s"
-    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
-      using conf no [OF x] by auto
-    then have e2: "0 \<le> e / 2"
-      by simp
-    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
-      apply (rule ccontr)
-      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
-      apply (simp add: del: ex_simps)
-      apply (drule spec [where x="cball (f x) (e / 2)"])
-      apply (drule spec [where x="- ball(f x) e"])
-      apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
-        apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
-       using centre_in_cball connected_component_refl_eq e2 x apply blast
-      using ccs
-      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
-      done
-    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
-      by (auto simp: connected_component_in)
-    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
-      by (auto simp: x)
-  }
-  with assms show ?thesis
-    by blast
-qed
-
-lemma finite_implies_discrete:
-  fixes s :: "'a::topological_space set"
-  assumes "finite (f ` s)"
-  shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
-proof -
-  have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
-  proof (cases "f ` s - {f x} = {}")
-    case True
-    with zero_less_numeral show ?thesis
-      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
-  next
-    case False
-    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
-      by blast
-    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
-      using assms by simp
-    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
-      apply (rule finite_imp_less_Inf)
-      using z apply force+
-      done
-    show ?thesis
-      by (force intro!: * cInf_le_finite [OF finn])
-  qed
-  with assms show ?thesis
-    by blast
-qed
-
-text\<open>This proof requires the existence of two separate values of the range type.\<close>
-lemma finite_range_constant_imp_connected:
-  assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
-    shows "connected s"
-proof -
-  { fix t u
-    assume clt: "closedin (subtopology euclidean s) t"
-       and clu: "closedin (subtopology euclidean s) u"
-       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
-    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
-      apply (subst tus [symmetric])
-      apply (rule continuous_on_cases_local)
-      using clt clu tue
-      apply (auto simp: tus continuous_on_const)
-      done
-    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
-      by (rule finite_subset [of _ "{0,1}"]) auto
-    have "t = {} \<or> u = {}"
-      using assms [OF conif fi] tus [symmetric]
-      by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
-  }
-  then show ?thesis
-    by (simp add: connected_closedin_eq)
-qed
-
-lemma continuous_disconnected_range_constant_eq:
-      "(connected s \<longleftrightarrow>
-           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-            \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
-            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
-  and continuous_discrete_range_constant_eq:
-      "(connected s \<longleftrightarrow>
-         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-          continuous_on s f \<and>
-          (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
-          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
-  and continuous_finite_range_constant_eq:
-      "(connected s \<longleftrightarrow>
-         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
-          continuous_on s f \<and> finite (f ` s)
-          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
-proof -
-  have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
-    \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
-    by blast
-  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
-    apply (rule *)
-    using continuous_disconnected_range_constant apply metis
-    apply clarify
-    apply (frule discrete_subset_disconnected; blast)
-    apply (blast dest: finite_implies_discrete)
-    apply (blast intro!: finite_range_constant_imp_connected)
-    done
-  then show ?thesis1 ?thesis2 ?thesis3
-    by blast+
-qed
-
-lemma continuous_discrete_range_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
-  assumes s: "connected s"
-      and "continuous_on s f"
-      and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
-    shows "\<exists>a. \<forall>x \<in> s. f x = a"
-  using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
-  by blast
-
-lemma continuous_finite_range_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
-  assumes "connected s"
-      and "continuous_on s f"
-      and "finite (f ` s)"
-    shows "\<exists>a. \<forall>x \<in> s. f x = a"
-  using assms continuous_finite_range_constant_eq
-  by blast
-
-
 text\<open>We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\<close>
 
 subsection\<open>Winding Numbers\<close>
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -6,6 +6,7 @@
 imports
   Complex_Analysis_Basics
   Summation_Tests
+   "~~/src/HOL/Library/Periodic_Fun"
 begin
 
 (* TODO: Figure out what to do with Möbius transformations *)
@@ -400,6 +401,89 @@
   apply (simp add: real_sqrt_mult)
   done
 
+
+lemma complex_sin_eq:
+  fixes w :: complex
+  shows "sin w = sin z \<longleftrightarrow> (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real((2*n + 1)*pi))"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have "sin w - sin z = 0"
+    by (auto simp: algebra_simps)
+  then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"
+    by (auto simp: sin_diff_sin)
+  then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
+    using mult_eq_0_iff by blast
+  then show ?rhs
+  proof cases
+    case 1
+    then show ?thesis
+      apply (auto simp: sin_eq_0 algebra_simps)
+      by (metis Ints_of_int of_real_of_int_eq)
+  next
+    case 2
+    then show ?thesis
+      apply (auto simp: cos_eq_0 algebra_simps)
+      by (metis Ints_of_int of_real_of_int_eq)
+  qed
+next
+  assume ?rhs
+  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
+                               w = -z + of_real ((2* of_int n + 1)*pi)"
+    using Ints_cases by blast
+  then show ?lhs
+    using Periodic_Fun.sin.plus_of_int [of z n]
+    apply (auto simp: algebra_simps)
+    by (metis (no_types, hide_lams) add_diff_cancel_left add_diff_cancel_left' add_minus_cancel
+              mult.commute sin.plus_of_int sin_minus sin_plus_pi)
+qed
+
+lemma complex_cos_eq:
+  fixes w :: complex
+  shows "cos w = cos z \<longleftrightarrow>
+         (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real(2*n*pi))"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have "cos w - cos z = 0"
+    by (auto simp: algebra_simps)
+  then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"
+    by (auto simp: cos_diff_cos)
+  then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
+    using mult_eq_0_iff by blast
+  then show ?rhs
+  proof cases
+    case 1
+    then show ?thesis
+      apply (auto simp: sin_eq_0 algebra_simps)
+      by (metis Ints_of_int of_real_of_int_eq)
+  next
+    case 2
+    then show ?thesis
+      apply (auto simp: sin_eq_0 algebra_simps)
+      by (metis Ints_of_int add_minus_cancel distrib_right mult_of_int_commute mult_zero_right of_int_0 of_int_add of_real_of_int_eq)
+  qed
+next
+  assume ?rhs
+  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
+                               w = -z + of_real(2*n*pi)"
+    using Ints_cases  by (metis of_int_mult of_int_numeral)
+  then show ?lhs
+    using Periodic_Fun.cos.plus_of_int [of z n]
+    apply (auto simp: algebra_simps)
+    by (metis cos.plus_of_int cos_minus minus_add_cancel mult.commute)
+qed
+
+lemma sin_eq:
+   "sin x = sin y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + (2*n + 1)*pi)"
+  using complex_sin_eq [of x y]
+  by (simp only: sin_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
+
+lemma cos_eq:
+   "cos x = cos y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + 2*n*pi)"
+  using complex_cos_eq [of x y]
+  by (simp only: cos_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
+
 lemma sinh_complex:
   fixes z :: complex
   shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
@@ -2837,6 +2921,19 @@
 lemma Re_Arccos_bound: "\<bar>Re(Arccos z)\<bar> \<le> pi"
   by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
 
+lemma Im_Arccos_bound: "\<bar>Im (Arccos w)\<bar> \<le> cmod w"
+proof -
+  have "(Im (Arccos w))\<^sup>2 \<le> (cmod (cos (Arccos w)))\<^sup>2 - (cos (Re (Arccos w)))\<^sup>2"
+    using norm_cos_squared [of "Arccos w"] real_le_abs_sinh [of "Im (Arccos w)"]
+    apply (simp only: abs_le_square_iff)
+    apply (simp add: divide_simps)
+    done
+  also have "... \<le> (cmod w)\<^sup>2"
+    by (auto simp: cmod_power2)
+  finally show ?thesis
+    using abs_le_square_iff by force 
+qed
+  
 lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
   unfolding Re_Arcsin
   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
@@ -2844,6 +2941,21 @@
 lemma Re_Arcsin_bound: "\<bar>Re(Arcsin z)\<bar> \<le> pi"
   by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
 
+lemma norm_Arccos_bounded:
+  fixes w :: complex
+  shows "norm (Arccos w) \<le> pi + norm w"
+proof -
+  have Re: "(Re (Arccos w))\<^sup>2 \<le> pi\<^sup>2" "(Im (Arccos w))\<^sup>2 \<le> (cmod w)\<^sup>2"
+    using Re_Arccos_bound [of w] Im_Arccos_bound [of w] abs_le_square_iff by force+
+  have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2"
+    using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"])
+  then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))"
+    apply (simp add: norm_le_square)
+    by (metis dot_square_norm norm_ge_zero norm_le_square pi_ge_zero triangle_lemma)
+  then show "cmod (Arccos w) \<le> pi + cmod w"
+    by auto
+qed
+
 
 subsection\<open>Interrelations between Arcsin and Arccos\<close>
 
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -14,6 +14,20 @@
   "~~/src/HOL/Library/Set_Algebras"
 begin
 
+lemma swap_continuous: (*move to Topological_Spaces?*)
+  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
+    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
+proof -
+  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
+    by auto
+  then show ?thesis
+    apply (rule ssubst)
+    apply (rule continuous_on_compose)
+    apply (simp add: split_def)
+    apply (rule continuous_intros | simp add: assms)+
+    done
+qed
+
 lemma dim_image_eq:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes lf: "linear f"
@@ -4651,7 +4665,7 @@
   ultimately show ?thesis by auto
 qed
 
-lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
+lemma interior_atLeastAtMost_real [simp]: "interior {a..b} = {a<..<b :: real}"
 proof-
   have "{a..b} = {a..} \<inter> {..b}" by auto
   also have "interior ... = {a<..} \<inter> {..<b}"
@@ -4660,12 +4674,15 @@
   finally show ?thesis .
 qed
 
-lemma frontier_real_Iic:
+lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
+  by (metis interior_atLeastAtMost_real interior_interior)
+
+lemma frontier_real_Iic [simp]:
   fixes a :: real
   shows "frontier {..a} = {a}"
   unfolding frontier_def by (auto simp add: interior_real_semiline')
 
-lemma rel_interior_real_box:
+lemma rel_interior_real_box [simp]:
   fixes a b :: real
   assumes "a < b"
   shows "rel_interior {a .. b} = {a <..< b}"
@@ -4679,7 +4696,7 @@
     by (simp split: if_split_asm del: box_real add: box_real[symmetric] interior_cbox)
 qed
 
-lemma rel_interior_real_semiline:
+lemma rel_interior_real_semiline [simp]:
   fixes a :: real
   shows "rel_interior {a..} = {a<..}"
 proof -
@@ -6596,7 +6613,7 @@
   apply rule
   apply rule
   apply (erule conjE)
-  apply (rule ccontr)
+  apply (rule ccontr)       
 proof -
   fix a b x
   assume as: "connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x \<notin> s"
@@ -6630,6 +6647,10 @@
   shows "is_interval s \<longleftrightarrow> convex s"
   by (metis is_interval_convex convex_connected is_interval_connected_1)
 
+lemma connected_compact_interval_1:
+     "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
+  by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
+
 lemma connected_convex_1:
   fixes s :: "real set"
   shows "connected s \<longleftrightarrow> convex s"
@@ -7315,6 +7336,12 @@
     unfolding midpoint_def scaleR_2 [symmetric] by simp
 qed
 
+lemma
+  fixes a::real
+  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
+                    and le_midpoint_1: "midpoint a b \<le> b"
+  by (simp_all add: midpoint_def assms)
+
 lemma dist_midpoint:
   fixes a b :: "'a::real_normed_vector" shows
   "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
@@ -7535,7 +7562,7 @@
   proof -
     have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
       using \<open>u \<le> 1\<close> by force
-    then show ?thesis
+    then show ?thesis                     
       by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   qed
   also have "... \<le> dist a b"
@@ -7639,6 +7666,19 @@
   shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
 by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
 
+lemma segment_to_closest_point:
+  fixes S :: "'a :: euclidean_space set"
+  shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
+  apply (subst disjoint_iff_not_equal)
+  apply (clarify dest!: dist_in_open_segment)
+  by (metis closest_point_le dist_commute le_less_trans less_irrefl)
+
+lemma segment_to_point_exists:
+  fixes S :: "'a :: euclidean_space set"
+    assumes "closed S" "S \<noteq> {}"
+    obtains b where "b \<in> S" "open_segment a b \<inter> S = {}"
+  by (metis assms segment_to_closest_point closest_point_exists that)
+
 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
 
 lemma segment_eq_compose:
@@ -8243,6 +8283,71 @@
   finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
 qed
 
+lemma closure_open_Int_superset:
+  assumes "open S" "S \<subseteq> closure T"
+  shows "closure(S \<inter> T) = closure S"
+proof -
+  have "closure S \<subseteq> closure(S \<inter> T)"
+    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
+  then show ?thesis
+    by (simp add: closure_mono dual_order.antisym)
+qed
+
+lemma convex_closure_interior:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" and int: "interior S \<noteq> {}"
+  shows "closure(interior S) = closure S"
+proof -
+  obtain a where a: "a \<in> interior S"
+    using int by auto
+  have "closure S \<subseteq> closure(interior S)"
+  proof
+    fix x
+    assume x: "x \<in> closure S"
+    show "x \<in> closure (interior S)"
+    proof (cases "x=a")
+      case True
+      then show ?thesis
+        using \<open>a \<in> interior S\<close> closure_subset by blast
+    next
+      case False
+      show ?thesis
+      proof (clarsimp simp add: closure_def islimpt_approachable)
+        fix e::real
+        assume xnotS: "x \<notin> interior S" and "0 < e"
+        show "\<exists>x'\<in>interior S. x' \<noteq> x \<and> dist x' x < e"
+        proof (intro bexI conjI)
+          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<noteq> x"
+            using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def)
+          show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
+            using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
+          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<in> interior S"
+            apply (clarsimp simp add: min_def a)
+            apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
+            using \<open>0 < e\<close> False apply (auto simp: divide_simps)
+            done
+        qed
+      qed
+    qed
+  qed
+  then show ?thesis
+    by (simp add: closure_mono interior_subset subset_antisym)
+qed
+
+lemma closure_convex_Int_superset:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" "interior S \<noteq> {}" "interior S \<subseteq> closure T"
+  shows "closure(S \<inter> T) = closure S"
+proof -
+  have "closure S \<subseteq> closure(interior S)"
+    by (simp add: convex_closure_interior assms)
+  also have "... \<subseteq> closure (S \<inter> T)"
+    using interior_subset [of S] assms
+    by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior)
+  finally show ?thesis
+    by (simp add: closure_mono dual_order.antisym)
+qed
+
 
 subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
 
@@ -14406,4 +14511,78 @@
 using paracompact_closedin [of UNIV S \<C>] assms
 by (auto simp: open_openin [symmetric] closed_closedin [symmetric])
 
+  
+subsection\<open>Closed-graph characterization of continuity\<close>
+
+lemma continuous_closed_graph_gen:
+  fixes T :: "'b::real_normed_vector set"
+  assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+    shows "closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
+proof -
+  have eq: "((\<lambda>x. Pair x (f x)) ` S) = {z. z \<in> S \<times> T \<and> (f \<circ> fst)z - snd z \<in> {0}}"
+    using fim by auto
+  show ?thesis
+    apply (subst eq)
+    apply (intro continuous_intros continuous_closedin_preimage continuous_on_subset [OF contf])
+    by auto
+qed
+
+lemma continuous_closed_graph_eq:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "compact T" and fim: "f ` S \<subseteq> T"
+  shows "continuous_on S f \<longleftrightarrow>
+         closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
+         (is "?lhs = ?rhs")
+proof -
+  have "?lhs" if ?rhs
+  proof (clarsimp simp add: continuous_on_closed_gen [OF fim])
+    fix U
+    assume U: "closedin (subtopology euclidean T) U"
+    have eq: "{x. x \<in> S \<and> f x \<in> U} = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
+      by (force simp: image_iff)
+    show "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+      by (simp add: U closedin_Int closedin_Times closed_map_fst [OF \<open>compact T\<close>] that eq)
+  qed
+  with continuous_closed_graph_gen assms show ?thesis by blast
+qed
+
+lemma continuous_closed_graph:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "closed S" and contf: "continuous_on S f"
+  shows "closed ((\<lambda>x. Pair x (f x)) ` S)"
+  apply (rule closedin_closed_trans)
+   apply (rule continuous_closed_graph_gen [OF contf subset_UNIV])
+  by (simp add: \<open>closed S\<close> closed_Times)
+
+lemma continuous_from_closed_graph:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "compact T" and fim: "f ` S \<subseteq> T" and clo: "closed ((\<lambda>x. Pair x (f x)) ` S)"
+  shows "continuous_on S f"
+    using fim clo
+    by (auto intro: closed_subset simp: continuous_closed_graph_eq [OF \<open>compact T\<close> fim])
+
+lemma continuous_on_Un_local_open:
+  assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
+      and opT: "openin (subtopology euclidean (S \<union> T)) T"
+      and contf: "continuous_on S f" and contg: "continuous_on T f"
+    shows "continuous_on (S \<union> T) f"
+using pasting_lemma [of "{S,T}" "S \<union> T" "\<lambda>i. i" "\<lambda>i. f" f] contf contg opS opT by blast
+
+lemma continuous_on_cases_local_open:
+  assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
+      and opT: "openin (subtopology euclidean (S \<union> T)) T"
+      and contf: "continuous_on S f" and contg: "continuous_on T g"
+      and fg: "\<And>x. x \<in> S \<and> ~P x \<or> x \<in> T \<and> P x \<Longrightarrow> f x = g x"
+    shows "continuous_on (S \<union> T) (\<lambda>x. if P x then f x else g x)"
+proof -
+  have "\<And>x. x \<in> S \<Longrightarrow> (if P x then f x else g x) = f x"  "\<And>x. x \<in> T \<Longrightarrow> (if P x then f x else g x) = g x"
+    by (simp_all add: fg)
+  then have "continuous_on S (\<lambda>x. if P x then f x else g x)" "continuous_on T (\<lambda>x. if P x then f x else g x)"
+    by (simp_all add: contf contg cong: continuous_on_cong)
+  then show ?thesis
+    by (rule continuous_on_Un_local_open [OF opS opT])
+qed
+
+
+  
 end
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -53,6 +53,9 @@
 lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
   by (metis ex_in_conv nonempty_Basis someI_ex)
 
+lemma norm_some_Basis [simp]: "norm (SOME i. i \<in> Basis) = 1"
+  by (simp add: SOME_Basis)
+
 lemma (in euclidean_space) inner_sum_left_Basis[simp]:
     "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
   by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases)
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -10,21 +10,6 @@
 begin
 
 (* BEGIN MOVE *)
-lemma swap_continuous:
-  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
-    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
-proof -
-  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
-    by auto
-  then show ?thesis
-    apply (rule ssubst)
-    apply (rule continuous_on_compose)
-    apply (simp add: split_def)
-    apply (rule continuous_intros | simp add: assms)+
-    done
-qed
-
-
 lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
   by (simp add: norm_minus_eqI)
 
@@ -44,10 +29,6 @@
 
 lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
   by blast
-
-lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
-  using nonempty_Basis
-  by (fastforce simp add: set_eq_iff mem_box)
 (* END MOVE *)
 
 subsection \<open>Content (length, area, volume...) of an interval.\<close>
@@ -6191,7 +6172,6 @@
       apply (rule le_less_trans[of _ "sum (\<lambda>x. k / (real (card r) + 1)) r"])
       unfolding sum_subtractf[symmetric]
       apply (rule sum_norm_le)
-      apply rule
       apply (drule qq)
       defer
       unfolding divide_inverse sum_distrib_right[symmetric]
@@ -6536,7 +6516,7 @@
             m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2"
             apply (rule le_less_trans[of _ "sum (\<lambda>i. e / 2^(i+2)) {0..s}"])
             apply (rule sum_norm_le)
-          proof
+          proof -
             show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
               unfolding power_add divide_inverse inverse_mult_distrib
               unfolding sum_distrib_left[symmetric] sum_distrib_right[symmetric]
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -1112,19 +1112,19 @@
 
 
 lemma homeomorphic_convex_compact_lemma:
-  fixes s :: "'a::euclidean_space set"
-  assumes "convex s"
-    and "compact s"
-    and "cball 0 1 \<subseteq> s"
-  shows "s homeomorphic (cball (0::'a) 1)"
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S"
+    and "compact S"
+    and "cball 0 1 \<subseteq> S"
+  shows "S homeomorphic (cball (0::'a) 1)"
 proof (rule starlike_compact_projective_special[OF assms(2-3)])
   fix x u
-  assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
+  assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
   have "open (ball (u *\<^sub>R x) (1 - u))"
     by (rule open_ball)
   moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
     unfolding centre_in_ball using \<open>u < 1\<close> by simp
-  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
+  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> S"
   proof
     fix y
     assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
@@ -1132,32 +1132,32 @@
       unfolding mem_ball .
     with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
       by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
-    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
-    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
-      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
-    then show "y \<in> s" using \<open>u < 1\<close>
+    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> S" ..
+    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> S"
+      using \<open>x \<in> S\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
+    then show "y \<in> S" using \<open>u < 1\<close>
       by simp
   qed
-  ultimately have "u *\<^sub>R x \<in> interior s" ..
-  then show "u *\<^sub>R x \<in> s - frontier s"
+  ultimately have "u *\<^sub>R x \<in> interior S" ..
+  then show "u *\<^sub>R x \<in> S - frontier S"
     using frontier_def and interior_subset by auto
 qed
 
 proposition homeomorphic_convex_compact_cball:
   fixes e :: real
-    and s :: "'a::euclidean_space set"
-  assumes "convex s"
-    and "compact s"
-    and "interior s \<noteq> {}"
+    and S :: "'a::euclidean_space set"
+  assumes "convex S"
+    and "compact S"
+    and "interior S \<noteq> {}"
     and "e > 0"
-  shows "s homeomorphic (cball (b::'a) e)"
+  shows "S homeomorphic (cball (b::'a) e)"
 proof -
-  obtain a where "a \<in> interior s"
+  obtain a where "a \<in> interior S"
     using assms(3) by auto
-  then obtain d where "d > 0" and d: "cball a d \<subseteq> s"
+  then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
     unfolding mem_interior_cball by auto
   let ?d = "inverse d" and ?n = "0::'a"
-  have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
+  have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` S"
     apply rule
     apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
     defer
@@ -1166,25 +1166,25 @@
     unfolding mem_cball dist_norm
     apply (auto simp add: mult_right_le_one_le)
     done
-  then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
-    using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
+  then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` S homeomorphic cball ?n 1"
+    using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` S",
       OF convex_affinity compact_affinity]
     using assms(1,2)
     by (auto simp add: scaleR_right_diff_distrib)
   then show ?thesis
     apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
-    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
+    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *\<^sub>R -a"]])
     using \<open>d>0\<close> \<open>e>0\<close>
     apply (auto simp add: scaleR_right_diff_distrib)
     done
 qed
 
 corollary homeomorphic_convex_compact:
-  fixes s :: "'a::euclidean_space set"
-    and t :: "'a set"
-  assumes "convex s" "compact s" "interior s \<noteq> {}"
-    and "convex t" "compact t" "interior t \<noteq> {}"
-  shows "s homeomorphic t"
+  fixes S :: "'a::euclidean_space set"
+    and T :: "'a set"
+  assumes "convex S" "compact S" "interior S \<noteq> {}"
+    and "convex T" "compact T" "interior T \<noteq> {}"
+  shows "S homeomorphic T"
   using assms
   by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
 
@@ -1193,31 +1193,31 @@
 definition covering_space
            :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
   where
-  "covering_space c p s \<equiv>
-       continuous_on c p \<and> p ` c = s \<and>
-       (\<forall>x \<in> s. \<exists>t. x \<in> t \<and> openin (subtopology euclidean s) t \<and>
-                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> t} \<and>
+  "covering_space c p S \<equiv>
+       continuous_on c p \<and> p ` c = S \<and>
+       (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and>
+                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> T} \<and>
                         (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
                         pairwise disjnt v \<and>
-                        (\<forall>u \<in> v. \<exists>q. homeomorphism u t p q)))"
+                        (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
 
-lemma covering_space_imp_continuous: "covering_space c p s \<Longrightarrow> continuous_on c p"
+lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
   by (simp add: covering_space_def)
 
-lemma covering_space_imp_surjective: "covering_space c p s \<Longrightarrow> p ` c = s"
+lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
   by (simp add: covering_space_def)
 
-lemma homeomorphism_imp_covering_space: "homeomorphism s t f g \<Longrightarrow> covering_space s f t"
+lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
   apply (simp add: homeomorphism_def covering_space_def, clarify)
-  apply (rule_tac x=t in exI, simp)
-  apply (rule_tac x="{s}" in exI, auto)
+  apply (rule_tac x=T in exI, simp)
+  apply (rule_tac x="{S}" in exI, auto)
   done
 
 lemma covering_space_local_homeomorphism:
-  assumes "covering_space c p s" "x \<in> c"
-  obtains t u q where "x \<in> t" "openin (subtopology euclidean c) t"
-                      "p x \<in> u" "openin (subtopology euclidean s) u"
-                      "homeomorphism t u p q"
+  assumes "covering_space c p S" "x \<in> c"
+  obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
+                      "p x \<in> u" "openin (subtopology euclidean S) u"
+                      "homeomorphism T u p q"
 using assms
 apply (simp add: covering_space_def, clarify)
 apply (drule_tac x="p x" in bspec, force)
@@ -1225,11 +1225,11 @@
 
 
 lemma covering_space_local_homeomorphism_alt:
-  assumes p: "covering_space c p s" and "y \<in> s"
-  obtains x t u q where "p x = y"
-                        "x \<in> t" "openin (subtopology euclidean c) t"
-                        "y \<in> u" "openin (subtopology euclidean s) u"
-                          "homeomorphism t u p q"
+  assumes p: "covering_space c p S" and "y \<in> S"
+  obtains x T u q where "p x = y"
+                        "x \<in> T" "openin (subtopology euclidean c) T"
+                        "y \<in> u" "openin (subtopology euclidean S) u"
+                          "homeomorphism T u p q"
 proof -
   obtain x where "p x = y" "x \<in> c"
     using assms covering_space_imp_surjective by blast
@@ -1239,50 +1239,50 @@
 qed
 
 proposition covering_space_open_map:
-  fixes s :: "'a :: metric_space set" and t :: "'b :: metric_space set"
-  assumes p: "covering_space c p s" and t: "openin (subtopology euclidean c) t"
-    shows "openin (subtopology euclidean s) (p ` t)"
+  fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
+  assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
+    shows "openin (subtopology euclidean S) (p ` T)"
 proof -
-  have pce: "p ` c = s"
+  have pce: "p ` c = S"
    and covs:
-       "\<And>x. x \<in> s \<Longrightarrow>
-            \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean s) X \<and>
+       "\<And>x. x \<in> S \<Longrightarrow>
+            \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
                   \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
                   (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
                   pairwise disjnt VS \<and>
                   (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
     using p by (auto simp: covering_space_def)
-  have "t \<subseteq> c"  by (metis openin_euclidean_subtopology_iff t)
-  have "\<exists>T. openin (subtopology euclidean s) T \<and> y \<in> T \<and> T \<subseteq> p ` t"
-          if "y \<in> p ` t" for y
+  have "T \<subseteq> c"  by (metis openin_euclidean_subtopology_iff T)
+  have "\<exists>X. openin (subtopology euclidean S) X \<and> y \<in> X \<and> X \<subseteq> p ` T"
+          if "y \<in> p ` T" for y
   proof -
-    have "y \<in> s" using \<open>t \<subseteq> c\<close> pce that by blast
-    obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean s) U"
+    have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast
+    obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U"
                   and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
                   and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
                   and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
-      using covs [OF \<open>y \<in> s\<close>] by auto
-    obtain x where "x \<in> c" "p x \<in> U" "x \<in> t" "p x = y"
+      using covs [OF \<open>y \<in> S\<close>] by auto
+    obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y"
       apply simp
-      using t [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` t\<close> by blast
+      using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
     with VS obtain V where "x \<in> V" "V \<in> VS" by auto
     then obtain q where q: "homeomorphism V U p q" using homVS by blast
-    then have ptV: "p ` (t \<inter> V) = U \<inter> {z. q z \<in> (t \<inter> V)}"
+    then have ptV: "p ` (T \<inter> V) = U \<inter> {z. q z \<in> (T \<inter> V)}"
       using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
     have ocv: "openin (subtopology euclidean c) V"
       by (simp add: \<open>V \<in> VS\<close> openVS)
-    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> t \<inter> V}"
+    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> T \<inter> V}"
       apply (rule continuous_on_open [THEN iffD1, rule_format])
        using homeomorphism_def q apply blast
-      using openin_subtopology_Int_subset [of c] q t unfolding homeomorphism_def
+      using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
       by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
-    then have os: "openin (subtopology euclidean s) (U \<inter> {z. q z \<in> t \<inter> V})"
+    then have os: "openin (subtopology euclidean S) (U \<inter> {z. q z \<in> T \<inter> V})"
       using openin_trans [of U] by (simp add: Collect_conj_eq U)
     show ?thesis
-      apply (rule_tac x = "p ` (t \<inter> V)" in exI)
+      apply (rule_tac x = "p ` (T \<inter> V)" in exI)
       apply (rule conjI)
       apply (simp only: ptV os)
-      using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> t\<close> apply blast
+      using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> apply blast
       done
   qed
   with openin_subopen show ?thesis by blast
@@ -1291,73 +1291,73 @@
 lemma covering_space_lift_unique_gen:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
-  assumes cov: "covering_space c p s"
+  assumes cov: "covering_space c p S"
       and eq: "g1 a = g2 a"
-      and f: "continuous_on t f"  "f ` t \<subseteq> s"
-      and g1: "continuous_on t g1"  "g1 ` t \<subseteq> c"
-      and fg1: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
-      and g2: "continuous_on t g2"  "g2 ` t \<subseteq> c"
-      and fg2: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
-      and u_compt: "u \<in> components t" and "a \<in> u" "x \<in> u"
+      and f: "continuous_on T f"  "f ` T \<subseteq> S"
+      and g1: "continuous_on T g1"  "g1 ` T \<subseteq> c"
+      and fg1: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
+      and g2: "continuous_on T g2"  "g2 ` T \<subseteq> c"
+      and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
+      and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
     shows "g1 x = g2 x"
 proof -
-  have "u \<subseteq> t" by (rule in_components_subset [OF u_compt])
-  def G12 \<equiv> "{x \<in> u. g1 x - g2 x = 0}"
-  have "connected u" by (rule in_components_connected [OF u_compt])
-  have contu: "continuous_on u g1" "continuous_on u g2"
-       using \<open>u \<subseteq> t\<close> continuous_on_subset g1 g2 by blast+
-  have o12: "openin (subtopology euclidean u) G12"
+  have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
+  def G12 \<equiv> "{x \<in> U. g1 x - g2 x = 0}"
+  have "connected U" by (rule in_components_connected [OF u_compt])
+  have contu: "continuous_on U g1" "continuous_on U g2"
+       using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+
+  have o12: "openin (subtopology euclidean U) G12"
   unfolding G12_def
   proof (subst openin_subopen, clarify)
     fix z
-    assume z: "z \<in> u" "g1 z - g2 z = 0"
+    assume z: "z \<in> U" "g1 z - g2 z = 0"
     obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v"
-                   and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean s) w"
+                   and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean S) w"
                    and hom: "homeomorphism v w p q"
       apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
-       using \<open>u \<subseteq> t\<close> \<open>z \<in> u\<close> g1(2) apply blast+
+       using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
       done
     have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
-    have gg: "{x \<in> u. g x \<in> v} = {x \<in> u. g x \<in> (v \<inter> g ` u)}" for g
+    have gg: "{x \<in> U. g x \<in> v} = {x \<in> U. g x \<in> (v \<inter> g ` U)}" for g
       by auto
-    have "openin (subtopology euclidean (g1 ` u)) (v \<inter> g1 ` u)"
-      using ocv \<open>u \<subseteq> t\<close> g1 by (fastforce simp add: openin_open)
-    then have 1: "openin (subtopology euclidean u) {x \<in> u. g1 x \<in> v}"
+    have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)"
+      using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
+    then have 1: "openin (subtopology euclidean U) {x \<in> U. g1 x \<in> v}"
       unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
-    have "openin (subtopology euclidean (g2 ` u)) (v \<inter> g2 ` u)"
-      using ocv \<open>u \<subseteq> t\<close> g2 by (fastforce simp add: openin_open)
-    then have 2: "openin (subtopology euclidean u) {x \<in> u. g2 x \<in> v}"
+    have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)"
+      using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
+    then have 2: "openin (subtopology euclidean U) {x \<in> U. g2 x \<in> v}"
       unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
-    show "\<exists>T. openin (subtopology euclidean u) T \<and>
-              z \<in> T \<and> T \<subseteq> {z \<in> u. g1 z - g2 z = 0}"
+    show "\<exists>T. openin (subtopology euclidean U) T \<and>
+              z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
       using z
-      apply (rule_tac x = "{x. x \<in> u \<and> g1 x \<in> v} \<inter> {x. x \<in> u \<and> g2 x \<in> v}" in exI)
+      apply (rule_tac x = "{x. x \<in> U \<and> g1 x \<in> v} \<inter> {x. x \<in> U \<and> g2 x \<in> v}" in exI)
       apply (intro conjI)
       apply (rule openin_Int [OF 1 2])
       using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
-      apply (metis \<open>u \<subseteq> t\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
+      apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
       done
   qed
-  have c12: "closedin (subtopology euclidean u) G12"
+  have c12: "closedin (subtopology euclidean U) G12"
     unfolding G12_def
     by (intro continuous_intros continuous_closedin_preimage_constant contu)
-  have "G12 = {} \<or> G12 = u"
-    by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected u\<close> conjI o12 c12)
-  with eq \<open>a \<in> u\<close> have "\<And>x. x \<in> u \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
+  have "G12 = {} \<or> G12 = U"
+    by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12)
+  with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
   then show ?thesis
-    using \<open>x \<in> u\<close> by force
+    using \<open>x \<in> U\<close> by force
 qed
 
 proposition covering_space_lift_unique:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
-  assumes "covering_space c p s"
+  assumes "covering_space c p S"
           "g1 a = g2 a"
-          "continuous_on t f"  "f ` t \<subseteq> s"
-          "continuous_on t g1"  "g1 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
-          "continuous_on t g2"  "g2 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
-          "connected t"  "a \<in> t"   "x \<in> t"
+          "continuous_on T f"  "f ` T \<subseteq> S"
+          "continuous_on T g1"  "g1 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
+          "continuous_on T g2"  "g2 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
+          "connected T"  "a \<in> T"   "x \<in> T"
    shows "g1 x = g2 x"
-using covering_space_lift_unique_gen [of c p s] in_components_self assms ex_in_conv by blast
+using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast
 
 end
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -1482,14 +1482,14 @@
 
 lemma sum_norm_le:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
+  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
   shows "norm (sum f S) \<le> sum g S"
   by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
 
 lemma sum_norm_bound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
-  shows "norm (sum f S) \<le> of_nat (card S) * K"
+  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
+  shows "norm (sum f S) \<le> of_nat (card S)*K"
   using sum_norm_le[OF K] sum_constant[symmetric]
   by simp
 
@@ -1946,11 +1946,9 @@
     also have "\<dots> = norm (sum ?g Basis)"
       by (simp add: linear_sum [OF lf] linear_cmul [OF lf])
     finally have th0: "norm (f x) = norm (sum ?g Basis)" .
-    have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
-    proof
-      fix i :: 'a
-      assume i: "i \<in> Basis"
-      from Basis_le_norm[OF i, of x]
+    have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
+    proof -
+      from Basis_le_norm[OF that, of x]
       show "norm (?g i) \<le> norm (f i) * norm x"
         unfolding norm_scaleR
         apply (subst mult.commute)
@@ -2023,7 +2021,6 @@
   show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
     apply (auto simp add: sum_distrib_right th sum.cartesian_product)
     apply (rule sum_norm_le)
-    apply simp
     apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
       field_simps simp del: scaleR_scaleR)
     apply (rule mult_mono)
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -15,6 +15,23 @@
   Norm_Arith
 begin
 
+(* FIXME: move to HOL/Real_Vector_Spaces.thy *)
+
+lemma scaleR_2:
+  fixes x :: "'a::real_vector"
+  shows "scaleR 2 x = x + x"
+  unfolding one_add_one [symmetric] scaleR_left_distrib by simp
+
+lemma scaleR_half_double [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "(1 / 2) *\<^sub>R (a + a) = a"
+proof -
+  have "\<And>r. r *\<^sub>R (a + a) = (r * 2) *\<^sub>R a"
+    by (metis scaleR_2 scaleR_scaleR)
+  then show ?thesis
+    by simp
+qed
+
 
 (* FIXME: move elsewhere *)
 
@@ -1675,6 +1692,9 @@
 lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
   by (simp add: box_ne_empty inner_Basis inner_sum_left) (simp add: sum.remove)
 
+lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
+  using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
+
 
 subsection \<open>Connectedness\<close>
 
@@ -4338,6 +4358,16 @@
   using l unfolding islimpt_eq_acc_point
   by (rule acc_point_range_imp_convergent_subsequence)
 
+lemma islimpt_eq_infinite_ball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> ball x e))"
+  apply (simp add: islimpt_eq_acc_point, safe)
+   apply (metis Int_commute open_ball centre_in_ball)
+  by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)
+
+lemma islimpt_eq_infinite_cball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> cball x e))"
+  apply (simp add: islimpt_eq_infinite_ball, safe)
+   apply (meson Int_mono ball_subset_cball finite_subset order_refl)
+  by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
+
 lemma sequence_unique_limpt:
   fixes f :: "nat \<Rightarrow> 'a::t2_space"
   assumes "(f \<longlongrightarrow> l) sequentially"
@@ -4475,6 +4505,7 @@
          \<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
 by (metis Int_Diff open_delete openin_open)
 
+
 text\<open>Compactness expressed with filters\<close>
 
 lemma closure_iff_nhds_not_empty:
@@ -5032,6 +5063,7 @@
   "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
   using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
 
+
 subsection \<open>Metric spaces with the Heine-Borel property\<close>
 
 text \<open>
@@ -5254,6 +5286,84 @@
   show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     using l r by fast
 qed
+  
+subsubsection \<open>Intersecting chains of compact sets\<close>
+
+proposition bounded_closed_chain:
+  fixes \<F> :: "'a::heine_borel set set"
+  assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
+      and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+    shows "\<Inter>\<F> \<noteq> {}"
+proof -
+  have "B \<inter> \<Inter>\<F> \<noteq> {}"
+  proof (rule compact_imp_fip)
+    show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
+      by (simp_all add: assms compact_eq_bounded_closed)
+    show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G>
+    proof (induction \<G> rule: finite_induct)
+      case empty
+      with assms show ?case by force
+    next
+      case (insert U \<G>)
+      then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto
+      then consider "B \<subseteq> U" | "U \<subseteq> B"
+          using \<open>B \<in> \<F>\<close> chain by blast
+        then show ?case
+        proof cases
+          case 1
+          then show ?thesis
+            using Int_left_commute ne by auto
+        next
+          case 2
+          have "U \<noteq> {}"
+            using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast
+          moreover
+          have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y"
+          proof -
+            have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U"
+              by (metis chain contra_subsetD insert.prems insert_subset that)
+            then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U"
+              by (metis all_not_in_conv \<open>U \<noteq> {}\<close>)
+            moreover obtain x where "x \<in> \<Inter>\<G>"
+              by (metis Int_emptyI ne)
+            ultimately show ?thesis
+              by (metis Inf_lower subset_eq that)
+          qed
+          with 2 show ?thesis
+            by blast
+        qed
+      qed
+  qed
+  then show ?thesis by blast
+qed
+
+corollary compact_chain:
+  fixes \<F> :: "'a::heine_borel set set"
+  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
+          "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+    shows "\<Inter> \<F> \<noteq> {}"
+proof (cases "\<F> = {}")
+  case True
+  then show ?thesis by auto
+next
+  case False
+  show ?thesis
+    by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
+qed
+
+lemma compact_nest:
+  fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
+  assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
+  shows "\<Inter>range F \<noteq> {}"
+proof -
+  have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+    by (metis mono image_iff le_cases)
+  show ?thesis
+    apply (rule compact_chain [OF _ _ *])
+    using F apply (blast intro: dest: *)+
+    done
+qed
+
 
 subsubsection \<open>Completeness\<close>
 
@@ -7446,7 +7556,7 @@
 qed
 
 
-subsection \<open>Topological stuff lifted from and dropped to R\<close>
+subsection \<open>Topological stuff about the set of Reals\<close>
 
 lemma open_real:
   fixes s :: "real set"
@@ -7697,11 +7807,17 @@
     using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
 qed
 
-text \<open>We can state this in terms of diameter of a set.\<close>
+subsection \<open>The diameter of a set.\<close>
 
 definition diameter :: "'a::metric_space set \<Rightarrow> real" where
   "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
 
+lemma diameter_empty [simp]: "diameter{} = 0"
+  by (auto simp: diameter_def)
+
+lemma diameter_singleton [simp]: "diameter{x} = 0"
+  by (auto simp: diameter_def)
+
 lemma diameter_le:
   assumes "S \<noteq> {} \<or> 0 \<le> d"
       and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
@@ -7772,7 +7888,180 @@
     by (metis b diameter_bounded_bound order_antisym xys)
 qed
 
-text \<open>Related results with closure as the conclusion.\<close>
+lemma diameter_ge_0:
+  assumes "bounded S"  shows "0 \<le> diameter S"
+  by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)
+
+lemma diameter_subset:
+  assumes "S \<subseteq> T" "bounded T"
+  shows "diameter S \<le> diameter T"
+proof (cases "S = {} \<or> T = {}")
+  case True
+  with assms show ?thesis
+    by (force simp: diameter_ge_0)
+next
+  case False
+  then have "bdd_above ((\<lambda>x. case x of (x, xa) \<Rightarrow> dist x xa) ` (T \<times> T))"
+    using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)
+  with False \<open>S \<subseteq> T\<close> show ?thesis
+    apply (simp add: diameter_def)
+    apply (rule cSUP_subset_mono, auto)
+    done
+qed
+
+lemma diameter_closure:
+  assumes "bounded S"
+  shows "diameter(closure S) = diameter S"
+proof (rule order_antisym)
+  have "False" if "diameter S < diameter (closure S)"
+  proof -
+    define d where "d = diameter(closure S) - diameter(S)"
+    have "d > 0"
+      using that by (simp add: d_def)
+    then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"
+      by simp
+    have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
+      by (simp add: d_def divide_simps)
+     have bocl: "bounded (closure S)"
+      using assms by blast
+    moreover have "0 \<le> diameter S"
+      using assms diameter_ge_0 by blast
+    ultimately obtain x y where "x \<in> closure S" "y \<in> closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
+      using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto
+    then obtain x' y' where x'y': "x' \<in> S" "dist x' x < d/4" "y' \<in> S" "dist y' y < d/4"
+      using closure_approachable
+      by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)
+    then have "dist x' y' \<le> diameter S"
+      using assms diameter_bounded_bound by blast
+    with x'y' have "dist x y \<le> d / 4 + diameter S + d / 4"
+      by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)
+    then show ?thesis
+      using xy d_def by linarith
+  qed
+  then show "diameter (closure S) \<le> diameter S"
+    by fastforce
+  next
+    show "diameter S \<le> diameter (closure S)"
+      by (simp add: assms bounded_closure closure_subset diameter_subset)
+qed
+
+lemma diameter_cball [simp]:
+  fixes a :: "'a::euclidean_space"
+  shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)"
+proof -
+  have "diameter(cball a r) = 2*r" if "r \<ge> 0"
+  proof (rule order_antisym)
+    show "diameter (cball a r) \<le> 2*r"
+    proof (rule diameter_le)
+      fix x y assume "x \<in> cball a r" "y \<in> cball a r"
+      then have "norm (x - a) \<le> r" "norm (a - y) \<le> r"
+        by (auto simp: dist_norm norm_minus_commute)
+      then have "norm (x - y) \<le> r+r"
+        using norm_diff_triangle_le by blast
+      then show "norm (x - y) \<le> 2*r" by simp
+    qed (simp add: that)
+    have "2*r = dist (a + r *\<^sub>R (SOME i. i \<in> Basis)) (a - r *\<^sub>R (SOME i. i \<in> Basis))"
+      apply (simp add: dist_norm)
+      by (metis abs_of_nonneg mult.right_neutral norm_numeral norm_scaleR norm_some_Basis real_norm_def scaleR_2 that)
+    also have "... \<le> diameter (cball a r)"
+      apply (rule diameter_bounded_bound)
+      using that by (auto simp: dist_norm)
+    finally show "2*r \<le> diameter (cball a r)" .
+  qed
+  then show ?thesis by simp
+qed
+
+lemma diameter_ball [simp]:
+  fixes a :: "'a::euclidean_space"
+  shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)"
+proof -
+  have "diameter(ball a r) = 2*r" if "r > 0"
+    by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that)
+  then show ?thesis
+    by (simp add: diameter_def)
+qed
+
+lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)"
+proof -
+  have "{a .. b} = cball ((a+b)/2) ((b-a)/2)"
+    by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
+  then show ?thesis
+    by simp
+qed
+
+lemma diameter_open_interval [simp]: "diameter {a<..<b} = (if b < a then 0 else b-a)"
+proof -
+  have "{a <..< b} = ball ((a+b)/2) ((b-a)/2)"
+    by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
+  then show ?thesis
+    by simp
+qed
+
+proposition Lebesgue_number_lemma:
+  assumes "compact S" "\<C> \<noteq> {}" "S \<subseteq> \<Union>\<C>" and ope: "\<And>B. B \<in> \<C> \<Longrightarrow> open B"
+  obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)
+next
+  case False
+  { fix x assume "x \<in> S"
+    then obtain C where C: "x \<in> C" "C \<in> \<C>"
+      using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
+    then obtain r where r: "r>0" "ball x (2*r) \<subseteq> C"
+      by (metis mult.commute mult_2_right not_le ope openE real_sum_of_halves zero_le_numeral zero_less_mult_iff)
+    then have "\<exists>r C. r > 0 \<and> ball x (2*r) \<subseteq> C \<and> C \<in> \<C>"
+      using C by blast
+  }
+  then obtain r where r: "\<And>x. x \<in> S \<Longrightarrow> r x > 0 \<and> (\<exists>C \<in> \<C>. ball x (2*r x) \<subseteq> C)"
+    by metis
+  then have "S \<subseteq> (\<Union>x \<in> S. ball x (r x))"
+    by auto
+  then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x)) ` S"
+    by (rule compactE [OF \<open>compact S\<close>]) auto
+  then obtain S0 where "S0 \<subseteq> S" "finite S0" and S0: "\<T> = (\<lambda>x. ball x (r x)) ` S0"
+    by (meson finite_subset_image)
+  then have "S0 \<noteq> {}"
+    using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto
+  define \<delta> where "\<delta> = Inf (r ` S0)"
+  have "\<delta> > 0"
+    using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)
+  show ?thesis
+  proof
+    show "0 < \<delta>"
+      by (simp add: \<open>0 < \<delta>\<close>)
+    show "\<exists>B \<in> \<C>. T \<subseteq> B" if "T \<subseteq> S" and dia: "diameter T < \<delta>" for T
+    proof (cases "T = {}")
+      case True
+      then show ?thesis
+        using \<open>\<C> \<noteq> {}\<close> by blast
+    next
+      case False
+      then obtain y where "y \<in> T" by blast
+      then have "y \<in> S"
+        using \<open>T \<subseteq> S\<close> by auto
+      then obtain x where "x \<in> S0" and x: "y \<in> ball x (r x)"
+        using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
+      have "ball y \<delta> \<subseteq> ball y (r x)"
+        by (metis \<delta>_def \<open>S0 \<noteq> {}\<close> \<open>finite S0\<close> \<open>x \<in> S0\<close> empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)
+      also have "... \<subseteq> ball x (2*r x)"
+        by clarsimp (metis dist_commute dist_triangle_less_add mem_ball mult_2 x)
+      finally obtain C where "C \<in> \<C>" "ball y \<delta> \<subseteq> C"
+        by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
+      have "bounded T"
+        using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
+      then have "T \<subseteq> ball y \<delta>"
+        using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
+      then show ?thesis
+        apply (rule_tac x=C in bexI)
+        using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto
+    qed
+  qed
+qed
+
+
+subsection \<open>Compact sets and the closure operation.\<close>
 
 lemma closed_scaling:
   fixes s :: "'a::real_normed_vector set"
@@ -8396,6 +8685,63 @@
   using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
   by (auto simp: compact_eq_seq_compact_metric)
 
+proposition is_interval_compact:
+   "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
+proof (cases "S = {}")
+  case True
+  with empty_as_interval show ?thesis by auto
+next
+  case False
+  show ?thesis
+  proof
+    assume L: ?lhs
+    then have "is_interval S" "compact S" by auto
+    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x:S. x \<bullet> i) *\<^sub>R i"
+    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x:S. x \<bullet> i) *\<^sub>R i"
+    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
+      by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
+    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+      by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
+    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
+                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)" for x
+    proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
+      fix i::'a
+      assume i: "i \<in> Basis"
+      have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
+        by (intro continuous_intros)
+      obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
+        using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
+      obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
+        using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
+      have "a \<bullet> i \<le> (INF x:S. x \<bullet> i)"
+        by (simp add: False a cINF_greatest)
+      also have "\<dots> \<le> x \<bullet> i"
+        by (simp add: i inf)
+      finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
+      have "x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+        by (simp add: i sup)
+      also have "(SUP x:S. x \<bullet> i) \<le> b \<bullet> i"
+        by (simp add: False b cSUP_least)
+      finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
+      show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
+        apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
+        apply (simp add: i)
+        apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
+        using i ai bi apply force
+        done
+    qed
+    have "S = cbox a b"
+      by (auto simp: a_def b_def mem_box intro: 1 2 3)
+    then show ?rhs
+      by blast
+  next
+    assume R: ?rhs
+    then show ?lhs
+      using compact_cbox is_interval_cbox by blast
+  qed
+qed
+
+
 lemma box_midpoint:
   fixes a :: "'a::euclidean_space"
   assumes "box a b \<noteq> {}"
@@ -9959,6 +10305,20 @@
               compact T \<and> T \<subseteq> S)"
 by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
 
+lemma continuous_imp_closed_map:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes "closedin (subtopology euclidean S) U"
+          "continuous_on S f" "image f S = T" "compact S"
+    shows "closedin (subtopology euclidean T) (image f U)"
+  by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
+
+lemma continuous_imp_quotient_map:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes "continuous_on S f" "image f S = T" "compact S" "U \<subseteq> T"
+    shows "openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> U} \<longleftrightarrow>
+           openin (subtopology euclidean T) U"
+  by (metis (no_types, lifting) Collect_cong assms closed_map_imp_quotient_map continuous_imp_closed_map)
+
 subsection\<open> Finite intersection property\<close>
 
 text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
@@ -10305,6 +10665,166 @@
   qed
   from X0(1,2) this show ?thesis ..
 qed
+  
+  
+subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
+
+text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
+
+lemma continuous_disconnected_range_constant:
+  assumes s: "connected s"
+      and conf: "continuous_on s f"
+      and fim: "f ` s \<subseteq> t"
+      and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
+    shows "\<exists>a. \<forall>x \<in> s. f x = a"
+proof (cases "s = {}")
+  case True then show ?thesis by force
+next
+  case False
+  { fix x assume "x \<in> s"
+    then have "f ` s \<subseteq> {f x}"
+    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
+  }
+  with False show ?thesis
+    by blast
+qed
+
+lemma discrete_subset_disconnected:
+  fixes s :: "'a::topological_space set"
+  fixes t :: "'b::real_normed_vector set"
+  assumes conf: "continuous_on s f"
+      and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
+   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
+proof -
+  { fix x assume x: "x \<in> s"
+    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
+      using conf no [OF x] by auto
+    then have e2: "0 \<le> e / 2"
+      by simp
+    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
+      apply (rule ccontr)
+      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
+      apply (simp add: del: ex_simps)
+      apply (drule spec [where x="cball (f x) (e / 2)"])
+      apply (drule spec [where x="- ball(f x) e"])
+      apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
+        apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
+       using centre_in_cball connected_component_refl_eq e2 x apply blast
+      using ccs
+      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
+      done
+    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
+      by (auto simp: connected_component_in)
+    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
+      by (auto simp: x)
+  }
+  with assms show ?thesis
+    by blast
+qed
+
+lemma finite_implies_discrete:
+  fixes s :: "'a::topological_space set"
+  assumes "finite (f ` s)"
+  shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
+proof -
+  have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
+  proof (cases "f ` s - {f x} = {}")
+    case True
+    with zero_less_numeral show ?thesis
+      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
+  next
+    case False
+    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
+      by blast
+    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
+      using assms by simp
+    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
+      apply (rule finite_imp_less_Inf)
+      using z apply force+
+      done
+    show ?thesis
+      by (force intro!: * cInf_le_finite [OF finn])
+  qed
+  with assms show ?thesis
+    by blast
+qed
+
+text\<open>This proof requires the existence of two separate values of the range type.\<close>
+lemma finite_range_constant_imp_connected:
+  assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
+    shows "connected s"
+proof -
+  { fix t u
+    assume clt: "closedin (subtopology euclidean s) t"
+       and clu: "closedin (subtopology euclidean s) u"
+       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
+    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
+      apply (subst tus [symmetric])
+      apply (rule continuous_on_cases_local)
+      using clt clu tue
+      apply (auto simp: tus continuous_on_const)
+      done
+    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
+      by (rule finite_subset [of _ "{0,1}"]) auto
+    have "t = {} \<or> u = {}"
+      using assms [OF conif fi] tus [symmetric]
+      by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
+  }
+  then show ?thesis
+    by (simp add: connected_closedin_eq)
+qed
+
+lemma continuous_disconnected_range_constant_eq:
+      "(connected s \<longleftrightarrow>
+           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+            \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
+            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
+  and continuous_discrete_range_constant_eq:
+      "(connected s \<longleftrightarrow>
+         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+          continuous_on s f \<and>
+          (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
+          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
+  and continuous_finite_range_constant_eq:
+      "(connected s \<longleftrightarrow>
+         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+          continuous_on s f \<and> finite (f ` s)
+          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
+proof -
+  have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
+    \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
+    by blast
+  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
+    apply (rule *)
+    using continuous_disconnected_range_constant apply metis
+    apply clarify
+    apply (frule discrete_subset_disconnected; blast)
+    apply (blast dest: finite_implies_discrete)
+    apply (blast intro!: finite_range_constant_imp_connected)
+    done
+  then show ?thesis1 ?thesis2 ?thesis3
+    by blast+
+qed
+
+lemma continuous_discrete_range_constant:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
+  assumes s: "connected s"
+      and "continuous_on s f"
+      and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
+    shows "\<exists>a. \<forall>x \<in> s. f x = a"
+  using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
+  by blast
+
+lemma continuous_finite_range_constant:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
+  assumes "connected s"
+      and "continuous_on s f"
+      and "finite (f ` s)"
+    shows "\<exists>a. \<forall>x \<in> s. f x = a"
+  using assms continuous_finite_range_constant_eq
+  by blast
+
 
 no_notation
   eucl_less (infix "<e" 50)
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Complex.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -437,6 +437,14 @@
   "continuous F f \<longleftrightarrow> continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
   by (simp only: continuous_def tendsto_complex_iff)
 
+lemma continuous_on_of_real_o_iff [simp]:
+     "continuous_on S (\<lambda>x. complex_of_real (g x)) = continuous_on S g"
+  using continuous_on_Re continuous_on_of_real  by fastforce
+
+lemma continuous_on_of_real_id [simp]:
+     "continuous_on S (of_real :: real \<Rightarrow> 'a::real_normed_algebra_1)"
+  by (rule continuous_on_of_real [OF continuous_on_id])
+
 lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow>
     ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
     ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -194,6 +194,64 @@
   using assms irreducible_altdef[of m]
   by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
 
+    
+subsection\<open>Largest exponent of a prime factor\<close>
+text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
+  
+lemma prime_power_cancel_less:
+  assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "\<not> p dvd m"
+  shows False
+proof -
+  obtain l where l: "k' = k + l" and "l > 0"
+    using less less_imp_add_positive by auto
+  have "m = m * (p ^ k) div (p ^ k)"
+    using \<open>prime p\<close> by simp
+  also have "\<dots> = m' * (p ^ k') div (p ^ k)"
+    using eq by simp
+  also have "\<dots> = m' * (p ^ l) * (p ^ k) div (p ^ k)"
+    by (simp add: l mult.commute mult.left_commute power_add)
+  also have "... = m' * (p ^ l)"
+    using \<open>prime p\<close> by simp
+  finally have "p dvd m"
+    using \<open>l > 0\<close> by simp
+  with assms show False
+    by simp
+qed
+
+lemma prime_power_cancel:
+  assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "\<not> p dvd m" "\<not> p dvd m'"
+  shows "k = k'"
+  using prime_power_cancel_less [OF \<open>prime p\<close>] assms
+  by (metis linorder_neqE_nat)
+
+lemma prime_power_cancel2:
+  assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "\<not> p dvd m" "\<not> p dvd m'"
+  obtains "m = m'" "k = k'"
+  using prime_power_cancel [OF assms] assms by auto
+
+lemma prime_power_canonical:
+  fixes m::nat
+  assumes "prime p" "m > 0"
+  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
+using \<open>m > 0\<close>
+proof (induction m rule: less_induct)
+  case (less m)
+  show ?case
+  proof (cases "p dvd m")
+    case True
+    then obtain m' where m': "m = p * m'"
+      using dvdE by blast
+    with \<open>prime p\<close> have "0 < m'" "m' < m"
+      using less.prems prime_nat_iff by auto
+    with m' less show ?thesis
+      by (metis power_Suc mult.left_commute)
+  next
+    case False
+    then show ?thesis
+      by (metis mult.right_neutral power_0)
+  qed
+qed
+
 
 subsubsection \<open>Make prime naively executable\<close>
 
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Set_Interval.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -1090,6 +1090,19 @@
      "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
 
+lemma bounded_Max_nat:
+  fixes P :: "nat \<Rightarrow> bool"
+  assumes x: "P x" and M: "\<And>x. P x \<Longrightarrow> x \<le> M"
+  obtains m where "P m" "\<And>x. P x \<Longrightarrow> x \<le> m"
+proof -
+  have "finite {x. P x}"
+    using M finite_nat_set_iff_bounded_le by auto
+  then have "Max {x. P x} \<in> {x. P x}"
+    using Max_in x by auto
+  then show ?thesis
+    by (simp add: \<open>finite {x. P x}\<close> that)
+qed
+
 
 text\<open>Any subset of an interval of natural numbers the size of the
 subset is exactly that interval.\<close>
diff -r 1ddc262514b8 -r 223b2ebdda79 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Jan 04 16:18:50 2017 +0000
@@ -1530,9 +1530,6 @@
 lemma tendsto_compose: "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
 
-lemma LIM_o: "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> f \<midarrow>a\<rightarrow> l \<Longrightarrow> (g \<circ> f) \<midarrow>a\<rightarrow> g l"
-  unfolding o_def by (rule tendsto_compose)
-
 lemma tendsto_compose_eventually:
   "g \<midarrow>l\<rightarrow> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
   by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)