# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1457361285 0
# Node ID bc25f3916a99c0369ace28fb12e4987487d83884
# Parent  edee1966fddf525fdc4a01c7e8c29f4196abddb8
new material to Blochj's theorem, as well as supporting lemmas

diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -2678,6 +2678,7 @@
 (** Existence of a primitive.*)
 
 lemma holomorphic_starlike_primitive:
+  fixes f :: "complex \<Rightarrow> complex"
   assumes contf: "continuous_on s f"
       and s: "starlike s" and os: "open s"
       and k: "finite k"
@@ -2796,6 +2797,8 @@
   done
 
 lemma holomorphic_convex_primitive:
+  fixes f :: "complex \<Rightarrow> complex"
+  shows
   "\<lbrakk>convex s; finite k; continuous_on s f;
     \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
    \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -277,11 +277,14 @@
 
 subsection\<open>Holomorphic functions\<close>
 
-text\<open>Could be generalized to real normed fields, but in practice that would only include the reals\<close>
-definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
+definition complex_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
            (infixr "(complex'_differentiable)" 50)
   where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
 
+lemma complex_differentiable_derivI:
+    "f complex_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
+by (simp add: complex_differentiable_def DERIV_deriv_iff_has_field_derivative)
+
 lemma complex_differentiable_imp_continuous_at:
     "f complex_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
   by (metis DERIV_continuous complex_differentiable_def)
@@ -297,24 +300,24 @@
   unfolding complex_differentiable_def
   by (metis DERIV_subset top_greatest)
 
-lemma complex_differentiable_linear [derivative_intros]: "(op * c) complex_differentiable F"
+lemma complex_differentiable_linear [simp,derivative_intros]: "(op * c) complex_differentiable F"
 proof -
   show ?thesis
     unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
     by (force intro: has_derivative_mult_right)
 qed
 
-lemma complex_differentiable_const [derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
+lemma complex_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
   unfolding complex_differentiable_def has_field_derivative_def
   by (rule exI [where x=0])
      (metis has_derivative_const lambda_zero)
 
-lemma complex_differentiable_ident [derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
+lemma complex_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
   unfolding complex_differentiable_def has_field_derivative_def
   by (rule exI [where x=1])
      (simp add: lambda_one [symmetric])
 
-lemma complex_differentiable_id [derivative_intros]: "id complex_differentiable F"
+lemma complex_differentiable_id [simp,derivative_intros]: "id complex_differentiable F"
   unfolding id_def by (rule complex_differentiable_ident)
 
 lemma complex_differentiable_minus [derivative_intros]:
@@ -328,6 +331,10 @@
   using assms unfolding complex_differentiable_def
   by (metis field_differentiable_add)
 
+lemma complex_differentiable_add_const [simp,derivative_intros]:
+     "op + c complex_differentiable F"
+  by (simp add: complex_differentiable_add)
+
 lemma complex_differentiable_setsum [derivative_intros]:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
   by (induct I rule: infinite_finite_induct)
@@ -503,6 +510,11 @@
   "DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
   unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
 
+lemma holomorphic_derivI:
+     "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
+      \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
+by (metis DERIV_deriv_iff_complex_differentiable at_within_open  holomorphic_on_def has_field_derivative_at_within)
+
 lemma complex_derivative_chain:
   "f complex_differentiable at x \<Longrightarrow> g complex_differentiable at (f x)
     \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
@@ -568,6 +580,20 @@
 apply (simp add: algebra_simps)
 done
 
+lemma nonzero_deriv_nonconstant:
+  assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0"
+    shows "\<not> f constant_on S"
+unfolding constant_on_def
+by (metis \<open>df \<noteq> 0\<close> DERIV_transform_within_open [OF df S] DERIV_const DERIV_unique)
+
+lemma holomorphic_nonconstant:
+  assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0"
+    shows "\<not> f constant_on S"
+    apply (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
+    using assms
+    apply (auto simp: holomorphic_derivI)
+    done
+
 subsection\<open>Analyticity on a set\<close>
 
 definition analytic_on (infixl "(analytic'_on)" 50)
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -1633,13 +1633,15 @@
   done
 
 lemma complex_differentiable_powr_right:
+  fixes w::complex
+  shows
     "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
 using complex_differentiable_def has_field_derivative_powr_right by blast
 
 lemma holomorphic_on_powr_right:
     "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
-    unfolding holomorphic_on_def
-    using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
+    unfolding holomorphic_on_def complex_differentiable_def
+by (metis (full_types) DERIV_chain' has_field_derivative_powr_right) 
 
 lemma norm_powr_real_powr:
   "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -1722,4 +1722,412 @@
     done
 qed
 
+subsection\<open>Bloch's theorem\<close>
+
+lemma Bloch_lemma_0:
+  assumes holf: "f holomorphic_on cball 0 r" and "0 < r"
+      and [simp]: "f 0 = 0"
+      and le: "\<And>z. norm z < r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f 0)"
+    shows "ball 0 ((3 - 2 * sqrt 2) * r * norm(deriv f 0)) \<subseteq> f ` ball 0 r"
+proof -
+  have "sqrt 2 < 3/2"
+    by (rule real_less_lsqrt) (auto simp: power2_eq_square)
+  then have sq3: "0 < 3 - 2 * sqrt 2" by simp
+  show ?thesis
+  proof (cases "deriv f 0 = 0")
+    case True then show ?thesis by simp
+  next
+    case False
+    def C \<equiv> "2 * norm(deriv f 0)"
+    have "0 < C" using False by (simp add: C_def)
+    have holf': "f holomorphic_on ball 0 r" using holf
+      using ball_subset_cball holomorphic_on_subset by blast
+    then have holdf': "deriv f holomorphic_on ball 0 r"
+      by (rule holomorphic_deriv [OF _ open_ball])
+    have "Le1": "norm(deriv f z - deriv f 0) \<le> norm z / (r - norm z) * C"
+                if "norm z < r" for z
+    proof -
+      have T1: "norm(deriv f z - deriv f 0) \<le> norm z / (R - norm z) * C"
+              if R: "norm z < R" "R < r" for R
+      proof -
+        have "0 < R" using R
+          by (metis less_trans norm_zero zero_less_norm_iff)
+        have df_le: "\<And>x. norm x < r \<Longrightarrow> norm (deriv f x) \<le> C"
+          using le by (simp add: C_def)
+        have hol_df: "deriv f holomorphic_on cball 0 R"
+          apply (rule holomorphic_on_subset) using R holdf' by auto
+        have *: "((\<lambda>w. deriv f w / (w - z)) has_contour_integral 2 * pi * \<i> * deriv f z) (circlepath 0 R)"
+                 if "norm z < R" for z
+          using \<open>0 < R\<close> that Cauchy_integral_formula_convex_simple [OF convex_cball hol_df, of _ "circlepath 0 R"]
+          by (force simp: winding_number_circlepath)
+        have **: "((\<lambda>x. deriv f x / (x - z) - deriv f x / x) has_contour_integral
+                   of_real (2 * pi) * \<i> * (deriv f z - deriv f 0))
+                  (circlepath 0 R)"
+           using has_contour_integral_diff [OF * [of z] * [of 0]] \<open>0 < R\<close> that
+           by (simp add: algebra_simps)
+        have [simp]: "\<And>x. norm x = R \<Longrightarrow> x \<noteq> z"  using that(1) by blast
+        have "norm (deriv f x / (x - z) - deriv f x / x)
+                     \<le> C * norm z / (R * (R - norm z))"
+                  if "norm x = R" for x
+        proof -
+          have [simp]: "norm (deriv f x * x - deriv f x * (x - z)) =
+                        norm (deriv f x) * norm z"
+            by (simp add: norm_mult right_diff_distrib')
+          show ?thesis
+            using  \<open>0 < R\<close> \<open>0 < C\<close> R that
+            apply (simp add: norm_mult norm_divide divide_simps)
+            using df_le norm_triangle_ineq2 \<open>0 < C\<close> apply (auto intro!: mult_mono)
+            done
+        qed
+        then show ?thesis
+          using has_contour_integral_bound_circlepath
+                  [OF **, of "C * norm z/(R*(R - norm z))"]
+                \<open>0 < R\<close> \<open>0 < C\<close> R
+          apply (simp add: norm_mult norm_divide)
+          apply (simp add: divide_simps mult.commute)
+          done
+      qed
+      obtain r' where r': "norm z < r'" "r' < r"
+        using Rats_dense_in_real [of "norm z" r] \<open>norm z < r\<close> by blast
+      then have [simp]: "closure {r'<..<r} = {r'..r}" by simp
+      show ?thesis
+        apply (rule continuous_ge_on_closure
+                 [where f = "\<lambda>r. norm z / (r - norm z) * C" and s = "{r'<..<r}",
+                  OF _ _ T1])
+        apply (intro continuous_intros)
+        using that r'
+        apply (auto simp: not_le)
+        done
+    qed
+    have "*": "(norm z - norm z^2/(r - norm z)) * norm(deriv f 0) \<le> norm(f z)"
+              if r: "norm z < r" for z
+    proof -
+      have 1: "\<And>x. x \<in> ball 0 r \<Longrightarrow>
+              ((\<lambda>z. f z - deriv f 0 * z) has_field_derivative deriv f x - deriv f 0)
+               (at x within ball 0 r)"
+        by (rule derivative_eq_intros holomorphic_derivI holf' | simp)+
+      have 2: "closed_segment 0 z \<subseteq> ball 0 r"
+        by (metis \<open>0 < r\<close> convex_ball convex_contains_segment dist_self mem_ball mem_ball_0 that)
+      have 3: "(\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C) integrable_on {0..1}"
+        apply (rule integrable_on_cmult_right [where 'b=real, simplified])
+        apply (rule integrable_on_cdivide [where 'b=real, simplified])
+        apply (rule integrable_on_cmult_left [where 'b=real, simplified])
+        apply (rule ident_integrable_on)
+        done
+      have 4: "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \<le> norm z * norm z * x * C / (r - norm z)"
+              if x: "0 \<le> x" "x \<le> 1" for x
+      proof -
+        have [simp]: "x * norm z < r"
+          using r x by (meson le_less_trans mult_le_cancel_right2 norm_not_less_zero)
+        have "norm (deriv f (x *\<^sub>R z) - deriv f 0) \<le> norm (x *\<^sub>R z) / (r - norm (x *\<^sub>R z)) * C"
+          apply (rule Le1) using r x \<open>0 < r\<close> by simp
+        also have "... \<le> norm (x *\<^sub>R z) / (r - norm z) * C"
+          using r x \<open>0 < r\<close>
+          apply (simp add: divide_simps)
+          by (simp add: \<open>0 < C\<close> mult.assoc mult_left_le_one_le ordered_comm_semiring_class.comm_mult_left_mono)
+        finally have "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \<le> norm (x *\<^sub>R z)  / (r - norm z) * C * norm z"
+          by (rule mult_right_mono) simp
+        with x show ?thesis by (simp add: algebra_simps)
+      qed
+      have le_norm: "abc \<le> norm d - e \<Longrightarrow> norm(f - d) \<le> e \<Longrightarrow> abc \<le> norm f" for abc d e and f::complex
+        by (metis add_diff_cancel_left' add_diff_eq diff_left_mono norm_diff_ineq order_trans)
+      have "norm (integral {0..1} (\<lambda>x. (deriv f (x *\<^sub>R z) - deriv f 0) * z))
+            \<le> integral {0..1} (\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C)"
+        apply (rule integral_norm_bound_integral)
+        using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
+        apply (simp add: has_contour_integral_linepath has_integral_integrable_integral)
+        apply (rule 3)
+        apply (simp add: norm_mult power2_eq_square 4)
+        done
+      then have int_le: "norm (f z - deriv f 0 * z) \<le> (norm z)\<^sup>2 * norm(deriv f 0) / ((r - norm z))"
+        using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
+        apply (simp add: has_contour_integral_linepath has_integral_integrable_integral C_def)
+        done
+      show ?thesis
+        apply (rule le_norm [OF _ int_le])
+        using \<open>norm z < r\<close>
+        apply (simp add: power2_eq_square divide_simps C_def norm_mult)
+        proof -
+          have "norm z * (norm (deriv f 0) * (r - norm z - norm z)) \<le> norm z * (norm (deriv f 0) * (r - norm z) - norm (deriv f 0) * norm z)"
+            by (simp add: linordered_field_class.sign_simps(38))
+          then show "(norm z * (r - norm z) - norm z * norm z) * norm (deriv f 0) \<le> norm (deriv f 0) * norm z * (r - norm z) - norm z * norm z * norm (deriv f 0)"
+            by (simp add: linordered_field_class.sign_simps(38) mult.commute mult.left_commute)
+        qed
+    qed
+    have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2)  < 1"
+      by (auto simp:  sqrt2_less_2)
+    have 1: "continuous_on (closure (ball 0 ((1 - sqrt 2 / 2) * r))) f"
+      apply (rule continuous_on_subset [OF holomorphic_on_imp_continuous_on [OF holf]])
+      apply (subst closure_ball)
+      using \<open>0 < r\<close> mult_pos_pos sq201
+      apply (auto simp: cball_subset_cball_iff)
+      done
+    have 2: "open (f ` interior (ball 0 ((1 - sqrt 2 / 2) * r)))"
+      apply (rule open_mapping_thm [OF holf' open_ball connected_ball], force)
+      using \<open>0 < r\<close> mult_pos_pos sq201 apply (simp add: ball_subset_ball_iff)
+      using False \<open>0 < r\<close> centre_in_ball holf' holomorphic_nonconstant by blast
+    have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv f 0)) =
+          ball (f 0) ((3 - 2 * sqrt 2) * r * norm (deriv f 0))"
+      by simp
+    also have "...  \<subseteq> f ` ball 0 ((1 - sqrt 2 / 2) * r)"
+    proof -
+      have 3: "(3 - 2 * sqrt 2) * r * norm (deriv f 0) \<le> norm (f z)"
+           if "norm z = (1 - sqrt 2 / 2) * r" for z
+        apply (rule order_trans [OF _ *])
+        using  \<open>0 < r\<close>
+        apply (simp_all add: field_simps  power2_eq_square that)
+        apply (simp add: mult.assoc [symmetric])
+        done
+      show ?thesis
+        apply (rule ball_subset_open_map_image [OF 1 2 _ bounded_ball])
+        using \<open>0 < r\<close> sq201 3 apply simp_all
+        using C_def \<open>0 < C\<close> sq3 apply force
+        done
+     qed
+    also have "...  \<subseteq> f ` ball 0 r"
+      apply (rule image_subsetI [OF imageI], simp)
+      apply (erule less_le_trans)
+      using \<open>0 < r\<close> apply (auto simp: field_simps)
+      done
+    finally show ?thesis .
+  qed
+qed
+
+lemma Bloch_lemma: 
+  assumes holf: "f holomorphic_on cball a r" and "0 < r"
+      and le: "\<And>z. z \<in> ball a r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f a)"
+    shows "ball (f a) ((3 - 2 * sqrt 2) * r * norm(deriv f a)) \<subseteq> f ` ball a r"
+proof -
+  have fz: "(\<lambda>z. f (a + z)) = f o (\<lambda>z. (a + z))"
+    by (simp add: o_def)
+  have hol0: "(\<lambda>z. f (a + z)) holomorphic_on cball 0 r"
+    unfolding fz by (intro holomorphic_intros holf holomorphic_on_compose | simp)+
+  then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) complex_differentiable at x"
+    by (metis Topology_Euclidean_Space.open_ball at_within_open ball_subset_cball diff_0 dist_norm holomorphic_on_def holomorphic_on_subset mem_ball norm_minus_cancel)
+  have [simp]: "\<And>z. norm z < r \<Longrightarrow> f complex_differentiable at (a + z)"
+    by (metis holf open_ball add_diff_cancel_left' dist_complex_def holomorphic_on_imp_differentiable_at holomorphic_on_subset interior_cball interior_subset mem_ball norm_minus_commute)
+  then have [simp]: "f complex_differentiable at a"
+    by (metis add.comm_neutral \<open>0 < r\<close> norm_eq_zero)
+  have hol1: "(\<lambda>z. f (a + z) - f a) holomorphic_on cball 0 r"
+    by (intro holomorphic_intros hol0)
+  then have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv (\<lambda>z. f (a + z) - f a) 0))
+             \<subseteq> (\<lambda>z. f (a + z) - f a) ` ball 0 r"
+    apply (rule Bloch_lemma_0)
+    apply (simp_all add: \<open>0 < r\<close>)
+    apply (simp add: fz complex_derivative_chain)
+    apply (simp add: dist_norm le)
+    done
+  then show ?thesis
+    apply clarify
+    apply (drule_tac c="x - f a" in subsetD)
+     apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain complex_differentiable_compose)+
+    done
+qed
+
+proposition Bloch_unit: 
+  assumes holf: "f holomorphic_on ball a 1" and [simp]: "deriv f a = 1"
+  obtains b r where "1/12 < r" "ball b r \<subseteq> f ` (ball a 1)"
+proof -
+  def r \<equiv> "249/256::real"
+  have "0 < r" "r < 1" by (auto simp: r_def)
+  def g \<equiv> "\<lambda>z. deriv f z * of_real(r - norm(z - a))"
+  have "deriv f holomorphic_on ball a 1"
+    by (rule holomorphic_deriv [OF holf open_ball])
+  then have "continuous_on (ball a 1) (deriv f)"
+    using holomorphic_on_imp_continuous_on by blast
+  then have "continuous_on (cball a r) (deriv f)"
+    by (rule continuous_on_subset) (simp add: cball_subset_ball_iff \<open>r < 1\<close>)
+  then have "continuous_on (cball a r) g"
+    by (simp add: g_def continuous_intros)
+  then have 1: "compact (g ` cball a r)"
+    by (rule compact_continuous_image [OF _ compact_cball])
+  have 2: "g ` cball a r \<noteq> {}"
+    using \<open>r > 0\<close> by auto
+  obtain p where pr: "p \<in> cball a r" 
+             and pge: "\<And>y. y \<in> cball a r \<Longrightarrow> norm (g y) \<le> norm (g p)"
+    using distance_attains_sup [OF 1 2, of 0] by force
+  def t \<equiv> "(r - norm(p - a)) / 2"
+  have "norm (p - a) \<noteq> r"
+    using pge [of a] \<open>r > 0\<close> by (auto simp: g_def norm_mult)
+  then have "norm (p - a) < r" using pr 
+    by (simp add: norm_minus_commute dist_norm)
+  then have "0 < t" 
+    by (simp add: t_def)
+  have cpt: "cball p t \<subseteq> ball a r"
+    using \<open>0 < t\<close> by (simp add: cball_subset_ball_iff dist_norm t_def field_simps)
+  have gen_le_dfp: "norm (deriv f y) * (r - norm (y - a)) / (r - norm (p - a)) \<le> norm (deriv f p)" 
+            if "y \<in> cball a r" for y
+  proof -
+    have [simp]: "norm (y - a) \<le> r"
+      using that by (simp add: dist_norm norm_minus_commute) 
+    have "norm (g y) \<le> norm (g p)"
+      using pge [OF that] by simp
+    then have "norm (deriv f y) * abs (r - norm (y - a)) \<le> norm (deriv f p) * abs (r - norm (p - a))"
+      by (simp only: dist_norm g_def norm_mult norm_of_real)
+    with that \<open>norm (p - a) < r\<close> show ?thesis
+      by (simp add: dist_norm divide_simps)
+  qed
+  have le_norm_dfp: "r / (r - norm (p - a)) \<le> norm (deriv f p)"
+    using gen_le_dfp [of a] \<open>r > 0\<close> by auto
+  have 1: "f holomorphic_on cball p t"
+    apply (rule holomorphic_on_subset [OF holf])
+    using cpt \<open>r < 1\<close> order_subst1 subset_ball by auto
+  have 2: "norm (deriv f z) \<le> 2 * norm (deriv f p)" if "z \<in> ball p t" for z
+  proof -
+    have z: "z \<in> cball a r"
+      by (meson ball_subset_cball subsetD cpt that)
+    then have "norm(z - a) < r"
+      by (metis ball_subset_cball contra_subsetD cpt dist_norm mem_ball norm_minus_commute that)
+    have "norm (deriv f z) * (r - norm (z - a)) / (r - norm (p - a)) \<le> norm (deriv f p)" 
+      using gen_le_dfp [OF z] by simp
+    with \<open>norm (z - a) < r\<close> \<open>norm (p - a) < r\<close> 
+    have "norm (deriv f z) \<le> (r - norm (p - a)) / (r - norm (z - a)) * norm (deriv f p)"
+       by (simp add: field_simps)
+    also have "... \<le> 2 * norm (deriv f p)"
+      apply (rule mult_right_mono)
+      using that \<open>norm (p - a) < r\<close> \<open>norm(z - a) < r\<close> 
+      apply (simp_all add: field_simps t_def dist_norm [symmetric])
+      using dist_triangle3 [of z a p] by linarith
+    finally show ?thesis .
+  qed
+  have sqrt2: "sqrt 2 < 2113/1494"
+    by (rule real_less_lsqrt) (auto simp: power2_eq_square)
+  then have sq3: "0 < 3 - 2 * sqrt 2" by simp
+  have "1 / 12 / ((3 - 2 * sqrt 2) / 2) < r"
+    using sq3 sqrt2 by (auto simp: field_simps r_def) 
+  also have "... \<le> cmod (deriv f p) * (r - cmod (p - a))"
+    using \<open>norm (p - a) < r\<close> le_norm_dfp   by (simp add: pos_divide_le_eq)    
+  finally have "1 / 12 < cmod (deriv f p) * (r - cmod (p - a)) * ((3 - 2 * sqrt 2) / 2)"  
+    using pos_divide_less_eq half_gt_zero_iff sq3 by blast
+  then have **: "1 / 12 < (3 - 2 * sqrt 2) * t * norm (deriv f p)"
+    using sq3 by (simp add: mult.commute t_def)
+  have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball p t"
+    by (rule Bloch_lemma [OF 1 \<open>0 < t\<close> 2])
+  also have "... \<subseteq> f ` ball a 1"
+    apply (rule image_mono)
+    apply (rule order_trans [OF ball_subset_cball])
+    apply (rule order_trans [OF cpt])
+    using \<open>0 < t\<close> \<open>r < 1\<close> apply (simp add: ball_subset_ball_iff dist_norm)
+    done
+  finally have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball a 1" .
+  with ** show ?thesis
+    by (rule that)
+qed
+
+
+theorem Bloch:
+  assumes holf: "f holomorphic_on ball a r" and "0 < r" 
+      and r': "r' \<le> r * norm (deriv f a) / 12"
+  obtains b where "ball b r' \<subseteq> f ` (ball a r)"
+proof (cases "deriv f a = 0")
+  case True with r' show ?thesis
+    using ball_eq_empty that by fastforce
+next
+  case False
+    def C \<equiv> "deriv f a"
+    have "0 < norm C" using False by (simp add: C_def)
+    have dfa: "f complex_differentiable at a"
+      apply (rule holomorphic_on_imp_differentiable_at [OF holf])
+      using \<open>0 < r\<close> by auto
+    have fo: "(\<lambda>z. f (a + of_real r * z)) = f o (\<lambda>z. (a + of_real r * z))"
+      by (simp add: o_def)
+    have holf': "f holomorphic_on (\<lambda>z. a + complex_of_real r * z) ` ball 0 1"
+      apply (rule holomorphic_on_subset [OF holf])
+      using \<open>0 < r\<close> apply (force simp: dist_norm norm_mult)
+      done
+    have 1: "(\<lambda>z. f (a + r * z) / (C * r)) holomorphic_on ball 0 1"
+      apply (rule holomorphic_intros holomorphic_on_compose holf' | simp add: fo)+
+      using \<open>0 < r\<close> by (simp add: C_def False)
+    have "((\<lambda>z. f (a + of_real r * z) / (C * of_real r)) has_field_derivative
+          (deriv f (a + of_real r * z) / C)) (at z)" 
+         if "norm z < 1" for z
+    proof -
+    have *: "((\<lambda>x. f (a + of_real r * x)) has_field_derivative
+             (deriv f (a + of_real r * z) * of_real r)) (at z)"
+        apply (simp add: fo)
+        apply (rule DERIV_chain [OF complex_differentiable_derivI])
+        apply (rule holomorphic_on_imp_differentiable_at [OF holf], simp)
+        using \<open>0 < r\<close> apply (simp add: dist_norm norm_mult that)
+        apply (rule derivative_eq_intros | simp)+
+        done
+      show ?thesis
+        apply (rule derivative_eq_intros * | simp)+
+        using \<open>0 < r\<close> by (auto simp: C_def False)
+    qed
+    have 2: "deriv (\<lambda>z. f (a + of_real r * z) / (C * of_real r)) 0 = 1"
+      apply (subst complex_derivative_cdivide_right)
+      apply (simp add: complex_differentiable_def fo)
+      apply (rule exI)
+      apply (rule DERIV_chain [OF complex_differentiable_derivI])
+      apply (simp add: dfa)
+      apply (rule derivative_eq_intros | simp add: C_def False fo)+
+      using \<open>0 < r\<close> 
+      apply (simp add: C_def False fo)
+      apply (simp add: derivative_intros dfa complex_derivative_chain)
+      done
+    have sb1: "op * (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1 
+               \<subseteq> f ` ball a r"
+      using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
+    have sb2: "ball (C * r * b) r' \<subseteq> op * (C * r) ` ball b t" 
+               if "1 / 12 < t" for b t
+    proof -
+      have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
+        using that \<open>0 < r\<close> less_eq_real_def mult.commute mult.right_neutral mult_left_mono norm_ge_zero times_divide_eq_right 
+        by auto
+      show ?thesis
+        apply clarify
+        apply (rule_tac x="x / (C * r)" in image_eqI)
+        using \<open>0 < r\<close>  
+        apply (simp_all add: dist_norm norm_mult norm_divide C_def False field_simps)
+        apply (erule less_le_trans)
+        apply (rule order_trans [OF r' *])
+        done
+    qed
+    show ?thesis
+      apply (rule Bloch_unit [OF 1 2])
+      apply (rename_tac t)
+      apply (rule_tac b="(C * of_real r) * b" in that)
+      apply (drule image_mono [where f = "\<lambda>z. (C * of_real r) * z"])
+      using sb1 sb2
+      apply force
+      done
+qed
+
+corollary Bloch_general:
+  assumes holf: "f holomorphic_on s" and "a \<in> s" 
+      and tle: "\<And>z. z \<in> frontier s \<Longrightarrow> t \<le> dist a z"
+      and rle: "r \<le> t * norm(deriv f a) / 12"
+  obtains b where "ball b r \<subseteq> f ` s"
+proof -
+  consider "r \<le> 0" | "0 < t * norm(deriv f a) / 12" using rle by force
+  then show ?thesis
+  proof cases
+    case 1 then show ?thesis
+      by (simp add: Topology_Euclidean_Space.ball_empty that)
+  next
+    case 2
+    show ?thesis
+    proof (cases "deriv f a = 0")
+      case True then show ?thesis
+        using rle by (simp add: Topology_Euclidean_Space.ball_empty that)
+    next
+      case False
+      then have "t > 0"
+        using 2 by (force simp: zero_less_mult_iff)
+      have "~ ball a t \<subseteq> s \<Longrightarrow> ball a t \<inter> frontier s \<noteq> {}"
+        apply (rule connected_Int_frontier [of "ball a t" s], simp_all)
+        using \<open>0 < t\<close> \<open>a \<in> s\<close> centre_in_ball apply blast
+        done
+      with tle have *: "ball a t \<subseteq> s" by fastforce
+      then have 1: "f holomorphic_on ball a t"
+        using holf using holomorphic_on_subset by blast
+      show ?thesis
+        apply (rule Bloch [OF 1 \<open>t > 0\<close> rle])
+        apply (rule_tac b=b in that)
+        using * apply force
+        done
+    qed
+  qed
+qed
+
 end
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -5277,7 +5277,7 @@
     proof -
       assume "v < 1"
       then show False
-        using v(3)[THEN spec[where x=1]] using x and fs by auto
+        using v(3)[THEN spec[where x=1]] using x fs by (simp add: pth_1 subset_iff)
     next
       assume "v > 1"
       then show False
@@ -5294,8 +5294,7 @@
       apply (cases "u = 1")
         using assms(3)[THEN bspec[where x=x], THEN spec[where x=u]]
         using \<open>0\<le>u\<close> and x and fs
-        apply auto
-        done
+        by auto
     qed auto
   qed
 
@@ -9866,7 +9865,7 @@
     apply (rule le_setdistI, blast)
     using False apply (fastforce intro: le_setdistI)
     apply (simp add: algebra_simps)
-    apply (metis dist_commute dist_triangle_alt order_trans [OF setdist_le_dist])
+    apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
     done
   then have "setdist s t - setdist {a} t \<le> setdist s {a}"
     using False by (fastforce intro: le_setdistI)
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -194,6 +194,9 @@
   unfolding differentiable_def
   by auto
 
+lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)"
+  using differentiable_on_def by blast
+
 lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
   unfolding differentiable_def
   using has_derivative_at_within
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -1384,6 +1384,8 @@
 
 
 lemma complex_differentiable_Polygamma:
+  fixes z::complex
+  shows
   "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n complex_differentiable (at z within A)"
   using has_field_derivative_Polygamma[of z n] unfolding complex_differentiable_def by auto
 
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -2501,6 +2501,12 @@
   shows "integral s (\<lambda>x. c * f x) = c * integral s f"
 by (simp add: mult.commute [of c])
 
+corollary integral_divide [simp]:
+  fixes z :: "'a::real_normed_field"
+  shows "integral S (\<lambda>x. f x / z) = integral S (\<lambda>x. f x) / z"
+using integral_mult_left [of S f "inverse z"]
+  by (simp add: divide_inverse_commute)
+
 lemma has_integral_mult_right:
   fixes c :: "'a :: real_normed_algebra"
   shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
@@ -2681,6 +2687,12 @@
   using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] \<open>c \<noteq> 0\<close>
   by auto
 
+lemma integrable_on_cmult_left:
+  assumes "f integrable_on s"
+  shows "(\<lambda>x. of_real c * f x) integrable_on s"
+    using integrable_cmul[of f s "of_real c"] assms
+    by (simp add: scaleR_conv_of_real)
+
 lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
   unfolding integrable_on_def by(auto intro: has_integral_neg)
 
@@ -2756,6 +2768,45 @@
   unfolding integral_def
 by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq)
 
+lemma integrable_on_cmult_left_iff [simp]:
+  assumes "c \<noteq> 0"
+  shows "(\<lambda>x. of_real c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have "(\<lambda>x. of_real (1 / c) * (of_real c * f x)) integrable_on s"
+    using integrable_cmul[of "\<lambda>x. of_real c * f x" s "1 / of_real c"]
+    by (simp add: scaleR_conv_of_real)
+  then have "(\<lambda>x. (of_real (1 / c) * of_real c * f x)) integrable_on s"
+    by (simp add: algebra_simps)
+  with \<open>c \<noteq> 0\<close> show ?rhs
+    by (metis (no_types, lifting) integrable_eq mult.left_neutral nonzero_divide_eq_eq of_real_1 of_real_mult)
+qed (blast intro: integrable_on_cmult_left)
+
+lemma integrable_on_cmult_right:
+  fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
+  assumes "f integrable_on s"
+  shows "(\<lambda>x. f x * of_real c) integrable_on s"
+using integrable_on_cmult_left [OF assms] by (simp add: mult.commute)
+
+lemma integrable_on_cmult_right_iff [simp]:
+  fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
+  assumes "c \<noteq> 0"
+  shows "(\<lambda>x. f x * of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
+using integrable_on_cmult_left_iff [OF assms] by (simp add: mult.commute)
+
+lemma integrable_on_cdivide:
+  fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
+  assumes "f integrable_on s"
+  shows "(\<lambda>x. f x / of_real c) integrable_on s"
+by (simp add: integrable_on_cmult_right divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+
+lemma integrable_on_cdivide_iff [simp]:
+  fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
+  assumes "c \<noteq> 0"
+  shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
+by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+
 lemma has_integral_null [intro]:
   assumes "content(cbox a b) = 0"
   shows "(f has_integral 0) (cbox a b)"
@@ -6065,6 +6116,30 @@
   qed
 qed
 
+lemma ident_has_integral:
+  fixes a::real
+  assumes "a \<le> b"
+  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2) / 2) {a..b}"
+proof -
+  have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
+    apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
+    unfolding power2_eq_square
+    by (rule derivative_eq_intros | simp)+
+  then show ?thesis
+    by (simp add: field_simps)
+qed
+
+lemma integral_ident [simp]:
+  fixes a::real
+  assumes "a \<le> b"
+  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2) / 2 else 0)"
+using ident_has_integral integral_unique by fastforce
+
+lemma ident_integrable_on:
+  fixes a::real
+  shows "(\<lambda>x. x) integrable_on {a..b}"
+by (metis atLeastatMost_empty_iff integrable_on_def has_integral_empty ident_has_integral)
+
 
 subsection \<open>Taylor series expansion\<close>
 
@@ -6737,27 +6812,18 @@
 lemma content_image_affinity_cbox:
   "content((\<lambda>x::'a::euclidean_space. m *\<^sub>R x + c) ` cbox a b) =
     \<bar>m\<bar> ^ DIM('a) * content (cbox a b)" (is "?l = ?r")
-proof -
-  {
-    presume *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
-    show ?thesis
-      apply cases
-      apply (rule *)
-      apply assumption
-      unfolding not_not
-      using content_empty
-      apply auto
-      done
-  }
-  assume as: "cbox a b \<noteq> {}"
+proof (cases "cbox a b = {}")
+  case True then show ?thesis by simp
+next
+  case False
   show ?thesis
   proof (cases "m \<ge> 0")
     case True
-    with as have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \<noteq> {}"
+    with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \<noteq> {}"
       unfolding box_ne_empty
       apply (intro ballI)
       apply (erule_tac x=i in ballE)
-      apply (auto simp: inner_simps intro!: mult_left_mono)
+      apply (auto simp: inner_simps mult_left_mono)
       done
     moreover from True have *: "\<And>i. (m *\<^sub>R b + c) \<bullet> i - (m *\<^sub>R a + c) \<bullet> i = m *\<^sub>R (b - a) \<bullet> i"
       by (simp add: inner_simps field_simps)
@@ -6766,11 +6832,11 @@
         setprod.distrib setprod_constant inner_diff_left)
   next
     case False
-    with as have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
+    with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
       unfolding box_ne_empty
       apply (intro ballI)
       apply (erule_tac x=i in ballE)
-      apply (auto simp: inner_simps intro!: mult_left_mono)
+      apply (auto simp: inner_simps mult_left_mono)
       done
     moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b - a) \<bullet> i"
       by (simp add: inner_simps field_simps)
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -556,6 +556,190 @@
   by (rule ext) (auto simp: mult.commute)
 
 
+subsection\<open>Some reversed and "if and only if" versions of joining theorems\<close>
+
+lemma path_join_path_ends: 
+  fixes g1 :: "real \<Rightarrow> 'a::metric_space"
+  assumes "path(g1 +++ g2)" "path g2" 
+    shows "pathfinish g1 = pathstart g2"
+proof (rule ccontr)
+  def e \<equiv> "dist (g1 1) (g2 0)"
+  assume Neg: "pathfinish g1 \<noteq> pathstart g2"
+  then have "0 < dist (pathfinish g1) (pathstart g2)"
+    by auto
+  then have "e > 0"
+    by (metis e_def pathfinish_def pathstart_def) 
+  then obtain d1 where "d1 > 0" 
+       and d1: "\<And>x'. \<lbrakk>x'\<in>{0..1}; norm x' < d1\<rbrakk> \<Longrightarrow> dist (g2 x') (g2 0) < e/2"
+    using assms(2) unfolding path_def continuous_on_iff
+    apply (drule_tac x=0 in bspec, simp)
+    by (metis half_gt_zero_iff norm_conv_dist)
+  obtain d2 where "d2 > 0" 
+       and d2: "\<And>x'. \<lbrakk>x'\<in>{0..1}; dist x' (1/2) < d2\<rbrakk> 
+                      \<Longrightarrow> dist ((g1 +++ g2) x') (g1 1) < e/2"
+    using assms(1) \<open>e > 0\<close> unfolding path_def continuous_on_iff
+    apply (drule_tac x="1/2" in bspec, simp)
+    apply (drule_tac x="e/2" in spec)
+    apply (force simp: joinpaths_def)
+    done
+  have int01_1: "min (1/2) (min d1 d2) / 2 \<in> {0..1}"
+    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
+  have dist1: "norm (min (1 / 2) (min d1 d2) / 2) < d1"
+    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
+  have int01_2: "1/2 + min (1/2) (min d1 d2) / 4 \<in> {0..1}"
+    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
+  have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2"
+    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
+  have [simp]: "~ min (1 / 2) (min d1 d2) \<le> 0"
+    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
+  have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2"
+       "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2"
+    using d1 [OF int01_1 dist1] d2 [OF int01_2 dist2] by (simp_all add: joinpaths_def)
+  then have "dist (g1 1) (g2 0) < e/2 + e/2"
+    using dist_triangle_half_r e_def by blast
+  then show False 
+    by (simp add: e_def [symmetric])
+qed
+
+lemma path_join_eq [simp]:  
+  fixes g1 :: "real \<Rightarrow> 'a::metric_space"
+  assumes "path g1" "path g2"
+    shows "path(g1 +++ g2) \<longleftrightarrow> pathfinish g1 = pathstart g2"
+  using assms by (metis path_join_path_ends path_join_imp)
+
+lemma simple_path_joinE: 
+  assumes "simple_path(g1 +++ g2)" and "pathfinish g1 = pathstart g2"
+  obtains "arc g1" "arc g2" 
+          "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
+proof -
+  have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk> 
+               \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
+    using assms by (simp add: simple_path_def)
+  have "path g1" 
+    using assms path_join simple_path_imp_path by blast
+  moreover have "inj_on g1 {0..1}"
+  proof (clarsimp simp: inj_on_def)
+    fix x y
+    assume "g1 x = g1 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
+    then show "x = y"
+      using * [of "x/2" "y/2"] by (simp add: joinpaths_def split_ifs)
+  qed
+  ultimately have "arc g1"
+    using assms  by (simp add: arc_def)
+  have [simp]: "g2 0 = g1 1"
+    using assms by (metis pathfinish_def pathstart_def) 
+  have "path g2"
+    using assms path_join simple_path_imp_path by blast
+  moreover have "inj_on g2 {0..1}"
+  proof (clarsimp simp: inj_on_def)
+    fix x y
+    assume "g2 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
+    then show "x = y"
+      using * [of "(x + 1) / 2" "(y + 1) / 2"]
+      by (force simp: joinpaths_def split_ifs divide_simps)
+  qed
+  ultimately have "arc g2"
+    using assms  by (simp add: arc_def)
+  have "g2 y = g1 0 \<or> g2 y = g1 1" 
+       if "g1 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" for x y
+      using * [of "x / 2" "(y + 1) / 2"] that
+      by (auto simp: joinpaths_def split_ifs divide_simps)
+  then have "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
+    by (fastforce simp: pathstart_def pathfinish_def path_image_def)
+  with \<open>arc g1\<close> \<open>arc g2\<close> show ?thesis using that by blast
+qed
+
+lemma simple_path_join_loop_eq:
+  assumes "pathfinish g2 = pathstart g1" "pathfinish g1 = pathstart g2" 
+    shows "simple_path(g1 +++ g2) \<longleftrightarrow>
+             arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
+by (metis assms simple_path_joinE simple_path_join_loop)
+
+lemma arc_join_eq:
+  assumes "pathfinish g1 = pathstart g2" 
+    shows "arc(g1 +++ g2) \<longleftrightarrow>
+           arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}"
+           (is "?lhs = ?rhs")
+proof 
+  assume ?lhs
+  then have "simple_path(g1 +++ g2)" by (rule arc_imp_simple_path)
+  then have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk> 
+               \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
+    using assms by (simp add: simple_path_def)
+  have False if "g1 0 = g2 u" "0 \<le> u" "u \<le> 1" for u
+    using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \<open>?lhs\<close>]
+    by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps)
+  then have n1: "~ (pathstart g1 \<in> path_image g2)"
+    unfolding pathstart_def path_image_def
+    using atLeastAtMost_iff by blast
+  show ?rhs using \<open>?lhs\<close>
+    apply (rule simple_path_joinE [OF arc_imp_simple_path assms])
+    using n1 by force
+next
+  assume ?rhs then show ?lhs
+    using assms
+    by (fastforce simp: pathfinish_def pathstart_def intro!: arc_join)
+qed
+
+lemma arc_join_eq_alt: 
+        "pathfinish g1 = pathstart g2
+        \<Longrightarrow> (arc(g1 +++ g2) \<longleftrightarrow>
+             arc g1 \<and> arc g2 \<and>
+             path_image g1 \<inter> path_image g2 = {pathstart g2})"
+using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
+
+
+subsection\<open>The joining of paths is associative\<close>
+
+lemma path_assoc:
+    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
+     \<Longrightarrow> path(p +++ (q +++ r)) \<longleftrightarrow> path((p +++ q) +++ r)"
+by simp
+
+lemma simple_path_assoc: 
+  assumes "pathfinish p = pathstart q" "pathfinish q = pathstart r" 
+    shows "simple_path (p +++ (q +++ r)) \<longleftrightarrow> simple_path ((p +++ q) +++ r)"
+proof (cases "pathstart p = pathfinish r")
+  case True show ?thesis
+  proof
+    assume "simple_path (p +++ q +++ r)"
+    with assms True show "simple_path ((p +++ q) +++ r)"
+      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join 
+                    dest: arc_distinct_ends [of r])
+  next
+    assume 0: "simple_path ((p +++ q) +++ r)"
+    with assms True have q: "pathfinish r \<notin> path_image q"
+      using arc_distinct_ends  
+      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join)
+    have "pathstart r \<notin> path_image p"
+      using assms
+      by (metis 0 IntI arc_distinct_ends arc_join_eq_alt empty_iff insert_iff 
+              pathfinish_in_path_image pathfinish_join simple_path_joinE)
+    with assms 0 q True show "simple_path (p +++ q +++ r)"
+      by (auto simp: simple_path_join_loop_eq arc_join_eq path_image_join 
+               dest!: subsetD [OF _ IntI])
+  qed
+next
+  case False
+  { fix x :: 'a
+    assume a: "path_image p \<inter> path_image q \<subseteq> {pathstart q}"
+              "(path_image p \<union> path_image q) \<inter> path_image r \<subseteq> {pathstart r}"
+              "x \<in> path_image p" "x \<in> path_image r"
+    have "pathstart r \<in> path_image q"
+      by (metis assms(2) pathfinish_in_path_image)
+    with a have "x = pathstart q"
+      by blast
+  }
+  with False assms show ?thesis 
+    by (auto simp: simple_path_eq_arc simple_path_join_loop_eq arc_join_eq path_image_join)
+qed
+
+lemma arc_assoc: 
+     "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
+      \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
+by (simp add: arc_simple_path simple_path_assoc)
+
+
 section\<open>Choosing a subpath of an existing path\<close>
 
 definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
@@ -2526,6 +2710,58 @@
   apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
   by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
 
+subsection\<open>Condition for an open map's image to contain a ball\<close>
+
+lemma ball_subset_open_map_image:
+  fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
+  assumes contf: "continuous_on (closure S) f"
+      and oint: "open (f ` interior S)"
+      and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
+      and "bounded S" "a \<in> S" "0 < r"
+    shows "ball (f a) r \<subseteq> f ` S"
+proof (cases "f ` S = UNIV")
+  case True then show ?thesis by simp
+next
+  case False
+    obtain w where w: "w \<in> frontier (f ` S)"
+               and dw_le: "\<And>y. y \<in> frontier (f ` S) \<Longrightarrow> norm (f a - w) \<le> norm (f a - y)"
+      apply (rule distance_attains_inf [of "frontier(f ` S)" "f a"])
+      using \<open>a \<in> S\<close> by (auto simp: frontier_eq_empty dist_norm False)
+    then obtain \<xi> where \<xi>: "\<And>n. \<xi> n \<in> f ` S" and tendsw: "\<xi> \<longlonglongrightarrow> w"
+      by (metis Diff_iff frontier_def closure_sequential)
+    then have "\<And>n. \<exists>x \<in> S. \<xi> n = f x" by force
+    then obtain z where zs: "\<And>n. z n \<in> S" and fz: "\<And>n. \<xi> n = f (z n)"
+      by metis
+    then obtain y K where y: "y \<in> closure S" and "subseq K" and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
+      using \<open>bounded S\<close>
+      apply (simp add: compact_closure [symmetric] compact_def)
+      apply (drule_tac x=z in spec)
+      using closure_subset apply force
+      done
+    then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
+      by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
+    have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
+    have "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
+      using fz by auto
+    moreover then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
+      by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
+    ultimately have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
+    have rle: "r \<le> norm (f y - f a)"
+      apply (rule le_no)
+      using w wy oint
+      by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
+    have **: "(~(b \<inter> (- S) = {}) \<and> ~(b - (- S) = {}) \<Longrightarrow> (b \<inter> f \<noteq> {}))
+              \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow>
+              b \<subseteq> S" for b f and S :: "'b set" 
+      by blast
+    show ?thesis
+      apply (rule **)   (*such a horrible mess*)
+      apply (rule connected_Int_frontier [where t = "f`S", OF connected_ball])
+      using \<open>a \<in> S\<close> \<open>0 < r\<close> 
+      apply (auto simp: disjoint_iff_not_equal  dist_norm)
+      by (metis dw_le norm_minus_commute not_less order_trans rle wy)
+qed
+
 section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
 
 text\<open> We often just want to require that it fixes some subset, but to take in
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -859,6 +859,24 @@
 lemma cball_diff_eq_sphere: "cball a r - ball a r =  {x. dist x a = r}"
   by (auto simp: cball_def ball_def dist_commute)
 
+lemma image_add_ball [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "op + b ` ball a r = ball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma image_add_cball [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "op + b ` cball a r = cball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
 lemma open_ball [intro, simp]: "open (ball x e)"
 proof -
   have "open (dist x -` {..<e})"
@@ -2191,7 +2209,7 @@
 
 definition "frontier S = closure S - interior S"
 
-lemma frontier_closed: "closed (frontier S)"
+lemma frontier_closed [iff]: "closed (frontier S)"
   by (simp add: frontier_def closed_Diff)
 
 lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
@@ -2202,11 +2220,11 @@
   shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
   unfolding frontier_def closure_interior
   by (auto simp add: mem_interior subset_eq ball_def)
-
+                                               
 lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
   by (metis frontier_def closure_closed Diff_subset)
 
-lemma frontier_empty[simp]: "frontier {} = {}"
+lemma frontier_empty [simp]: "frontier {} = {}"
   by (simp add: frontier_def)
 
 lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
@@ -2221,7 +2239,7 @@
   then show ?thesis using frontier_subset_closed[of S] ..
 qed
 
-lemma frontier_complement  [simp]: "frontier (- S) = frontier S"
+lemma frontier_complement [simp]: "frontier (- S) = frontier S"
   by (auto simp add: frontier_def closure_complement interior_complement)
 
 lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
@@ -4465,6 +4483,11 @@
     by auto
 qed
 
+lemma compact_closure [simp]:
+  fixes S :: "'a::heine_borel set"
+  shows "compact(closure S) \<longleftrightarrow> bounded S"
+by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
+
 lemma compact_components:
   fixes s :: "'a::heine_borel set"
   shows "\<lbrakk>compact s; c \<in> components s\<rbrakk> \<Longrightarrow> compact c"
@@ -5541,10 +5564,6 @@
 
 subsubsection \<open>Structural rules for pointwise continuity\<close>
 
-lemmas continuous_within_id = continuous_ident
-
-lemmas continuous_at_id = continuous_ident
-
 lemma continuous_infdist[continuous_intros]:
   assumes "continuous F f"
   shows "continuous F (\<lambda>x. infdist (f x) A)"
@@ -5890,6 +5909,111 @@
   qed
 qed
 
+subsection\<open> Theorems relating continuity and uniform continuity to closures\<close>
+
+lemma continuous_on_closure:
+   "continuous_on (closure S) f \<longleftrightarrow>
+    (\<forall>x e. x \<in> closure S \<and> 0 < e
+           \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"
+   (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding continuous_on_iff  by (metis Un_iff closure_def)
+next
+  assume R [rule_format]: ?rhs
+  show ?lhs
+  proof
+    fix x and e::real
+    assume "0 < e" and x: "x \<in> closure S"
+    obtain \<delta>::real where "\<delta> > 0" 
+                   and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
+      using R [of x "e/2"] \<open>0 < e\<close> x by auto 
+    have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
+    proof -
+      obtain \<delta>'::real where "\<delta>' > 0" 
+                      and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
+        using R [of y "e/2"] \<open>0 < e\<close> y by auto 
+      obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
+        using closure_approachable y
+        by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
+      have "dist (f z) (f y) < e/2"
+        apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
+        using z \<open>0 < \<delta>'\<close> by linarith 
+      moreover have "dist (f z) (f x) < e/2"
+        apply (rule \<delta> [OF \<open>z \<in> S\<close>])
+        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto 
+      ultimately show ?thesis
+        by (metis dist_commute dist_triangle_half_l less_imp_le)
+    qed
+    then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
+      by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
+  qed
+qed
+
+lemma continuous_on_closure_sequentially:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"
+  shows
+   "continuous_on (closure S) f \<longleftrightarrow>
+    (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)"
+   (is "?lhs = ?rhs")
+proof -
+  have "continuous_on (closure S) f \<longleftrightarrow> 
+           (\<forall>x \<in> closure S. continuous (at x within S) f)"
+    by (force simp: continuous_on_closure Topology_Euclidean_Space.continuous_within_eps_delta)
+  also have "... = ?rhs"
+    by (force simp: continuous_within_sequentially)
+  finally show ?thesis .
+qed
+
+lemma uniformly_continuous_on_closure:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes ucont: "uniformly_continuous_on S f"
+      and cont: "continuous_on (closure S) f"
+    shows "uniformly_continuous_on (closure S) f"
+unfolding uniformly_continuous_on_def
+proof (intro allI impI)
+  fix e::real
+  assume "0 < e"
+  then obtain d::real 
+    where "d>0" 
+      and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3"
+    using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
+  show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
+  proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
+    fix x y
+    assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
+    obtain d1::real where "d1 > 0" 
+           and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
+      using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
+     obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
+        using closure_approachable [of x S] 
+        by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral) 
+    obtain d2::real where "d2 > 0" 
+           and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
+      using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
+     obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
+        using closure_approachable [of y S] 
+        by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
+     have "dist x' x < d/3" using x' by auto
+     moreover have "dist x y < d/3"
+       by (metis dist_commute dyx less_divide_eq_numeral1(1)) 
+     moreover have "dist y y' < d/3"
+       by (metis (no_types) dist_commute min_less_iff_conj y') 
+     ultimately have "dist x' y' < d/3 + d/3 + d/3"
+       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
+     then have "dist x' y' < d" by simp 
+     then have "dist (f x') (f y') < e/3" 
+       by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
+     moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
+       by (simp add: closure_def)
+     moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
+       by (simp add: closure_def)
+     ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
+       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
+    then show "dist (f y) (f x) < e" by simp
+  qed
+qed
+
 subsection \<open>A function constant on a set\<close>
 
 definition constant_on  (infixl "(constant'_on)" 50)
@@ -6047,7 +6171,7 @@
   {
     fix x
     have "continuous (at x) (\<lambda>x. x - a)"
-      by (intro continuous_diff continuous_at_id continuous_const)
+      by (intro continuous_diff continuous_ident continuous_const)
   }
   moreover have "{x. x - a \<in> s} = op + a ` s"
     by force
@@ -6385,7 +6509,7 @@
   have "?B \<noteq> {}" using \<open>b \<in> s\<close>
     by (auto simp: dist_commute)
   moreover have "continuous_on ?B (dist a)"
-    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const)
+    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
   moreover have "compact ?B"
     by (intro closed_inter_compact \<open>closed s\<close> compact_cball)
   ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
@@ -6828,7 +6952,7 @@
   then have "s \<noteq> {}" "t \<noteq> {}" by auto
   let ?inf = "\<lambda>x. infdist x t"
   have "continuous_on s ?inf"
-    by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_at_id)
+    by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)
   then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y"
     using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto
   then have "0 < ?inf x"
@@ -7134,7 +7258,7 @@
 lemma open_box[intro]: "open (box a b)"
 proof -
   have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
-    by (auto intro!: continuous_open_vimage continuous_inner continuous_at_id continuous_const)
+    by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
   also have "(\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
     by (auto simp add: box_def inner_commute)
   finally show ?thesis .
@@ -8344,7 +8468,7 @@
   let ?D = "(\<lambda>x. (x, x)) ` s"
   have D: "compact ?D" "?D \<noteq> {}"
     by (rule compact_continuous_image)
-       (auto intro!: s continuous_Pair continuous_within_id simp: continuous_on_eq_continuous_within)
+       (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)
 
   have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"
     using dist by fastforce
@@ -8353,7 +8477,7 @@
   then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
     unfolding continuous_on_eq_continuous_within
     by (intro continuous_dist ballI continuous_within_compose)
-       (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
+       (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)
 
   obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
     using continuous_attains_inf[OF D cont] by auto
@@ -8408,7 +8532,7 @@
 next
   assume ?rhs then show ?lhs
     apply (auto simp: ball_def dist_norm)
-    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans)
+    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans)
     done
 qed
 
@@ -8448,7 +8572,7 @@
 next
   assume ?rhs then show ?lhs
     apply (auto simp: ball_def dist_norm )
-    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans)
+    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans)
     done
 qed
 
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Probability/Regularity.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -249,7 +249,7 @@
         fix d
         have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
         also have "open \<dots>"
-          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
+          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident)
         finally have "open (?G d)" .
       } note open_G = this
       from in_closed_iff_infdist_zero[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>]
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -1050,15 +1050,14 @@
     using dist_triangle2 [of y x y] by simp
 qed
 
+lemma dist_commute_lessI: "dist y x < e \<Longrightarrow> dist x y < e"
+  by (simp add: dist_commute)
+
 lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
-using dist_triangle2 [of x z y] by (simp add: dist_commute)
+  using dist_triangle2 [of x z y] by (simp add: dist_commute)
 
 lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
-using dist_triangle2 [of x y a] by (simp add: dist_commute)
-
-lemma dist_triangle_alt:
-  shows "dist y z <= dist x y + dist x z"
-by (rule dist_triangle3)
+  using dist_triangle2 [of x y a] by (simp add: dist_commute)
 
 lemma dist_pos_lt:
   shows "x \<noteq> y ==> 0 < dist x y"
@@ -1337,6 +1336,11 @@
   assumes "linear D" obtains d where "D = (\<lambda>x. x *\<^sub>R d)"
   by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def)
 
+corollary real_linearD:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "linear f" obtains c where "f = op* c"
+by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
+
 lemma linearI:
   assumes "\<And>x y. f (x + y) = f x + f y"
   assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
diff -r edee1966fddf -r bc25f3916a99 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Mar 07 14:34:45 2016 +0000
@@ -399,7 +399,7 @@
 definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
   where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)"
 
-definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
+definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_)/ within (_)" [1000, 60] 60)
   where "at a within s = inf (nhds a) (principal (s - {a}))"
 
 abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where