src/HOL/Analysis/Path_Connected.thy
changeset 66793 deabce3ccf1f
parent 66456 621897f47fab
child 66826 0d60d2118544
     1.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Mon Oct 09 15:34:23 2017 +0100
     1.3 @@ -166,6 +166,9 @@
     1.4  lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)"
     1.5    by (simp add: arc_simple_path)
     1.6  
     1.7 +lemma path_image_const [simp]: "path_image (\<lambda>t. a) = {a}"
     1.8 +  by (force simp: path_image_def)
     1.9 +
    1.10  lemma path_image_nonempty [simp]: "path_image g \<noteq> {}"
    1.11    unfolding path_image_def image_is_empty box_eq_empty
    1.12    by auto
    1.13 @@ -1511,13 +1514,7 @@
    1.14    assumes "convex s"
    1.15    shows "path_connected s"
    1.16    unfolding path_connected_def
    1.17 -  apply rule
    1.18 -  apply rule
    1.19 -  apply (rule_tac x = "linepath x y" in exI)
    1.20 -  unfolding path_image_linepath
    1.21 -  using assms [unfolded convex_contains_segment]
    1.22 -  apply auto
    1.23 -  done
    1.24 +  using assms convex_contains_segment by fastforce
    1.25  
    1.26  lemma path_connected_UNIV [iff]: "path_connected (UNIV :: 'a::real_normed_vector set)"
    1.27    by (simp add: convex_imp_path_connected)
    1.28 @@ -1528,13 +1525,7 @@
    1.29  lemma path_connected_imp_connected:
    1.30    assumes "path_connected S"
    1.31    shows "connected S"
    1.32 -  unfolding connected_def not_ex
    1.33 -  apply rule
    1.34 -  apply rule
    1.35 -  apply (rule ccontr)
    1.36 -  unfolding not_not
    1.37 -  apply (elim conjE)
    1.38 -proof -
    1.39 +proof (rule connectedI)
    1.40    fix e1 e2
    1.41    assume as: "open e1" "open e2" "S \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> S = {}" "e1 \<inter> S \<noteq> {}" "e2 \<inter> S \<noteq> {}"
    1.42    then obtain x1 x2 where obt:"x1 \<in> e1 \<inter> S" "x2 \<in> e2 \<inter> S"
    1.43 @@ -1570,31 +1561,14 @@
    1.44    fix y
    1.45    assume as: "y \<in> path_component_set S x"
    1.46    then have "y \<in> S"
    1.47 -    apply -
    1.48 -    apply (rule path_component_mem(2))
    1.49 -    unfolding mem_Collect_eq
    1.50 -    apply auto
    1.51 -    done
    1.52 +    by (simp add: path_component_mem(2))
    1.53    then obtain e where e: "e > 0" "ball y e \<subseteq> S"
    1.54      using assms[unfolded open_contains_ball]
    1.55      by auto
    1.56 -  show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
    1.57 -    apply (rule_tac x=e in exI)
    1.58 -    apply (rule,rule \<open>e>0\<close>)
    1.59 -    apply rule
    1.60 -    unfolding mem_ball mem_Collect_eq
    1.61 -  proof -
    1.62 -    fix z
    1.63 -    assume "dist y z < e"
    1.64 -    then show "path_component S x z"
    1.65 -      apply (rule_tac path_component_trans[of _ _ y])
    1.66 -      defer
    1.67 -      apply (rule path_component_of_subset[OF e(2)])
    1.68 -      apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
    1.69 -      using \<open>e > 0\<close> as
    1.70 -      apply auto
    1.71 -      done
    1.72 -  qed
    1.73 +have "\<And>u. dist y u < e \<Longrightarrow> path_component S x u"
    1.74 +      by (metis (full_types) as centre_in_ball convex_ball convex_imp_path_connected e mem_Collect_eq mem_ball path_component_eq path_component_of_subset path_connected_component)
    1.75 +  then show "\<exists>e > 0. ball y e \<subseteq> path_component_set S x"
    1.76 +    using \<open>e>0\<close> by auto
    1.77  qed
    1.78  
    1.79  lemma open_non_path_component:
    1.80 @@ -1904,6 +1878,8 @@
    1.81  using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
    1.82  
    1.83  
    1.84 +subsection\<open>Path components\<close>
    1.85 +
    1.86  lemma Union_path_component [simp]:
    1.87     "Union {path_component_set S x |x. x \<in> S} = S"
    1.88  apply (rule subset_antisym)
    1.89 @@ -2151,7 +2127,6 @@
    1.90      by (auto simp: path_connected_component)
    1.91  qed
    1.92  
    1.93 -
    1.94  lemma connected_complement_bounded_convex:
    1.95      fixes s :: "'a :: euclidean_space set"
    1.96      assumes "bounded s" "convex s" "2 \<le> DIM('a)"
    1.97 @@ -2300,6 +2275,65 @@
    1.98  qed
    1.99  
   1.100  
   1.101 +subsection\<open>Every annulus is a connected set\<close>
   1.102 +
   1.103 +lemma path_connected_2DIM_I:
   1.104 +  fixes a :: "'N::euclidean_space"
   1.105 +  assumes 2: "2 \<le> DIM('N)" and pc: "path_connected {r. 0 \<le> r \<and> P r}"
   1.106 +  shows "path_connected {x. P(norm(x - a))}"
   1.107 +proof -
   1.108 +  have "{x. P(norm(x - a))} = op+a ` {x. P(norm x)}"
   1.109 +    by force
   1.110 +  moreover have "path_connected {x::'N. P(norm x)}"
   1.111 +  proof -
   1.112 +    let ?D = "{x. 0 \<le> x \<and> P x} \<times> sphere (0::'N) 1"
   1.113 +    have "x \<in> (\<lambda>z. fst z *\<^sub>R snd z) ` ?D"
   1.114 +      if "P (norm x)" for x::'N
   1.115 +    proof (cases "x=0")
   1.116 +      case True
   1.117 +      with that show ?thesis
   1.118 +        apply (simp add: image_iff)
   1.119 +        apply (rule_tac x=0 in exI, simp)
   1.120 +        using vector_choose_size zero_le_one by blast
   1.121 +    next
   1.122 +      case False
   1.123 +      with that show ?thesis
   1.124 +        by (rule_tac x="(norm x, x /\<^sub>R norm x)" in image_eqI) auto
   1.125 +    qed
   1.126 +    then have *: "{x::'N. P(norm x)} =  (\<lambda>z. fst z *\<^sub>R snd z) ` ?D"
   1.127 +      by auto
   1.128 +    have "continuous_on ?D (\<lambda>z:: real\<times>'N. fst z *\<^sub>R snd z)"
   1.129 +      by (intro continuous_intros)
   1.130 +    moreover have "path_connected ?D"
   1.131 +      by (metis path_connected_Times [OF pc] path_connected_sphere 2)
   1.132 +    ultimately show ?thesis
   1.133 +      apply (subst *)
   1.134 +      apply (rule path_connected_continuous_image, auto)
   1.135 +      done
   1.136 +  qed
   1.137 +  ultimately show ?thesis
   1.138 +    using path_connected_translation by metis
   1.139 +qed
   1.140 +
   1.141 +lemma path_connected_annulus:
   1.142 +  fixes a :: "'N::euclidean_space"
   1.143 +  assumes "2 \<le> DIM('N)"
   1.144 +  shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
   1.145 +        "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
   1.146 +        "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
   1.147 +        "path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
   1.148 +  by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
   1.149 +
   1.150 +lemma connected_annulus:
   1.151 +  fixes a :: "'N::euclidean_space"
   1.152 +  assumes "2 \<le> DIM('N::euclidean_space)"
   1.153 +  shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
   1.154 +        "connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
   1.155 +        "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
   1.156 +        "connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
   1.157 +  by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
   1.158 +
   1.159 +
   1.160  subsection\<open>Relations between components and path components\<close>
   1.161  
   1.162  lemma open_connected_component:
   1.163 @@ -2894,11 +2928,21 @@
   1.164      shows "outside s = - s"
   1.165    by (metis ComplD assms convex_in_outside equalityI inside_Un_outside subsetI sup.cobounded2)
   1.166  
   1.167 +lemma outside_singleton [simp]:
   1.168 +  fixes x :: "'a :: {real_normed_vector, perfect_space}"
   1.169 +  shows "outside {x} = -{x}"
   1.170 +  by (auto simp: outside_convex)
   1.171 +
   1.172  lemma inside_convex:
   1.173    fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   1.174    shows "convex s \<Longrightarrow> inside s = {}"
   1.175    by (simp add: inside_outside outside_convex)
   1.176  
   1.177 +lemma inside_singleton [simp]:
   1.178 +  fixes x :: "'a :: {real_normed_vector, perfect_space}"
   1.179 +  shows "inside {x} = {}"
   1.180 +  by (auto simp: inside_convex)
   1.181 +
   1.182  lemma outside_subset_convex:
   1.183    fixes s :: "'a :: {real_normed_vector, perfect_space} set"
   1.184    shows "\<lbrakk>convex t; s \<subseteq> t\<rbrakk> \<Longrightarrow> - t \<subseteq> outside s"
   1.185 @@ -4119,6 +4163,39 @@
   1.186      by (blast intro: homotopic_loops_trans)
   1.187  qed
   1.188  
   1.189 +lemma homotopic_paths_loop_parts:
   1.190 +  assumes loops: "homotopic_loops S (p +++ reversepath q) (linepath a a)" and "path q"
   1.191 +  shows "homotopic_paths S p q"
   1.192 +proof -
   1.193 +  have paths: "homotopic_paths S (p +++ reversepath q) (linepath (pathstart p) (pathstart p))"
   1.194 +    using homotopic_loops_imp_homotopic_paths_null [OF loops] by simp
   1.195 +  then have "path p"
   1.196 +    using \<open>path q\<close> homotopic_loops_imp_path loops path_join path_join_path_ends path_reversepath by blast
   1.197 +  show ?thesis
   1.198 +  proof (cases "pathfinish p = pathfinish q")
   1.199 +    case True
   1.200 +    have pipq: "path_image p \<subseteq> S" "path_image q \<subseteq> S"
   1.201 +      by (metis Un_subset_iff paths \<open>path p\<close> \<open>path q\<close> homotopic_loops_imp_subset homotopic_paths_imp_path loops
   1.202 +           path_image_join path_image_reversepath path_imp_reversepath path_join_eq)+
   1.203 +    have "homotopic_paths S p (p +++ (linepath (pathfinish p) (pathfinish p)))"
   1.204 +      using \<open>path p\<close> \<open>path_image p \<subseteq> S\<close> homotopic_paths_rid homotopic_paths_sym by blast
   1.205 +    moreover have "homotopic_paths S (p +++ (linepath (pathfinish p) (pathfinish p))) (p +++ (reversepath q +++ q))"
   1.206 +      by (simp add: True \<open>path p\<close> \<open>path q\<close> pipq homotopic_paths_join homotopic_paths_linv homotopic_paths_sym)
   1.207 +    moreover have "homotopic_paths S (p +++ (reversepath q +++ q)) ((p +++ reversepath q) +++ q)"
   1.208 +      by (simp add: True \<open>path p\<close> \<open>path q\<close> homotopic_paths_assoc pipq)
   1.209 +    moreover have "homotopic_paths S ((p +++ reversepath q) +++ q) (linepath (pathstart p) (pathstart p) +++ q)"
   1.210 +      by (simp add: \<open>path q\<close> homotopic_paths_join paths pipq)
   1.211 +    moreover then have "homotopic_paths S (linepath (pathstart p) (pathstart p) +++ q) q"
   1.212 +      by (metis \<open>path q\<close> homotopic_paths_imp_path homotopic_paths_lid linepath_trivial path_join_path_ends pathfinish_def pipq(2))
   1.213 +    ultimately show ?thesis
   1.214 +      using homotopic_paths_trans by metis
   1.215 +  next
   1.216 +    case False
   1.217 +    then show ?thesis
   1.218 +      using \<open>path q\<close> homotopic_loops_imp_path loops path_join_path_ends by fastforce
   1.219 +  qed
   1.220 +qed
   1.221 +
   1.222  
   1.223  subsection\<open> Homotopy of "nearby" function, paths and loops.\<close>
   1.224