# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1477406767 -3600
# Node ID 141e1ed8d5a011fe812bfb38cc88d96c0f4f398b
# Parent  ad2c5f37f6590e1d261d0ec32298af95500e8534
more new material

diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -2493,6 +2493,24 @@
 by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def
           rel_frontier_retract_of_punctured_affine_hull)
 
+lemma path_connected_sphere_gen:
+  assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
+  shows "path_connected(rel_frontier S)"
+proof (cases "rel_interior S = {}")
+  case True
+  then show ?thesis
+    by (simp add: \<open>convex S\<close> convex_imp_path_connected rel_frontier_def)
+next
+  case False
+  then show ?thesis
+    by (metis aff_dim_affine_hull affine_affine_hull affine_imp_convex all_not_in_conv assms path_connected_punctured_convex rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected)
+qed
+
+lemma connected_sphere_gen:
+  assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
+  shows "connected(rel_frontier S)"
+  by (simp add: assms path_connected_imp_connected path_connected_sphere_gen)
+
 subsection\<open>Borsuk-style characterization of separation\<close>
 
 lemma continuous_on_Borsuk_map:
@@ -4326,4 +4344,5 @@
   using connected_complement_homeomorphic_convex_compact [OF assms]
   using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
 
+
 end
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -605,7 +605,7 @@
 
 proposition valid_path_compose:
   assumes "valid_path g"
-      and der: "\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
+      and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)"
       and con: "continuous_on (path_image g) (deriv f)"
     shows "valid_path (f o g)"
 proof -
@@ -617,11 +617,8 @@
         by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
     next
       have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
-      then obtain f' where "(f has_field_derivative f') (at (g t))"
-        using der by auto
-      then have " (f has_derivative op * f') (at (g t))"
-        using has_field_derivative_imp_has_derivative[of f f' "at (g t)"] by auto
-      then show "f differentiable at (g t)" using differentiableI by auto
+      then show "f differentiable at (g t)" 
+        using der[THEN field_differentiable_imp_differentiable] by auto
     qed
   moreover have "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
     proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
@@ -642,24 +639,15 @@
           show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
         next
           have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
-          then obtain f' where "(f has_field_derivative f') (at (g t))"
-            using der by auto
-          then show "\<exists>g'. (f has_field_derivative g') (at (g t))" by auto
+          then show "f field_differentiable at (g t)" using der by auto
         qed
     qed
   ultimately have "f o g C1_differentiable_on {0..1} - s"
     using C1_differentiable_on_eq by blast
-  moreover have "path (f o g)"
-    proof -
-      have "isCont f x" when "x\<in>path_image g" for x
-        proof -
-          obtain f' where "(f has_field_derivative f') (at x)"
-            using der[rule_format] \<open>x\<in>path_image g\<close> by auto
-          thus ?thesis using DERIV_isCont by auto
-        qed
-      then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
-      then show ?thesis using path_continuous_image \<open>valid_path g\<close> valid_path_imp_path by auto
-    qed
+  moreover have "path (f \<circ> g)" 
+    apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
+    using der
+    by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
   ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
     using \<open>finite s\<close> by auto
 qed
@@ -5730,8 +5718,8 @@
   shows "valid_path (f o g)"
 proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
   fix x assume "x \<in> path_image g"
-  then show "\<exists>f'. (f has_field_derivative f') (at x)"
-    using holo holomorphic_on_open[OF \<open>open s\<close>] \<open>path_image g \<subseteq> s\<close> by auto
+  then show "f field_differentiable at x"
+    using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
 next
   have "deriv f holomorphic_on s"
     using holomorphic_deriv holo \<open>open s\<close> by auto
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -277,144 +277,7 @@
 
 subsection\<open>Holomorphic functions\<close>
 
-definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
-           (infixr "(field'_differentiable)" 50)
-  where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
-
-lemma field_differentiable_derivI:
-    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
-by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
-
-lemma field_differentiable_imp_continuous_at:
-    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
-  by (metis DERIV_continuous field_differentiable_def)
-
-lemma field_differentiable_within_subset:
-    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
-     \<Longrightarrow> f field_differentiable (at x within t)"
-  by (metis DERIV_subset field_differentiable_def)
-
-lemma field_differentiable_at_within:
-    "\<lbrakk>f field_differentiable (at x)\<rbrakk>
-     \<Longrightarrow> f field_differentiable (at x within s)"
-  unfolding field_differentiable_def
-  by (metis DERIV_subset top_greatest)
-
-lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
-proof -
-  show ?thesis
-    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
-    by (force intro: has_derivative_mult_right)
-qed
-
-lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
-  unfolding field_differentiable_def has_field_derivative_def
-  by (rule exI [where x=0])
-     (metis has_derivative_const lambda_zero)
-
-lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
-  unfolding field_differentiable_def has_field_derivative_def
-  by (rule exI [where x=1])
-     (simp add: lambda_one [symmetric])
-
-lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
-  unfolding id_def by (rule field_differentiable_ident)
-
-lemma field_differentiable_minus [derivative_intros]:
-  "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
-  unfolding field_differentiable_def
-  by (metis field_differentiable_minus)
-
-lemma field_differentiable_add [derivative_intros]:
-  assumes "f field_differentiable F" "g field_differentiable F"
-    shows "(\<lambda>z. f z + g z) field_differentiable F"
-  using assms unfolding field_differentiable_def
-  by (metis field_differentiable_add)
-
-lemma field_differentiable_add_const [simp,derivative_intros]:
-     "op + c field_differentiable F"
-  by (simp add: field_differentiable_add)
-
-lemma field_differentiable_sum [derivative_intros]:
-  "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
-  by (induct I rule: infinite_finite_induct)
-     (auto intro: field_differentiable_add field_differentiable_const)
-
-lemma field_differentiable_diff [derivative_intros]:
-  assumes "f field_differentiable F" "g field_differentiable F"
-    shows "(\<lambda>z. f z - g z) field_differentiable F"
-  using assms unfolding field_differentiable_def
-  by (metis field_differentiable_diff)
-
-lemma field_differentiable_inverse [derivative_intros]:
-  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
-  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
-  using assms unfolding field_differentiable_def
-  by (metis DERIV_inverse_fun)
-
-lemma field_differentiable_mult [derivative_intros]:
-  assumes "f field_differentiable (at a within s)"
-          "g field_differentiable (at a within s)"
-    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
-  using assms unfolding field_differentiable_def
-  by (metis DERIV_mult [of f _ a s g])
-
-lemma field_differentiable_divide [derivative_intros]:
-  assumes "f field_differentiable (at a within s)"
-          "g field_differentiable (at a within s)"
-          "g a \<noteq> 0"
-    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
-  using assms unfolding field_differentiable_def
-  by (metis DERIV_divide [of f _ a s g])
-
-lemma field_differentiable_power [derivative_intros]:
-  assumes "f field_differentiable (at a within s)"
-    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
-  using assms unfolding field_differentiable_def
-  by (metis DERIV_power)
-
-lemma field_differentiable_transform_within:
-  "0 < d \<Longrightarrow>
-        x \<in> s \<Longrightarrow>
-        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
-        f field_differentiable (at x within s)
-        \<Longrightarrow> g field_differentiable (at x within s)"
-  unfolding field_differentiable_def has_field_derivative_def
-  by (blast intro: has_derivative_transform_within)
-
-lemma field_differentiable_compose_within:
-  assumes "f field_differentiable (at a within s)"
-          "g field_differentiable (at (f a) within f`s)"
-    shows "(g o f) field_differentiable (at a within s)"
-  using assms unfolding field_differentiable_def
-  by (metis DERIV_image_chain)
-
-lemma field_differentiable_compose:
-  "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
-          \<Longrightarrow> (g o f) field_differentiable at z"
-by (metis field_differentiable_at_within field_differentiable_compose_within)
-
-lemma field_differentiable_within_open:
-     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
-                          f field_differentiable at a"
-  unfolding field_differentiable_def
-  by (metis at_within_open)
-
-subsection\<open>Caratheodory characterization\<close>
-
-lemma field_differentiable_caratheodory_at:
-  "f field_differentiable (at z) \<longleftrightarrow>
-         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
-  using CARAT_DERIV [of f]
-  by (simp add: field_differentiable_def has_field_derivative_def)
-
-lemma field_differentiable_caratheodory_within:
-  "f field_differentiable (at z within s) \<longleftrightarrow>
-         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
-  using DERIV_caratheodory_within [of f]
-  by (simp add: field_differentiable_def has_field_derivative_def)
-
-subsection\<open>Holomorphic\<close>
+subsection\<open>Holomorphic functions\<close>
 
 definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
            (infixl "(holomorphic'_on)" 50)
@@ -428,6 +291,11 @@
 lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x within s)"
   by (simp add: holomorphic_on_def)
 
+lemma holomorphic_on_imp_differentiable_on:
+    "f holomorphic_on s \<Longrightarrow> f differentiable_on s"
+  unfolding holomorphic_on_def differentiable_on_def
+  by (simp add: field_differentiable_imp_differentiable)
+
 lemma holomorphic_on_imp_differentiable_at:
    "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x)"
 using at_within_open holomorphic_on_def by fastforce
@@ -594,6 +462,20 @@
     apply (auto simp: holomorphic_derivI)
     done
 
+subsection\<open>Caratheodory characterization\<close>
+
+lemma field_differentiable_caratheodory_at:
+  "f field_differentiable (at z) \<longleftrightarrow>
+         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
+  using CARAT_DERIV [of f]
+  by (simp add: field_differentiable_def has_field_derivative_def)
+
+lemma field_differentiable_caratheodory_within:
+  "f field_differentiable (at z within s) \<longleftrightarrow>
+         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
+  using DERIV_caratheodory_within [of f]
+  by (simp add: field_differentiable_def has_field_derivative_def)
+
 subsection\<open>Analyticity on a set\<close>
 
 definition analytic_on (infixl "(analytic'_on)" 50)
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -693,8 +693,8 @@
     and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
   using Arg by auto
 
-lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(\<i> * of_real t))"
-  using Arg [of z] by auto
+lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
+  by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
 
 lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
   apply (rule Arg_unique_lemma [OF _ Arg_eq])
@@ -2300,7 +2300,7 @@
   by simp
 
 lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
-  by (simp add: complex_norm_eq_1_exp)
+  by simp
 
 lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
   unfolding Arctan_def divide_complex_def
@@ -3261,4 +3261,190 @@
   apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
   done
 
+subsection\<open> Formulation of loop homotopy in terms of maps out of type complex\<close>
+
+lemma homotopic_circlemaps_imp_homotopic_loops:
+  assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
+                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
+proof -
+  have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
+    using assms by (auto simp: sphere_def)
+  moreover have "continuous_on {0..1} (exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
+     by (intro continuous_intros)
+  moreover have "(exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>)) ` {0..1} \<subseteq> {z. cmod z = 1}"
+    by (auto simp: norm_mult)
+  ultimately
+  show ?thesis
+    apply (simp add: homotopic_loops_def comp_assoc)
+    apply (rule homotopic_with_compose_continuous_right)
+      apply (auto simp: pathstart_def pathfinish_def)
+    done
+qed
+
+lemma homotopic_loops_imp_homotopic_circlemaps:
+  assumes "homotopic_loops S p q"
+    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
+                          (p \<circ> (\<lambda>z. (Arg z / (2 * pi))))
+                          (q \<circ> (\<lambda>z. (Arg z / (2 * pi))))"
+proof -
+  obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
+             and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
+             and h0: "(\<forall>x. h (0, x) = p x)"
+             and h1: "(\<forall>x. h (1, x) = q x)"
+             and h01: "(\<forall>t\<in>{0..1}. h (t, 1) = h (t, 0)) "
+    using assms
+    by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
+  define j where "j \<equiv> \<lambda>z. if 0 \<le> Im (snd z)
+                          then h (fst z, Arg (snd z) / (2 * pi))
+                          else h (fst z, 1 - Arg (cnj (snd z)) / (2 * pi))"
+  have Arg_eq: "1 - Arg (cnj y) / (2 * pi) = Arg y / (2 * pi) \<or> Arg y = 0 \<and> Arg (cnj y) = 0" if "cmod y = 1" for y
+    using that Arg_eq_0_pi Arg_eq_pi by (force simp: Arg_cnj divide_simps)
+  show ?thesis
+  proof (simp add: homotopic_with; intro conjI ballI exI)
+    show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg (snd w) / (2 * pi)))"
+    proof (rule continuous_on_eq)
+      show j: "j x = h (fst x, Arg (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
+        using Arg_eq that h01 by (force simp: j_def)
+      have eq:  "S = S \<inter> (UNIV \<times> {z. 0 \<le> Im z}) \<union> S \<inter> (UNIV \<times> {z. Im z \<le> 0})" for S :: "(real*complex)set"
+        by auto
+      have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg (snd x) / (2 * pi)))"
+        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
+            apply (auto simp: Arg)
+        apply (meson Arg_lt_2pi linear not_le)
+        done
+      have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg (cnj (snd x)) / (2 * pi)))"
+        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
+            apply (auto simp: Arg)
+        apply (meson Arg_lt_2pi linear not_le)
+        done
+      show "continuous_on ({0..1} \<times> sphere 0 1) j"
+        apply (simp add: j_def)
+        apply (subst eq)
+        apply (rule continuous_on_cases_local)
+            apply (simp_all add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)
+        using Arg_eq h01
+        by force
+    qed
+    have "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
+      by (auto simp: Arg_ge_0 Arg_lt_2pi less_imp_le)
+    also have "... \<subseteq> S"
+      using him by blast
+    finally show "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
+  qed (auto simp: h0 h1)
+qed
+
+lemma simply_connected_homotopic_loops:
+  "simply_connected S \<longleftrightarrow>
+       (\<forall>p q. homotopic_loops S p p \<and> homotopic_loops S q q \<longrightarrow> homotopic_loops S p q)"
+unfolding simply_connected_def using homotopic_loops_refl by metis
+
+
+lemma simply_connected_eq_homotopic_circlemaps1:
+  fixes f :: "complex \<Rightarrow> 'a::topological_space" and g :: "complex \<Rightarrow> 'a"
+  assumes S: "simply_connected S"
+      and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
+      and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
+    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+proof -
+  have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * ii)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi *  t) * ii))"
+    apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
+    apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
+    done
+  then show ?thesis
+    apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps])
+      apply (auto simp: o_def complex_norm_eq_1_exp mult.commute)
+    done
+qed
+
+lemma simply_connected_eq_homotopic_circlemaps2a:
+  fixes h :: "complex \<Rightarrow> 'a::topological_space"
+  assumes conth: "continuous_on (sphere 0 1) h" and him: "h ` (sphere 0 1) \<subseteq> S"
+      and hom: "\<And>f g::complex \<Rightarrow> 'a.
+                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
+                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+            shows "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
+    apply (rule_tac x="h 1" in exI)
+    apply (rule hom)
+    using assms
+    by (auto simp: continuous_on_const)
+
+lemma simply_connected_eq_homotopic_circlemaps2b:
+  fixes S :: "'a::real_normed_vector set"
+  assumes "\<And>f g::complex \<Rightarrow> 'a.
+                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
+                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+  shows "path_connected S"
+proof (clarsimp simp add: path_connected_eq_homotopic_points)
+  fix a b
+  assume "a \<in> S" "b \<in> S"
+  then show "homotopic_loops S (linepath a a) (linepath b b)"
+    using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "\<lambda>x. a" "\<lambda>x. b"]]
+    by (auto simp: o_def continuous_on_const linepath_def)
+qed
+
+lemma simply_connected_eq_homotopic_circlemaps3:
+  fixes h :: "complex \<Rightarrow> 'a::real_normed_vector"
+  assumes "path_connected S"
+      and hom: "\<And>f::complex \<Rightarrow> 'a.
+                  \<lbrakk>continuous_on (sphere 0 1) f; f `(sphere 0 1) \<subseteq> S\<rbrakk>
+                  \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
+    shows "simply_connected S"
+proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms)
+  fix p
+  assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
+  then have "homotopic_loops S p p"
+    by (simp add: homotopic_loops_refl)
+  then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg z / (2 * pi))) (\<lambda>x. a)"
+    by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
+  show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
+  proof (intro exI conjI)
+    show "a \<in> S"
+      using homotopic_with_imp_subset2 [OF homp]
+      by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
+    have teq: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk>
+               \<Longrightarrow> t = Arg (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg (exp (2 * of_real pi * of_real t * \<i>)) = 0"
+      apply (rule disjCI)
+      using Arg_of_real [of 1] apply (auto simp: Arg_exp)
+      done
+    have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
+      apply (rule homotopic_loops_eq [OF p])
+      using p teq apply (fastforce simp: pathfinish_def pathstart_def)
+      done
+    then
+    show "homotopic_loops S p (linepath a a)"
+      by (simp add: linepath_refl  homotopic_loops_trans [OF _ homotopic_circlemaps_imp_homotopic_loops [OF homp, simplified K_record_comp]])
+  qed
+qed
+
+
+proposition simply_connected_eq_homotopic_circlemaps:
+  fixes S :: "'a::real_normed_vector set"
+  shows "simply_connected S \<longleftrightarrow>
+         (\<forall>f g::complex \<Rightarrow> 'a.
+              continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
+              continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
+              \<longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g)"
+  apply (rule iffI)
+   apply (blast elim: dest: simply_connected_eq_homotopic_circlemaps1)
+  by (simp add: simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
+
+proposition simply_connected_eq_contractible_circlemap:
+  fixes S :: "'a::real_normed_vector set"
+  shows "simply_connected S \<longleftrightarrow>
+         path_connected S \<and>
+         (\<forall>f::complex \<Rightarrow> 'a.
+              continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
+              \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
+  apply (rule iffI)
+   apply (simp add: simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b)
+  using simply_connected_eq_homotopic_circlemaps3 by blast
+
+corollary homotopy_eqv_simple_connectedness:
+  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+  shows "S homotopy_eqv T \<Longrightarrow> simply_connected S \<longleftrightarrow> simply_connected T"
+  by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality)
+
 end
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -3590,8 +3590,9 @@
             using contra_subsetD path_image_def path_fg t_def that by fastforce
           ultimately have "(h has_field_derivative der t) (at t)"
             unfolding h_def der_def using g_holo f_holo \<open>open s\<close>
-            by (auto intro!: holomorphic_derivI derivative_eq_intros )
-          then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto
+            by (auto intro!: holomorphic_derivI derivative_eq_intros)
+          then show "h field_differentiable at (\<gamma> x)" 
+            unfolding t_def field_differentiable_def by blast
         qed
       then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>)
           = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -3115,6 +3115,9 @@
 lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
   unfolding affine_def convex_def by auto
 
+lemma convex_affine_hull [simp]: "convex (affine hull S)"
+  by (simp add: affine_imp_convex)
+
 lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
   using subspace_imp_affine affine_imp_convex by auto
 
@@ -7662,6 +7665,12 @@
   using segment_degen_1 [of "1-u" b a]
   by (auto simp: algebra_simps)
 
+lemma add_scaleR_degen:
+  fixes a b ::"'a::real_vector"
+  assumes  "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)"  "u \<noteq> v"
+  shows "a=b"
+  by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
+  
 lemma closed_segment_image_interval:
      "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
   by (auto simp: set_eq_iff image_iff closed_segment_def)
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -359,6 +359,23 @@
   using has_derivative_compose[of f f' x UNIV g g']
   by (simp add: comp_def)
 
+lemma field_vector_diff_chain_within:
+ assumes Df: "(f has_vector_derivative f') (at x within s)"
+     and Dg: "(g has_field_derivative g') (at (f x) within f`s)"
+ shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within s)"
+using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
+                       Dg [unfolded has_field_derivative_def]]
+ by (auto simp: o_def mult.commute has_vector_derivative_def)
+
+lemma vector_derivative_diff_chain_within:
+  assumes Df: "(f has_vector_derivative f') (at x within s)"
+     and Dg: "(g has_derivative g') (at (f x) within f`s)"
+  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within s)"
+using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
+  linear.scaleR[OF has_derivative_linear[OF Dg]]
+  unfolding has_vector_derivative_def o_def
+  by (auto simp: o_def mult.commute has_vector_derivative_def)
+
 
 subsection \<open>Composition rules stated just for differentiability\<close>
 
@@ -2563,13 +2580,149 @@
                        Dg [unfolded has_field_derivative_def]]
  by (auto simp: o_def mult.commute has_vector_derivative_def)
 
-lemma vector_derivative_chain_at_general:  (*thanks to Wenda Li*)
- assumes "f differentiable at x" "(\<exists>g'. (g has_field_derivative g') (at (f x)))"
- shows "vector_derivative (g \<circ> f) (at x) =
-        vector_derivative f (at x) * deriv g (f x)"
-apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
-using assms
-by (auto simp: vector_derivative_works DERIV_deriv_iff_has_field_derivative)
+lemma vector_derivative_chain_within: 
+  assumes "at x within s \<noteq> bot" "f differentiable (at x within s)" 
+    "(g has_derivative g') (at (f x) within f ` s)" 
+  shows "vector_derivative (g \<circ> f) (at x within s) =
+        g' (vector_derivative f (at x within s)) "
+  apply (rule vector_derivative_within [OF \<open>at x within s \<noteq> bot\<close>])
+  apply (rule vector_derivative_diff_chain_within)
+  using assms(2-3) vector_derivative_works
+  by auto
+
+subsection\<open>The notion of being field differentiable\<close>
+
+definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
+           (infixr "(field'_differentiable)" 50)
+  where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
+
+lemma field_differentiable_imp_differentiable:
+  "f field_differentiable F \<Longrightarrow> f differentiable F"
+  unfolding field_differentiable_def differentiable_def 
+  using has_field_derivative_imp_has_derivative by auto
+
+lemma field_differentiable_derivI:
+    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
+by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
+
+lemma field_differentiable_imp_continuous_at:
+    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+  by (metis DERIV_continuous field_differentiable_def)
+
+lemma field_differentiable_within_subset:
+    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
+     \<Longrightarrow> f field_differentiable (at x within t)"
+  by (metis DERIV_subset field_differentiable_def)
+
+lemma field_differentiable_at_within:
+    "\<lbrakk>f field_differentiable (at x)\<rbrakk>
+     \<Longrightarrow> f field_differentiable (at x within s)"
+  unfolding field_differentiable_def
+  by (metis DERIV_subset top_greatest)
+
+lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
+proof -
+  show ?thesis
+    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
+    by (force intro: has_derivative_mult_right)
+qed
+
+lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
+  unfolding field_differentiable_def has_field_derivative_def
+  using DERIV_const has_field_derivative_imp_has_derivative by blast
+
+lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
+  unfolding field_differentiable_def has_field_derivative_def
+  using DERIV_ident has_field_derivative_def by blast
+
+lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
+  unfolding id_def by (rule field_differentiable_ident)
+
+lemma field_differentiable_minus [derivative_intros]:
+  "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
+  unfolding field_differentiable_def
+  by (metis field_differentiable_minus)
+
+lemma field_differentiable_add [derivative_intros]:
+  assumes "f field_differentiable F" "g field_differentiable F"
+    shows "(\<lambda>z. f z + g z) field_differentiable F"
+  using assms unfolding field_differentiable_def
+  by (metis field_differentiable_add)
+
+lemma field_differentiable_add_const [simp,derivative_intros]:
+     "op + c field_differentiable F"
+  by (simp add: field_differentiable_add)
+
+lemma field_differentiable_sum [derivative_intros]:
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
+  by (induct I rule: infinite_finite_induct)
+     (auto intro: field_differentiable_add field_differentiable_const)
+
+lemma field_differentiable_diff [derivative_intros]:
+  assumes "f field_differentiable F" "g field_differentiable F"
+    shows "(\<lambda>z. f z - g z) field_differentiable F"
+  using assms unfolding field_differentiable_def
+  by (metis field_differentiable_diff)
+
+lemma field_differentiable_inverse [derivative_intros]:
+  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
+  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
+  by (metis DERIV_inverse_fun)
+
+lemma field_differentiable_mult [derivative_intros]:
+  assumes "f field_differentiable (at a within s)"
+          "g field_differentiable (at a within s)"
+    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
+  by (metis DERIV_mult [of f _ a s g])
+
+lemma field_differentiable_divide [derivative_intros]:
+  assumes "f field_differentiable (at a within s)"
+          "g field_differentiable (at a within s)"
+          "g a \<noteq> 0"
+    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
+  by (metis DERIV_divide [of f _ a s g])
+
+lemma field_differentiable_power [derivative_intros]:
+  assumes "f field_differentiable (at a within s)"
+    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
+  by (metis DERIV_power)
+
+lemma field_differentiable_transform_within:
+  "0 < d \<Longrightarrow>
+        x \<in> s \<Longrightarrow>
+        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
+        f field_differentiable (at x within s)
+        \<Longrightarrow> g field_differentiable (at x within s)"
+  unfolding field_differentiable_def has_field_derivative_def
+  by (blast intro: has_derivative_transform_within)
+
+lemma field_differentiable_compose_within:
+  assumes "f field_differentiable (at a within s)"
+          "g field_differentiable (at (f a) within f`s)"
+    shows "(g o f) field_differentiable (at a within s)"
+  using assms unfolding field_differentiable_def
+  by (metis DERIV_image_chain)
+
+lemma field_differentiable_compose:
+  "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
+          \<Longrightarrow> (g o f) field_differentiable at z"
+by (metis field_differentiable_at_within field_differentiable_compose_within)
+
+lemma field_differentiable_within_open:
+     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
+                          f field_differentiable at a"
+  unfolding field_differentiable_def
+  by (metis at_within_open)
+
+lemma vector_derivative_chain_at_general: 
+  assumes "f differentiable at x" "g field_differentiable at (f x)"
+  shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
+  apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
+  using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
 
 lemma exp_scaleR_has_vector_derivative_right:
   "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)"
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -3094,4 +3094,83 @@
   qed
 qed
 
+subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
+
+lemma homeomorphic_subspaces_eq:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "subspace S" "subspace T"
+  shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
+proof
+  assume "S homeomorphic T"
+  then obtain f g where hom: "homeomorphism S T f g"
+    using homeomorphic_def by blast
+  show "dim S = dim T"
+  proof (rule order_antisym)
+    show "dim S \<le> dim T"
+      by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le)
+    show "dim T \<le> dim S"
+      by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le)
+  qed
+next
+  assume "dim S = dim T"
+  then show "S homeomorphic T"
+    by (simp add: assms homeomorphic_subspaces)
+qed
+
+lemma homeomorphic_affine_sets_eq:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "affine S" "affine T"
+  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
+proof (cases "S = {} \<or> T = {}")
+  case True
+  then show ?thesis
+    using assms homeomorphic_affine_sets by force
+next
+  case False
+  then obtain a b where "a \<in> S" "b \<in> T"
+    by blast
+  then have "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
+    using affine_diffs_subspace assms by blast+
+  then show ?thesis
+    by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
+qed
+
+
+lemma homeomorphic_hyperplanes_eq:
+  fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
+  assumes "a \<noteq> 0" "c \<noteq> 0"
+  shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
+  apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
+  by (metis DIM_positive Suc_pred)
+
+lemma homeomorphic_UNIV_UNIV:
+  shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
+    DIM('a::euclidean_space) = DIM('b::euclidean_space)"
+  by (simp add: homeomorphic_subspaces_eq)
+
+lemma simply_connected_sphere_gen:
+   assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
+   shows "simply_connected(rel_frontier S)"
+proof -
+  have pa: "path_connected (rel_frontier S)"
+    using assms by (simp add: path_connected_sphere_gen)
+  show ?thesis
+  proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa)
+    fix f
+    assume f: "continuous_on (sphere (0::complex) 1) f" "f ` sphere 0 1 \<subseteq> rel_frontier S"
+    have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)"
+      by simp
+    have "convex (cball (0::complex) 1)"
+      by (rule convex_cball)
+    then obtain c where "homotopic_with (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
+      apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \<open>convex S\<close> \<open>bounded S\<close>, where f=f])
+      using f 3
+         apply (auto simp: aff_dim_cball)
+      done
+    then show "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
+      by blast
+  qed
+qed
+
+
 end
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -129,6 +129,68 @@
     by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
 qed
 
+proposition rel_frontier_not_sing:
+  fixes a :: "'a::euclidean_space"
+  assumes "bounded S"
+    shows "rel_frontier S \<noteq> {a}"
+proof (cases "S = {}")
+  case True  then show ?thesis  by simp
+next
+  case False
+  then obtain z where "z \<in> S"
+    by blast
+  then show ?thesis
+  proof (cases "S = {z}")
+    case True then show ?thesis  by simp
+  next
+    case False
+    then obtain w where "w \<in> S" "w \<noteq> z"
+      using \<open>z \<in> S\<close> by blast
+    show ?thesis
+    proof
+      assume "rel_frontier S = {a}"
+      then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
+        using \<open>w \<noteq> z\<close> by auto
+      then show False
+      proof cases
+        case 1
+        then have w: "w \<in> rel_interior S"
+          using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
+        have "w + (w - z) \<in> affine hull S"
+          by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+        then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
+          using \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
+        moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
+          using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"]  \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close>
+          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+        ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
+          using \<open>rel_frontier S = {a}\<close> by force
+        moreover have "e \<noteq> -d "
+          using \<open>0 < e\<close> \<open>0 < d\<close> by force
+        ultimately show False
+          by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+      next
+        case 2
+        then have z: "z \<in> rel_interior S"
+          using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
+        have "z + (z - w) \<in> affine hull S"
+          by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+        then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
+          using \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
+        moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
+          using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"]  \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close>
+          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+        ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
+          using \<open>rel_frontier S = {a}\<close> by force
+        moreover have "e \<noteq> -d "
+          using \<open>0 < e\<close> \<open>0 < d\<close> by force
+        ultimately show False
+          by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+      qed
+    qed
+  qed
+qed
+
 proposition
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and 0: "0 \<in> rel_interior S"
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -1205,6 +1205,9 @@
 lemma linepath_trivial [simp]: "linepath a a x = a"
   by (simp add: linepath_def real_vector.scale_left_diff_distrib)
 
+lemma linepath_refl: "linepath a a = (\<lambda>x. a)"
+  by auto
+
 lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
   by (simp add: subpath_def linepath_def algebra_simps)
 
@@ -4362,6 +4365,7 @@
     by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
 qed
 
+
 subsection\<open>Contractible sets\<close>
 
 definition contractible where
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -8985,6 +8985,18 @@
     done
 qed
 
+lemma homeomorphic_spheres:
+  fixes a b ::"'a::real_normed_vector"
+  assumes "0 < d"  "0 < e"
+  shows "(sphere a d) homeomorphic (sphere b e)"
+unfolding homeomorphic_minimal
+    apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
+    apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
+    using assms
+    apply (auto intro!: continuous_intros
+      simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
+    done
+
 subsection\<open>Inverse function property for open/closed maps\<close>
 
 lemma continuous_on_inverse_open_map:
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Limits.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -1367,7 +1367,7 @@
 
 lemma tendsto_mult_filterlim_at_infinity:
   fixes c :: "'a::real_normed_field"
-  assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
+  assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
   assumes "filterlim g at_infinity F"
   shows "filterlim (\<lambda>x. f x * g x) at_infinity F"
 proof -
@@ -1379,7 +1379,7 @@
     by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
   then show ?thesis
     by (subst filterlim_inverse_at_iff[symmetric]) simp_all
-qed
+qed  
 
 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
  by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
diff -r ad2c5f37f659 -r 141e1ed8d5a0 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Oct 25 15:46:07 2016 +0100
@@ -855,14 +855,21 @@
 
 lemma tendsto_imp_eventually_ne:
   fixes c :: "'a::t1_space"
-  assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
+  assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
   shows "eventually (\<lambda>z. f z \<noteq> c') F"
-proof (rule ccontr)
-  assume "\<not> eventually (\<lambda>z. f z \<noteq> c') F"
-  then have "frequently (\<lambda>z. f z = c') F"
-    by (simp add: frequently_def)
-  from limit_frequently_eq[OF assms(1) this assms(2)] and assms(3) show False
-    by contradiction
+proof (cases "F=bot")
+  case True
+  thus ?thesis by auto
+next
+  case False
+  show ?thesis
+  proof (rule ccontr)
+    assume "\<not> eventually (\<lambda>z. f z \<noteq> c') F"
+    then have "frequently (\<lambda>z. f z = c') F"
+      by (simp add: frequently_def)
+    from limit_frequently_eq[OF False this \<open>(f \<longlongrightarrow> c) F\<close>] and \<open>c \<noteq> c'\<close> show False
+      by contradiction
+  qed
 qed
 
 lemma tendsto_le: