New results about paths, segments, etc. The notion of simply_connected.
authorpaulson <lp15@cam.ac.uk>
Mon Mar 14 15:58:02 2016 +0000 (2016-03-14)
changeset 62620d21dab28b3f9
parent 62619 7f17ebd3293e
child 62621 a1e73be79c0b
New results about paths, segments, etc. The notion of simply_connected.
src/HOL/Complex.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Complex.thy	Mon Mar 14 14:25:11 2016 +0000
     1.2 +++ b/src/HOL/Complex.thy	Mon Mar 14 15:58:02 2016 +0000
     1.3 @@ -673,9 +673,10 @@
     1.4  
     1.5  subsection\<open>Polar Form for Complex Numbers\<close>
     1.6  
     1.7 -lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
     1.8 -  using sincos_total_2pi [of "Re z" "Im z"]
     1.9 -  by auto (metis cmod_power2 complex_eq power_one)
    1.10 +lemma complex_unimodular_polar:
    1.11 +  assumes "(norm z = 1)"
    1.12 +  obtains t where "0 \<le> t" "t < 2*pi" "z = Complex (cos t) (sin t)"
    1.13 +by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms)
    1.14  
    1.15  subsubsection \<open>$\cos \theta + i \sin \theta$\<close>
    1.16  
     2.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 14 14:25:11 2016 +0000
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 14 15:58:02 2016 +0000
     2.3 @@ -6,6 +6,38 @@
     2.4  imports Complex_Transcendental Weierstrass Ordered_Euclidean_Space
     2.5  begin
     2.6  
     2.7 +subsection\<open>Homeomorphisms of arc images\<close>
     2.8 +
     2.9 +lemma homeomorphism_arc:
    2.10 +  fixes g :: "real \<Rightarrow> 'a::t2_space"
    2.11 +  assumes "arc g"
    2.12 +  obtains h where "homeomorphism {0..1} (path_image g) g h"
    2.13 +using assms by (force simp add: arc_def homeomorphism_compact path_def path_image_def)
    2.14 +
    2.15 +lemma homeomorphic_arc_image_interval:
    2.16 +  fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
    2.17 +  assumes "arc g" "a < b"
    2.18 +  shows "(path_image g) homeomorphic {a..b}"
    2.19 +proof -
    2.20 +  have "(path_image g) homeomorphic {0..1::real}"
    2.21 +    by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
    2.22 +  also have "... homeomorphic {a..b}"
    2.23 +    using assms by (force intro: homeomorphic_closed_intervals_real)
    2.24 +  finally show ?thesis .
    2.25 +qed
    2.26 +
    2.27 +lemma homeomorphic_arc_images:
    2.28 +  fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
    2.29 +  assumes "arc g" "arc h"
    2.30 +  shows "(path_image g) homeomorphic (path_image h)"
    2.31 +proof -
    2.32 +  have "(path_image g) homeomorphic {0..1::real}"
    2.33 +    by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
    2.34 +  also have "... homeomorphic (path_image h)"
    2.35 +    by (meson assms homeomorphic_def homeomorphism_arc)
    2.36 +  finally show ?thesis .
    2.37 +qed
    2.38 +
    2.39  subsection \<open>Piecewise differentiable functions\<close>
    2.40  
    2.41  definition piecewise_differentiable_on
     3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 14 14:25:11 2016 +0000
     3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 14 15:58:02 2016 +0000
     3.3 @@ -3661,6 +3661,14 @@
     3.4    then show ?thesis using * by auto
     3.5  qed
     3.6  
     3.7 +lemma rel_interior_eq:
     3.8 +   "rel_interior s = s \<longleftrightarrow> openin(subtopology euclidean (affine hull s)) s"
     3.9 +using rel_open rel_open_def by blast
    3.10 +
    3.11 +lemma rel_interior_openin:
    3.12 +   "openin(subtopology euclidean (affine hull s)) s \<Longrightarrow> rel_interior s = s"
    3.13 +by (simp add: rel_interior_eq)
    3.14 +
    3.15  
    3.16  subsubsection\<open>Relative interior preserves under linear transformations\<close>
    3.17  
    3.18 @@ -6678,6 +6686,226 @@
    3.19      by (auto intro: rel_interior_closure_convex_shrink)
    3.20  qed
    3.21  
    3.22 +subsection\<open>More results about segments\<close>
    3.23 +
    3.24 +lemma dist_half_times2:
    3.25 +  fixes a :: "'a :: real_normed_vector"
    3.26 +  shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
    3.27 +proof -
    3.28 +  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
    3.29 +    by simp
    3.30 +  also have "... = norm ((a + b) - 2 *\<^sub>R x)"
    3.31 +    by (simp add: real_vector.scale_right_diff_distrib)
    3.32 +  finally show ?thesis
    3.33 +    by (simp only: dist_norm)
    3.34 +qed
    3.35 +
    3.36 +lemma closed_segment_as_ball:
    3.37 +    "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
    3.38 +proof (cases "b = a")
    3.39 +  case True then show ?thesis by (auto simp: hull_inc)
    3.40 +next
    3.41 +  case False
    3.42 +  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    3.43 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
    3.44 +                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
    3.45 +  proof -
    3.46 +    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    3.47 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
    3.48 +          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
    3.49 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
    3.50 +      unfolding eq_diff_eq [symmetric] by simp
    3.51 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.52 +                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
    3.53 +      by (simp add: dist_half_times2) (simp add: dist_norm)
    3.54 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.55 +            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
    3.56 +      by auto
    3.57 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.58 +                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
    3.59 +      by (simp add: algebra_simps scaleR_2)
    3.60 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.61 +                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
    3.62 +      by simp
    3.63 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
    3.64 +      by (simp add: mult_le_cancel_right2 False)
    3.65 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
    3.66 +      by auto
    3.67 +    finally show ?thesis .
    3.68 +  qed
    3.69 +  show ?thesis
    3.70 +    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
    3.71 +qed
    3.72 +
    3.73 +lemma open_segment_as_ball:
    3.74 +    "open_segment a b =
    3.75 +     affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
    3.76 +proof (cases "b = a")
    3.77 +  case True then show ?thesis by (auto simp: hull_inc)
    3.78 +next
    3.79 +  case False
    3.80 +  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    3.81 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
    3.82 +                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
    3.83 +  proof -
    3.84 +    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    3.85 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
    3.86 +          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
    3.87 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
    3.88 +      unfolding eq_diff_eq [symmetric] by simp
    3.89 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.90 +                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
    3.91 +      by (simp add: dist_half_times2) (simp add: dist_norm)
    3.92 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.93 +            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
    3.94 +      by auto
    3.95 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.96 +                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
    3.97 +      by (simp add: algebra_simps scaleR_2)
    3.98 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    3.99 +                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
   3.100 +      by simp
   3.101 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
   3.102 +      by (simp add: mult_le_cancel_right2 False)
   3.103 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
   3.104 +      by auto
   3.105 +    finally show ?thesis .
   3.106 +  qed
   3.107 +  show ?thesis
   3.108 +    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
   3.109 +qed
   3.110 +
   3.111 +lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
   3.112 +
   3.113 +lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
   3.114 +  by auto
   3.115 +
   3.116 +lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
   3.117 +proof -
   3.118 +  { assume a1: "open_segment a b = {}"
   3.119 +    have "{} \<noteq> {0::real<..<1}"
   3.120 +      by simp
   3.121 +    then have "a = b"
   3.122 +      using a1 open_segment_image_interval by fastforce
   3.123 +  } then show ?thesis by auto
   3.124 +qed
   3.125 +
   3.126 +lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
   3.127 +  using open_segment_eq_empty by blast
   3.128 +
   3.129 +lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
   3.130 +
   3.131 +lemma inj_segment:
   3.132 +  fixes a :: "'a :: real_vector"
   3.133 +  assumes "a \<noteq> b"
   3.134 +    shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
   3.135 +proof
   3.136 +  fix x y
   3.137 +  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
   3.138 +  then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
   3.139 +    by (simp add: algebra_simps)
   3.140 +  with assms show "x = y"
   3.141 +    by (simp add: real_vector.scale_right_imp_eq)
   3.142 +qed
   3.143 +
   3.144 +lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
   3.145 +  apply auto
   3.146 +  apply (rule ccontr)
   3.147 +  apply (simp add: segment_image_interval)
   3.148 +  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
   3.149 +  done
   3.150 +
   3.151 +lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
   3.152 +  by (auto simp: open_segment_def)
   3.153 +
   3.154 +lemmas finite_segment = finite_closed_segment finite_open_segment
   3.155 +
   3.156 +lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
   3.157 +  by auto
   3.158 +
   3.159 +lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
   3.160 +  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
   3.161 +
   3.162 +lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
   3.163 +
   3.164 +lemma subset_closed_segment:
   3.165 +    "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
   3.166 +     a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   3.167 +  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
   3.168 +
   3.169 +lemma subset_co_segment:
   3.170 +    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
   3.171 +     a \<in> open_segment c d \<and> b \<in> open_segment c d"
   3.172 +using closed_segment_subset by blast
   3.173 +
   3.174 +lemma subset_open_segment:
   3.175 +  fixes a :: "'a::euclidean_space"
   3.176 +  shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
   3.177 +         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   3.178 +        (is "?lhs = ?rhs")
   3.179 +proof (cases "a = b")
   3.180 +  case True then show ?thesis by simp
   3.181 +next
   3.182 +  case False show ?thesis
   3.183 +  proof
   3.184 +    assume rhs: ?rhs
   3.185 +    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
   3.186 +      using closed_segment_idem singleton_iff by auto
   3.187 +    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) =
   3.188 +               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
   3.189 +        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
   3.190 +           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
   3.191 +           and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
   3.192 +        for u ua ub
   3.193 +    proof -
   3.194 +      have "ua \<noteq> ub"
   3.195 +        using neq by auto
   3.196 +      moreover have "(u - 1) * ua \<le> 0" using u uab
   3.197 +        by (simp add: mult_nonpos_nonneg)
   3.198 +      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
   3.199 +        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
   3.200 +      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
   3.201 +      proof -
   3.202 +        have "\<not> p \<le> 0" "\<not> q \<le> 0"
   3.203 +          using p q not_less by blast+
   3.204 +        then show ?thesis
   3.205 +          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
   3.206 +                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
   3.207 +      qed
   3.208 +      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
   3.209 +        by (metis diff_add_cancel diff_gt_0_iff_gt)
   3.210 +      with lt show ?thesis
   3.211 +        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
   3.212 +    qed
   3.213 +    with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
   3.214 +      unfolding open_segment_image_interval closed_segment_def
   3.215 +      by (fastforce simp add:)
   3.216 +  next
   3.217 +    assume lhs: ?lhs
   3.218 +    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
   3.219 +      by (meson finite_open_segment rev_finite_subset)
   3.220 +    have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
   3.221 +      using lhs closure_mono by blast
   3.222 +    then have "closed_segment a b \<subseteq> closed_segment c d"
   3.223 +      by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
   3.224 +    then show ?rhs
   3.225 +      by (force simp: \<open>a \<noteq> b\<close>)
   3.226 +  qed
   3.227 +qed
   3.228 +
   3.229 +lemma subset_oc_segment:
   3.230 +  fixes a :: "'a::euclidean_space"
   3.231 +  shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
   3.232 +         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   3.233 +apply (simp add: subset_open_segment [symmetric])
   3.234 +apply (rule iffI)
   3.235 + apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
   3.236 +apply (meson dual_order.trans segment_open_subset_closed)
   3.237 +done
   3.238 +
   3.239 +lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
   3.240 +
   3.241 +
   3.242  subsection\<open>Betweenness\<close>
   3.243  
   3.244  lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   3.245 @@ -7647,6 +7875,35 @@
   3.246    shows "A \<inter> closure S = {} \<longleftrightarrow> A \<inter> rel_interior S = {}"
   3.247    by (metis assms convex_closure_rel_interior open_inter_closure_eq_empty)
   3.248  
   3.249 +lemma rel_interior_open_segment:
   3.250 +  fixes a :: "'a :: euclidean_space"
   3.251 +  shows "rel_interior(open_segment a b) = open_segment a b"
   3.252 +proof (cases "a = b")
   3.253 +  case True then show ?thesis by auto
   3.254 +next
   3.255 +  case False then show ?thesis
   3.256 +    apply (simp add: rel_interior_eq openin_open)
   3.257 +    apply (rule_tac x="ball (inverse 2 *\<^sub>R (a + b)) (norm(b - a) / 2)" in exI)
   3.258 +    apply (simp add: open_segment_as_ball)
   3.259 +    done
   3.260 +qed
   3.261 +
   3.262 +lemma rel_interior_closed_segment:
   3.263 +  fixes a :: "'a :: euclidean_space"
   3.264 +  shows "rel_interior(closed_segment a b) =
   3.265 +         (if a = b then {a} else open_segment a b)"
   3.266 +proof (cases "a = b")
   3.267 +  case True then show ?thesis by auto
   3.268 +next
   3.269 +  case False then show ?thesis
   3.270 +    by simp
   3.271 +       (metis closure_open_segment convex_open_segment convex_rel_interior_closure
   3.272 +              rel_interior_open_segment)
   3.273 +qed
   3.274 +
   3.275 +lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
   3.276 +
   3.277 +
   3.278  definition "rel_frontier S = closure S - rel_interior S"
   3.279  
   3.280  lemma closed_affine_hull:
   3.281 @@ -8037,7 +8294,6 @@
   3.282    then show ?thesis by auto
   3.283  qed
   3.284  
   3.285 -
   3.286  lemma convex_closure_inter:
   3.287    assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
   3.288      and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"
   3.289 @@ -8172,6 +8428,19 @@
   3.290      using convex_closure_inter_two[of S T] assms affine_imp_convex by auto
   3.291  qed
   3.292  
   3.293 +lemma connected_component_1_gen:
   3.294 +  fixes S :: "'a :: euclidean_space set"
   3.295 +  assumes "DIM('a) = 1"
   3.296 +  shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
   3.297 +unfolding connected_component_def
   3.298 +by (metis (no_types, lifting) assms subsetD subsetI convex_contains_segment convex_segment(1)
   3.299 +            ends_in_segment connected_convex_1_gen)
   3.300 +
   3.301 +lemma connected_component_1:
   3.302 +  fixes S :: "real set"
   3.303 +  shows "connected_component S a b \<longleftrightarrow> closed_segment a b \<subseteq> S"
   3.304 +by (simp add: connected_component_1_gen)
   3.305 +
   3.306  lemma convex_affine_rel_interior_inter:
   3.307    fixes S T :: "'n::euclidean_space set"
   3.308    assumes "convex S"
   3.309 @@ -9448,6 +9717,126 @@
   3.310      done
   3.311  qed
   3.312  
   3.313 +lemma interior_closed_segment_ge2:
   3.314 +  fixes a :: "'a::euclidean_space"
   3.315 +  assumes "2 \<le> DIM('a)"
   3.316 +    shows  "interior(closed_segment a b) = {}"
   3.317 +using assms unfolding segment_convex_hull
   3.318 +proof -
   3.319 +  have "card {a, b} \<le> DIM('a)"
   3.320 +    using assms
   3.321 +    by (simp add: card_insert_if linear not_less_eq_eq numeral_2_eq_2)
   3.322 +  then show "interior (convex hull {a, b}) = {}"
   3.323 +    by (metis empty_interior_convex_hull finite.insertI finite.emptyI)
   3.324 +qed
   3.325 +
   3.326 +lemma interior_open_segment:
   3.327 +  fixes a :: "'a::euclidean_space"
   3.328 +  shows  "interior(open_segment a b) =
   3.329 +                 (if 2 \<le> DIM('a) then {} else open_segment a b)"
   3.330 +proof (simp add: not_le, intro conjI impI)
   3.331 +  assume "2 \<le> DIM('a)"
   3.332 +  then show "interior (open_segment a b) = {}"
   3.333 +    apply (simp add: segment_convex_hull open_segment_def)
   3.334 +    apply (metis Diff_subset interior_mono segment_convex_hull subset_empty interior_closed_segment_ge2)
   3.335 +    done
   3.336 +next
   3.337 +  assume le2: "DIM('a) < 2"
   3.338 +  show "interior (open_segment a b) = open_segment a b"
   3.339 +  proof (cases "a = b")
   3.340 +    case True then show ?thesis by auto
   3.341 +  next
   3.342 +    case False
   3.343 +    with le2 have "affine hull (open_segment a b) = UNIV"
   3.344 +      apply simp
   3.345 +      apply (rule affine_independent_span_gt)
   3.346 +      apply (simp_all add: affine_dependent_def insert_Diff_if)
   3.347 +      done
   3.348 +    then show "interior (open_segment a b) = open_segment a b"
   3.349 +      using rel_interior_interior rel_interior_open_segment by blast
   3.350 +  qed
   3.351 +qed
   3.352 +
   3.353 +lemma interior_closed_segment:
   3.354 +  fixes a :: "'a::euclidean_space"
   3.355 +  shows "interior(closed_segment a b) =
   3.356 +                 (if 2 \<le> DIM('a) then {} else open_segment a b)"
   3.357 +proof (cases "a = b")
   3.358 +  case True then show ?thesis by simp
   3.359 +next
   3.360 +  case False
   3.361 +  then have "closure (open_segment a b) = closed_segment a b"
   3.362 +    by simp
   3.363 +  then show ?thesis
   3.364 +    by (metis (no_types) convex_interior_closure convex_open_segment interior_open_segment)
   3.365 +qed
   3.366 +
   3.367 +lemmas interior_segment = interior_closed_segment interior_open_segment
   3.368 +
   3.369 +lemma closed_segment_eq [simp]:
   3.370 +  fixes a :: "'a::euclidean_space"
   3.371 +  shows "closed_segment a b = closed_segment c d \<longleftrightarrow> {a,b} = {c,d}"
   3.372 +proof
   3.373 +  assume abcd: "closed_segment a b = closed_segment c d"
   3.374 +  show "{a,b} = {c,d}"
   3.375 +  proof (cases "a=b \<or> c=d")
   3.376 +    case True with abcd show ?thesis by force
   3.377 +  next
   3.378 +    case False
   3.379 +    then have neq: "a \<noteq> b \<and> c \<noteq> d" by force
   3.380 +    have *: "closed_segment c d - {a, b} = rel_interior (closed_segment c d)"
   3.381 +      using neq abcd by (metis (no_types) open_segment_def rel_interior_closed_segment)
   3.382 +    have "b \<in> {c, d}"
   3.383 +    proof -
   3.384 +      have "insert b (closed_segment c d) = closed_segment c d"
   3.385 +        using abcd by blast
   3.386 +      then show ?thesis
   3.387 +        by (metis DiffD2 Diff_insert2 False * insertI1 insert_Diff_if open_segment_def rel_interior_closed_segment)
   3.388 +    qed
   3.389 +    moreover have "a \<in> {c, d}"
   3.390 +      by (metis Diff_iff False * abcd ends_in_segment(1) insertI1 open_segment_def rel_interior_closed_segment)
   3.391 +    ultimately show "{a, b} = {c, d}"
   3.392 +      using neq by fastforce
   3.393 +  qed
   3.394 +next
   3.395 +  assume "{a,b} = {c,d}"
   3.396 +  then show "closed_segment a b = closed_segment c d"
   3.397 +    by (simp add: segment_convex_hull)
   3.398 +qed
   3.399 +
   3.400 +lemma closed_open_segment_eq [simp]:
   3.401 +  fixes a :: "'a::euclidean_space"
   3.402 +  shows "closed_segment a b \<noteq> open_segment c d"
   3.403 +by (metis DiffE closed_segment_neq_empty closure_closed_segment closure_open_segment ends_in_segment(1) insertI1 open_segment_def)
   3.404 +
   3.405 +lemma open_closed_segment_eq [simp]:
   3.406 +  fixes a :: "'a::euclidean_space"
   3.407 +  shows "open_segment a b \<noteq> closed_segment c d"
   3.408 +using closed_open_segment_eq by blast
   3.409 +
   3.410 +lemma open_segment_eq [simp]:
   3.411 +  fixes a :: "'a::euclidean_space"
   3.412 +  shows "open_segment a b = open_segment c d \<longleftrightarrow> a = b \<and> c = d \<or> {a,b} = {c,d}"
   3.413 +        (is "?lhs = ?rhs")
   3.414 +proof
   3.415 +  assume abcd: ?lhs
   3.416 +  show ?rhs
   3.417 +  proof (cases "a=b \<or> c=d")
   3.418 +    case True with abcd show ?thesis
   3.419 +      using finite_open_segment by fastforce
   3.420 +  next
   3.421 +    case False
   3.422 +    then have a2: "a \<noteq> b \<and> c \<noteq> d" by force
   3.423 +    with abcd show ?rhs
   3.424 +      unfolding open_segment_def
   3.425 +      by (metis (no_types) abcd closed_segment_eq closure_open_segment)
   3.426 +  qed
   3.427 +next
   3.428 +  assume ?rhs
   3.429 +  then show ?lhs
   3.430 +    by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
   3.431 +qed
   3.432 +
   3.433  subsection\<open>Similar results for closure and (relative or absolute) frontier.\<close>
   3.434  
   3.435  lemma closure_convex_hull [simp]:
   3.436 @@ -9646,6 +10035,21 @@
   3.437      by blast
   3.438  qed
   3.439  
   3.440 +lemma collinear_closed_segment [simp]: "collinear (closed_segment a b)"
   3.441 +by (metis affine_hull_convex_hull collinear_affine_hull hull_subset segment_convex_hull)
   3.442 +
   3.443 +lemma collinear_open_segment [simp]: "collinear (open_segment a b)"
   3.444 +  unfolding open_segment_def
   3.445 +  by (metis convex_hull_subset_affine_hull segment_convex_hull dual_order.trans
   3.446 +    convex_hull_subset_affine_hull Diff_subset collinear_affine_hull)
   3.447 +
   3.448 +lemma subset_continuous_image_segment_1:
   3.449 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
   3.450 +  assumes "continuous_on (closed_segment a b) f"
   3.451 +  shows "closed_segment (f a) (f b) \<subseteq> image f (closed_segment a b)"
   3.452 +by (metis connected_segment convex_contains_segment ends_in_segment imageI
   3.453 +           is_interval_connected_1 is_interval_convex connected_continuous_image [OF assms])
   3.454 +
   3.455  lemma collinear_imp_coplanar:
   3.456    "collinear s ==> coplanar s"
   3.457  by (metis collinear_affine_hull coplanar_def insert_absorb2)
     4.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Mon Mar 14 14:25:11 2016 +0000
     4.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Mon Mar 14 15:58:02 2016 +0000
     4.3 @@ -223,6 +223,20 @@
     4.4    shows "compact {a .. b}"
     4.5    by (metis compact_cbox interval_cbox)
     4.6  
     4.7 +lemma homeomorphic_closed_intervals:
     4.8 +  fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
     4.9 +  assumes "box a b \<noteq> {}" and "box c d \<noteq> {}"
    4.10 +    shows "(cbox a b) homeomorphic (cbox c d)"
    4.11 +apply (rule homeomorphic_convex_compact)
    4.12 +using assms apply auto
    4.13 +done
    4.14 +
    4.15 +lemma homeomorphic_closed_intervals_real:
    4.16 +  fixes a::real and b and c::real and d
    4.17 +  assumes "a<b" and "c<d"
    4.18 +    shows "{a..b} homeomorphic {c..d}"
    4.19 +by (metis assms compact_interval continuous_on_id convex_real_interval(5) emptyE homeomorphic_convex_compact interior_atLeastAtMost_real mvt)
    4.20 +
    4.21  no_notation
    4.22    eucl_less (infix "<e" 50)
    4.23  
     5.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 14 14:25:11 2016 +0000
     5.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 14 15:58:02 2016 +0000
     5.3 @@ -739,6 +739,22 @@
     5.4        \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
     5.5  by (simp add: arc_simple_path simple_path_assoc)
     5.6  
     5.7 +subsubsection\<open>Symmetry and loops\<close>
     5.8 +
     5.9 +lemma path_sym:
    5.10 +    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
    5.11 +  by auto
    5.12 +
    5.13 +lemma simple_path_sym:
    5.14 +    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
    5.15 +     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
    5.16 +by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
    5.17 +
    5.18 +lemma path_image_sym:
    5.19 +    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
    5.20 +     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
    5.21 +by (simp add: path_image_join sup_commute)
    5.22 +
    5.23  
    5.24  section\<open>Choosing a subpath of an existing path\<close>
    5.25  
    5.26 @@ -1334,7 +1350,7 @@
    5.27    done
    5.28  
    5.29  
    5.30 -text \<open>Can also consider it as a set, as the name suggests.\<close>
    5.31 +subsubsection \<open>Path components as sets\<close>
    5.32  
    5.33  lemma path_component_set:
    5.34    "path_component_set s x =
    5.35 @@ -1372,7 +1388,7 @@
    5.36       "\<lbrakk>x \<in> t; path_connected t; t \<subseteq> s\<rbrakk> \<Longrightarrow> t \<subseteq> (path_component_set s x)"
    5.37    by (metis path_component_mono path_connected_component_set)
    5.38  
    5.39 -subsection \<open>Some useful lemmas about path-connectedness\<close>
    5.40 +subsection \<open>More about path-connectedness\<close>
    5.41  
    5.42  lemma convex_imp_path_connected:
    5.43    fixes s :: "'a::real_normed_vector set"
    5.44 @@ -1387,6 +1403,12 @@
    5.45    apply auto
    5.46    done
    5.47  
    5.48 +lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)"
    5.49 +  by (simp add: convex_imp_path_connected)
    5.50 +
    5.51 +lemma path_component_UNIV: "path_component_set UNIV x = (UNIV :: 'a::real_normed_vector set)"
    5.52 +  using path_connected_component_set by auto
    5.53 +
    5.54  lemma path_connected_imp_connected:
    5.55    assumes "path_connected s"
    5.56    shows "connected s"
    5.57 @@ -1679,6 +1701,72 @@
    5.58      using path_component_eq_empty by auto
    5.59  qed
    5.60  
    5.61 +subsection\<open>Lemmas about path-connectedness\<close>
    5.62 +
    5.63 +lemma path_connected_linear_image:
    5.64 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    5.65 +  assumes "path_connected s" "bounded_linear f"
    5.66 +    shows "path_connected(f ` s)"
    5.67 +by (auto simp: linear_continuous_on assms path_connected_continuous_image)
    5.68 +
    5.69 +lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
    5.70 +  by (simp add: convex_imp_path_connected is_interval_convex)
    5.71 +
    5.72 +lemma linear_homeomorphic_image:
    5.73 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
    5.74 +  assumes "linear f" "inj f"
    5.75 +    shows "s homeomorphic f ` s"
    5.76 +    using assms unfolding homeomorphic_def homeomorphism_def
    5.77 +    apply (rule_tac x=f in exI)
    5.78 +    apply (rule_tac x="inv f" in exI)
    5.79 +    using inj_linear_imp_inv_linear linear_continuous_on
    5.80 +    apply (auto simp:  linear_conv_bounded_linear)
    5.81 +    done
    5.82 +
    5.83 +lemma path_connected_Times:
    5.84 +  assumes "path_connected s" "path_connected t"
    5.85 +    shows "path_connected (s \<times> t)"
    5.86 +proof (simp add: path_connected_def Sigma_def, clarify)
    5.87 +  fix x1 y1 x2 y2
    5.88 +  assume "x1 \<in> s" "y1 \<in> t" "x2 \<in> s" "y2 \<in> t"
    5.89 +  obtain g where "path g" and g: "path_image g \<subseteq> s" and gs: "pathstart g = x1" and gf: "pathfinish g = x2"
    5.90 +    using \<open>x1 \<in> s\<close> \<open>x2 \<in> s\<close> assms by (force simp: path_connected_def)
    5.91 +  obtain h where "path h" and h: "path_image h \<subseteq> t" and hs: "pathstart h = y1" and hf: "pathfinish h = y2"
    5.92 +    using \<open>y1 \<in> t\<close> \<open>y2 \<in> t\<close> assms by (force simp: path_connected_def)
    5.93 +  have "path (\<lambda>z. (x1, h z))"
    5.94 +    using \<open>path h\<close>
    5.95 +    apply (simp add: path_def)
    5.96 +    apply (rule continuous_on_compose2 [where f = h])
    5.97 +    apply (rule continuous_intros | force)+
    5.98 +    done
    5.99 +  moreover have "path (\<lambda>z. (g z, y2))"
   5.100 +    using \<open>path g\<close>
   5.101 +    apply (simp add: path_def)
   5.102 +    apply (rule continuous_on_compose2 [where f = g])
   5.103 +    apply (rule continuous_intros | force)+
   5.104 +    done
   5.105 +  ultimately have 1: "path ((\<lambda>z. (x1, h z)) +++ (\<lambda>z. (g z, y2)))"
   5.106 +    by (metis hf gs path_join_imp pathstart_def pathfinish_def)
   5.107 +  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))"
   5.108 +    by (rule Path_Connected.path_image_join_subset)
   5.109 +  also have "... \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)})"
   5.110 +    using g h \<open>x1 \<in> s\<close> \<open>y2 \<in> t\<close> by (force simp: path_image_def)
   5.111 +  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)})" .
   5.112 +  show "\<exists>g. path g \<and> path_image g \<subseteq> (\<Union>x\<in>s. \<Union>x1\<in>t. {(x, x1)}) \<and>
   5.113 +            pathstart g = (x1, y1) \<and> pathfinish g = (x2, y2)"
   5.114 +    apply (intro exI conjI)
   5.115 +       apply (rule 1)
   5.116 +      apply (rule 2)
   5.117 +     apply (metis hs pathstart_def pathstart_join)
   5.118 +    by (metis gf pathfinish_def pathfinish_join)
   5.119 +qed
   5.120 +
   5.121 +lemma is_interval_path_connected_1:
   5.122 +  fixes s :: "real set"
   5.123 +  shows "is_interval s \<longleftrightarrow> path_connected s"
   5.124 +using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
   5.125 +
   5.126 +
   5.127  subsection \<open>Sphere is path-connected\<close>
   5.128  
   5.129  lemma path_connected_punctured_universe:
   5.130 @@ -2285,6 +2373,45 @@
   5.131    then show ?thesis by (auto simp: frontier_def)
   5.132  qed
   5.133  
   5.134 +lemma frontier_Union_subset_closure:
   5.135 +  fixes F :: "'a::real_normed_vector set set"
   5.136 +  shows "frontier(\<Union>F) \<subseteq> closure(\<Union>t \<in> F. frontier t)"
   5.137 +proof -
   5.138 +  have "\<exists>y\<in>F. \<exists>y\<in>frontier y. dist y x < e"
   5.139 +       if "T \<in> F" "y \<in> T" "dist y x < e"
   5.140 +          "x \<notin> interior (\<Union>F)" "0 < e" for x y e T
   5.141 +  proof (cases "x \<in> T")
   5.142 +    case True with that show ?thesis
   5.143 +      by (metis Diff_iff Sup_upper closure_subset contra_subsetD dist_self frontier_def interior_mono)
   5.144 +  next
   5.145 +    case False
   5.146 +    have 1: "closed_segment x y \<inter> T \<noteq> {}" using \<open>y \<in> T\<close> by blast
   5.147 +    have 2: "closed_segment x y - T \<noteq> {}"
   5.148 +      using False by blast
   5.149 +    obtain c where "c \<in> closed_segment x y" "c \<in> frontier T"
   5.150 +       using False connected_Int_frontier [OF connected_segment 1 2] by auto
   5.151 +    then show ?thesis
   5.152 +    proof -
   5.153 +      have "norm (y - x) < e"
   5.154 +        by (metis dist_norm \<open>dist y x < e\<close>)
   5.155 +      moreover have "norm (c - x) \<le> norm (y - x)"
   5.156 +        by (simp add: \<open>c \<in> closed_segment x y\<close> segment_bound(1))
   5.157 +      ultimately have "norm (c - x) < e"
   5.158 +        by linarith
   5.159 +      then show ?thesis
   5.160 +        by (metis (no_types) \<open>c \<in> frontier T\<close> dist_norm that(1))
   5.161 +    qed
   5.162 +  qed
   5.163 +  then show ?thesis
   5.164 +    by (fastforce simp add: frontier_def closure_approachable)
   5.165 +qed
   5.166 +
   5.167 +lemma frontier_Union_subset:
   5.168 +  fixes F :: "'a::real_normed_vector set set"
   5.169 +  shows "finite F \<Longrightarrow> frontier(\<Union>F) \<subseteq> (\<Union>t \<in> F. frontier t)"
   5.170 +by (rule order_trans [OF frontier_Union_subset_closure])
   5.171 +   (auto simp: closure_subset_eq)
   5.172 +
   5.173  lemma connected_component_UNIV:
   5.174      fixes x :: "'a::real_normed_vector"
   5.175      shows "connected_component_set UNIV x = UNIV"
   5.176 @@ -3710,4 +3837,220 @@
   5.177  apply (rule le_cases3 [of u v w])
   5.178  using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
   5.179  
   5.180 +text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
   5.181 +
   5.182 +lemma path_component_imp_homotopic_points:
   5.183 +    "path_component S a b \<Longrightarrow> homotopic_loops S (linepath a a) (linepath b b)"
   5.184 +apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
   5.185 +                 pathstart_def pathfinish_def path_image_def path_def, clarify)
   5.186 +apply (rule_tac x="g o fst" in exI)
   5.187 +apply (intro conjI continuous_intros continuous_on_compose)+
   5.188 +apply (auto elim!: continuous_on_subset)
   5.189 +done
   5.190 +
   5.191 +lemma homotopic_loops_imp_path_component_value:
   5.192 +   "\<lbrakk>homotopic_loops S p q; 0 \<le> t; t \<le> 1\<rbrakk>
   5.193 +        \<Longrightarrow> path_component S (p t) (q t)"
   5.194 +apply (simp add: path_component_def homotopic_loops_def homotopic_with_def
   5.195 +                 pathstart_def pathfinish_def path_image_def path_def, clarify)
   5.196 +apply (rule_tac x="h o (\<lambda>u. (u, t))" in exI)
   5.197 +apply (intro conjI continuous_intros continuous_on_compose)+
   5.198 +apply (auto elim!: continuous_on_subset)
   5.199 +done
   5.200 +
   5.201 +lemma homotopic_points_eq_path_component:
   5.202 +   "homotopic_loops S (linepath a a) (linepath b b) \<longleftrightarrow>
   5.203 +        path_component S a b"
   5.204 +by (auto simp: path_component_imp_homotopic_points 
   5.205 +         dest: homotopic_loops_imp_path_component_value [where t=1])
   5.206 +
   5.207 +lemma path_connected_eq_homotopic_points:
   5.208 +    "path_connected S \<longleftrightarrow>
   5.209 +      (\<forall>a b. a \<in> S \<and> b \<in> S \<longrightarrow> homotopic_loops S (linepath a a) (linepath b b))"
   5.210 +by (auto simp: path_connected_def path_component_def homotopic_points_eq_path_component)
   5.211 +
   5.212 +
   5.213 +subsection\<open>Simply connected sets\<close>
   5.214 +
   5.215 +text\<open>defined as "all loops are homotopic (as loops)\<close>
   5.216 +
   5.217 +definition simply_connected where
   5.218 +  "simply_connected S \<equiv>
   5.219 +        \<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
   5.220 +              path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
   5.221 +              \<longrightarrow> homotopic_loops S p q"
   5.222 +
   5.223 +lemma simply_connected_empty [iff]: "simply_connected {}"
   5.224 +  by (simp add: simply_connected_def)
   5.225 +
   5.226 +lemma simply_connected_imp_path_connected:
   5.227 +  fixes S :: "_::real_normed_vector set"
   5.228 +  shows "simply_connected S \<Longrightarrow> path_connected S"
   5.229 +by (simp add: simply_connected_def path_connected_eq_homotopic_points)
   5.230 +
   5.231 +lemma simply_connected_imp_connected:
   5.232 +  fixes S :: "_::real_normed_vector set"
   5.233 +  shows "simply_connected S \<Longrightarrow> connected S"
   5.234 +by (simp add: path_connected_imp_connected simply_connected_imp_path_connected)
   5.235 +
   5.236 +lemma simply_connected_eq_contractible_loop_any:
   5.237 +  fixes S :: "_::real_normed_vector set"
   5.238 +  shows "simply_connected S \<longleftrightarrow>
   5.239 +            (\<forall>p a. path p \<and> path_image p \<subseteq> S \<and>
   5.240 +                  pathfinish p = pathstart p \<and> a \<in> S
   5.241 +                  \<longrightarrow> homotopic_loops S p (linepath a a))"
   5.242 +apply (simp add: simply_connected_def)
   5.243 +apply (rule iffI, force, clarify)
   5.244 +apply (rule_tac q = "linepath (pathstart p) (pathstart p)" in homotopic_loops_trans)
   5.245 +apply (fastforce simp add:)
   5.246 +using homotopic_loops_sym apply blast
   5.247 +done
   5.248 +
   5.249 +lemma simply_connected_eq_contractible_loop_some:
   5.250 +  fixes S :: "_::real_normed_vector set"
   5.251 +  shows "simply_connected S \<longleftrightarrow>
   5.252 +                path_connected S \<and>
   5.253 +                (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
   5.254 +                    \<longrightarrow> (\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)))"
   5.255 +apply (rule iffI)
   5.256 + apply (fastforce simp: simply_connected_imp_path_connected simply_connected_eq_contractible_loop_any)
   5.257 +apply (clarsimp simp add: simply_connected_eq_contractible_loop_any)
   5.258 +apply (drule_tac x=p in spec)
   5.259 +using homotopic_loops_trans path_connected_eq_homotopic_points 
   5.260 +  apply blast
   5.261 +done
   5.262 +
   5.263 +lemma simply_connected_eq_contractible_loop_all: 
   5.264 +  fixes S :: "_::real_normed_vector set"
   5.265 +  shows "simply_connected S \<longleftrightarrow>
   5.266 +         S = {} \<or>
   5.267 +         (\<exists>a \<in> S. \<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
   5.268 +                \<longrightarrow> homotopic_loops S p (linepath a a))"
   5.269 +        (is "?lhs = ?rhs")
   5.270 +proof (cases "S = {}")
   5.271 +  case True then show ?thesis by force
   5.272 +next
   5.273 +  case False
   5.274 +  then obtain a where "a \<in> S" by blast
   5.275 +  show ?thesis
   5.276 +  proof  
   5.277 +    assume "simply_connected S"
   5.278 +    then show ?rhs
   5.279 +      using \<open>a \<in> S\<close> \<open>simply_connected S\<close> simply_connected_eq_contractible_loop_any 
   5.280 +      by blast
   5.281 +  next     
   5.282 +    assume ?rhs
   5.283 +    then show "simply_connected S"
   5.284 +      apply (simp add: simply_connected_eq_contractible_loop_any False)
   5.285 +      by (meson homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans 
   5.286 +             path_component_imp_homotopic_points path_component_refl)
   5.287 +  qed
   5.288 +qed
   5.289 +
   5.290 +lemma simply_connected_eq_contractible_path: 
   5.291 +  fixes S :: "_::real_normed_vector set"
   5.292 +  shows "simply_connected S \<longleftrightarrow>
   5.293 +           path_connected S \<and>
   5.294 +           (\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
   5.295 +            \<longrightarrow> homotopic_paths S p (linepath (pathstart p) (pathstart p)))"
   5.296 +apply (rule iffI)
   5.297 + apply (simp add: simply_connected_imp_path_connected)
   5.298 + apply (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null)
   5.299 +by (meson homotopic_paths_imp_homotopic_loops pathfinish_linepath pathstart_in_path_image 
   5.300 +         simply_connected_eq_contractible_loop_some subset_iff)
   5.301 +
   5.302 +lemma simply_connected_eq_homotopic_paths:
   5.303 +  fixes S :: "_::real_normed_vector set"
   5.304 +  shows "simply_connected S \<longleftrightarrow>
   5.305 +          path_connected S \<and>
   5.306 +          (\<forall>p q. path p \<and> path_image p \<subseteq> S \<and>
   5.307 +                path q \<and> path_image q \<subseteq> S \<and>
   5.308 +                pathstart q = pathstart p \<and> pathfinish q = pathfinish p
   5.309 +                \<longrightarrow> homotopic_paths S p q)"
   5.310 +         (is "?lhs = ?rhs")
   5.311 +proof
   5.312 +  assume ?lhs
   5.313 +  then have pc: "path_connected S" 
   5.314 +        and *:  "\<And>p. \<lbrakk>path p; path_image p \<subseteq> S;
   5.315 +                       pathfinish p = pathstart p\<rbrakk> 
   5.316 +                      \<Longrightarrow> homotopic_paths S p (linepath (pathstart p) (pathstart p))"
   5.317 +    by (auto simp: simply_connected_eq_contractible_path)
   5.318 +  have "homotopic_paths S p q" 
   5.319 +        if "path p" "path_image p \<subseteq> S" "path q"
   5.320 +           "path_image q \<subseteq> S" "pathstart q = pathstart p"
   5.321 +           "pathfinish q = pathfinish p" for p q
   5.322 +  proof -
   5.323 +    have "homotopic_paths S p (p +++ linepath (pathfinish p) (pathfinish p))" 
   5.324 +      by (simp add: homotopic_paths_rid homotopic_paths_sym that)
   5.325 +    also have "homotopic_paths S (p +++ linepath (pathfinish p) (pathfinish p))
   5.326 +                                 (p +++ reversepath q +++ q)"
   5.327 +      using that
   5.328 +      by (metis homotopic_paths_join homotopic_paths_linv homotopic_paths_refl homotopic_paths_sym_eq pathstart_linepath)
   5.329 +    also have "homotopic_paths S (p +++ reversepath q +++ q) 
   5.330 +                                 ((p +++ reversepath q) +++ q)"
   5.331 +      by (simp add: that homotopic_paths_assoc)
   5.332 +    also have "homotopic_paths S ((p +++ reversepath q) +++ q)
   5.333 +                                 (linepath (pathstart q) (pathstart q) +++ q)"
   5.334 +      using * [of "p +++ reversepath q"] that
   5.335 +      by (simp add: homotopic_paths_join path_image_join)
   5.336 +    also have "homotopic_paths S (linepath (pathstart q) (pathstart q) +++ q) q"
   5.337 +      using that homotopic_paths_lid by blast
   5.338 +    finally show ?thesis .
   5.339 +  qed
   5.340 +  then show ?rhs
   5.341 +    by (blast intro: pc *)
   5.342 +next
   5.343 +  assume ?rhs 
   5.344 +  then show ?lhs
   5.345 +    by (force simp: simply_connected_eq_contractible_path)
   5.346 +qed
   5.347 +
   5.348 +proposition simply_connected_Times:
   5.349 +  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
   5.350 +  assumes S: "simply_connected S" and T: "simply_connected T"
   5.351 +    shows "simply_connected(S \<times> T)"
   5.352 +proof -
   5.353 +  have "homotopic_loops (S \<times> T) p (linepath (a, b) (a, b))"
   5.354 +       if "path p" "path_image p \<subseteq> S \<times> T" "p 1 = p 0" "a \<in> S" "b \<in> T"
   5.355 +       for p a b
   5.356 +  proof -
   5.357 +    have "path (fst \<circ> p)"
   5.358 +      apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
   5.359 +      apply (rule continuous_intros)+
   5.360 +      done
   5.361 +    moreover have "path_image (fst \<circ> p) \<subseteq> S"
   5.362 +      using that apply (simp add: path_image_def) by force
   5.363 +    ultimately have p1: "homotopic_loops S (fst o p) (linepath a a)"
   5.364 +      using S that
   5.365 +      apply (simp add: simply_connected_eq_contractible_loop_any)
   5.366 +      apply (drule_tac x="fst o p" in spec)
   5.367 +      apply (drule_tac x=a in spec)
   5.368 +      apply (auto simp: pathstart_def pathfinish_def)
   5.369 +      done
   5.370 +    have "path (snd \<circ> p)"
   5.371 +      apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
   5.372 +      apply (rule continuous_intros)+
   5.373 +      done
   5.374 +    moreover have "path_image (snd \<circ> p) \<subseteq> T"
   5.375 +      using that apply (simp add: path_image_def) by force
   5.376 +    ultimately have p2: "homotopic_loops T (snd o p) (linepath b b)"
   5.377 +      using T that
   5.378 +      apply (simp add: simply_connected_eq_contractible_loop_any)
   5.379 +      apply (drule_tac x="snd o p" in spec)
   5.380 +      apply (drule_tac x=b in spec)
   5.381 +      apply (auto simp: pathstart_def pathfinish_def)
   5.382 +      done
   5.383 +    show ?thesis
   5.384 +      using p1 p2
   5.385 +      apply (simp add: homotopic_loops, clarify)
   5.386 +      apply (rename_tac h k)
   5.387 +      apply (rule_tac x="\<lambda>z. Pair (h z) (k z)" in exI)
   5.388 +      apply (intro conjI continuous_intros | assumption)+
   5.389 +      apply (auto simp: pathstart_def pathfinish_def)
   5.390 +      done
   5.391 +  qed
   5.392 +  with assms show ?thesis
   5.393 +    by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
   5.394 +qed
   5.395 +
   5.396  end
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 14:25:11 2016 +0000
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 15:58:02 2016 +0000
     6.3 @@ -7792,10 +7792,10 @@
     6.4    unfolding homeomorphism_def
     6.5    by blast
     6.6  
     6.7 -lemma homeomorphic_trans:
     6.8 +lemma homeomorphic_trans [trans]:
     6.9    assumes "s homeomorphic t"
    6.10 -    and "t homeomorphic u"
    6.11 -  shows "s homeomorphic u"
    6.12 +      and "t homeomorphic u"
    6.13 +    shows "s homeomorphic u"
    6.14  proof -
    6.15    obtain f1 g1 where fg1: "\<forall>x\<in>s. g1 (f1 x) = x"  "f1 ` s = t"
    6.16      "continuous_on s f1" "\<forall>y\<in>t. f1 (g1 y) = y" "g1 ` t = s" "continuous_on t g1"