# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1457971082 0
# Node ID d21dab28b3f9f6597c6c5cce1398dc778a094dfc
# Parent  7f17ebd3293ec3a08f38502ec79e111172073313
New results about paths, segments, etc. The notion of simply_connected.

diff -r 7f17ebd3293e -r d21dab28b3f9 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Complex.thy	Mon Mar 14 15:58:02 2016 +0000
@@ -673,9 +673,10 @@
 
 subsection\<open>Polar Form for Complex Numbers\<close>
 
-lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
-  using sincos_total_2pi [of "Re z" "Im z"]
-  by auto (metis cmod_power2 complex_eq power_one)
+lemma complex_unimodular_polar:
+  assumes "(norm z = 1)"
+  obtains t where "0 \<le> t" "t < 2*pi" "z = Complex (cos t) (sin t)"
+by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms)
 
 subsubsection \<open>$\cos \theta + i \sin \theta$\<close>
 
diff -r 7f17ebd3293e -r d21dab28b3f9 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 14 15:58:02 2016 +0000
@@ -6,6 +6,38 @@
 imports Complex_Transcendental Weierstrass Ordered_Euclidean_Space
 begin
 
+subsection\<open>Homeomorphisms of arc images\<close>
+
+lemma homeomorphism_arc:
+  fixes g :: "real \<Rightarrow> 'a::t2_space"
+  assumes "arc g"
+  obtains h where "homeomorphism {0..1} (path_image g) g h"
+using assms by (force simp add: arc_def homeomorphism_compact path_def path_image_def)
+
+lemma homeomorphic_arc_image_interval:
+  fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
+  assumes "arc g" "a < b"
+  shows "(path_image g) homeomorphic {a..b}"
+proof -
+  have "(path_image g) homeomorphic {0..1::real}"
+    by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
+  also have "... homeomorphic {a..b}"
+    using assms by (force intro: homeomorphic_closed_intervals_real)
+  finally show ?thesis .
+qed
+
+lemma homeomorphic_arc_images:
+  fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
+  assumes "arc g" "arc h"
+  shows "(path_image g) homeomorphic (path_image h)"
+proof -
+  have "(path_image g) homeomorphic {0..1::real}"
+    by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
+  also have "... homeomorphic (path_image h)"
+    by (meson assms homeomorphic_def homeomorphism_arc)
+  finally show ?thesis .
+qed
+
 subsection \<open>Piecewise differentiable functions\<close>
 
 definition piecewise_differentiable_on
diff -r 7f17ebd3293e -r d21dab28b3f9 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 14 15:58:02 2016 +0000
@@ -3661,6 +3661,14 @@
   then show ?thesis using * by auto
 qed
 
+lemma rel_interior_eq:
+   "rel_interior s = s \<longleftrightarrow> openin(subtopology euclidean (affine hull s)) s"
+using rel_open rel_open_def by blast
+
+lemma rel_interior_openin:
+   "openin(subtopology euclidean (affine hull s)) s \<Longrightarrow> rel_interior s = s"
+by (simp add: rel_interior_eq)
+
 
 subsubsection\<open>Relative interior preserves under linear transformations\<close>
 
@@ -6678,6 +6686,226 @@
     by (auto intro: rel_interior_closure_convex_shrink)
 qed
 
+subsection\<open>More results about segments\<close>
+
+lemma dist_half_times2:
+  fixes a :: "'a :: real_normed_vector"
+  shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
+proof -
+  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
+    by simp
+  also have "... = norm ((a + b) - 2 *\<^sub>R x)"
+    by (simp add: real_vector.scale_right_diff_distrib)
+  finally show ?thesis
+    by (simp only: dist_norm)
+qed
+
+lemma closed_segment_as_ball:
+    "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+  case True then show ?thesis by (auto simp: hull_inc)
+next
+  case False
+  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
+  proof -
+    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
+          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
+      unfolding eq_diff_eq [symmetric] by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
+      by (simp add: dist_half_times2) (simp add: dist_norm)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
+      by auto
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
+      by (simp add: algebra_simps scaleR_2)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
+      by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
+      by (simp add: mult_le_cancel_right2 False)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
+      by auto
+    finally show ?thesis .
+  qed
+  show ?thesis
+    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
+qed
+
+lemma open_segment_as_ball:
+    "open_segment a b =
+     affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
+proof (cases "b = a")
+  case True then show ?thesis by (auto simp: hull_inc)
+next
+  case False
+  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
+  proof -
+    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
+          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
+                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
+      unfolding eq_diff_eq [symmetric] by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
+      by (simp add: dist_half_times2) (simp add: dist_norm)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
+      by auto
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
+      by (simp add: algebra_simps scaleR_2)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
+                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
+      by simp
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
+      by (simp add: mult_le_cancel_right2 False)
+    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
+      by auto
+    finally show ?thesis .
+  qed
+  show ?thesis
+    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
+qed
+
+lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
+
+lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
+  by auto
+
+lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
+proof -
+  { assume a1: "open_segment a b = {}"
+    have "{} \<noteq> {0::real<..<1}"
+      by simp
+    then have "a = b"
+      using a1 open_segment_image_interval by fastforce
+  } then show ?thesis by auto
+qed
+
+lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
+  using open_segment_eq_empty by blast
+
+lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
+
+lemma inj_segment:
+  fixes a :: "'a :: real_vector"
+  assumes "a \<noteq> b"
+    shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
+proof
+  fix x y
+  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
+  then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
+    by (simp add: algebra_simps)
+  with assms show "x = y"
+    by (simp add: real_vector.scale_right_imp_eq)
+qed
+
+lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
+  apply auto
+  apply (rule ccontr)
+  apply (simp add: segment_image_interval)
+  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
+  done
+
+lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
+  by (auto simp: open_segment_def)
+
+lemmas finite_segment = finite_closed_segment finite_open_segment
+
+lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
+  by auto
+
+lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
+  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
+
+lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
+
+lemma subset_closed_segment:
+    "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+     a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
+
+lemma subset_co_segment:
+    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+     a \<in> open_segment c d \<and> b \<in> open_segment c d"
+using closed_segment_subset by blast
+
+lemma subset_open_segment:
+  fixes a :: "'a::euclidean_space"
+  shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
+         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+        (is "?lhs = ?rhs")
+proof (cases "a = b")
+  case True then show ?thesis by simp
+next
+  case False show ?thesis
+  proof
+    assume rhs: ?rhs
+    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+      using closed_segment_idem singleton_iff by auto
+    have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
+               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
+        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
+           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
+           and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
+        for u ua ub
+    proof -
+      have "ua \<noteq> ub"
+        using neq by auto
+      moreover have "(u - 1) * ua \<le> 0" using u uab
+        by (simp add: mult_nonpos_nonneg)
+      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
+        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
+      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
+      proof -
+        have "\<not> p \<le> 0" "\<not> q \<le> 0"
+          using p q not_less by blast+
+        then show ?thesis
+          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
+                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
+      qed
+      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
+        by (metis diff_add_cancel diff_gt_0_iff_gt)
+      with lt show ?thesis
+        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
+    qed
+    with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
+      unfolding open_segment_image_interval closed_segment_def
+      by (fastforce simp add:)
+  next
+    assume lhs: ?lhs
+    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
+      by (meson finite_open_segment rev_finite_subset)
+    have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
+      using lhs closure_mono by blast
+    then have "closed_segment a b \<subseteq> closed_segment c d"
+      by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
+    then show ?rhs
+      by (force simp: \<open>a \<noteq> b\<close>)
+  qed
+qed
+
+lemma subset_oc_segment:
+  fixes a :: "'a::euclidean_space"
+  shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
+         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
+apply (simp add: subset_open_segment [symmetric])
+apply (rule iffI)
+ apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
+apply (meson dual_order.trans segment_open_subset_closed)
+done
+
+lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
+
+
 subsection\<open>Betweenness\<close>
 
 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
@@ -7647,6 +7875,35 @@
   shows "A \<inter> closure S = {} \<longleftrightarrow> A \<inter> rel_interior S = {}"
   by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty)
 
+lemma rel_interior_open_segment:
+  fixes a :: "'a :: euclidean_space"
+  shows "rel_interior(open_segment a b) = open_segment a b"
+proof (cases "a = b")
+  case True then show ?thesis by auto
+next
+  case False then show ?thesis
+    apply (simp add: rel_interior_eq openin_open)
+    apply (rule_tac x="ball (inverse 2 *\<^sub>R (a + b)) (norm(b - a) / 2)" in exI)
+    apply (simp add: open_segment_as_ball)
+    done
+qed
+
+lemma rel_interior_closed_segment:
+  fixes a :: "'a :: euclidean_space"
+  shows "rel_interior(closed_segment a b) =
+         (if a = b then {a} else open_segment a b)"
+proof (cases "a = b")
+  case True then show ?thesis by auto
+next
+  case False then show ?thesis
+    by simp
+       (metis closure_open_segment convex_open_segment convex_rel_interior_closure
+              rel_interior_open_segment)
+qed
+
+lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
+
+
 definition "rel_frontier S = closure S - rel_interior S"
 
 lemma closed_affine_hull:
@@ -8037,7 +8294,6 @@
   then show ?thesis by auto
 qed
 
-
 lemma convex_closure_inter:
   assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
     and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
@@ -8172,6 +8428,19 @@
     using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
 qed
 
+lemma connected_component_1_gen:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "DIM('a) = 1"
+  shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
+unfolding connected_component_def
+by (metis (no_types, lifting) assms subsetD subsetI convex_contains_segment convex_segment(1)
+            ends_in_segment connected_convex_1_gen)
+
+lemma connected_component_1:
+  fixes S :: "real set"
+  shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
+by (simp add: connected_component_1_gen)
+
 lemma convex_affine_rel_interior_inter:
   fixes S T :: "'n::euclidean_space set"
   assumes "convex S"
@@ -9448,6 +9717,126 @@
     done
 qed
 
+lemma interior_closed_segment_ge2:
+  fixes a :: "'a::euclidean_space"
+  assumes "2 \<le> DIM('a)"
+    shows  "interior(closed_segment a b) = {}"
+using assms unfolding segment_convex_hull
+proof -
+  have "card {a, b} \<le> DIM('a)"
+    using assms
+    by (simp add: card_insert_if linear not_less_eq_eq numeral_2_eq_2)
+  then show "interior (convex hull {a, b}) = {}"
+    by (metis empty_interior_convex_hull finite.insertI finite.emptyI)
+qed
+
+lemma interior_open_segment:
+  fixes a :: "'a::euclidean_space"
+  shows  "interior(open_segment a b) =
+                 (if 2 \<le> DIM('a) then {} else open_segment a b)"
+proof (simp add: not_le, intro conjI impI)
+  assume "2 \<le> DIM('a)"
+  then show "interior (open_segment a b) = {}"
+    apply (simp add: segment_convex_hull open_segment_def)
+    apply (metis Diff_subset interior_mono segment_convex_hull subset_empty interior_closed_segment_ge2)
+    done
+next
+  assume le2: "DIM('a) < 2"
+  show "interior (open_segment a b) = open_segment a b"
+  proof (cases "a = b")
+    case True then show ?thesis by auto
+  next
+    case False
+    with le2 have "affine hull (open_segment a b) = UNIV"
+      apply simp
+      apply (rule affine_independent_span_gt)
+      apply (simp_all add: affine_dependent_def insert_Diff_if)
+      done
+    then show "interior (open_segment a b) = open_segment a b"
+      using rel_interior_interior rel_interior_open_segment by blast
+  qed
+qed
+
+lemma interior_closed_segment:
+  fixes a :: "'a::euclidean_space"
+  shows "interior(closed_segment a b) =
+                 (if 2 \<le> DIM('a) then {} else open_segment a b)"
+proof (cases "a = b")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "closure (open_segment a b) = closed_segment a b"
+    by simp
+  then show ?thesis
+    by (metis (no_types) convex_interior_closure convex_open_segment interior_open_segment)
+qed
+
+lemmas interior_segment = interior_closed_segment interior_open_segment
+
+lemma closed_segment_eq [simp]:
+  fixes a :: "'a::euclidean_space"
+  shows "closed_segment a b = closed_segment c d \<longleftrightarrow> {a,b} = {c,d}"
+proof
+  assume abcd: "closed_segment a b = closed_segment c d"
+  show "{a,b} = {c,d}"
+  proof (cases "a=b \<or> c=d")
+    case True with abcd show ?thesis by force
+  next
+    case False
+    then have neq: "a \<noteq> b \<and> c \<noteq> d" by force
+    have *: "closed_segment c d - {a, b} = rel_interior (closed_segment c d)"
+      using neq abcd by (metis (no_types) open_segment_def rel_interior_closed_segment)
+    have "b \<in> {c, d}"
+    proof -
+      have "insert b (closed_segment c d) = closed_segment c d"
+        using abcd by blast
+      then show ?thesis
+        by (metis DiffD2 Diff_insert2 False * insertI1 insert_Diff_if open_segment_def rel_interior_closed_segment)
+    qed
+    moreover have "a \<in> {c, d}"
+      by (metis Diff_iff False * abcd ends_in_segment(1) insertI1 open_segment_def rel_interior_closed_segment)
+    ultimately show "{a, b} = {c, d}"
+      using neq by fastforce
+  qed
+next
+  assume "{a,b} = {c,d}"
+  then show "closed_segment a b = closed_segment c d"
+    by (simp add: segment_convex_hull)
+qed
+
+lemma closed_open_segment_eq [simp]:
+  fixes a :: "'a::euclidean_space"
+  shows "closed_segment a b \<noteq> open_segment c d"
+by (metis DiffE closed_segment_neq_empty closure_closed_segment closure_open_segment ends_in_segment(1) insertI1 open_segment_def)
+
+lemma open_closed_segment_eq [simp]:
+  fixes a :: "'a::euclidean_space"
+  shows "open_segment a b \<noteq> closed_segment c d"
+using closed_open_segment_eq by blast
+
+lemma open_segment_eq [simp]:
+  fixes a :: "'a::euclidean_space"
+  shows "open_segment a b = open_segment c d \<longleftrightarrow> a = b \<and> c = d \<or> {a,b} = {c,d}"
+        (is "?lhs = ?rhs")
+proof
+  assume abcd: ?lhs
+  show ?rhs
+  proof (cases "a=b \<or> c=d")
+    case True with abcd show ?thesis
+      using finite_open_segment by fastforce
+  next
+    case False
+    then have a2: "a \<noteq> b \<and> c \<noteq> d" by force
+    with abcd show ?rhs
+      unfolding open_segment_def
+      by (metis (no_types) abcd closed_segment_eq closure_open_segment)
+  qed
+next
+  assume ?rhs
+  then show ?lhs
+    by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
+qed
+
 subsection\<open>Similar results for closure and (relative or absolute) frontier.\<close>
 
 lemma closure_convex_hull [simp]:
@@ -9646,6 +10035,21 @@
     by blast
 qed
 
+lemma collinear_closed_segment [simp]: "collinear (closed_segment a b)"
+by (metis affine_hull_convex_hull collinear_affine_hull hull_subset segment_convex_hull)
+
+lemma collinear_open_segment [simp]: "collinear (open_segment a b)"
+  unfolding open_segment_def
+  by (metis convex_hull_subset_affine_hull segment_convex_hull dual_order.trans
+    convex_hull_subset_affine_hull Diff_subset collinear_affine_hull)
+
+lemma subset_continuous_image_segment_1:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes "continuous_on (closed_segment a b) f"
+  shows "closed_segment (f a) (f b) \<subseteq> image f (closed_segment a b)"
+by (metis connected_segment convex_contains_segment ends_in_segment imageI
+           is_interval_connected_1 is_interval_convex connected_continuous_image [OF assms])
+
 lemma collinear_imp_coplanar:
   "collinear s ==> coplanar s"
 by (metis collinear_affine_hull coplanar_def insert_absorb2)
diff -r 7f17ebd3293e -r d21dab28b3f9 src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Mon Mar 14 15:58:02 2016 +0000
@@ -223,6 +223,20 @@
   shows "compact {a .. b}"
   by (metis compact_cbox interval_cbox)
 
+lemma homeomorphic_closed_intervals:
+  fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
+  assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
+    shows "(cbox a b) homeomorphic (cbox c d)"
+apply (rule homeomorphic_convex_compact)
+using assms apply auto
+done
+
+lemma homeomorphic_closed_intervals_real:
+  fixes a::real and b and c::real and d
+  assumes "a<b" and "c<d"
+    shows "{a..b} homeomorphic {c..d}"
+by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
+
 no_notation
   eucl_less (infix "<e" 50)
 
diff -r 7f17ebd3293e -r d21dab28b3f9 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 14 15:58:02 2016 +0000
@@ -739,6 +739,22 @@
       \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
 by (simp add: arc_simple_path simple_path_assoc)
 
+subsubsection\<open>Symmetry and loops\<close>
+
+lemma path_sym:
+    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
+  by auto
+
+lemma simple_path_sym:
+    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
+by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
+
+lemma path_image_sym:
+    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
+by (simp add: path_image_join sup_commute)
+
 
 section\<open>Choosing a subpath of an existing path\<close>
 
@@ -1334,7 +1350,7 @@
   done
 
 
-text \<open>Can also consider it as a set, as the name suggests.\<close>
+subsubsection \<open>Path components as sets\<close>
 
 lemma path_component_set:
   "path_component_set s x =
@@ -1372,7 +1388,7 @@
      "\<lbrakk>x \<in> t; path_connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (path_component_set s x)"
   by (metis path_component_mono path_connected_component_set)
 
-subsection \<open>Some useful lemmas about path-connectedness\<close>
+subsection \<open>More about path-connectedness\<close>
 
 lemma convex_imp_path_connected:
   fixes s :: "'a::real_normed_vector set"
@@ -1387,6 +1403,12 @@
   apply auto
   done
 
+lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)"
+  by (simp add: convex_imp_path_connected)
+
+lemma path_component_UNIV: "path_component_set UNIV x = (UNIV :: 'a::real_normed_vector set)"
+  using path_connected_component_set by auto
+
 lemma path_connected_imp_connected:
   assumes "path_connected s"
   shows "connected s"
@@ -1679,6 +1701,72 @@
     using path_component_eq_empty by auto
 qed
 
+subsection\<open>Lemmas about path-connectedness\<close>
+
+lemma path_connected_linear_image:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes "path_connected s" "bounded_linear f"
+    shows "path_connected(f ` s)"
+by (auto simp: linear_continuous_on assms path_connected_continuous_image)
+
+lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
+  by (simp add: convex_imp_path_connected is_interval_convex)
+
+lemma linear_homeomorphic_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes "linear f" "inj f"
+    shows "s homeomorphic f ` s"
+    using assms unfolding homeomorphic_def homeomorphism_def
+    apply (rule_tac x=f in exI)
+    apply (rule_tac x="inv f" in exI)
+    using inj_linear_imp_inv_linear linear_continuous_on
+    apply (auto simp:  linear_conv_bounded_linear)
+    done
+
+lemma path_connected_Times:
+  assumes "path_connected s" "path_connected t"
+    shows "path_connected (s \<times> t)"
+proof (simp add: path_connected_def Sigma_def, clarify)
+  fix x1 y1 x2 y2
+  assume "x1 \<in> s" "y1 \<in> t" "x2 \<in> s" "y2 \<in> t"
+  obtain g where "path g" and g: "path_image g \<subseteq> s" and gs: "pathstart g = x1" and gf: "pathfinish g = x2"
+    using \<open>x1 \<in> s\<close> \<open>x2 \<in> s\<close> assms by (force simp: path_connected_def)
+  obtain h where "path h" and h: "path_image h \<subseteq> t" and hs: "pathstart h = y1" and hf: "pathfinish h = y2"
+    using \<open>y1 \<in> t\<close> \<open>y2 \<in> t\<close> assms by (force simp: path_connected_def)
+  have "path (\<lambda>z. (x1, h z))"
+    using \<open>path h\<close>
+    apply (simp add: path_def)
+    apply (rule continuous_on_compose2 [where f = h])
+    apply (rule continuous_intros | force)+
+    done
+  moreover have "path (\<lambda>z. (g z, y2))"
+    using \<open>path g\<close>
+    apply (simp add: path_def)
+    apply (rule continuous_on_compose2 [where f = g])
+    apply (rule continuous_intros | force)+
+    done
+  ultimately have 1: "path ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2)))"
+    by (metis hf gs path_join_imp pathstart_def pathfinish_def)
+  have "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> path_image (\<lambda>z. (x1, h z)) \<union> path_image (\<lambda>z. (g z, y2))"
+    by (rule Path_Connected.path_image_join_subset)
+  also have "... \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
+    using g h \<open>x1 \<in> s\<close> \<open>y2 \<in> t\<close> by (force simp: path_image_def)
+  finally have 2: "path_image ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2))) \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})" .
+  show "\<exists>g. path g \<and> path_image g \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)}) \<and>
+            pathstart g = (x1, y1) \<and> pathfinish g = (x2, y2)"
+    apply (intro exI conjI)
+       apply (rule 1)
+      apply (rule 2)
+     apply (metis hs pathstart_def pathstart_join)
+    by (metis gf pathfinish_def pathfinish_join)
+qed
+
+lemma is_interval_path_connected_1:
+  fixes s :: "real set"
+  shows "is_interval s \<longleftrightarrow> path_connected s"
+using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
+
+
 subsection \<open>Sphere is path-connected\<close>
 
 lemma path_connected_punctured_universe:
@@ -2285,6 +2373,45 @@
   then show ?thesis by (auto simp: frontier_def)
 qed
 
+lemma frontier_Union_subset_closure:
+  fixes F :: "'a::real_normed_vector set set"
+  shows "frontier(\<Union>F) \<subseteq> closure(\<Union>t \<in> F. frontier t)"
+proof -
+  have "\<exists>y\<in>F. \<exists>y\<in>frontier y. dist y x < e"
+       if "T \<in> F" "y \<in> T" "dist y x < e"
+          "x \<notin> interior (\<Union>F)" "0 < e" for x y e T
+  proof (cases "x \<in> T")
+    case True with that show ?thesis
+      by (metis Diff_iff Sup_upper closure_subset contra_subsetD dist_self frontier_def interior_mono)
+  next
+    case False
+    have 1: "closed_segment x y \<inter> T \<noteq> {}" using \<open>y \<in> T\<close> by blast
+    have 2: "closed_segment x y - T \<noteq> {}"
+      using False by blast
+    obtain c where "c \<in> closed_segment x y" "c \<in> frontier T"
+       using False connected_Int_frontier [OF connected_segment 1 2] by auto
+    then show ?thesis
+    proof -
+      have "norm (y - x) < e"
+        by (metis dist_norm \<open>dist y x < e\<close>)
+      moreover have "norm (c - x) \<le> norm (y - x)"
+        by (simp add: \<open>c \<in> closed_segment x y\<close> segment_bound(1))
+      ultimately have "norm (c - x) < e"
+        by linarith
+      then show ?thesis
+        by (metis (no_types) \<open>c \<in> frontier T\<close> dist_norm that(1))
+    qed
+  qed
+  then show ?thesis
+    by (fastforce simp add: frontier_def closure_approachable)
+qed
+
+lemma frontier_Union_subset:
+  fixes F :: "'a::real_normed_vector set set"
+  shows "finite F \<Longrightarrow> frontier(\<Union>F) \<subseteq> (\<Union>t \<in> F. frontier t)"
+by (rule order_trans [OF frontier_Union_subset_closure])
+   (auto simp: closure_subset_eq)
+
 lemma connected_component_UNIV:
     fixes x :: "'a::real_normed_vector"
     shows "connected_component_set UNIV x = UNIV"
@@ -3710,4 +3837,220 @@
 apply (rule le_cases3 [of u v w])
 using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
 
+text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
+
+lemma path_component_imp_homotopic_points:
+    "path_component S a b \<Longrightarrow> homotopic_loops S (linepath a a) (linepath b b)"
+apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
+                 pathstart_def pathfinish_def path_image_def path_def, clarify)
+apply (rule_tac x="g o fst" in exI)
+apply (intro conjI continuous_intros continuous_on_compose)+
+apply (auto elim!: continuous_on_subset)
+done
+
+lemma homotopic_loops_imp_path_component_value:
+   "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk>
+        \<Longrightarrow> path_component S (p t) (q t)"
+apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
+                 pathstart_def pathfinish_def path_image_def path_def, clarify)
+apply (rule_tac x="h o (\<lambda>u. (u, t))" in exI)
+apply (intro conjI continuous_intros continuous_on_compose)+
+apply (auto elim!: continuous_on_subset)
+done
+
+lemma homotopic_points_eq_path_component:
+   "homotopic_loops S (linepath a a) (linepath b b) \<longleftrightarrow>
+        path_component S a b"
+by (auto simp: path_component_imp_homotopic_points 
+         dest: homotopic_loops_imp_path_component_value [where t=1])
+
+lemma path_connected_eq_homotopic_points:
+    "path_connected S \<longleftrightarrow>
+      (\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
+by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
+
+
+subsection\<open>Simply connected sets\<close>
+
+text\<open>defined as "all loops are homotopic (as loops)\<close>
+
+definition simply_connected where
+  "simply_connected S \<equiv>
+        \<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
+              path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
+              \<longrightarrow> homotopic_loops S p q"
+
+lemma simply_connected_empty [iff]: "simply_connected {}"
+  by (simp add: simply_connected_def)
+
+lemma simply_connected_imp_path_connected:
+  fixes S :: "_::real_normed_vector set"
+  shows "simply_connected S \<Longrightarrow> path_connected S"
+by (simp add: simply_connected_def path_connected_eq_homotopic_points)
+
+lemma simply_connected_imp_connected:
+  fixes S :: "_::real_normed_vector set"
+  shows "simply_connected S \<Longrightarrow> connected S"
+by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)
+
+lemma simply_connected_eq_contractible_loop_any:
+  fixes S :: "_::real_normed_vector set"
+  shows "simply_connected S \<longleftrightarrow>
+            (\<forall>p a. path p \<and> path_image p \<subseteq> S \<and>
+                  pathfinish p = pathstart p \<and> a \<in> S
+                  \<longrightarrow> homotopic_loops S p (linepath a a))"
+apply (simp add: simply_connected_def)
+apply (rule iffI, force, clarify)
+apply (rule_tac q = "linepath (pathstart p) (pathstart p)" in homotopic_loops_trans)
+apply (fastforce simp add:)
+using homotopic_loops_sym apply blast
+done
+
+lemma simply_connected_eq_contractible_loop_some:
+  fixes S :: "_::real_normed_vector set"
+  shows "simply_connected S \<longleftrightarrow>
+                path_connected S \<and>
+                (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
+                    \<longrightarrow> (\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)))"
+apply (rule iffI)
+ apply (fastforce simp: simply_connected_imp_path_connected simply_connected_eq_contractible_loop_any)
+apply (clarsimp simp add: simply_connected_eq_contractible_loop_any)
+apply (drule_tac x=p in spec)
+using homotopic_loops_trans path_connected_eq_homotopic_points 
+  apply blast
+done
+
+lemma simply_connected_eq_contractible_loop_all: 
+  fixes S :: "_::real_normed_vector set"
+  shows "simply_connected S \<longleftrightarrow>
+         S = {} \<or>
+         (\<exists>a \<in> S. \<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
+                \<longrightarrow> homotopic_loops S p (linepath a a))"
+        (is "?lhs = ?rhs")
+proof (cases "S = {}")
+  case True then show ?thesis by force
+next
+  case False
+  then obtain a where "a \<in> S" by blast
+  show ?thesis
+  proof  
+    assume "simply_connected S"
+    then show ?rhs
+      using \<open>a \<in> S\<close> \<open>simply_connected S\<close> simply_connected_eq_contractible_loop_any 
+      by blast
+  next     
+    assume ?rhs
+    then show "simply_connected S"
+      apply (simp add: simply_connected_eq_contractible_loop_any False)
+      by (meson homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans 
+             path_component_imp_homotopic_points path_component_refl)
+  qed
+qed
+
+lemma simply_connected_eq_contractible_path: 
+  fixes S :: "_::real_normed_vector set"
+  shows "simply_connected S \<longleftrightarrow>
+           path_connected S \<and>
+           (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
+            \<longrightarrow> homotopic_paths S p (linepath (pathstart p) (pathstart p)))"
+apply (rule iffI)
+ apply (simp add: simply_connected_imp_path_connected)
+ apply (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null)
+by (meson homotopic_paths_imp_homotopic_loops pathfinish_linepath pathstart_in_path_image 
+         simply_connected_eq_contractible_loop_some subset_iff)
+
+lemma simply_connected_eq_homotopic_paths:
+  fixes S :: "_::real_normed_vector set"
+  shows "simply_connected S \<longleftrightarrow>
+          path_connected S \<and>
+          (\<forall>p q. path p \<and> path_image p \<subseteq> S \<and>
+                path q \<and> path_image q \<subseteq> S \<and>
+                pathstart q = pathstart p \<and> pathfinish q = pathfinish p
+                \<longrightarrow> homotopic_paths S p q)"
+         (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have pc: "path_connected S" 
+        and *:  "\<And>p. \<lbrakk>path p; path_image p \<subseteq> S;
+                       pathfinish p = pathstart p\<rbrakk> 
+                      \<Longrightarrow> homotopic_paths S p (linepath (pathstart p) (pathstart p))"
+    by (auto simp: simply_connected_eq_contractible_path)
+  have "homotopic_paths S p q" 
+        if "path p" "path_image p \<subseteq> S" "path q"
+           "path_image q \<subseteq> S" "pathstart q = pathstart p"
+           "pathfinish q = pathfinish p" for p q
+  proof -
+    have "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))" 
+      by (simp add: homotopic_paths_rid homotopic_paths_sym that)
+    also have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
+                                 (p +++ reversepath q +++ q)"
+      using that
+      by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl homotopic_paths_sym_eq pathstart_linepath)
+    also have "homotopic_paths S (p +++ reversepath q +++ q) 
+                                 ((p +++ reversepath q) +++ q)"
+      by (simp add: that homotopic_paths_assoc)
+    also have "homotopic_paths S ((p +++ reversepath q) +++ q)
+                                 (linepath (pathstart q) (pathstart q) +++ q)"
+      using * [of "p +++ reversepath q"] that
+      by (simp add: homotopic_paths_join path_image_join)
+    also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q"
+      using that homotopic_paths_lid by blast
+    finally show ?thesis .
+  qed
+  then show ?rhs
+    by (blast intro: pc *)
+next
+  assume ?rhs 
+  then show ?lhs
+    by (force simp: simply_connected_eq_contractible_path)
+qed
+
+proposition simply_connected_Times:
+  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+  assumes S: "simply_connected S" and T: "simply_connected T"
+    shows "simply_connected(S \<times> T)"
+proof -
+  have "homotopic_loops (S \<times> T) p (linepath (a, b) (a, b))"
+       if "path p" "path_image p \<subseteq> S \<times> T" "p 1 = p 0" "a \<in> S" "b \<in> T"
+       for p a b
+  proof -
+    have "path (fst \<circ> p)"
+      apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
+      apply (rule continuous_intros)+
+      done
+    moreover have "path_image (fst \<circ> p) \<subseteq> S"
+      using that apply (simp add: path_image_def) by force
+    ultimately have p1: "homotopic_loops S (fst o p) (linepath a a)"
+      using S that
+      apply (simp add: simply_connected_eq_contractible_loop_any)
+      apply (drule_tac x="fst o p" in spec)
+      apply (drule_tac x=a in spec)
+      apply (auto simp: pathstart_def pathfinish_def)
+      done
+    have "path (snd \<circ> p)"
+      apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
+      apply (rule continuous_intros)+
+      done
+    moreover have "path_image (snd \<circ> p) \<subseteq> T"
+      using that apply (simp add: path_image_def) by force
+    ultimately have p2: "homotopic_loops T (snd o p) (linepath b b)"
+      using T that
+      apply (simp add: simply_connected_eq_contractible_loop_any)
+      apply (drule_tac x="snd o p" in spec)
+      apply (drule_tac x=b in spec)
+      apply (auto simp: pathstart_def pathfinish_def)
+      done
+    show ?thesis
+      using p1 p2
+      apply (simp add: homotopic_loops, clarify)
+      apply (rename_tac h k)
+      apply (rule_tac x="\<lambda>z. Pair (h z) (k z)" in exI)
+      apply (intro conjI continuous_intros | assumption)+
+      apply (auto simp: pathstart_def pathfinish_def)
+      done
+  qed
+  with assms show ?thesis
+    by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
+qed
+
 end
diff -r 7f17ebd3293e -r d21dab28b3f9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 14:25:11 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 15:58:02 2016 +0000
@@ -7792,10 +7792,10 @@
   unfolding homeomorphism_def
   by blast
 
-lemma homeomorphic_trans:
+lemma homeomorphic_trans [trans]:
   assumes "s homeomorphic t"
-    and "t homeomorphic u"
-  shows "s homeomorphic u"
+      and "t homeomorphic u"
+    shows "s homeomorphic u"
 proof -
   obtain f1 g1 where fg1: "\<forall>x\<in>s. g1 (f1 x) = x"  "f1 ` s = t"
     "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1"