author  wenzelm 
Sat, 14 Sep 2013 23:52:36 +0200  
changeset 53640  3170b5eb9f5a 
parent 53593  a7bcbb5a17d8 
child 56188  0268784f60da 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Path_Connected.thy 
36583  2 
Author: Robert Himmelmann, TU Muenchen 
3 
*) 

4 

5 
header {* Continuous paths and pathconnected sets *} 

6 

7 
theory Path_Connected 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

8 
imports Convex_Euclidean_Space 
36583  9 
begin 
10 

11 
subsection {* Paths. *} 

12 

49653  13 
definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool" 
53640  14 
where "path g \<longleftrightarrow> continuous_on {0..1} g" 
36583  15 

49653  16 
definition pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a" 
36583  17 
where "pathstart g = g 0" 
18 

49653  19 
definition pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a" 
36583  20 
where "pathfinish g = g 1" 
21 

49653  22 
definition path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set" 
36583  23 
where "path_image g = g ` {0 .. 1}" 
24 

53640  25 
definition reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a" 
36583  26 
where "reversepath g = (\<lambda>x. g(1  x))" 
27 

53640  28 
definition joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a" 
36583  29 
(infixr "+++" 75) 
30 
where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x  1))" 

31 

49653  32 
definition simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool" 
36583  33 
where "simple_path g \<longleftrightarrow> 
49653  34 
(\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)" 
36583  35 

49653  36 
definition injective_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool" 
36583  37 
where "injective_path g \<longleftrightarrow> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)" 
38 

49653  39 

36583  40 
subsection {* Some lemmas about these concepts. *} 
41 

49653  42 
lemma injective_imp_simple_path: "injective_path g \<Longrightarrow> simple_path g" 
53640  43 
unfolding injective_path_def simple_path_def 
44 
by auto 

36583  45 

46 
lemma path_image_nonempty: "path_image g \<noteq> {}" 

53640  47 
unfolding path_image_def image_is_empty interval_eq_empty 
48 
by auto 

36583  49 

53640  50 
lemma pathstart_in_path_image[intro]: "pathstart g \<in> path_image g" 
51 
unfolding pathstart_def path_image_def 

52 
by auto 

36583  53 

53640  54 
lemma pathfinish_in_path_image[intro]: "pathfinish g \<in> path_image g" 
55 
unfolding pathfinish_def path_image_def 

56 
by auto 

57 

58 
lemma connected_path_image[intro]: "path g \<Longrightarrow> connected (path_image g)" 

36583  59 
unfolding path_def path_image_def 
60 
apply (erule connected_continuous_image) 

49653  61 
apply (rule convex_connected, rule convex_real_interval) 
62 
done 

36583  63 

53640  64 
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact (path_image g)" 
36583  65 
unfolding path_def path_image_def 
53640  66 
apply (erule compact_continuous_image) 
67 
apply (rule compact_interval) 

68 
done 

36583  69 

53640  70 
lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g" 
71 
unfolding reversepath_def 

72 
by auto 

36583  73 

53640  74 
lemma pathstart_reversepath[simp]: "pathstart (reversepath g) = pathfinish g" 
75 
unfolding pathstart_def reversepath_def pathfinish_def 

76 
by auto 

36583  77 

53640  78 
lemma pathfinish_reversepath[simp]: "pathfinish (reversepath g) = pathstart g" 
79 
unfolding pathstart_def reversepath_def pathfinish_def 

80 
by auto 

36583  81 

49653  82 
lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1" 
53640  83 
unfolding pathstart_def joinpaths_def pathfinish_def 
84 
by auto 

36583  85 

49653  86 
lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2" 
53640  87 
unfolding pathstart_def joinpaths_def pathfinish_def 
88 
by auto 

36583  89 

53640  90 
lemma path_image_reversepath[simp]: "path_image (reversepath g) = path_image g" 
49653  91 
proof  
53640  92 
have *: "\<And>g. path_image (reversepath g) \<subseteq> path_image g" 
49653  93 
unfolding path_image_def subset_eq reversepath_def Ball_def image_iff 
53640  94 
apply rule 
95 
apply rule 

96 
apply (erule bexE) 

97 
apply (rule_tac x="1  xa" in bexI) 

49653  98 
apply auto 
99 
done 

100 
show ?thesis 

101 
using *[of g] *[of "reversepath g"] 

53640  102 
unfolding reversepath_reversepath 
103 
by auto 

49653  104 
qed 
36583  105 

53640  106 
lemma path_reversepath [simp]: "path (reversepath g) \<longleftrightarrow> path g" 
49653  107 
proof  
108 
have *: "\<And>g. path g \<Longrightarrow> path (reversepath g)" 

109 
unfolding path_def reversepath_def 

110 
apply (rule continuous_on_compose[unfolded o_def, of _ "\<lambda>x. 1  x"]) 

111 
apply (intro continuous_on_intros) 

53640  112 
apply (rule continuous_on_subset[of "{0..1}"]) 
113 
apply assumption 

49653  114 
apply auto 
115 
done 

116 
show ?thesis 

117 
using *[of "reversepath g"] *[of g] 

118 
unfolding reversepath_reversepath 

119 
by (rule iffI) 

120 
qed 

121 

122 
lemmas reversepath_simps = 

123 
path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath 

36583  124 

49653  125 
lemma path_join[simp]: 
126 
assumes "pathfinish g1 = pathstart g2" 

127 
shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> path g2" 

128 
unfolding path_def pathfinish_def pathstart_def 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

129 
proof safe 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

130 
assume cont: "continuous_on {0..1} (g1 +++ g2)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

131 
have g1: "continuous_on {0..1} g1 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

132 
by (intro continuous_on_cong refl) (auto simp: joinpaths_def) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

133 
have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))" 
53640  134 
using assms 
135 
by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def) 

136 
show "continuous_on {0..1} g1" and "continuous_on {0..1} g2" 

51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51478
diff
changeset

137 
unfolding g1 g2 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51478
diff
changeset

138 
by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply) 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

139 
next 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

140 
assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

141 
have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}" 
36583  142 
by auto 
53640  143 
{ 
144 
fix x :: real 

145 
assume "0 \<le> x" and "x \<le> 1" 

146 
then have "x \<in> (\<lambda>x. x * 2) ` {0..1 / 2}" 

147 
by (intro image_eqI[where x="x/2"]) auto 

148 
} 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

149 
note 1 = this 
53640  150 
{ 
151 
fix x :: real 

152 
assume "0 \<le> x" and "x \<le> 1" 

153 
then have "x \<in> (\<lambda>x. x * 2  1) ` {1 / 2..1}" 

154 
by (intro image_eqI[where x="x/2 + 1/2"]) auto 

155 
} 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

156 
note 2 = this 
49653  157 
show "continuous_on {0..1} (g1 +++ g2)" 
53640  158 
using assms 
159 
unfolding joinpaths_def 01 

160 
apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros) 

161 
apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) 

162 
done 

49653  163 
qed 
36583  164 

53640  165 
lemma path_image_join_subset: "path_image (g1 +++ g2) \<subseteq> path_image g1 \<union> path_image g2" 
166 
unfolding path_image_def joinpaths_def 

167 
by auto 

36583  168 

169 
lemma subset_path_image_join: 

53640  170 
assumes "path_image g1 \<subseteq> s" 
171 
and "path_image g2 \<subseteq> s" 

172 
shows "path_image (g1 +++ g2) \<subseteq> s" 

173 
using path_image_join_subset[of g1 g2] and assms 

174 
by auto 

36583  175 

176 
lemma path_image_join: 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

177 
assumes "pathfinish g1 = pathstart g2" 
53640  178 
shows "path_image (g1 +++ g2) = path_image g1 \<union> path_image g2" 
179 
apply rule 

180 
apply (rule path_image_join_subset) 

181 
apply rule 

49653  182 
unfolding Un_iff 
183 
proof (erule disjE) 

184 
fix x 

185 
assume "x \<in> path_image g1" 

53640  186 
then obtain y where y: "y \<in> {0..1}" "x = g1 y" 
49653  187 
unfolding path_image_def image_iff by auto 
49654  188 
then show "x \<in> path_image (g1 +++ g2)" 
49653  189 
unfolding joinpaths_def path_image_def image_iff 
190 
apply (rule_tac x="(1/2) *\<^sub>R y" in bexI) 

191 
apply auto 

192 
done 

193 
next 

194 
fix x 

195 
assume "x \<in> path_image g2" 

53640  196 
then obtain y where y: "y \<in> {0..1}" "x = g2 y" 
49653  197 
unfolding path_image_def image_iff by auto 
198 
then show "x \<in> path_image (g1 +++ g2)" 

199 
unfolding joinpaths_def path_image_def image_iff 

53640  200 
apply (rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
50935
diff
changeset

201 
using assms(1)[unfolded pathfinish_def pathstart_def] 
53640  202 
apply (auto simp add: add_divide_distrib) 
49653  203 
done 
204 
qed 

36583  205 

206 
lemma not_in_path_image_join: 

53640  207 
assumes "x \<notin> path_image g1" 
208 
and "x \<notin> path_image g2" 

209 
shows "x \<notin> path_image (g1 +++ g2)" 

210 
using assms and path_image_join_subset[of g1 g2] 

211 
by auto 

36583  212 

49653  213 
lemma simple_path_reversepath: 
214 
assumes "simple_path g" 

215 
shows "simple_path (reversepath g)" 

216 
using assms 

217 
unfolding simple_path_def reversepath_def 

218 
apply  

219 
apply (rule ballI)+ 

53640  220 
apply (erule_tac x="1x" in ballE) 
221 
apply (erule_tac x="1y" in ballE) 

49653  222 
apply auto 
223 
done 

36583  224 

225 
lemma simple_path_join_loop: 

53640  226 
assumes "injective_path g1" 
227 
and "injective_path g2" 

228 
and "pathfinish g2 = pathstart g1" 

229 
and "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}" 

230 
shows "simple_path (g1 +++ g2)" 

49653  231 
unfolding simple_path_def 
53640  232 
proof (intro ballI impI) 
49653  233 
let ?g = "g1 +++ g2" 
36583  234 
note inj = assms(1,2)[unfolded injective_path_def, rule_format] 
49653  235 
fix x y :: real 
236 
assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "?g x = ?g y" 

237 
show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" 

53640  238 
proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) 
49653  239 
assume as: "x \<le> 1 / 2" "y \<le> 1 / 2" 
49654  240 
then have "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" 
53640  241 
using xy(3) 
242 
unfolding joinpaths_def 

243 
by auto 

244 
moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" 

245 
using xy(1,2) as 

36583  246 
by auto 
53640  247 
ultimately show ?thesis 
248 
using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] 

249 
by auto 

49653  250 
next 
53640  251 
assume as: "x > 1 / 2" "y > 1 / 2" 
49654  252 
then have "g2 (2 *\<^sub>R x  1) = g2 (2 *\<^sub>R y  1)" 
53640  253 
using xy(3) 
254 
unfolding joinpaths_def 

255 
by auto 

256 
moreover have "2 *\<^sub>R x  1 \<in> {0..1}" "2 *\<^sub>R y  1 \<in> {0..1}" 

257 
using xy(1,2) as 

258 
by auto 

259 
ultimately show ?thesis 

260 
using inj(2)[of "2*\<^sub>R x  1" "2*\<^sub>R y  1"] by auto 

49653  261 
next 
53640  262 
assume as: "x \<le> 1 / 2" "y > 1 / 2" 
49654  263 
then have "?g x \<in> path_image g1" "?g y \<in> path_image g2" 
49653  264 
unfolding path_image_def joinpaths_def 
36583  265 
using xy(1,2) by auto 
53640  266 
moreover have "?g y \<noteq> pathstart g2" 
267 
using as(2) 

268 
unfolding pathstart_def joinpaths_def 

36583  269 
using inj(2)[of "2 *\<^sub>R y  1" 0] and xy(2) 
270 
by (auto simp add: field_simps) 

53640  271 
ultimately have *: "?g x = pathstart g1" 
272 
using assms(4) 

273 
unfolding xy(3) 

274 
by auto 

275 
then have "x = 0" 

276 
unfolding pathstart_def joinpaths_def 

277 
using as(1) and xy(1) 

278 
using inj(1)[of "2 *\<^sub>R x" 0] 

279 
by auto 

280 
moreover have "y = 1" 

281 
using * 

282 
unfolding xy(3) assms(3)[symmetric] 

283 
unfolding joinpaths_def pathfinish_def 

284 
using as(2) and xy(2) 

285 
using inj(2)[of "2 *\<^sub>R y  1" 1] 

286 
by auto 

287 
ultimately show ?thesis 

288 
by auto 

49653  289 
next 
290 
assume as: "x > 1 / 2" "y \<le> 1 / 2" 

53640  291 
then have "?g x \<in> path_image g2" and "?g y \<in> path_image g1" 
49653  292 
unfolding path_image_def joinpaths_def 
36583  293 
using xy(1,2) by auto 
53640  294 
moreover have "?g x \<noteq> pathstart g2" 
295 
using as(1) 

296 
unfolding pathstart_def joinpaths_def 

36583  297 
using inj(2)[of "2 *\<^sub>R x  1" 0] and xy(1) 
298 
by (auto simp add: field_simps) 

53640  299 
ultimately have *: "?g y = pathstart g1" 
300 
using assms(4) 

301 
unfolding xy(3) 

302 
by auto 

303 
then have "y = 0" 

304 
unfolding pathstart_def joinpaths_def 

305 
using as(2) and xy(2) 

306 
using inj(1)[of "2 *\<^sub>R y" 0] 

307 
by auto 

308 
moreover have "x = 1" 

309 
using * 

310 
unfolding xy(3)[symmetric] assms(3)[symmetric] 

36583  311 
unfolding joinpaths_def pathfinish_def using as(1) and xy(1) 
53640  312 
using inj(2)[of "2 *\<^sub>R x  1" 1] 
313 
by auto 

314 
ultimately show ?thesis 

315 
by auto 

49653  316 
qed 
317 
qed 

36583  318 

319 
lemma injective_path_join: 

53640  320 
assumes "injective_path g1" 
321 
and "injective_path g2" 

322 
and "pathfinish g1 = pathstart g2" 

323 
and "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}" 

324 
shows "injective_path (g1 +++ g2)" 

49653  325 
unfolding injective_path_def 
326 
proof (rule, rule, rule) 

327 
let ?g = "g1 +++ g2" 

36583  328 
note inj = assms(1,2)[unfolded injective_path_def, rule_format] 
49653  329 
fix x y 
330 
assume xy: "x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" 

331 
show "x = y" 

332 
proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le) 

53640  333 
assume "x \<le> 1 / 2" and "y \<le> 1 / 2" 
334 
then show ?thesis 

335 
using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy 

36583  336 
unfolding joinpaths_def by auto 
49653  337 
next 
53640  338 
assume "x > 1 / 2" and "y > 1 / 2" 
339 
then show ?thesis 

340 
using inj(2)[of "2*\<^sub>R x  1" "2*\<^sub>R y  1"] and xy 

36583  341 
unfolding joinpaths_def by auto 
49653  342 
next 
343 
assume as: "x \<le> 1 / 2" "y > 1 / 2" 

53640  344 
then have "?g x \<in> path_image g1" and "?g y \<in> path_image g2" 
49653  345 
unfolding path_image_def joinpaths_def 
53640  346 
using xy(1,2) 
347 
by auto 

348 
then have "?g x = pathfinish g1" and "?g y = pathstart g2" 

349 
using assms(4) 

350 
unfolding assms(3) xy(3) 

351 
by auto 

49654  352 
then show ?thesis 
49653  353 
using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y  1" 0] and xy(1,2) 
36583  354 
unfolding pathstart_def pathfinish_def joinpaths_def 
355 
by auto 

49653  356 
next 
53640  357 
assume as:"x > 1 / 2" "y \<le> 1 / 2" 
358 
then have "?g x \<in> path_image g2" and "?g y \<in> path_image g1" 

49653  359 
unfolding path_image_def joinpaths_def 
53640  360 
using xy(1,2) 
361 
by auto 

362 
then have "?g x = pathstart g2" and "?g y = pathfinish g1" 

363 
using assms(4) 

364 
unfolding assms(3) xy(3) 

365 
by auto 

49654  366 
then show ?thesis using as and inj(2)[of "2 *\<^sub>R x  1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2) 
36583  367 
unfolding pathstart_def pathfinish_def joinpaths_def 
49653  368 
by auto 
369 
qed 

370 
qed 

36583  371 

372 
lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join 

53640  373 

49653  374 

53640  375 
subsection {* Reparametrizing a closed curve to start at some chosen point *} 
36583  376 

53640  377 
definition shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a" 
378 
where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x  1))" 

36583  379 

53640  380 
lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a" 
36583  381 
unfolding pathstart_def shiftpath_def by auto 
382 

49653  383 
lemma pathfinish_shiftpath: 
53640  384 
assumes "0 \<le> a" 
385 
and "pathfinish g = pathstart g" 

386 
shows "pathfinish (shiftpath a g) = g a" 

387 
using assms 

388 
unfolding pathstart_def pathfinish_def shiftpath_def 

36583  389 
by auto 
390 

391 
lemma endpoints_shiftpath: 

53640  392 
assumes "pathfinish g = pathstart g" 
393 
and "a \<in> {0 .. 1}" 

394 
shows "pathfinish (shiftpath a g) = g a" 

395 
and "pathstart (shiftpath a g) = g a" 

396 
using assms 

397 
by (auto intro!: pathfinish_shiftpath pathstart_shiftpath) 

36583  398 

399 
lemma closed_shiftpath: 

53640  400 
assumes "pathfinish g = pathstart g" 
401 
and "a \<in> {0..1}" 

402 
shows "pathfinish (shiftpath a g) = pathstart (shiftpath a g)" 

403 
using endpoints_shiftpath[OF assms] 

404 
by auto 

36583  405 

406 
lemma path_shiftpath: 

53640  407 
assumes "path g" 
408 
and "pathfinish g = pathstart g" 

409 
and "a \<in> {0..1}" 

410 
shows "path (shiftpath a g)" 

49653  411 
proof  
53640  412 
have *: "{0 .. 1} = {0 .. 1a} \<union> {1a .. 1}" 
413 
using assms(3) by auto 

49653  414 
have **: "\<And>x. x + a = 1 \<Longrightarrow> g (x + a  1) = g (x + a)" 
53640  415 
using assms(2)[unfolded pathfinish_def pathstart_def] 
416 
by auto 

49653  417 
show ?thesis 
418 
unfolding path_def shiftpath_def * 

419 
apply (rule continuous_on_union) 

420 
apply (rule closed_real_atLeastAtMost)+ 

53640  421 
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) 
422 
prefer 3 

423 
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a  1 + x)"]) 

424 
defer 

425 
prefer 3 

426 
apply (rule continuous_on_intros)+ 

427 
prefer 2 

49653  428 
apply (rule continuous_on_intros)+ 
429 
apply (rule_tac[12] continuous_on_subset[OF assms(1)[unfolded path_def]]) 

430 
using assms(3) and ** 

53640  431 
apply auto 
432 
apply (auto simp add: field_simps) 

49653  433 
done 
434 
qed 

36583  435 

49653  436 
lemma shiftpath_shiftpath: 
53640  437 
assumes "pathfinish g = pathstart g" 
438 
and "a \<in> {0..1}" 

439 
and "x \<in> {0..1}" 

36583  440 
shows "shiftpath (1  a) (shiftpath a g) x = g x" 
53640  441 
using assms 
442 
unfolding pathfinish_def pathstart_def shiftpath_def 

443 
by auto 

36583  444 

445 
lemma path_image_shiftpath: 

53640  446 
assumes "a \<in> {0..1}" 
447 
and "pathfinish g = pathstart g" 

448 
shows "path_image (shiftpath a g) = path_image g" 

49653  449 
proof  
450 
{ fix x 

53640  451 
assume as: "g 1 = g 0" "x \<in> {0..1::real}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1}. g x \<noteq> g (a + y  1)" 
49654  452 
then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)" 
49653  453 
proof (cases "a \<le> x") 
454 
case False 

49654  455 
then show ?thesis 
49653  456 
apply (rule_tac x="1 + x  a" in bexI) 
36583  457 
using as(1,2) and as(3)[THEN bspec[where x="1 + x  a"]] and assms(1) 
49653  458 
apply (auto simp add: field_simps atomize_not) 
459 
done 

460 
next 

461 
case True 

53640  462 
then show ?thesis 
463 
using as(12) and assms(1) 

464 
apply (rule_tac x="x  a" in bexI) 

465 
apply (auto simp add: field_simps) 

466 
done 

49653  467 
qed 
468 
} 

49654  469 
then show ?thesis 
53640  470 
using assms 
471 
unfolding shiftpath_def path_image_def pathfinish_def pathstart_def 

472 
by (auto simp add: image_iff) 

49653  473 
qed 
474 

36583  475 

53640  476 
subsection {* Special case of straightline paths *} 
36583  477 

49653  478 
definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a" 
479 
where "linepath a b = (\<lambda>x. (1  x) *\<^sub>R a + x *\<^sub>R b)" 

36583  480 

53640  481 
lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a" 
482 
unfolding pathstart_def linepath_def 

483 
by auto 

36583  484 

53640  485 
lemma pathfinish_linepath[simp]: "pathfinish (linepath a b) = b" 
486 
unfolding pathfinish_def linepath_def 

487 
by auto 

36583  488 

489 
lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" 

53640  490 
unfolding linepath_def 
491 
by (intro continuous_intros) 

36583  492 

493 
lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" 

53640  494 
using continuous_linepath_at 
495 
by (auto intro!: continuous_at_imp_continuous_on) 

36583  496 

53640  497 
lemma path_linepath[intro]: "path (linepath a b)" 
498 
unfolding path_def 

499 
by (rule continuous_on_linepath) 

36583  500 

53640  501 
lemma path_image_linepath[simp]: "path_image (linepath a b) = closed_segment a b" 
49653  502 
unfolding path_image_def segment linepath_def 
53640  503 
apply (rule set_eqI) 
504 
apply rule 

505 
defer 

49653  506 
unfolding mem_Collect_eq image_iff 
53640  507 
apply (erule exE) 
508 
apply (rule_tac x="u *\<^sub>R 1" in bexI) 

49653  509 
apply auto 
510 
done 

511 

53640  512 
lemma reversepath_linepath[simp]: "reversepath (linepath a b) = linepath b a" 
49653  513 
unfolding reversepath_def linepath_def 
36583  514 
by auto 
515 

516 
lemma injective_path_linepath: 

49653  517 
assumes "a \<noteq> b" 
518 
shows "injective_path (linepath a b)" 

36583  519 
proof  
53640  520 
{ 
521 
fix x y :: "real" 

36583  522 
assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" 
53640  523 
then have "(x  y) *\<^sub>R a = (x  y) *\<^sub>R b" 
524 
by (simp add: algebra_simps) 

525 
with assms have "x = y" 

526 
by simp 

527 
} 

49654  528 
then show ?thesis 
49653  529 
unfolding injective_path_def linepath_def 
530 
by (auto simp add: algebra_simps) 

531 
qed 

36583  532 

53640  533 
lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path (linepath a b)" 
534 
by (auto intro!: injective_imp_simple_path injective_path_linepath) 

49653  535 

36583  536 

53640  537 
subsection {* Bounding a point away from a path *} 
36583  538 

539 
lemma not_on_path_ball: 

540 
fixes g :: "real \<Rightarrow> 'a::heine_borel" 

53640  541 
assumes "path g" 
542 
and "z \<notin> path_image g" 

543 
shows "\<exists>e > 0. ball z e \<inter> path_image g = {}" 

49653  544 
proof  
545 
obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y" 

36583  546 
using distance_attains_inf[OF _ path_image_nonempty, of g z] 
547 
using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto 

49654  548 
then show ?thesis 
49653  549 
apply (rule_tac x="dist z a" in exI) 
550 
using assms(2) 

551 
apply (auto intro!: dist_pos_lt) 

552 
done 

553 
qed 

36583  554 

555 
lemma not_on_path_cball: 

556 
fixes g :: "real \<Rightarrow> 'a::heine_borel" 

53640  557 
assumes "path g" 
558 
and "z \<notin> path_image g" 

49653  559 
shows "\<exists>e>0. cball z e \<inter> (path_image g) = {}" 
560 
proof  

53640  561 
obtain e where "ball z e \<inter> path_image g = {}" "e > 0" 
49653  562 
using not_on_path_ball[OF assms] by auto 
53640  563 
moreover have "cball z (e/2) \<subseteq> ball z e" 
564 
using `e > 0` by auto 

565 
ultimately show ?thesis 

566 
apply (rule_tac x="e/2" in exI) 

567 
apply auto 

568 
done 

49653  569 
qed 
570 

36583  571 

53640  572 
subsection {* Path component, considered as a "joinability" relation (from Tom Hales) *} 
36583  573 

49653  574 
definition "path_component s x y \<longleftrightarrow> 
575 
(\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)" 

36583  576 

53640  577 
lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def 
36583  578 

49653  579 
lemma path_component_mem: 
580 
assumes "path_component s x y" 

53640  581 
shows "x \<in> s" and "y \<in> s" 
582 
using assms 

583 
unfolding path_defs 

584 
by auto 

36583  585 

49653  586 
lemma path_component_refl: 
587 
assumes "x \<in> s" 

588 
shows "path_component s x x" 

589 
unfolding path_defs 

590 
apply (rule_tac x="\<lambda>u. x" in exI) 

53640  591 
using assms 
592 
apply (auto intro!: continuous_on_intros) 

593 
done 

36583  594 

595 
lemma path_component_refl_eq: "path_component s x x \<longleftrightarrow> x \<in> s" 

49653  596 
by (auto intro!: path_component_mem path_component_refl) 
36583  597 

598 
lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x" 

49653  599 
using assms 
600 
unfolding path_component_def 

601 
apply (erule exE) 

602 
apply (rule_tac x="reversepath g" in exI) 

603 
apply auto 

604 
done 

36583  605 

49653  606 
lemma path_component_trans: 
53640  607 
assumes "path_component s x y" 
608 
and "path_component s y z" 

49653  609 
shows "path_component s x z" 
610 
using assms 

611 
unfolding path_component_def 

53640  612 
apply (elim exE) 
49653  613 
apply (rule_tac x="g +++ ga" in exI) 
614 
apply (auto simp add: path_image_join) 

615 
done 

36583  616 

53640  617 
lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y" 
36583  618 
unfolding path_component_def by auto 
619 

49653  620 

53640  621 
text {* Can also consider it as a set, as the name suggests. *} 
36583  622 

49653  623 
lemma path_component_set: 
624 
"{y. path_component s x y} = 

625 
{y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)}" 

626 
apply (rule set_eqI) 

627 
unfolding mem_Collect_eq 

628 
unfolding path_component_def 

629 
apply auto 

630 
done 

36583  631 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
41959
diff
changeset

632 
lemma path_component_subset: "{y. path_component s x y} \<subseteq> s" 
53640  633 
apply rule 
634 
apply (rule path_component_mem(2)) 

49653  635 
apply auto 
636 
done 

36583  637 

44170
510ac30f44c0
make Multivariate_Analysis work with separate set type
huffman
parents:
41959
diff
changeset

638 
lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s" 
49653  639 
apply rule 
53640  640 
apply (drule equals0D[of _ x]) 
641 
defer 

49653  642 
apply (rule equals0I) 
643 
unfolding mem_Collect_eq 

644 
apply (drule path_component_mem(1)) 

645 
using path_component_refl 

646 
apply auto 

647 
done 

648 

36583  649 

53640  650 
subsection {* Path connectedness of a space *} 
36583  651 

49653  652 
definition "path_connected s \<longleftrightarrow> 
53640  653 
(\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)" 
36583  654 

655 
lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)" 

656 
unfolding path_connected_def path_component_def by auto 

657 

53640  658 
lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)" 
49653  659 
unfolding path_connected_component 
53640  660 
apply rule 
661 
apply rule 

662 
apply rule 

663 
apply (rule path_component_subset) 

49653  664 
unfolding subset_eq mem_Collect_eq Ball_def 
665 
apply auto 

666 
done 

667 

36583  668 

53640  669 
subsection {* Some useful lemmas about pathconnectedness *} 
36583  670 

671 
lemma convex_imp_path_connected: 

672 
fixes s :: "'a::real_normed_vector set" 

53640  673 
assumes "convex s" 
674 
shows "path_connected s" 

49653  675 
unfolding path_connected_def 
53640  676 
apply rule 
677 
apply rule 

678 
apply (rule_tac x = "linepath x y" in exI) 

49653  679 
unfolding path_image_linepath 
680 
using assms [unfolded convex_contains_segment] 

681 
apply auto 

682 
done 

36583  683 

49653  684 
lemma path_connected_imp_connected: 
685 
assumes "path_connected s" 

686 
shows "connected s" 

687 
unfolding connected_def not_ex 

53640  688 
apply rule 
689 
apply rule 

690 
apply (rule ccontr) 

49653  691 
unfolding not_not 
53640  692 
apply (elim conjE) 
49653  693 
proof  
694 
fix e1 e2 

695 
assume as: "open e1" "open e2" "s \<subseteq> e1 \<union> e2" "e1 \<inter> e2 \<inter> s = {}" "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}" 

53640  696 
then obtain x1 x2 where obt:"x1 \<in> e1 \<inter> s" "x2 \<in> e2 \<inter> s" 
697 
by auto 

698 
then obtain g where g: "path g" "path_image g \<subseteq> s" "pathstart g = x1" "pathfinish g = x2" 

36583  699 
using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto 
49653  700 
have *: "connected {0..1::real}" 
701 
by (auto intro!: convex_connected convex_real_interval) 

702 
have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}" 

703 
using as(3) g(2)[unfolded path_defs] by blast 

704 
moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}" 

53640  705 
using as(4) g(2)[unfolded path_defs] 
706 
unfolding subset_eq 

707 
by auto 

49653  708 
moreover have "{x \<in> {0..1}. g x \<in> e1} \<noteq> {} \<and> {x \<in> {0..1}. g x \<in> e2} \<noteq> {}" 
53640  709 
using g(3,4)[unfolded path_defs] 
710 
using obt 

36583  711 
by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) 
49653  712 
ultimately show False 
53640  713 
using *[unfolded connected_local not_ex, rule_format, 
714 
of "{x\<in>{0..1}. g x \<in> e1}" "{x\<in>{0..1}. g x \<in> e2}"] 

36583  715 
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] 
49653  716 
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] 
717 
by auto 

718 
qed 

36583  719 

720 
lemma open_path_component: 

53593  721 
fixes s :: "'a::real_normed_vector set" 
49653  722 
assumes "open s" 
723 
shows "open {y. path_component s x y}" 

724 
unfolding open_contains_ball 

725 
proof 

726 
fix y 

727 
assume as: "y \<in> {y. path_component s x y}" 

49654  728 
then have "y \<in> s" 
49653  729 
apply  
730 
apply (rule path_component_mem(2)) 

731 
unfolding mem_Collect_eq 

732 
apply auto 

733 
done 

53640  734 
then obtain e where e: "e > 0" "ball y e \<subseteq> s" 
735 
using assms[unfolded open_contains_ball] 

736 
by auto 

49653  737 
show "\<exists>e > 0. ball y e \<subseteq> {y. path_component s x y}" 
738 
apply (rule_tac x=e in exI) 

53640  739 
apply (rule,rule `e>0`) 
740 
apply rule 

49653  741 
unfolding mem_ball mem_Collect_eq 
742 
proof  

743 
fix z 

744 
assume "dist y z < e" 

49654  745 
then show "path_component s x z" 
53640  746 
apply (rule_tac path_component_trans[of _ _ y]) 
747 
defer 

49653  748 
apply (rule path_component_of_subset[OF e(2)]) 
749 
apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) 

53640  750 
using `e > 0` as 
49653  751 
apply auto 
752 
done 

753 
qed 

754 
qed 

36583  755 

756 
lemma open_non_path_component: 

53593  757 
fixes s :: "'a::real_normed_vector set" 
49653  758 
assumes "open s" 
53640  759 
shows "open (s  {y. path_component s x y})" 
49653  760 
unfolding open_contains_ball 
761 
proof 

762 
fix y 

53640  763 
assume as: "y \<in> s  {y. path_component s x y}" 
764 
then obtain e where e: "e > 0" "ball y e \<subseteq> s" 

765 
using assms [unfolded open_contains_ball] 

766 
by auto 

49653  767 
show "\<exists>e>0. ball y e \<subseteq> s  {y. path_component s x y}" 
768 
apply (rule_tac x=e in exI) 

53640  769 
apply rule 
770 
apply (rule `e>0`) 

771 
apply rule 

772 
apply rule 

773 
defer 

49653  774 
proof (rule ccontr) 
775 
fix z 

776 
assume "z \<in> ball y e" "\<not> z \<notin> {y. path_component s x y}" 

49654  777 
then have "y \<in> {y. path_component s x y}" 
49653  778 
unfolding not_not mem_Collect_eq using `e>0` 
779 
apply  

780 
apply (rule path_component_trans, assumption) 

781 
apply (rule path_component_of_subset[OF e(2)]) 

782 
apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) 

783 
apply auto 

784 
done 

53640  785 
then show False 
786 
using as by auto 

49653  787 
qed (insert e(2), auto) 
788 
qed 

36583  789 

790 
lemma connected_open_path_connected: 

53593  791 
fixes s :: "'a::real_normed_vector set" 
53640  792 
assumes "open s" 
793 
and "connected s" 

49653  794 
shows "path_connected s" 
795 
unfolding path_connected_component_set 

796 
proof (rule, rule, rule path_component_subset, rule) 

797 
fix x y 

53640  798 
assume "x \<in> s" and "y \<in> s" 
49653  799 
show "y \<in> {y. path_component s x y}" 
800 
proof (rule ccontr) 

53640  801 
assume "\<not> ?thesis" 
802 
moreover have "{y. path_component s x y} \<inter> s \<noteq> {}" 

803 
using `x \<in> s` path_component_eq_empty path_component_subset[of s x] 

804 
by auto 

49653  805 
ultimately 
806 
show False 

53640  807 
using `y \<in> s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] 
808 
using assms(2)[unfolded connected_def not_ex, rule_format, 

809 
of"{y. path_component s x y}" "s  {y. path_component s x y}"] 

49653  810 
by auto 
811 
qed 

812 
qed 

36583  813 

814 
lemma path_connected_continuous_image: 

53640  815 
assumes "continuous_on s f" 
816 
and "path_connected s" 

49653  817 
shows "path_connected (f ` s)" 
818 
unfolding path_connected_def 

819 
proof (rule, rule) 

820 
fix x' y' 

821 
assume "x' \<in> f ` s" "y' \<in> f ` s" 

53640  822 
then obtain x y where x: "x \<in> s" and y: "y \<in> s" and x': "x' = f x" and y': "y' = f y" 
823 
by auto 

824 
from x y obtain g where "path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y" 

825 
using assms(2)[unfolded path_connected_def] by fast 

49654  826 
then show "\<exists>g. path g \<and> path_image g \<subseteq> f ` s \<and> pathstart g = x' \<and> pathfinish g = y'" 
53640  827 
unfolding x' y' 
49653  828 
apply (rule_tac x="f \<circ> g" in exI) 
829 
unfolding path_defs 

51481
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51478
diff
changeset

830 
apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)]) 
ef949192e5d6
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents:
51478
diff
changeset

831 
apply auto 
49653  832 
done 
833 
qed 

36583  834 

835 
lemma homeomorphic_path_connectedness: 

53640  836 
"s homeomorphic t \<Longrightarrow> path_connected s \<longleftrightarrow> path_connected t" 
49653  837 
unfolding homeomorphic_def homeomorphism_def 
53640  838 
apply (erule exEerule conjE)+ 
49653  839 
apply rule 
53640  840 
apply (drule_tac f=f in path_connected_continuous_image) 
841 
prefer 3 

49653  842 
apply (drule_tac f=g in path_connected_continuous_image) 
843 
apply auto 

844 
done 

36583  845 

846 
lemma path_connected_empty: "path_connected {}" 

847 
unfolding path_connected_def by auto 

848 

849 
lemma path_connected_singleton: "path_connected {a}" 

850 
unfolding path_connected_def pathstart_def pathfinish_def path_image_def 

53640  851 
apply clarify 
852 
apply (rule_tac x="\<lambda>x. a" in exI) 

853 
apply (simp add: image_constant_conv) 

36583  854 
apply (simp add: path_def continuous_on_const) 
855 
done 

856 

49653  857 
lemma path_connected_Un: 
53640  858 
assumes "path_connected s" 
859 
and "path_connected t" 

860 
and "s \<inter> t \<noteq> {}" 

49653  861 
shows "path_connected (s \<union> t)" 
862 
unfolding path_connected_component 

863 
proof (rule, rule) 

864 
fix x y 

865 
assume as: "x \<in> s \<union> t" "y \<in> s \<union> t" 

53640  866 
from assms(3) obtain z where "z \<in> s \<inter> t" 
867 
by auto 

49654  868 
then show "path_component (s \<union> t) x y" 
49653  869 
using as and assms(12)[unfolded path_connected_component] 
53640  870 
apply  
49653  871 
apply (erule_tac[!] UnE)+ 
872 
apply (rule_tac[23] path_component_trans[of _ _ z]) 

873 
apply (auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) 

874 
done 

875 
qed 

36583  876 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

877 
lemma path_connected_UNION: 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

878 
assumes "\<And>i. i \<in> A \<Longrightarrow> path_connected (S i)" 
49653  879 
and "\<And>i. i \<in> A \<Longrightarrow> z \<in> S i" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

880 
shows "path_connected (\<Union>i\<in>A. S i)" 
49653  881 
unfolding path_connected_component 
882 
proof clarify 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

883 
fix x i y j 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

884 
assume *: "i \<in> A" "x \<in> S i" "j \<in> A" "y \<in> S j" 
49654  885 
then have "path_component (S i) x z" and "path_component (S j) z y" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

886 
using assms by (simp_all add: path_connected_component) 
49654  887 
then have "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y" 
48125
602dc0215954
tuned proofs  prefer direct "rotated" instead of oldstyle COMP;
wenzelm
parents:
44647
diff
changeset

888 
using *(1,3) by (auto elim!: path_component_of_subset [rotated]) 
49654  889 
then show "path_component (\<Union>i\<in>A. S i) x y" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

890 
by (rule path_component_trans) 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

891 
qed 
36583  892 

49653  893 

53640  894 
subsection {* Sphere is pathconnected *} 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36583
diff
changeset

895 

36583  896 
lemma path_connected_punctured_universe: 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

897 
assumes "2 \<le> DIM('a::euclidean_space)" 
53640  898 
shows "path_connected ((UNIV::'a set)  {a})" 
49653  899 
proof  
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

900 
let ?A = "{x::'a. \<exists>i\<in>Basis. x \<bullet> i < a \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

901 
let ?B = "{x::'a. \<exists>i\<in>Basis. a \<bullet> i < x \<bullet> i}" 
36583  902 

49653  903 
have A: "path_connected ?A" 
904 
unfolding Collect_bex_eq 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

905 
proof (rule path_connected_UNION) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

906 
fix i :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

907 
assume "i \<in> Basis" 
53640  908 
then show "(\<Sum>i\<in>Basis. (a \<bullet> i  1)*\<^sub>R i) \<in> {x::'a. x \<bullet> i < a \<bullet> i}" 
909 
by simp 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

910 
show "path_connected {x. x \<bullet> i < a \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

911 
using convex_imp_path_connected [OF convex_halfspace_lt, of i "a \<bullet> i"] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

912 
by (simp add: inner_commute) 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

913 
qed 
53640  914 
have B: "path_connected ?B" 
915 
unfolding Collect_bex_eq 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

916 
proof (rule path_connected_UNION) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

917 
fix i :: 'a 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

918 
assume "i \<in> Basis" 
53640  919 
then show "(\<Sum>i\<in>Basis. (a \<bullet> i + 1) *\<^sub>R i) \<in> {x::'a. a \<bullet> i < x \<bullet> i}" 
920 
by simp 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

921 
show "path_connected {x. a \<bullet> i < x \<bullet> i}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

922 
using convex_imp_path_connected [OF convex_halfspace_gt, of "a \<bullet> i" i] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

923 
by (simp add: inner_commute) 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

924 
qed 
53640  925 
obtain S :: "'a set" where "S \<subseteq> Basis" and "card S = Suc (Suc 0)" 
926 
using ex_card[OF assms] 

927 
by auto 

928 
then obtain b0 b1 :: 'a where "b0 \<in> Basis" and "b1 \<in> Basis" and "b0 \<noteq> b1" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

929 
unfolding card_Suc_eq by auto 
53640  930 
then have "a + b0  b1 \<in> ?A \<inter> ?B" 
931 
by (auto simp: inner_simps inner_Basis) 

932 
then have "?A \<inter> ?B \<noteq> {}" 

933 
by fast 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

934 
with A B have "path_connected (?A \<union> ?B)" 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

935 
by (rule path_connected_Un) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49654
diff
changeset

936 
also have "?A \<union> ?B = {x. \<exists>i\<in>Basis. x \<bullet> i \<noteq> a \<bullet> i}" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

937 
unfolding neq_iff bex_disj_distrib Collect_disj_eq .. 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

938 
also have "\<dots> = {x. x \<noteq> a}" 
53640  939 
unfolding euclidean_eq_iff [where 'a='a] 
940 
by (simp add: Bex_def) 

941 
also have "\<dots> = UNIV  {a}" 

942 
by auto 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

943 
finally show ?thesis . 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

944 
qed 
36583  945 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

946 
lemma path_connected_sphere: 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

947 
assumes "2 \<le> DIM('a::euclidean_space)" 
53640  948 
shows "path_connected {x::'a. norm (x  a) = r}" 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

949 
proof (rule linorder_cases [of r 0]) 
49653  950 
assume "r < 0" 
53640  951 
then have "{x::'a. norm(x  a) = r} = {}" 
952 
by auto 

953 
then show ?thesis 

954 
using path_connected_empty by simp 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

955 
next 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

956 
assume "r = 0" 
53640  957 
then show ?thesis 
958 
using path_connected_singleton by simp 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

959 
next 
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

960 
assume r: "0 < r" 
53640  961 
have *: "{x::'a. norm(x  a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" 
962 
apply (rule set_eqI) 

963 
apply rule 

49653  964 
unfolding image_iff 
965 
apply (rule_tac x="(1/r) *\<^sub>R (x  a)" in bexI) 

966 
unfolding mem_Collect_eq norm_scaleR 

53640  967 
using r 
49653  968 
apply (auto simp add: scaleR_right_diff_distrib) 
969 
done 

970 
have **: "{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV  {0})" 

53640  971 
apply (rule set_eqI) 
972 
apply rule 

49653  973 
unfolding image_iff 
974 
apply (rule_tac x=x in bexI) 

975 
unfolding mem_Collect_eq 

53640  976 
apply (auto split: split_if_asm) 
49653  977 
done 
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

978 
have "continuous_on (UNIV  {0}) (\<lambda>x::'a. 1 / norm x)" 
53640  979 
unfolding field_divide_inverse 
980 
by (simp add: continuous_on_intros) 

981 
then show ?thesis 

982 
unfolding * ** 

983 
using path_connected_punctured_universe[OF assms] 

49653  984 
by (auto intro!: path_connected_continuous_image continuous_on_intros) 
37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

985 
qed 
36583  986 

53640  987 
lemma connected_sphere: "2 \<le> DIM('a::euclidean_space) \<Longrightarrow> connected {x::'a. norm (x  a) = r}" 
988 
using path_connected_sphere path_connected_imp_connected 

989 
by auto 

36583  990 

991 
end 