author  paulson 
Tue, 26 May 2015 21:58:04 +0100  
changeset 60303  00c06f1315d0 
parent 59557  ebd8ecacfba6 
child 60420  884f54e01427 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Path_Connected.thy 
60303  2 
Author: Robert Himmelmann, TU Muenchen, and LCP with material from HOL Light 
36583  3 
*) 
4 

58877  5 
section {* Continuous paths and pathconnected sets *} 
36583  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 

60303  11 
(*FIXME move up?*) 
12 
lemma image_add_atLeastAtMost [simp]: 

13 
fixes d::"'a::linordered_idom" shows "(op + d ` {a..b}) = {a+d..b+d}" 

14 
apply auto 

15 
apply (rule_tac x="xd" in rev_image_eqI, auto) 

16 
done 

17 

18 
lemma image_diff_atLeastAtMost [simp]: 

19 
fixes d::"'a::linordered_idom" shows "(op  d ` {a..b}) = {db..da}" 

20 
apply auto 

21 
apply (rule_tac x="dx" in rev_image_eqI, auto) 

22 
done 

23 

24 
lemma image_mult_atLeastAtMost [simp]: 

25 
fixes d::"'a::linordered_field" 

26 
assumes "d>0" shows "(op * d ` {a..b}) = {d*a..d*b}" 

27 
using assms 

28 
apply auto 

29 
apply (rule_tac x="x/d" in rev_image_eqI) 

30 
apply (auto simp: field_simps) 

31 
done 

32 

33 
lemma image_affinity_interval: 

34 
fixes c :: "'a::ordered_real_vector" 

35 
shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {} 

36 
else if 0 <= m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} 

37 
else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" 

38 
apply (case_tac "m=0", force) 

39 
apply (auto simp: scaleR_left_mono) 

40 
apply (rule_tac x="inverse m *\<^sub>R (xc)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg) 

41 
apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive) 

42 
apply (rule_tac x="inverse m *\<^sub>R (xc)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq) 

43 
using le_diff_eq scaleR_le_cancel_left_neg 

44 
apply fastforce 

45 
done 

46 

47 
lemma image_affinity_atLeastAtMost: 

48 
fixes c :: "'a::linordered_field" 

49 
shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {} 

50 
else if 0 \<le> m then {m*a + c .. m *b + c} 

51 
else {m*b + c .. m*a + c})" 

52 
apply (case_tac "m=0", auto) 

53 
apply (rule_tac x="inverse m*(xc)" in rev_image_eqI, auto simp: field_simps) 

54 
apply (rule_tac x="inverse m*(xc)" in rev_image_eqI, auto simp: field_simps) 

55 
done 

56 

57 
lemma image_affinity_atLeastAtMost_diff: 

58 
fixes c :: "'a::linordered_field" 

59 
shows "((\<lambda>x. m*x  c) ` {a..b}) = (if {a..b}={} then {} 

60 
else if 0 \<le> m then {m*a  c .. m*b  c} 

61 
else {m*b  c .. m*a  c})" 

62 
using image_affinity_atLeastAtMost [of m "c" a b] 

63 
by simp 

64 

65 
lemma image_affinity_atLeastAtMost_div_diff: 

66 
fixes c :: "'a::linordered_field" 

67 
shows "((\<lambda>x. x/m  c) ` {a..b}) = (if {a..b}={} then {} 

68 
else if 0 \<le> m then {a/m  c .. b/m  c} 

69 
else {b/m  c .. a/m  c})" 

70 
using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] 

71 
by (simp add: field_class.field_divide_inverse algebra_simps) 

72 

73 
lemma closed_segment_real_eq: 

74 
fixes u::real shows "closed_segment u v = (\<lambda>x. (v  u) * x + u) ` {0..1}" 

75 
by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) 

76 

77 
subsection {* Paths and Arcs *} 

36583  78 

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

49653  82 
definition pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a" 
36583  83 
where "pathstart g = g 0" 
84 

49653  85 
definition pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a" 
36583  86 
where "pathfinish g = g 1" 
87 

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

53640  91 
definition reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a" 
36583  92 
where "reversepath g = (\<lambda>x. g(1  x))" 
93 

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

97 

49653  98 
definition simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool" 
36583  99 
where "simple_path g \<longleftrightarrow> 
60303  100 
path g \<and> (\<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  101 

60303  102 
definition arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool" 
103 
where "arc g \<longleftrightarrow> path g \<and> inj_on g {0..1}" 

36583  104 

49653  105 

60303  106 
subsection{*Invariance theorems*} 
107 

108 
lemma path_eq: "path p \<Longrightarrow> (\<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t) \<Longrightarrow> path q" 

109 
using continuous_on_eq path_def by blast 

110 

111 
lemma path_continuous_image: "path g \<Longrightarrow> continuous_on (path_image g) f \<Longrightarrow> path(f o g)" 

112 
unfolding path_def path_image_def 

113 
using continuous_on_compose by blast 

114 

115 
lemma path_translation_eq: 

116 
fixes g :: "real \<Rightarrow> 'a :: real_normed_vector" 

117 
shows "path((\<lambda>x. a + x) o g) = path g" 

118 
proof  

119 
have g: "g = (\<lambda>x. a + x) o ((\<lambda>x. a + x) o g)" 

120 
by (rule ext) simp 

121 
show ?thesis 

122 
unfolding path_def 

123 
apply safe 

124 
apply (subst g) 

125 
apply (rule continuous_on_compose) 

126 
apply (auto intro: continuous_intros) 

127 
done 

128 
qed 

129 

130 
lemma path_linear_image_eq: 

131 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 

132 
assumes "linear f" "inj f" 

133 
shows "path(f o g) = path g" 

134 
proof  

135 
from linear_injective_left_inverse [OF assms] 

136 
obtain h where h: "linear h" "h \<circ> f = id" 

137 
by blast 

138 
then have g: "g = h o (f o g)" 

139 
by (metis comp_assoc id_comp) 

140 
show ?thesis 

141 
unfolding path_def 

142 
using h assms 

143 
by (metis g continuous_on_compose linear_continuous_on linear_conv_bounded_linear) 

144 
qed 

145 

146 
lemma pathstart_translation: "pathstart((\<lambda>x. a + x) o g) = a + pathstart g" 

147 
by (simp add: pathstart_def) 

148 

149 
lemma pathstart_linear_image_eq: "linear f \<Longrightarrow> pathstart(f o g) = f(pathstart g)" 

150 
by (simp add: pathstart_def) 

151 

152 
lemma pathfinish_translation: "pathfinish((\<lambda>x. a + x) o g) = a + pathfinish g" 

153 
by (simp add: pathfinish_def) 

154 

155 
lemma pathfinish_linear_image: "linear f \<Longrightarrow> pathfinish(f o g) = f(pathfinish g)" 

156 
by (simp add: pathfinish_def) 

157 

158 
lemma path_image_translation: "path_image((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) ` (path_image g)" 

159 
by (simp add: image_comp path_image_def) 

160 

161 
lemma path_image_linear_image: "linear f \<Longrightarrow> path_image(f o g) = f ` (path_image g)" 

162 
by (simp add: image_comp path_image_def) 

163 

164 
lemma reversepath_translation: "reversepath((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) o reversepath g" 

165 
by (rule ext) (simp add: reversepath_def) 

36583  166 

60303  167 
lemma reversepath_linear_image: "linear f \<Longrightarrow> reversepath(f o g) = f o reversepath g" 
168 
by (rule ext) (simp add: reversepath_def) 

169 

170 
lemma joinpaths_translation: 

171 
"((\<lambda>x. a + x) o g1) +++ ((\<lambda>x. a + x) o g2) = (\<lambda>x. a + x) o (g1 +++ g2)" 

172 
by (rule ext) (simp add: joinpaths_def) 

173 

174 
lemma joinpaths_linear_image: "linear f \<Longrightarrow> (f o g1) +++ (f o g2) = f o (g1 +++ g2)" 

175 
by (rule ext) (simp add: joinpaths_def) 

176 

177 
lemma simple_path_translation_eq: 

178 
fixes g :: "real \<Rightarrow> 'a::euclidean_space" 

179 
shows "simple_path((\<lambda>x. a + x) o g) = simple_path g" 

180 
by (simp add: simple_path_def path_translation_eq) 

181 

182 
lemma simple_path_linear_image_eq: 

183 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 

184 
assumes "linear f" "inj f" 

185 
shows "simple_path(f o g) = simple_path g" 

186 
using assms inj_on_eq_iff [of f] 

187 
by (auto simp: path_linear_image_eq simple_path_def path_translation_eq) 

188 

189 
lemma arc_translation_eq: 

190 
fixes g :: "real \<Rightarrow> 'a::euclidean_space" 

191 
shows "arc((\<lambda>x. a + x) o g) = arc g" 

192 
by (auto simp: arc_def inj_on_def path_translation_eq) 

193 

194 
lemma arc_linear_image_eq: 

195 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 

196 
assumes "linear f" "inj f" 

197 
shows "arc(f o g) = arc g" 

198 
using assms inj_on_eq_iff [of f] 

199 
by (auto simp: arc_def inj_on_def path_linear_image_eq) 

200 

201 
subsection{*Basic lemmas about paths*} 

202 

203 
lemma arc_imp_simple_path: "arc g \<Longrightarrow> simple_path g" 

204 
by (simp add: arc_def inj_on_def simple_path_def) 

205 

206 
lemma arc_imp_path: "arc g \<Longrightarrow> path g" 

207 
using arc_def by blast 

208 

209 
lemma simple_path_imp_path: "simple_path g \<Longrightarrow> path g" 

210 
using simple_path_def by blast 

211 

212 
lemma simple_path_cases: "simple_path g \<Longrightarrow> arc g \<or> pathfinish g = pathstart g" 

213 
unfolding simple_path_def arc_def inj_on_def pathfinish_def pathstart_def 

214 
by (force) 

215 

216 
lemma simple_path_imp_arc: "simple_path g \<Longrightarrow> pathfinish g \<noteq> pathstart g \<Longrightarrow> arc g" 

217 
using simple_path_cases by auto 

218 

219 
lemma arc_distinct_ends: "arc g \<Longrightarrow> pathfinish g \<noteq> pathstart g" 

220 
unfolding arc_def inj_on_def pathfinish_def pathstart_def 

221 
by fastforce 

222 

223 
lemma arc_simple_path: "arc g \<longleftrightarrow> simple_path g \<and> pathfinish g \<noteq> pathstart g" 

224 
using arc_distinct_ends arc_imp_simple_path simple_path_cases by blast 

225 

226 
lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)" 

227 
by (simp add: arc_simple_path) 

36583  228 

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

56188  230 
unfolding path_image_def image_is_empty box_eq_empty 
53640  231 
by auto 
36583  232 

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

235 
by auto 

36583  236 

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

239 
by auto 

240 

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

36583  242 
unfolding path_def path_image_def 
60303  243 
using connected_continuous_image connected_Icc by blast 
36583  244 

53640  245 
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact (path_image g)" 
36583  246 
unfolding path_def path_image_def 
60303  247 
using compact_continuous_image connected_Icc by blast 
36583  248 

53640  249 
lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g" 
250 
unfolding reversepath_def 

251 
by auto 

36583  252 

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

255 
by auto 

36583  256 

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

259 
by auto 

36583  260 

49653  261 
lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1" 
53640  262 
unfolding pathstart_def joinpaths_def pathfinish_def 
263 
by auto 

36583  264 

49653  265 
lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2" 
53640  266 
unfolding pathstart_def joinpaths_def pathfinish_def 
267 
by auto 

36583  268 

53640  269 
lemma path_image_reversepath[simp]: "path_image (reversepath g) = path_image g" 
49653  270 
proof  
53640  271 
have *: "\<And>g. path_image (reversepath g) \<subseteq> path_image g" 
49653  272 
unfolding path_image_def subset_eq reversepath_def Ball_def image_iff 
60303  273 
by force 
49653  274 
show ?thesis 
275 
using *[of g] *[of "reversepath g"] 

53640  276 
unfolding reversepath_reversepath 
277 
by auto 

49653  278 
qed 
36583  279 

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

283 
unfolding path_def reversepath_def 

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

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56188
diff
changeset

285 
apply (intro continuous_intros) 
53640  286 
apply (rule continuous_on_subset[of "{0..1}"]) 
287 
apply assumption 

49653  288 
apply auto 
289 
done 

290 
show ?thesis 

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

292 
unfolding reversepath_reversepath 

293 
by (rule iffI) 

294 
qed 

295 

60303  296 
lemma arc_reversepath: 
297 
assumes "arc g" shows "arc(reversepath g)" 

298 
proof  

299 
have injg: "inj_on g {0..1}" 

300 
using assms 

301 
by (simp add: arc_def) 

302 
have **: "\<And>x y::real. 1x = 1y \<Longrightarrow> x = y" 

303 
by simp 

304 
show ?thesis 

305 
apply (auto simp: arc_def inj_on_def path_reversepath) 

306 
apply (simp add: arc_imp_path assms) 

307 
apply (rule **) 

308 
apply (rule inj_onD [OF injg]) 

309 
apply (auto simp: reversepath_def) 

310 
done 

311 
qed 

312 

313 
lemma simple_path_reversepath: "simple_path g \<Longrightarrow> simple_path (reversepath g)" 

314 
apply (simp add: simple_path_def) 

315 
apply (force simp: reversepath_def) 

316 
done 

317 

49653  318 
lemmas reversepath_simps = 
319 
path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath 

36583  320 

49653  321 
lemma path_join[simp]: 
322 
assumes "pathfinish g1 = pathstart g2" 

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

324 
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

325 
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

326 
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

327 
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

328 
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

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

332 
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

333 
unfolding g1 g2 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56188
diff
changeset

334 
by (auto intro!: continuous_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

335 
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

336 
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

337 
have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}" 
36583  338 
by auto 
53640  339 
{ 
340 
fix x :: real 

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

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

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

344 
} 

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

345 
note 1 = this 
53640  346 
{ 
347 
fix x :: real 

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

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

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

351 
} 

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

352 
note 2 = this 
49653  353 
show "continuous_on {0..1} (g1 +++ g2)" 
53640  354 
using assms 
355 
unfolding joinpaths_def 01 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56188
diff
changeset

356 
apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_intros) 
53640  357 
apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) 
358 
done 

49653  359 
qed 
36583  360 

60303  361 
section {*Path Images*} 
362 

363 
lemma bounded_path_image: "path g \<Longrightarrow> bounded(path_image g)" 

364 
by (simp add: compact_imp_bounded compact_path_image) 

365 

366 
lemma closed_path_image: 

367 
fixes g :: "real \<Rightarrow> 'a::t2_space" 

368 
shows "path g \<Longrightarrow> closed(path_image g)" 

369 
by (metis compact_path_image compact_imp_closed) 

370 

371 
lemma connected_simple_path_image: "simple_path g \<Longrightarrow> connected(path_image g)" 

372 
by (metis connected_path_image simple_path_imp_path) 

373 

374 
lemma compact_simple_path_image: "simple_path g \<Longrightarrow> compact(path_image g)" 

375 
by (metis compact_path_image simple_path_imp_path) 

376 

377 
lemma bounded_simple_path_image: "simple_path g \<Longrightarrow> bounded(path_image g)" 

378 
by (metis bounded_path_image simple_path_imp_path) 

379 

380 
lemma closed_simple_path_image: 

381 
fixes g :: "real \<Rightarrow> 'a::t2_space" 

382 
shows "simple_path g \<Longrightarrow> closed(path_image g)" 

383 
by (metis closed_path_image simple_path_imp_path) 

384 

385 
lemma connected_arc_image: "arc g \<Longrightarrow> connected(path_image g)" 

386 
by (metis connected_path_image arc_imp_path) 

387 

388 
lemma compact_arc_image: "arc g \<Longrightarrow> compact(path_image g)" 

389 
by (metis compact_path_image arc_imp_path) 

390 

391 
lemma bounded_arc_image: "arc g \<Longrightarrow> bounded(path_image g)" 

392 
by (metis bounded_path_image arc_imp_path) 

393 

394 
lemma closed_arc_image: 

395 
fixes g :: "real \<Rightarrow> 'a::t2_space" 

396 
shows "arc g \<Longrightarrow> closed(path_image g)" 

397 
by (metis closed_path_image arc_imp_path) 

398 

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

401 
by auto 

36583  402 

403 
lemma subset_path_image_join: 

53640  404 
assumes "path_image g1 \<subseteq> s" 
405 
and "path_image g2 \<subseteq> s" 

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

407 
using path_image_join_subset[of g1 g2] and assms 

408 
by auto 

36583  409 

410 
lemma path_image_join: 

60303  411 
"pathfinish g1 = pathstart g2 \<Longrightarrow> path_image(g1 +++ g2) = path_image g1 \<union> path_image g2" 
412 
apply (rule subset_antisym [OF path_image_join_subset]) 

413 
apply (auto simp: pathfinish_def pathstart_def path_image_def joinpaths_def image_def) 

414 
apply (drule sym) 

415 
apply (rule_tac x="xa/2" in bexI, auto) 

416 
apply (rule ccontr) 

417 
apply (drule_tac x="(xa+1)/2" in bspec) 

418 
apply (auto simp: field_simps) 

419 
apply (drule_tac x="1/2" in bspec, auto) 

420 
done 

36583  421 

422 
lemma not_in_path_image_join: 

53640  423 
assumes "x \<notin> path_image g1" 
424 
and "x \<notin> path_image g2" 

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

426 
using assms and path_image_join_subset[of g1 g2] 

427 
by auto 

36583  428 

60303  429 
lemma pathstart_compose: "pathstart(f o p) = f(pathstart p)" 
430 
by (simp add: pathstart_def) 

431 

432 
lemma pathfinish_compose: "pathfinish(f o p) = f(pathfinish p)" 

433 
by (simp add: pathfinish_def) 

434 

435 
lemma path_image_compose: "path_image (f o p) = f ` (path_image p)" 

436 
by (simp add: image_comp path_image_def) 

437 

438 
lemma path_compose_join: "f o (p +++ q) = (f o p) +++ (f o q)" 

439 
by (rule ext) (simp add: joinpaths_def) 

440 

441 
lemma path_compose_reversepath: "f o reversepath p = reversepath(f o p)" 

442 
by (rule ext) (simp add: reversepath_def) 

443 

444 
lemma join_paths_eq: 

445 
"(\<And>t. t \<in> {0..1} \<Longrightarrow> p t = p' t) \<Longrightarrow> 

446 
(\<And>t. t \<in> {0..1} \<Longrightarrow> q t = q' t) 

447 
\<Longrightarrow> t \<in> {0..1} \<Longrightarrow> (p +++ q) t = (p' +++ q') t" 

448 
by (auto simp: joinpaths_def) 

449 

450 
lemma simple_path_inj_on: "simple_path g \<Longrightarrow> inj_on g {0<..<1}" 

451 
by (auto simp: simple_path_def path_image_def inj_on_def less_eq_real_def Ball_def) 

452 

453 

454 
subsection{*Simple paths with the endpoints removed*} 

455 

456 
lemma simple_path_endless: 

457 
"simple_path c \<Longrightarrow> path_image c  {pathstart c,pathfinish c} = c ` {0<..<1}" 

458 
apply (auto simp: simple_path_def path_image_def pathstart_def pathfinish_def Ball_def Bex_def image_def) 

459 
apply (metis eq_iff le_less_linear) 

460 
apply (metis leD linear) 

461 
using less_eq_real_def zero_le_one apply blast 

462 
using less_eq_real_def zero_le_one apply blast 

49653  463 
done 
36583  464 

60303  465 
lemma connected_simple_path_endless: 
466 
"simple_path c \<Longrightarrow> connected(path_image c  {pathstart c,pathfinish c})" 

467 
apply (simp add: simple_path_endless) 

468 
apply (rule connected_continuous_image) 

469 
apply (meson continuous_on_subset greaterThanLessThan_subseteq_atLeastAtMost_iff le_numeral_extra(3) le_numeral_extra(4) path_def simple_path_imp_path) 

470 
by auto 

471 

472 
lemma nonempty_simple_path_endless: 

473 
"simple_path c \<Longrightarrow> path_image c  {pathstart c,pathfinish c} \<noteq> {}" 

474 
by (simp add: simple_path_endless) 

475 

476 

477 
subsection{* The operations on paths*} 

478 

479 
lemma path_image_subset_reversepath: "path_image(reversepath g) \<le> path_image g" 

480 
by (auto simp: path_image_def reversepath_def) 

481 

482 
lemma continuous_on_op_minus: "continuous_on (s::real set) (op  x)" 

483 
by (rule continuous_intros  simp)+ 

484 

485 
lemma path_imp_reversepath: "path g \<Longrightarrow> path(reversepath g)" 

486 
apply (auto simp: path_def reversepath_def) 

487 
using continuous_on_compose [of "{0..1}" "\<lambda>x. 1  x" g] 

488 
apply (auto simp: continuous_on_op_minus) 

489 
done 

490 

491 
lemma forall_01_trivial: "(\<forall>x\<in>{0..1}. x \<le> 0 \<longrightarrow> P x) \<longleftrightarrow> P (0::real)" 

492 
by auto 

493 

494 
lemma forall_half1_trivial: "(\<forall>x\<in>{1/2..1}. x * 2 \<le> 1 \<longrightarrow> P x) \<longleftrightarrow> P (1/2::real)" 

495 
by auto (metis add_divide_distrib mult_2_right real_sum_of_halves) 

496 

497 
lemma continuous_on_joinpaths: 

498 
assumes "continuous_on {0..1} g1" "continuous_on {0..1} g2" "pathfinish g1 = pathstart g2" 

499 
shows "continuous_on {0..1} (g1 +++ g2)" 

500 
proof  

501 
have *: "{0..1::real} = {0..1/2} \<union> {1/2..1}" 

502 
by auto 

503 
have gg: "g2 0 = g1 1" 

504 
by (metis assms(3) pathfinish_def pathstart_def) 

505 
have 1: "continuous_on {0..1 / 2} (g1 +++ g2)" 

506 
apply (rule continuous_on_eq [of _ "g1 o (\<lambda>x. 2*x)"]) 

507 
apply (simp add: joinpaths_def) 

508 
apply (rule continuous_intros  simp add: assms)+ 

509 
done 

510 
have 2: "continuous_on {1 / 2..1} (g1 +++ g2)" 

511 
apply (rule continuous_on_eq [of _ "g2 o (\<lambda>x. 2*x1)"]) 

512 
apply (simp add: joinpaths_def) 

513 
apply (rule continuous_intros  simp add: forall_half1_trivial gg)+ 

514 
apply (rule continuous_on_subset) 

515 
apply (rule assms, auto) 

516 
done 

517 
show ?thesis 

518 
apply (subst *) 

519 
apply (rule continuous_on_union) 

520 
using 1 2 

521 
apply auto 

522 
done 

523 
qed 

524 

525 
lemma path_join_imp: "\<lbrakk>path g1; path g2; pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> path(g1 +++ g2)" 

526 
by (simp add: path_join) 

527 

528 
lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join 

529 

36583  530 
lemma simple_path_join_loop: 
60303  531 
assumes "arc g1" "arc g2" 
532 
"pathfinish g1 = pathstart g2" "pathfinish g2 = pathstart g1" 

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

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

535 
proof  

536 
have injg1: "inj_on g1 {0..1}" 

537 
using assms 

538 
by (simp add: arc_def) 

539 
have injg2: "inj_on g2 {0..1}" 

540 
using assms 

541 
by (simp add: arc_def) 

542 
have g12: "g1 1 = g2 0" 

543 
and g21: "g2 1 = g1 0" 

544 
and sb: "g1 ` {0..1} \<inter> g2 ` {0..1} \<subseteq> {g1 0, g2 0}" 

545 
using assms 

546 
by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) 

547 
{ fix x and y::real 

548 
assume xyI: "x = 1 \<longrightarrow> y \<noteq> 0" 

549 
and xy: "x \<le> 1" "0 \<le> y" " y * 2 \<le> 1" "\<not> x * 2 \<le> 1" "g2 (2 * x  1) = g1 (2 * y)" 

550 
have g1im: "g1 (2 * y) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}" 

551 
using xy 

552 
apply simp 

553 
apply (rule_tac x="2 * x  1" in image_eqI, auto) 

554 
done 

555 
have False 

556 
using subsetD [OF sb g1im] xy 

557 
apply auto 

558 
apply (drule inj_onD [OF injg1]) 

559 
using g21 [symmetric] xyI 

560 
apply (auto dest: inj_onD [OF injg2]) 

561 
done 

562 
} note * = this 

563 
{ fix x and y::real 

564 
assume xy: "y \<le> 1" "0 \<le> x" "\<not> y * 2 \<le> 1" "x * 2 \<le> 1" "g1 (2 * x) = g2 (2 * y  1)" 

565 
have g1im: "g1 (2 * x) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}" 

566 
using xy 

567 
apply simp 

568 
apply (rule_tac x="2 * x" in image_eqI, auto) 

569 
done 

570 
have "x = 0 \<and> y = 1" 

571 
using subsetD [OF sb g1im] xy 

572 
apply auto 

573 
apply (force dest: inj_onD [OF injg1]) 

574 
using g21 [symmetric] 

575 
apply (auto dest: inj_onD [OF injg2]) 

576 
done 

577 
} note ** = this 

578 
show ?thesis 

579 
using assms 

580 
apply (simp add: arc_def simple_path_def path_join, clarify) 

581 
apply (simp add: joinpaths_def split: split_if_asm) 

582 
apply (force dest: inj_onD [OF injg1]) 

583 
apply (metis *) 

584 
apply (metis **) 

585 
apply (force dest: inj_onD [OF injg2]) 

586 
done 

587 
qed 

588 

589 
lemma arc_join: 

590 
assumes "arc g1" "arc g2" 

591 
"pathfinish g1 = pathstart g2" 

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

593 
shows "arc(g1 +++ g2)" 

594 
proof  

595 
have injg1: "inj_on g1 {0..1}" 

596 
using assms 

597 
by (simp add: arc_def) 

598 
have injg2: "inj_on g2 {0..1}" 

599 
using assms 

600 
by (simp add: arc_def) 

601 
have g11: "g1 1 = g2 0" 

602 
and sb: "g1 ` {0..1} \<inter> g2 ` {0..1} \<subseteq> {g2 0}" 

603 
using assms 

604 
by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) 

605 
{ fix x and y::real 

606 
assume xy: "x \<le> 1" "0 \<le> y" " y * 2 \<le> 1" "\<not> x * 2 \<le> 1" "g2 (2 * x  1) = g1 (2 * y)" 

607 
have g1im: "g1 (2 * y) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}" 

608 
using xy 

609 
apply simp 

610 
apply (rule_tac x="2 * x  1" in image_eqI, auto) 

611 
done 

612 
have False 

613 
using subsetD [OF sb g1im] xy 

614 
by (auto dest: inj_onD [OF injg2]) 

615 
} note * = this 

616 
show ?thesis 

617 
apply (simp add: arc_def inj_on_def) 

618 
apply (clarsimp simp add: arc_imp_path assms path_join) 

619 
apply (simp add: joinpaths_def split: split_if_asm) 

620 
apply (force dest: inj_onD [OF injg1]) 

621 
apply (metis *) 

622 
apply (metis *) 

623 
apply (force dest: inj_onD [OF injg2]) 

624 
done 

625 
qed 

626 

627 
lemma reversepath_joinpaths: 

628 
"pathfinish g1 = pathstart g2 \<Longrightarrow> reversepath(g1 +++ g2) = reversepath g2 +++ reversepath g1" 

629 
unfolding reversepath_def pathfinish_def pathstart_def joinpaths_def 

630 
by (rule ext) (auto simp: mult.commute) 

631 

632 

633 
subsection{* Choosing a subpath of an existing path*} 

634 

635 
definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector" 

636 
where "subpath a b g \<equiv> \<lambda>x. g((b  a) * x + a)" 

637 

638 
lemma path_image_subpath_gen [simp]: 

639 
fixes g :: "real \<Rightarrow> 'a::real_normed_vector" 

640 
shows "path_image(subpath u v g) = g ` (closed_segment u v)" 

641 
apply (simp add: closed_segment_real_eq path_image_def subpath_def) 

642 
apply (subst o_def [of g, symmetric]) 

643 
apply (simp add: image_comp [symmetric]) 

644 
done 

645 

646 
lemma path_image_subpath [simp]: 

647 
fixes g :: "real \<Rightarrow> 'a::real_normed_vector" 

648 
shows "path_image(subpath u v g) = (if u \<le> v then g ` {u..v} else g ` {v..u})" 

649 
by (simp add: closed_segment_eq_real_ivl) 

650 

651 
lemma path_subpath [simp]: 

652 
fixes g :: "real \<Rightarrow> 'a::real_normed_vector" 

653 
assumes "path g" "u \<in> {0..1}" "v \<in> {0..1}" 

654 
shows "path(subpath u v g)" 

655 
proof  

656 
have "continuous_on {0..1} (g o (\<lambda>x. ((vu) * x+ u)))" 

657 
apply (rule continuous_intros  simp)+ 

658 
apply (simp add: image_affinity_atLeastAtMost [where c=u]) 

659 
using assms 

660 
apply (auto simp: path_def continuous_on_subset) 

661 
done 

662 
then show ?thesis 

663 
by (simp add: path_def subpath_def) 

49653  664 
qed 
36583  665 

60303  666 
lemma pathstart_subpath [simp]: "pathstart(subpath u v g) = g(u)" 
667 
by (simp add: pathstart_def subpath_def) 

668 

669 
lemma pathfinish_subpath [simp]: "pathfinish(subpath u v g) = g(v)" 

670 
by (simp add: pathfinish_def subpath_def) 

671 

672 
lemma subpath_trivial [simp]: "subpath 0 1 g = g" 

673 
by (simp add: subpath_def) 

674 

675 
lemma subpath_reversepath: "subpath 1 0 g = reversepath g" 

676 
by (simp add: reversepath_def subpath_def) 

677 

678 
lemma reversepath_subpath: "reversepath(subpath u v g) = subpath v u g" 

679 
by (simp add: reversepath_def subpath_def algebra_simps) 

680 

681 
lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) o g) = (\<lambda>x. a + x) o subpath u v g" 

682 
by (rule ext) (simp add: subpath_def) 

683 

684 
lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f o g) = f o subpath u v g" 

685 
by (rule ext) (simp add: subpath_def) 

686 

687 
lemma affine_ineq: 

688 
fixes x :: "'a::linordered_idom" 

689 
assumes "x \<le> 1" "v < u" 

690 
shows "v + x * u \<le> u + x * v" 

691 
proof  

692 
have "(1x)*(uv) \<ge> 0" 

693 
using assms by auto 

694 
then show ?thesis 

695 
by (simp add: algebra_simps) 

49653  696 
qed 
36583  697 

60303  698 
lemma simple_path_subpath_eq: 
699 
"simple_path(subpath u v g) \<longleftrightarrow> 

700 
path(subpath u v g) \<and> u\<noteq>v \<and> 

701 
(\<forall>x y. x \<in> closed_segment u v \<and> y \<in> closed_segment u v \<and> g x = g y 

702 
\<longrightarrow> x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u)" 

703 
(is "?lhs = ?rhs") 

704 
proof (rule iffI) 

705 
assume ?lhs 

706 
then have p: "path (\<lambda>x. g ((v  u) * x + u))" 

707 
and sim: "(\<And>x y. \<lbrakk>x\<in>{0..1}; y\<in>{0..1}; g ((v  u) * x + u) = g ((v  u) * y + u)\<rbrakk> 

708 
\<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)" 

709 
by (auto simp: simple_path_def subpath_def) 

710 
{ fix x y 

711 
assume "x \<in> closed_segment u v" "y \<in> closed_segment u v" "g x = g y" 

712 
then have "x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u" 

713 
using sim [of "(xu)/(vu)" "(yu)/(vu)"] p 

714 
by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost divide_simps 

715 
split: split_if_asm) 

716 
} moreover 

717 
have "path(subpath u v g) \<and> u\<noteq>v" 

718 
using sim [of "1/3" "2/3"] p 

719 
by (auto simp: subpath_def) 

720 
ultimately show ?rhs 

721 
by metis 

722 
next 

723 
assume ?rhs 

724 
then 

725 
have d1: "\<And>x y. \<lbrakk>g x = g y; u \<le> x; x \<le> v; u \<le> y; y \<le> v\<rbrakk> \<Longrightarrow> x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u" 

726 
and d2: "\<And>x y. \<lbrakk>g x = g y; v \<le> x; x \<le> u; v \<le> y; y \<le> u\<rbrakk> \<Longrightarrow> x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u" 

727 
and ne: "u < v \<or> v < u" 

728 
and psp: "path (subpath u v g)" 

729 
by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost) 

730 
have [simp]: "\<And>x. u + x * v = v + x * u \<longleftrightarrow> u=v \<or> x=1" 

731 
by algebra 

732 
show ?lhs using psp ne 

733 
unfolding simple_path_def subpath_def 

734 
by (fastforce simp add: algebra_simps affine_ineq mult_left_mono crossproduct_eq dest: d1 d2) 

735 
qed 

736 

737 
lemma arc_subpath_eq: 

738 
"arc(subpath u v g) \<longleftrightarrow> path(subpath u v g) \<and> u\<noteq>v \<and> inj_on g (closed_segment u v)" 

739 
(is "?lhs = ?rhs") 

740 
proof (rule iffI) 

741 
assume ?lhs 

742 
then have p: "path (\<lambda>x. g ((v  u) * x + u))" 

743 
and sim: "(\<And>x y. \<lbrakk>x\<in>{0..1}; y\<in>{0..1}; g ((v  u) * x + u) = g ((v  u) * y + u)\<rbrakk> 

744 
\<Longrightarrow> x = y)" 

745 
by (auto simp: arc_def inj_on_def subpath_def) 

746 
{ fix x y 

747 
assume "x \<in> closed_segment u v" "y \<in> closed_segment u v" "g x = g y" 

748 
then have "x = y" 

749 
using sim [of "(xu)/(vu)" "(yu)/(vu)"] p 

750 
by (force simp add: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps 

751 
split: split_if_asm) 

752 
} moreover 

753 
have "path(subpath u v g) \<and> u\<noteq>v" 

754 
using sim [of "1/3" "2/3"] p 

755 
by (auto simp: subpath_def) 

756 
ultimately show ?rhs 

757 
unfolding inj_on_def 

758 
by metis 

759 
next 

760 
assume ?rhs 

761 
then 

762 
have d1: "\<And>x y. \<lbrakk>g x = g y; u \<le> x; x \<le> v; u \<le> y; y \<le> v\<rbrakk> \<Longrightarrow> x = y" 

763 
and d2: "\<And>x y. \<lbrakk>g x = g y; v \<le> x; x \<le> u; v \<le> y; y \<le> u\<rbrakk> \<Longrightarrow> x = y" 

764 
and ne: "u < v \<or> v < u" 

765 
and psp: "path (subpath u v g)" 

766 
by (auto simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost) 

767 
show ?lhs using psp ne 

768 
unfolding arc_def subpath_def inj_on_def 

769 
by (auto simp: algebra_simps affine_ineq mult_left_mono crossproduct_eq dest: d1 d2) 

770 
qed 

771 

772 

773 
lemma simple_path_subpath: 

774 
assumes "simple_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<noteq> v" 

775 
shows "simple_path(subpath u v g)" 

776 
using assms 

777 
apply (simp add: simple_path_subpath_eq simple_path_imp_path) 

778 
apply (simp add: simple_path_def closed_segment_real_eq image_affinity_atLeastAtMost, fastforce) 

779 
done 

780 

781 
lemma arc_simple_path_subpath: 

782 
"\<lbrakk>simple_path g; u \<in> {0..1}; v \<in> {0..1}; g u \<noteq> g v\<rbrakk> \<Longrightarrow> arc(subpath u v g)" 

783 
by (force intro: simple_path_subpath simple_path_imp_arc) 

784 

785 
lemma arc_subpath_arc: 

786 
"\<lbrakk>arc g; u \<in> {0..1}; v \<in> {0..1}; u \<noteq> v\<rbrakk> \<Longrightarrow> arc(subpath u v g)" 

787 
by (meson arc_def arc_imp_simple_path arc_simple_path_subpath inj_onD) 

788 

789 
lemma arc_simple_path_subpath_interior: 

790 
"\<lbrakk>simple_path g; u \<in> {0..1}; v \<in> {0..1}; u \<noteq> v; \<bar>uv\<bar> < 1\<rbrakk> \<Longrightarrow> arc(subpath u v g)" 

791 
apply (rule arc_simple_path_subpath) 

792 
apply (force simp: simple_path_def)+ 

793 
done 

794 

795 
lemma path_image_subpath_subset: 

796 
"\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g" 

797 
apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost) 

798 
apply (auto simp: path_image_def) 

799 
done 

800 

801 
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p" 

802 
by (rule ext) (simp add: joinpaths_def subpath_def divide_simps) 

53640  803 

49653  804 

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

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

36583  809 

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

49653  813 
lemma pathfinish_shiftpath: 
53640  814 
assumes "0 \<le> a" 
815 
and "pathfinish g = pathstart g" 

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

817 
using assms 

818 
unfolding pathstart_def pathfinish_def shiftpath_def 

36583  819 
by auto 
820 

821 
lemma endpoints_shiftpath: 

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

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

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

826 
using assms 

827 
by (auto intro!: pathfinish_shiftpath pathstart_shiftpath) 

36583  828 

829 
lemma closed_shiftpath: 

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

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

833 
using endpoints_shiftpath[OF assms] 

834 
by auto 

36583  835 

836 
lemma path_shiftpath: 

53640  837 
assumes "path g" 
838 
and "pathfinish g = pathstart g" 

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

840 
shows "path (shiftpath a g)" 

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

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

49653  847 
show ?thesis 
848 
unfolding path_def shiftpath_def * 

849 
apply (rule continuous_on_union) 

850 
apply (rule closed_real_atLeastAtMost)+ 

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

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

854 
defer 

855 
prefer 3 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56188
diff
changeset

856 
apply (rule continuous_intros)+ 
53640  857 
prefer 2 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56188
diff
changeset

858 
apply (rule continuous_intros)+ 
49653  859 
apply (rule_tac[12] continuous_on_subset[OF assms(1)[unfolded path_def]]) 
860 
using assms(3) and ** 

53640  861 
apply auto 
862 
apply (auto simp add: field_simps) 

49653  863 
done 
864 
qed 

36583  865 

49653  866 
lemma shiftpath_shiftpath: 
53640  867 
assumes "pathfinish g = pathstart g" 
868 
and "a \<in> {0..1}" 

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

36583  870 
shows "shiftpath (1  a) (shiftpath a g) x = g x" 
53640  871 
using assms 
872 
unfolding pathfinish_def pathstart_def shiftpath_def 

873 
by auto 

36583  874 

875 
lemma path_image_shiftpath: 

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

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

49653  879 
proof  
880 
{ fix x 

53640  881 
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  882 
then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)" 
49653  883 
proof (cases "a \<le> x") 
884 
case False 

49654  885 
then show ?thesis 
49653  886 
apply (rule_tac x="1 + x  a" in bexI) 
36583  887 
using as(1,2) and as(3)[THEN bspec[where x="1 + x  a"]] and assms(1) 
49653  888 
apply (auto simp add: field_simps atomize_not) 
889 
done 

890 
next 

891 
case True 

53640  892 
then show ?thesis 
893 
using as(12) and assms(1) 

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

895 
apply (auto simp add: field_simps) 

896 
done 

49653  897 
qed 
898 
} 

49654  899 
then show ?thesis 
53640  900 
using assms 
901 
unfolding shiftpath_def path_image_def pathfinish_def pathstart_def 

902 
by (auto simp add: image_iff) 

49653  903 
qed 
904 

36583  905 

53640  906 
subsection {* Special case of straightline paths *} 
36583  907 

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

36583  910 

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

913 
by auto 

36583  914 

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

917 
by auto 

36583  918 

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

53640  920 
unfolding linepath_def 
921 
by (intro continuous_intros) 

36583  922 

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

53640  924 
using continuous_linepath_at 
925 
by (auto intro!: continuous_at_imp_continuous_on) 

36583  926 

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

929 
by (rule continuous_on_linepath) 

36583  930 

53640  931 
lemma path_image_linepath[simp]: "path_image (linepath a b) = closed_segment a b" 
49653  932 
unfolding path_image_def segment linepath_def 
60303  933 
by auto 
49653  934 

53640  935 
lemma reversepath_linepath[simp]: "reversepath (linepath a b) = linepath b a" 
49653  936 
unfolding reversepath_def linepath_def 
36583  937 
by auto 
938 

60303  939 
lemma arc_linepath: 
49653  940 
assumes "a \<noteq> b" 
60303  941 
shows "arc (linepath a b)" 
36583  942 
proof  
53640  943 
{ 
944 
fix x y :: "real" 

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

948 
with assms have "x = y" 

949 
by simp 

950 
} 

49654  951 
then show ?thesis 
60303  952 
unfolding arc_def inj_on_def 
953 
by (simp add: path_linepath) (force simp: algebra_simps linepath_def) 

49653  954 
qed 
36583  955 

53640  956 
lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path (linepath a b)" 
60303  957 
by (simp add: arc_imp_simple_path arc_linepath) 
49653  958 

36583  959 

53640  960 
subsection {* Bounding a point away from a path *} 
36583  961 

962 
lemma not_on_path_ball: 

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

53640  964 
assumes "path g" 
965 
and "z \<notin> path_image g" 

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

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

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

49654  971 
then show ?thesis 
49653  972 
apply (rule_tac x="dist z a" in exI) 
973 
using assms(2) 

974 
apply (auto intro!: dist_pos_lt) 

975 
done 

976 
qed 

36583  977 

978 
lemma not_on_path_cball: 

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

53640  980 
assumes "path g" 
981 
and "z \<notin> path_image g" 

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

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

988 
ultimately show ?thesis 

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

990 
apply auto 

991 
done 

49653  992 
qed 
993 

36583  994 

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

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

36583  999 

53640  1000 
lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def 
36583  1001 

49653  1002 
lemma path_component_mem: 
1003 
assumes "path_component s x y" 

53640  1004 
shows "x \<in> s" and "y \<in> s" 
1005 
using assms 

1006 
unfolding path_defs 

1007 
by auto 

36583  1008 

49653  1009 
lemma path_component_refl: 
1010 
assumes "x \<in> s" 

1011 
shows "path_component s x x" 

1012 
unfolding path_defs 

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

53640  1014 
using assms 
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56188
diff
changeset

1015 
apply (auto intro!: continuous_intros) 
53640  1016 
done 
36583  1017 

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

49653  1019 
by (auto intro!: path_component_mem path_component_refl) 
36583  1020 

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

49653  1022 
using assms 
1023 
unfolding path_component_def 

1024 
apply (erule exE) 

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

1026 
apply auto 

1027 
done 

36583  1028 

49653  1029 
lemma path_component_trans: 
53640  1030 
assumes "path_component s x y" 
1031 
and "path_component s y z" 

49653  1032 
shows "path_component s x z" 
1033 
using assms 

1034 
unfolding path_component_def 

53640  1035 
apply (elim exE) 
49653  1036 
apply (rule_tac x="g +++ ga" in exI) 
1037 
apply (auto simp add: path_image_join) 

1038 
done 

36583  1039 

53640  1040 
lemma path_component_of_subset: "s \<subseteq> t \<Longrightarrow> path_component s x y \<Longrightarrow> path_component t x y" 
36583  1041 
unfolding path_component_def by auto 
1042 

49653  1043 

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

49653  1046 
lemma path_component_set: 
1047 
"{y. path_component s x y} = 

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

60303  1049 
unfolding mem_Collect_eq path_component_def 
49653  1050 
apply auto 
1051 
done 

36583  1052 

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

1053 
lemma path_component_subset: "{y. path_component s x y} \<subseteq> s" 
60303  1054 
by (auto simp add: path_component_mem(2)) 
36583  1055 

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

1056 
lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s" 
60303  1057 
using path_component_mem path_component_refl_eq 
1058 
by fastforce 

36583  1059 

53640  1060 
subsection {* Path connectedness of a space *} 
36583  1061 

49653  1062 
definition "path_connected s \<longleftrightarrow> 
53640  1063 
(\<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  1064 

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

1066 
unfolding path_connected_def path_component_def by auto 

1067 

53640  1068 
lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)" 
60303  1069 
unfolding path_connected_component path_component_subset 
49653  1070 
apply auto 
60303  1071 
using path_component_mem(2) by blast 
36583  1072 

53640  1073 
subsection {* Some useful lemmas about pathconnectedness *} 
36583  1074 

1075 
lemma convex_imp_path_connected: 

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

53640  1077 
assumes "convex s" 
1078 
shows "path_connected s" 

49653  1079 
unfolding path_connected_def 
53640  1080 
apply rule 
1081 
apply rule 

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

49653  1083 
unfolding path_image_linepath 
1084 
using assms [unfolded convex_contains_segment] 

1085 
apply auto 

1086 
done 

36583  1087 

49653  1088 
lemma path_connected_imp_connected: 
1089 
assumes "path_connected s" 

1090 
shows "connected s" 

1091 
unfolding connected_def not_ex 

53640  1092 
apply rule 
1093 
apply rule 

1094 
apply (rule ccontr) 

49653  1095 
unfolding not_not 
53640  1096 
apply (elim conjE) 
49653  1097 
proof  
1098 
fix e1 e2 

1099 
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  1100 
then obtain x1 x2 where obt:"x1 \<in> e1 \<inter> s" "x2 \<in> e2 \<inter> s" 
1101 
by auto 

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

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

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

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

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

53640  1109 
using as(4) g(2)[unfolded path_defs] 
1110 
unfolding subset_eq 

1111 
by auto 

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

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

36583  1119 
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] 
49653  1120 
using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] 
1121 
by auto 

1122 
qed 

36583  1123 

1124 
lemma open_path_component: 

53593  1125 
fixes s :: "'a::real_normed_vector set" 
49653  1126 
assumes "open s" 
1127 
shows "open {y. path_component s x y}" 

1128 
unfolding open_contains_ball 

1129 
proof 

1130 
fix y 

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

49654  1132 
then have "y \<in> s" 
49653  1133 
apply  
1134 
apply (rule path_component_mem(2)) 

1135 
unfolding mem_Collect_eq 

1136 
apply auto 

1137 
done 

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

1140 
by auto 

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

53640  1143 
apply (rule,rule `e>0`) 
1144 
apply rule 

49653  1145 
unfolding mem_ball mem_Collect_eq 
1146 
proof  

1147 
fix z 

1148 
assume "dist y z < e" 

49654  1149 
then show "path_component s x z" 
53640  1150 
apply (rule_tac path_component_trans[of _ _ y]) 
1151 
defer 

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

53640  1154 
using `e > 0` as 
49653  1155 
apply auto 
1156 
done 

1157 
qed 

1158 
qed 

36583  1159 

1160 
lemma open_non_path_component: 

53593  1161 
fixes s :: "'a::real_normed_vector set" 
49653  1162 
assumes "open s" 
53640  1163 
shows "open (s  {y. path_component s x y})" 
49653  1164 
unfolding open_contains_ball 
1165 
proof 

1166 
fix y 

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

1169 
using assms [unfolded open_contains_ball] 

1170 
by auto 

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

53640  1173 
apply rule 
1174 
apply (rule `e>0`) 

1175 
apply rule 

1176 
apply rule 

1177 
defer 

49653  1178 
proof (rule ccontr) 
1179 
fix z 

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

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

1184 
apply (rule path_component_trans, assumption) 

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

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

1187 
apply auto 

1188 
done 

53640  1189 
then show False 
1190 
using as by auto 

49653  1191 
qed (insert e(2), auto) 
1192 
qed 

36583  1193 

1194 
lemma connected_open_path_connected: 

53593  1195 
fixes s :: "'a::real_normed_vector set" 
53640  1196 
assumes "open s" 
1197 
and "connected s" 

49653  1198 
shows "path_connected s" 
1199 
unfolding path_connected_component_set 

1200 
proof (rule, rule, rule path_component_subset, rule) 

1201 
fix x y 

53640
3170b5eb9f5a
tuned proofs;
wenzelm< 