author  paulson <lp15@cam.ac.uk> 
Mon, 23 May 2016 16:03:29 +0100  
changeset 63126  2b50f79829d2 
parent 63125  f2d3f8427bc2 
child 63151  82df5181d699 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Path_Connected.thy 
61806
d2e62ae01cd8
Cauchy's integral formula for circles. Starting to fix eventually_mono.
paulson <lp15@cam.ac.uk>
parents:
61762
diff
changeset

2 
Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light 
36583  3 
*) 
4 

60420  5 
section \<open>Continuous paths and pathconnected sets\<close> 
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 

60420  11 
subsection \<open>Paths and Arcs\<close> 
36583  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> 
60303  34 
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  35 

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

36583  38 

49653  39 

60420  40 
subsection\<open>Invariance theorems\<close> 
60303  41 

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

43 
using continuous_on_eq path_def by blast 

44 

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

46 
unfolding path_def path_image_def 

47 
using continuous_on_compose by blast 

48 

49 
lemma path_translation_eq: 

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

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

52 
proof  

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

54 
by (rule ext) simp 

55 
show ?thesis 

56 
unfolding path_def 

57 
apply safe 

58 
apply (subst g) 

59 
apply (rule continuous_on_compose) 

60 
apply (auto intro: continuous_intros) 

61 
done 

62 
qed 

63 

64 
lemma path_linear_image_eq: 

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

66 
assumes "linear f" "inj f" 

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

68 
proof  

69 
from linear_injective_left_inverse [OF assms] 

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

71 
by blast 

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

73 
by (metis comp_assoc id_comp) 

74 
show ?thesis 

75 
unfolding path_def 

76 
using h assms 

77 
by (metis g continuous_on_compose linear_continuous_on linear_conv_bounded_linear) 

78 
qed 

79 

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

81 
by (simp add: pathstart_def) 

82 

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

84 
by (simp add: pathstart_def) 

85 

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

87 
by (simp add: pathfinish_def) 

88 

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

90 
by (simp add: pathfinish_def) 

91 

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

93 
by (simp add: image_comp path_image_def) 

94 

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

96 
by (simp add: image_comp path_image_def) 

97 

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

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

36583  100 

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

103 

104 
lemma joinpaths_translation: 

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

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

107 

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

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

110 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

111 
lemma simple_path_translation_eq: 
60303  112 
fixes g :: "real \<Rightarrow> 'a::euclidean_space" 
113 
shows "simple_path((\<lambda>x. a + x) o g) = simple_path g" 

114 
by (simp add: simple_path_def path_translation_eq) 

115 

116 
lemma simple_path_linear_image_eq: 

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

118 
assumes "linear f" "inj f" 

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

120 
using assms inj_on_eq_iff [of f] 

121 
by (auto simp: path_linear_image_eq simple_path_def path_translation_eq) 

122 

123 
lemma arc_translation_eq: 

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

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

126 
by (auto simp: arc_def inj_on_def path_translation_eq) 

127 

128 
lemma arc_linear_image_eq: 

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

130 
assumes "linear f" "inj f" 

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

132 
using assms inj_on_eq_iff [of f] 

133 
by (auto simp: arc_def inj_on_def path_linear_image_eq) 

134 

60420  135 
subsection\<open>Basic lemmas about paths\<close> 
60303  136 

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

138 
by (simp add: arc_def inj_on_def simple_path_def) 

139 

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

141 
using arc_def by blast 

142 

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

144 
using simple_path_def by blast 

145 

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

147 
unfolding simple_path_def arc_def inj_on_def pathfinish_def pathstart_def 

148 
by (force) 

149 

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

151 
using simple_path_cases by auto 

152 

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

154 
unfolding arc_def inj_on_def pathfinish_def pathstart_def 

155 
by fastforce 

156 

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

158 
using arc_distinct_ends arc_imp_simple_path simple_path_cases by blast 

159 

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

161 
by (simp add: arc_simple_path) 

36583  162 

60974
6a6f15d8fbc4
New material and fixes related to the forthcoming StoneWeierstrass development
paulson <lp15@cam.ac.uk>
parents:
60809
diff
changeset

163 
lemma path_image_nonempty [simp]: "path_image g \<noteq> {}" 
56188  164 
unfolding path_image_def image_is_empty box_eq_empty 
53640  165 
by auto 
36583  166 

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

169 
by auto 

36583  170 

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

173 
by auto 

174 

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

36583  176 
unfolding path_def path_image_def 
60303  177 
using connected_continuous_image connected_Icc by blast 
36583  178 

53640  179 
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact (path_image g)" 
36583  180 
unfolding path_def path_image_def 
60303  181 
using compact_continuous_image connected_Icc by blast 
36583  182 

53640  183 
lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g" 
184 
unfolding reversepath_def 

185 
by auto 

36583  186 

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

189 
by auto 

36583  190 

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

193 
by auto 

36583  194 

49653  195 
lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1" 
53640  196 
unfolding pathstart_def joinpaths_def pathfinish_def 
197 
by auto 

36583  198 

49653  199 
lemma pathfinish_join[simp]: "pathfinish (g1 +++ g2) = pathfinish g2" 
53640  200 
unfolding pathstart_def joinpaths_def pathfinish_def 
201 
by auto 

36583  202 

53640  203 
lemma path_image_reversepath[simp]: "path_image (reversepath g) = path_image g" 
49653  204 
proof  
53640  205 
have *: "\<And>g. path_image (reversepath g) \<subseteq> path_image g" 
49653  206 
unfolding path_image_def subset_eq reversepath_def Ball_def image_iff 
60303  207 
by force 
49653  208 
show ?thesis 
209 
using *[of g] *[of "reversepath g"] 

53640  210 
unfolding reversepath_reversepath 
211 
by auto 

49653  212 
qed 
36583  213 

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

217 
unfolding path_def reversepath_def 

218 
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

219 
apply (intro continuous_intros) 
53640  220 
apply (rule continuous_on_subset[of "{0..1}"]) 
221 
apply assumption 

49653  222 
apply auto 
223 
done 

224 
show ?thesis 

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

226 
unfolding reversepath_reversepath 

227 
by (rule iffI) 

228 
qed 

229 

60303  230 
lemma arc_reversepath: 
231 
assumes "arc g" shows "arc(reversepath g)" 

232 
proof  

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

234 
using assms 

235 
by (simp add: arc_def) 

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

237 
by simp 

238 
show ?thesis 

239 
apply (auto simp: arc_def inj_on_def path_reversepath) 

240 
apply (simp add: arc_imp_path assms) 

241 
apply (rule **) 

242 
apply (rule inj_onD [OF injg]) 

243 
apply (auto simp: reversepath_def) 

244 
done 

245 
qed 

246 

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

248 
apply (simp add: simple_path_def) 

249 
apply (force simp: reversepath_def) 

250 
done 

251 

49653  252 
lemmas reversepath_simps = 
253 
path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath 

36583  254 

49653  255 
lemma path_join[simp]: 
256 
assumes "pathfinish g1 = pathstart g2" 

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

258 
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

259 
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

260 
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

261 
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

262 
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

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

266 
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

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

268 
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

269 
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

270 
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

271 
have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}" 
36583  272 
by auto 
53640  273 
{ 
274 
fix x :: real 

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

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

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

278 
} 

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

279 
note 1 = this 
53640  280 
{ 
281 
fix x :: real 

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

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

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

285 
} 

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

286 
note 2 = this 
49653  287 
show "continuous_on {0..1} (g1 +++ g2)" 
53640  288 
using assms 
289 
unfolding joinpaths_def 01 

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

290 
apply (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_intros) 
53640  291 
apply (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) 
292 
done 

49653  293 
qed 
36583  294 

60420  295 
section \<open>Path Images\<close> 
60303  296 

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

298 
by (simp add: compact_imp_bounded compact_path_image) 

299 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

300 
lemma closed_path_image: 
60303  301 
fixes g :: "real \<Rightarrow> 'a::t2_space" 
302 
shows "path g \<Longrightarrow> closed(path_image g)" 

303 
by (metis compact_path_image compact_imp_closed) 

304 

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

306 
by (metis connected_path_image simple_path_imp_path) 

307 

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

309 
by (metis compact_path_image simple_path_imp_path) 

310 

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

312 
by (metis bounded_path_image simple_path_imp_path) 

313 

314 
lemma closed_simple_path_image: 

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

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

317 
by (metis closed_path_image simple_path_imp_path) 

318 

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

320 
by (metis connected_path_image arc_imp_path) 

321 

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

323 
by (metis compact_path_image arc_imp_path) 

324 

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

326 
by (metis bounded_path_image arc_imp_path) 

327 

328 
lemma closed_arc_image: 

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

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

331 
by (metis closed_path_image arc_imp_path) 

332 

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

335 
by auto 

36583  336 

337 
lemma subset_path_image_join: 

53640  338 
assumes "path_image g1 \<subseteq> s" 
339 
and "path_image g2 \<subseteq> s" 

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

341 
using path_image_join_subset[of g1 g2] and assms 

342 
by auto 

36583  343 

344 
lemma path_image_join: 

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

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

348 
apply (drule sym) 

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

350 
apply (rule ccontr) 

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

352 
apply (auto simp: field_simps) 

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

354 
done 

36583  355 

356 
lemma not_in_path_image_join: 

53640  357 
assumes "x \<notin> path_image g1" 
358 
and "x \<notin> path_image g2" 

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

360 
using assms and path_image_join_subset[of g1 g2] 

361 
by auto 

36583  362 

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

365 

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

367 
by (simp add: pathfinish_def) 

368 

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

370 
by (simp add: image_comp path_image_def) 

371 

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

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

374 

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

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

377 

61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

378 
lemma joinpaths_eq: 
60303  379 
"(\<And>t. t \<in> {0..1} \<Longrightarrow> p t = p' t) \<Longrightarrow> 
380 
(\<And>t. t \<in> {0..1} \<Longrightarrow> q t = q' t) 

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

382 
by (auto simp: joinpaths_def) 

383 

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

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

386 

387 

60420  388 
subsection\<open>Simple paths with the endpoints removed\<close> 
60303  389 

390 
lemma simple_path_endless: 

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

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

393 
apply (metis eq_iff le_less_linear) 

394 
apply (metis leD linear) 

395 
using less_eq_real_def zero_le_one apply blast 

396 
using less_eq_real_def zero_le_one apply blast 

49653  397 
done 
36583  398 

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

401 
apply (simp add: simple_path_endless) 

402 
apply (rule connected_continuous_image) 

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

404 
by auto 

405 

406 
lemma nonempty_simple_path_endless: 

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

408 
by (simp add: simple_path_endless) 

409 

410 

60420  411 
subsection\<open>The operations on paths\<close> 
60303  412 

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

414 
by (auto simp: path_image_def reversepath_def) 

415 

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

417 
apply (auto simp: path_def reversepath_def) 

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

419 
apply (auto simp: continuous_on_op_minus) 

420 
done 

421 

61204  422 
lemma half_bounded_equal: "1 \<le> x * 2 \<Longrightarrow> x * 2 \<le> 1 \<longleftrightarrow> x = (1/2::real)" 
423 
by simp 

60303  424 

425 
lemma continuous_on_joinpaths: 

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

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

428 
proof  

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

430 
by auto 

431 
have gg: "g2 0 = g1 1" 

432 
by (metis assms(3) pathfinish_def pathstart_def) 

61204  433 
have 1: "continuous_on {0..1/2} (g1 +++ g2)" 
60303  434 
apply (rule continuous_on_eq [of _ "g1 o (\<lambda>x. 2*x)"]) 
61204  435 
apply (rule continuous_intros  simp add: joinpaths_def assms)+ 
60303  436 
done 
61204  437 
have "continuous_on {1/2..1} (g2 o (\<lambda>x. 2*x1))" 
438 
apply (rule continuous_on_subset [of "{1/2..1}"]) 

439 
apply (rule continuous_intros  simp add: image_affinity_atLeastAtMost_diff assms)+ 

440 
done 

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

442 
apply (rule continuous_on_eq [of "{1/2..1}" "g2 o (\<lambda>x. 2*x1)"]) 

443 
apply (rule assms continuous_intros  simp add: joinpaths_def mult.commute half_bounded_equal gg)+ 

60303  444 
done 
445 
show ?thesis 

446 
apply (subst *) 

62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62381
diff
changeset

447 
apply (rule continuous_on_closed_Un) 
60303  448 
using 1 2 
449 
apply auto 

450 
done 

451 
qed 

452 

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

454 
by (simp add: path_join) 

455 

36583  456 
lemma simple_path_join_loop: 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

457 
assumes "arc g1" "arc g2" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

458 
"pathfinish g1 = pathstart g2" "pathfinish g2 = pathstart g1" 
60303  459 
"path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}" 
460 
shows "simple_path(g1 +++ g2)" 

461 
proof  

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

463 
using assms 

464 
by (simp add: arc_def) 

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

466 
using assms 

467 
by (simp add: arc_def) 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

468 
have g12: "g1 1 = g2 0" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

469 
and g21: "g2 1 = g1 0" 
60303  470 
and sb: "g1 ` {0..1} \<inter> g2 ` {0..1} \<subseteq> {g1 0, g2 0}" 
471 
using assms 

472 
by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) 

473 
{ fix x and y::real 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

474 
assume xyI: "x = 1 \<longrightarrow> y \<noteq> 0" 
60303  475 
and xy: "x \<le> 1" "0 \<le> y" " y * 2 \<le> 1" "\<not> x * 2 \<le> 1" "g2 (2 * x  1) = g1 (2 * y)" 
476 
have g1im: "g1 (2 * y) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}" 

477 
using xy 

478 
apply simp 

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

480 
done 

481 
have False 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

482 
using subsetD [OF sb g1im] xy 
60303  483 
apply auto 
484 
apply (drule inj_onD [OF injg1]) 

485 
using g21 [symmetric] xyI 

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

487 
done 

488 
} note * = this 

489 
{ fix x and y::real 

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

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

492 
using xy 

493 
apply simp 

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

495 
done 

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

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

497 
using subsetD [OF sb g1im] xy 
60303  498 
apply auto 
499 
apply (force dest: inj_onD [OF injg1]) 

500 
using g21 [symmetric] 

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

502 
done 

503 
} note ** = this 

504 
show ?thesis 

505 
using assms 

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

62390  507 
apply (simp add: joinpaths_def split: if_split_asm) 
60303  508 
apply (force dest: inj_onD [OF injg1]) 
509 
apply (metis *) 

510 
apply (metis **) 

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

512 
done 

513 
qed 

514 

515 
lemma arc_join: 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

516 
assumes "arc g1" "arc g2" 
60303  517 
"pathfinish g1 = pathstart g2" 
518 
"path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}" 

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

520 
proof  

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

522 
using assms 

523 
by (simp add: arc_def) 

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

525 
using assms 

526 
by (simp add: arc_def) 

527 
have g11: "g1 1 = g2 0" 

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

529 
using assms 

530 
by (simp_all add: arc_def pathfinish_def pathstart_def path_image_def) 

531 
{ fix x and y::real 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

532 
assume xy: "x \<le> 1" "0 \<le> y" " y * 2 \<le> 1" "\<not> x * 2 \<le> 1" "g2 (2 * x  1) = g1 (2 * y)" 
60303  533 
have g1im: "g1 (2 * y) \<in> g1 ` {0..1} \<inter> g2 ` {0..1}" 
534 
using xy 

535 
apply simp 

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

537 
done 

538 
have False 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

539 
using subsetD [OF sb g1im] xy 
60303  540 
by (auto dest: inj_onD [OF injg2]) 
541 
} note * = this 

542 
show ?thesis 

543 
apply (simp add: arc_def inj_on_def) 

544 
apply (clarsimp simp add: arc_imp_path assms path_join) 

62390  545 
apply (simp add: joinpaths_def split: if_split_asm) 
60303  546 
apply (force dest: inj_onD [OF injg1]) 
547 
apply (metis *) 

548 
apply (metis *) 

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

550 
done 

551 
qed 

552 

553 
lemma reversepath_joinpaths: 

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

555 
unfolding reversepath_def pathfinish_def pathstart_def joinpaths_def 

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

557 

558 

62533
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

559 
subsection\<open>Some reversed and "if and only if" versions of joining theorems\<close> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

560 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

561 
lemma path_join_path_ends: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

562 
fixes g1 :: "real \<Rightarrow> 'a::metric_space" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

563 
assumes "path(g1 +++ g2)" "path g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

564 
shows "pathfinish g1 = pathstart g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

565 
proof (rule ccontr) 
63040  566 
define e where "e = dist (g1 1) (g2 0)" 
62533
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

567 
assume Neg: "pathfinish g1 \<noteq> pathstart g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

568 
then have "0 < dist (pathfinish g1) (pathstart g2)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

569 
by auto 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

570 
then have "e > 0" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

571 
by (metis e_def pathfinish_def pathstart_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

572 
then obtain d1 where "d1 > 0" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

573 
and d1: "\<And>x'. \<lbrakk>x'\<in>{0..1}; norm x' < d1\<rbrakk> \<Longrightarrow> dist (g2 x') (g2 0) < e/2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

574 
using assms(2) unfolding path_def continuous_on_iff 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

575 
apply (drule_tac x=0 in bspec, simp) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

576 
by (metis half_gt_zero_iff norm_conv_dist) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

577 
obtain d2 where "d2 > 0" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

578 
and d2: "\<And>x'. \<lbrakk>x'\<in>{0..1}; dist x' (1/2) < d2\<rbrakk> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

579 
\<Longrightarrow> dist ((g1 +++ g2) x') (g1 1) < e/2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

580 
using assms(1) \<open>e > 0\<close> unfolding path_def continuous_on_iff 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

581 
apply (drule_tac x="1/2" in bspec, simp) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

582 
apply (drule_tac x="e/2" in spec) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

583 
apply (force simp: joinpaths_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

584 
done 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

585 
have int01_1: "min (1/2) (min d1 d2) / 2 \<in> {0..1}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

586 
using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

587 
have dist1: "norm (min (1 / 2) (min d1 d2) / 2) < d1" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

588 
using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

589 
have int01_2: "1/2 + min (1/2) (min d1 d2) / 4 \<in> {0..1}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

590 
using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

591 
have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

592 
using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

593 
have [simp]: "~ min (1 / 2) (min d1 d2) \<le> 0" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

594 
using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

595 
have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

596 
"dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

597 
using d1 [OF int01_1 dist1] d2 [OF int01_2 dist2] by (simp_all add: joinpaths_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

598 
then have "dist (g1 1) (g2 0) < e/2 + e/2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

599 
using dist_triangle_half_r e_def by blast 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

600 
then show False 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

601 
by (simp add: e_def [symmetric]) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

602 
qed 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

603 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

604 
lemma path_join_eq [simp]: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

605 
fixes g1 :: "real \<Rightarrow> 'a::metric_space" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

606 
assumes "path g1" "path g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

607 
shows "path(g1 +++ g2) \<longleftrightarrow> pathfinish g1 = pathstart g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

608 
using assms by (metis path_join_path_ends path_join_imp) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

609 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

610 
lemma simple_path_joinE: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

611 
assumes "simple_path(g1 +++ g2)" and "pathfinish g1 = pathstart g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

612 
obtains "arc g1" "arc g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

613 
"path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

614 
proof  
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

615 
have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

616 
\<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

617 
using assms by (simp add: simple_path_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

618 
have "path g1" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

619 
using assms path_join simple_path_imp_path by blast 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

620 
moreover have "inj_on g1 {0..1}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

621 
proof (clarsimp simp: inj_on_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

622 
fix x y 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

623 
assume "g1 x = g1 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

624 
then show "x = y" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

625 
using * [of "x/2" "y/2"] by (simp add: joinpaths_def split_ifs) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

626 
qed 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

627 
ultimately have "arc g1" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

628 
using assms by (simp add: arc_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

629 
have [simp]: "g2 0 = g1 1" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

630 
using assms by (metis pathfinish_def pathstart_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

631 
have "path g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

632 
using assms path_join simple_path_imp_path by blast 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

633 
moreover have "inj_on g2 {0..1}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

634 
proof (clarsimp simp: inj_on_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

635 
fix x y 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

636 
assume "g2 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

637 
then show "x = y" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

638 
using * [of "(x + 1) / 2" "(y + 1) / 2"] 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

639 
by (force simp: joinpaths_def split_ifs divide_simps) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

640 
qed 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

641 
ultimately have "arc g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

642 
using assms by (simp add: arc_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

643 
have "g2 y = g1 0 \<or> g2 y = g1 1" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

644 
if "g1 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" for x y 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

645 
using * [of "x / 2" "(y + 1) / 2"] that 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

646 
by (auto simp: joinpaths_def split_ifs divide_simps) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

647 
then have "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

648 
by (fastforce simp: pathstart_def pathfinish_def path_image_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

649 
with \<open>arc g1\<close> \<open>arc g2\<close> show ?thesis using that by blast 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

650 
qed 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

651 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

652 
lemma simple_path_join_loop_eq: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

653 
assumes "pathfinish g2 = pathstart g1" "pathfinish g1 = pathstart g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

654 
shows "simple_path(g1 +++ g2) \<longleftrightarrow> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

655 
arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

656 
by (metis assms simple_path_joinE simple_path_join_loop) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

657 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

658 
lemma arc_join_eq: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

659 
assumes "pathfinish g1 = pathstart g2" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

660 
shows "arc(g1 +++ g2) \<longleftrightarrow> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

661 
arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

662 
(is "?lhs = ?rhs") 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

663 
proof 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

664 
assume ?lhs 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

665 
then have "simple_path(g1 +++ g2)" by (rule arc_imp_simple_path) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

666 
then have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

667 
\<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

668 
using assms by (simp add: simple_path_def) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

669 
have False if "g1 0 = g2 u" "0 \<le> u" "u \<le> 1" for u 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

670 
using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \<open>?lhs\<close>] 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

671 
by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

672 
then have n1: "~ (pathstart g1 \<in> path_image g2)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

673 
unfolding pathstart_def path_image_def 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

674 
using atLeastAtMost_iff by blast 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

675 
show ?rhs using \<open>?lhs\<close> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

676 
apply (rule simple_path_joinE [OF arc_imp_simple_path assms]) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

677 
using n1 by force 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

678 
next 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

679 
assume ?rhs then show ?lhs 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

680 
using assms 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

681 
by (fastforce simp: pathfinish_def pathstart_def intro!: arc_join) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

682 
qed 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

683 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

684 
lemma arc_join_eq_alt: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

685 
"pathfinish g1 = pathstart g2 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

686 
\<Longrightarrow> (arc(g1 +++ g2) \<longleftrightarrow> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

687 
arc g1 \<and> arc g2 \<and> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

688 
path_image g1 \<inter> path_image g2 = {pathstart g2})" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

689 
using pathfinish_in_path_image by (fastforce simp: arc_join_eq) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

690 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

691 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

692 
subsection\<open>The joining of paths is associative\<close> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

693 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

694 
lemma path_assoc: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

695 
"\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

696 
\<Longrightarrow> path(p +++ (q +++ r)) \<longleftrightarrow> path((p +++ q) +++ r)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

697 
by simp 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

698 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

699 
lemma simple_path_assoc: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

700 
assumes "pathfinish p = pathstart q" "pathfinish q = pathstart r" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

701 
shows "simple_path (p +++ (q +++ r)) \<longleftrightarrow> simple_path ((p +++ q) +++ r)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

702 
proof (cases "pathstart p = pathfinish r") 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

703 
case True show ?thesis 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

704 
proof 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

705 
assume "simple_path (p +++ q +++ r)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

706 
with assms True show "simple_path ((p +++ q) +++ r)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

707 
by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

708 
dest: arc_distinct_ends [of r]) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

709 
next 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

710 
assume 0: "simple_path ((p +++ q) +++ r)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

711 
with assms True have q: "pathfinish r \<notin> path_image q" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

712 
using arc_distinct_ends 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

713 
by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

714 
have "pathstart r \<notin> path_image p" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

715 
using assms 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

716 
by (metis 0 IntI arc_distinct_ends arc_join_eq_alt empty_iff insert_iff 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

717 
pathfinish_in_path_image pathfinish_join simple_path_joinE) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

718 
with assms 0 q True show "simple_path (p +++ q +++ r)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

719 
by (auto simp: simple_path_join_loop_eq arc_join_eq path_image_join 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

720 
dest!: subsetD [OF _ IntI]) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

721 
qed 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

722 
next 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

723 
case False 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

724 
{ fix x :: 'a 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

725 
assume a: "path_image p \<inter> path_image q \<subseteq> {pathstart q}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

726 
"(path_image p \<union> path_image q) \<inter> path_image r \<subseteq> {pathstart r}" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

727 
"x \<in> path_image p" "x \<in> path_image r" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

728 
have "pathstart r \<in> path_image q" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

729 
by (metis assms(2) pathfinish_in_path_image) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

730 
with a have "x = pathstart q" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

731 
by blast 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

732 
} 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

733 
with False assms show ?thesis 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

734 
by (auto simp: simple_path_eq_arc simple_path_join_loop_eq arc_join_eq path_image_join) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

735 
qed 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

736 

bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

737 
lemma arc_assoc: 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

738 
"\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk> 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

739 
\<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)" 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

740 
by (simp add: arc_simple_path simple_path_assoc) 
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

741 

62620
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

742 
subsubsection\<open>Symmetry and loops\<close> 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

743 

d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

744 
lemma path_sym: 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

745 
"\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

746 
by auto 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

747 

d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

748 
lemma simple_path_sym: 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

749 
"\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

750 
\<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

751 
by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop) 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

752 

d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

753 
lemma path_image_sym: 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

754 
"\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

755 
\<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)" 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

756 
by (simp add: path_image_join sup_commute) 
d21dab28b3f9
New results about paths, segments, etc. The notion of simply_connected.
paulson <lp15@cam.ac.uk>
parents:
62618
diff
changeset

757 

62533
bc25f3916a99
new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents:
62398
diff
changeset

758 

61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

759 
section\<open>Choosing a subpath of an existing path\<close> 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

760 

60303  761 
definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector" 
762 
where "subpath a b g \<equiv> \<lambda>x. g((b  a) * x + a)" 

763 

61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

764 
lemma path_image_subpath_gen: 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

765 
fixes g :: "_ \<Rightarrow> 'a::real_normed_vector" 
60303  766 
shows "path_image(subpath u v g) = g ` (closed_segment u v)" 
767 
apply (simp add: closed_segment_real_eq path_image_def subpath_def) 

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

769 
apply (simp add: image_comp [symmetric]) 

770 
done 

771 

61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

772 
lemma path_image_subpath: 
60303  773 
fixes g :: "real \<Rightarrow> 'a::real_normed_vector" 
774 
shows "path_image(subpath u v g) = (if u \<le> v then g ` {u..v} else g ` {v..u})" 

61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

775 
by (simp add: path_image_subpath_gen closed_segment_eq_real_ivl) 
60303  776 

777 
lemma path_subpath [simp]: 

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

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

780 
shows "path(subpath u v g)" 

781 
proof  

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

783 
apply (rule continuous_intros  simp)+ 

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

785 
using assms 

786 
apply (auto simp: path_def continuous_on_subset) 

787 
done 

788 
then show ?thesis 

789 
by (simp add: path_def subpath_def) 

49653  790 
qed 
36583  791 

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

794 

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

796 
by (simp add: pathfinish_def subpath_def) 

797 

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

799 
by (simp add: subpath_def) 

800 

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

802 
by (simp add: reversepath_def subpath_def) 

803 

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

805 
by (simp add: reversepath_def subpath_def algebra_simps) 

806 

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

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

809 

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

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

812 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

813 
lemma affine_ineq: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

814 
fixes x :: "'a::linordered_idom" 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

815 
assumes "x \<le> 1" "v \<le> u" 
60303  816 
shows "v + x * u \<le> u + x * v" 
817 
proof  

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

819 
using assms by auto 

820 
then show ?thesis 

821 
by (simp add: algebra_simps) 

49653  822 
qed 
36583  823 

61711
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

824 
lemma sum_le_prod1: 
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

825 
fixes a::real shows "\<lbrakk>a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a + b \<le> 1 + a * b" 
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

826 
by (metis add.commute affine_ineq less_eq_real_def mult.right_neutral) 
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61699
diff
changeset

827 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

828 
lemma simple_path_subpath_eq: 
60303  829 
"simple_path(subpath u v g) \<longleftrightarrow> 
830 
path(subpath u v g) \<and> u\<noteq>v \<and> 

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

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

833 
(is "?lhs = ?rhs") 

834 
proof (rule iffI) 

835 
assume ?lhs 

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

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

837 
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> 
60303  838 
\<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)" 
839 
by (auto simp: simple_path_def subpath_def) 

840 
{ fix x y 

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

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

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

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

844 
by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost divide_simps 
62390  845 
split: if_split_asm) 
60303  846 
} moreover 
847 
have "path(subpath u v g) \<and> u\<noteq>v" 

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

849 
by (auto simp: subpath_def) 

850 
ultimately show ?rhs 

851 
by metis 

852 
next 

853 
assume ?rhs 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

854 
then 
60303  855 
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" 
856 
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" 

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

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

859 
by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost) 

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

861 
by algebra 

862 
show ?lhs using psp ne 

863 
unfolding simple_path_def subpath_def 

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

865 
qed 

866 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

867 
lemma arc_subpath_eq: 
60303  868 
"arc(subpath u v g) \<longleftrightarrow> path(subpath u v g) \<and> u\<noteq>v \<and> inj_on g (closed_segment u v)" 
869 
(is "?lhs = ?rhs") 

870 
proof (rule iffI) 

871 
assume ?lhs 

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

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

873 
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> 
60303  874 
\<Longrightarrow> x = y)" 
875 
by (auto simp: arc_def inj_on_def subpath_def) 

876 
{ fix x y 

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

878 
then have "x = y" 

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

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

880 
by (force simp add: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps 
62390  881 
split: if_split_asm) 
60303  882 
} moreover 
883 
have "path(subpath u v g) \<and> u\<noteq>v" 

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

885 
by (auto simp: subpath_def) 

886 
ultimately show ?rhs 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

887 
unfolding inj_on_def 
60303  888 
by metis 
889 
next 

890 
assume ?rhs 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

891 
then 
60303  892 
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" 
893 
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" 

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

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

896 
by (auto simp: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost) 

897 
show ?lhs using psp ne 

898 
unfolding arc_def subpath_def inj_on_def 

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

900 
qed 

901 

902 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

903 
lemma simple_path_subpath: 
60303  904 
assumes "simple_path g" "u \<in> {0..1}" "v \<in> {0..1}" "u \<noteq> v" 
905 
shows "simple_path(subpath u v g)" 

906 
using assms 

907 
apply (simp add: simple_path_subpath_eq simple_path_imp_path) 

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

909 
done 

910 

911 
lemma arc_simple_path_subpath: 

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

913 
by (force intro: simple_path_subpath simple_path_imp_arc) 

914 

915 
lemma arc_subpath_arc: 

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

917 
by (meson arc_def arc_imp_simple_path arc_simple_path_subpath inj_onD) 

918 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

919 
lemma arc_simple_path_subpath_interior: 
60303  920 
"\<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)" 
921 
apply (rule arc_simple_path_subpath) 

922 
apply (force simp: simple_path_def)+ 

923 
done 

924 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60420
diff
changeset

925 
lemma path_image_subpath_subset: 
60303  926 
"\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g" 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

927 
apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath) 
60303  928 
apply (auto simp: path_image_def) 
929 
done 

930 

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

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

53640  933 

61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

934 
subsection\<open>There is a subpath to the frontier\<close> 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

935 

ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

936 
lemma subpath_to_frontier_explicit: 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

937 
fixes S :: "'a::metric_space set" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

938 
assumes g: "path g" and "pathfinish g \<notin> S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

939 
obtains u where "0 \<le> u" "u \<le> 1" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

940 
"\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

941 
"(g u \<notin> interior S)" "(u = 0 \<or> g u \<in> closure S)" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

942 
proof  
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

943 
have gcon: "continuous_on {0..1} g" using g by (simp add: path_def) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

944 
then have com: "compact ({0..1} \<inter> {u. g u \<in> closure ( S)})" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

945 
apply (simp add: Int_commute [of "{0..1}"] compact_eq_bounded_closed closed_vimage_Int [unfolded vimage_def]) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

946 
using compact_eq_bounded_closed apply fastforce 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

947 
done 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

948 
have "1 \<in> {u. g u \<in> closure ( S)}" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

949 
using assms by (simp add: pathfinish_def closure_def) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

950 
then have dis: "{0..1} \<inter> {u. g u \<in> closure ( S)} \<noteq> {}" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

951 
using atLeastAtMost_iff zero_le_one by blast 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

952 
then obtain u where "0 \<le> u" "u \<le> 1" and gu: "g u \<in> closure ( S)" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

953 
and umin: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; g t \<in> closure ( S)\<rbrakk> \<Longrightarrow> u \<le> t" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

954 
using compact_attains_inf [OF com dis] by fastforce 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

955 
then have umin': "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1; t < u\<rbrakk> \<Longrightarrow> g t \<in> S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

956 
using closure_def by fastforce 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

957 
{ assume "u \<noteq> 0" 
61808  958 
then have "u > 0" using \<open>0 \<le> u\<close> by auto 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

959 
{ fix e::real assume "e > 0" 
62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62381
diff
changeset

960 
obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {0..1}; dist x' u \<le> d\<rbrakk> \<Longrightarrow> dist (g x') (g u) < e" 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62381
diff
changeset

961 
using continuous_onE [OF gcon _ \<open>e > 0\<close>] \<open>0 \<le> _\<close> \<open>_ \<le> 1\<close> atLeastAtMost_iff by auto 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62381
diff
changeset

962 
have *: "dist (max 0 (u  d / 2)) u \<le> d" 
61808  963 
using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close> by (simp add: dist_real_def) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

964 
have "\<exists>y\<in>S. dist y (g u) < e" 
61808  965 
using \<open>0 < u\<close> \<open>u \<le> 1\<close> \<open>d > 0\<close> 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

966 
by (force intro: d [OF _ *] umin') 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

967 
} 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

968 
then have "g u \<in> closure S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

969 
by (simp add: frontier_def closure_approachable) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

970 
} 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

971 
then show ?thesis 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

972 
apply (rule_tac u=u in that) 
61808  973 
apply (auto simp: \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> gu interior_closure umin) 
974 
using \<open>_ \<le> 1\<close> interior_closure umin apply fastforce 

61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

975 
done 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

976 
qed 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

977 

ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

978 
lemma subpath_to_frontier_strong: 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

979 
assumes g: "path g" and "pathfinish g \<notin> S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

980 
obtains u where "0 \<le> u" "u \<le> 1" "g u \<notin> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

981 
"u = 0 \<or> (\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

982 
proof  
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

983 
obtain u where "0 \<le> u" "u \<le> 1" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

984 
and gxin: "\<And>x. 0 \<le> x \<and> x < u \<Longrightarrow> g x \<in> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

985 
and gunot: "(g u \<notin> interior S)" and u0: "(u = 0 \<or> g u \<in> closure S)" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

986 
using subpath_to_frontier_explicit [OF assms] by blast 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

987 
show ?thesis 
61808  988 
apply (rule that [OF \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>]) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

989 
apply (simp add: gunot) 
61808  990 
using \<open>0 \<le> u\<close> u0 by (force simp: subpath_def gxin) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

991 
qed 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

992 

ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

993 
lemma subpath_to_frontier: 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

994 
assumes g: "path g" and g0: "pathstart g \<in> closure S" and g1: "pathfinish g \<notin> S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

995 
obtains u where "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g)  {g u}) \<subseteq> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

996 
proof  
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

997 
obtain u where "0 \<le> u" "u \<le> 1" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

998 
and notin: "g u \<notin> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

999 
and disj: "u = 0 \<or> 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1000 
(\<forall>x. 0 \<le> x \<and> x < 1 \<longrightarrow> subpath 0 u g x \<in> interior S) \<and> g u \<in> closure S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1001 
using subpath_to_frontier_strong [OF g g1] by blast 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1002 
show ?thesis 
61808  1003 
apply (rule that [OF \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>]) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1004 
apply (metis DiffI disj frontier_def g0 notin pathstart_def) 
61808  1005 
using \<open>0 \<le> u\<close> g0 disj 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

1006 
apply (simp add: path_image_subpath_gen) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1007 
apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1008 
apply (rename_tac y) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1009 
apply (drule_tac x="y/u" in spec) 
62390  1010 
apply (auto split: if_split_asm) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1011 
done 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1012 
qed 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1013 

ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1014 
lemma exists_path_subpath_to_frontier: 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1015 
fixes S :: "'a::real_normed_vector set" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1016 
assumes "path g" "pathstart g \<in> closure S" "pathfinish g \<notin> S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1017 
obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1018 
"path_image h  {pathfinish h} \<subseteq> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1019 
"pathfinish h \<in> frontier S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1020 
proof  
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1021 
obtain u where u: "0 \<le> u" "u \<le> 1" "g u \<in> frontier S" "(path_image(subpath 0 u g)  {g u}) \<subseteq> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1022 
using subpath_to_frontier [OF assms] by blast 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1023 
show ?thesis 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1024 
apply (rule that [of "subpath 0 u g"]) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1025 
using assms u 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61738
diff
changeset

1026 
apply (simp_all add: path_image_subpath) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1027 
apply (simp add: pathstart_def) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1028 
apply (force simp: closed_segment_eq_real_ivl path_image_def) 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1029 
done 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1030 
qed 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1031 

ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1032 
lemma exists_path_subpath_to_frontier_closed: 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1033 
fixes S :: "'a::real_normed_vector set" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1034 
assumes S: "closed S" and g: "path g" and g0: "pathstart g \<in> S" and g1: "pathfinish g \<notin> S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1035 
obtains h where "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g \<inter> S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1036 
"pathfinish h \<in> frontier S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1037 
proof  
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1038 
obtain h where h: "path h" "pathstart h = pathstart g" "path_image h \<subseteq> path_image g" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1039 
"path_image h  {pathfinish h} \<subseteq> interior S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1040 
"pathfinish h \<in> frontier S" 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1041 
using exists_path_subpath_to_frontier [OF g _ g1] closure_closed [OF S] g0 by auto 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1042 
show ?thesis 
61808  1043 
apply (rule that [OF \<open>path h\<close>]) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1044 
using assms h 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1045 
apply auto 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61808
diff
changeset

1046 
apply (metis Diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff) 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1047 
done 
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61426
diff
changeset

1048 
qed 
49653  1049 

60420  1050 
subsection \<open>Reparametrizing a closed curve to start at some chosen point\<close> 
36583  1051 

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

36583  1054 

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

49653  1058 
lemma pathfinish_shiftpath: 
53640  1059 
assumes "0 \<le> a" 
1060 
and "pathfinish g = pathstart g" 

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

1062 
using assms 

1063 
unfolding pathstart_def pathfinish_def shiftpath_def 

36583  1064 
by auto 
1065 

1066 
lemma endpoints_shiftpath: 

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

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

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

1071 
using assms 

1072 
by (auto intro!: pathfinish_shiftpath pathstart_shiftpath) 

36583  1073 

1074 
lemma closed_shiftpath: 

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

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

1078 
using endpoints_shiftpath[OF assms] 

1079 
by auto 

36583  1080 

1081 
lemma path_shiftpath: 

53640  1082 
assumes "path g" 
1083 
and "pathfinish g = pathstart g" 

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

1085 
shows "path (shiftpath a g)" 

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

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

49653  1092 
show ?thesis 
1093 
unfolding path_def shiftpath_def * 

62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62381
diff
changeset

1094 
apply (rule continuous_on_closed_Un) 
49653  1095 
apply (rule closed_real_atLeastAtMost)+ 
53640  1096 
apply (rule continuous_on_eq[of _ "g \<circ> (\<lambda>x. a + x)"]) 
1097 
prefer 3 

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

1099 
prefer 3 

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

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

1102 
apply (rule continuous_intros)+ 
49653  1103 
apply (rule_tac[12] continuous_on_subset[OF assms(1)[unfolded path_def]]) 
1104 
using assms(3) and ** 

53640  1105 
apply auto 
1106 
apply (auto simp add: field_simps) 

49653  1107 
done 
1108 
qed 

36583  1109 

49653  1110 
lemma shiftpath_shiftpath: 
53640  1111 
assumes "pathfinish g = pathstart g" 
1112 
and "a \<in> {0..1}" 

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

36583  1114 
shows "shiftpath (1  a) (shiftpath a g) x = g x" 
53640  1115 
using assms 
1116 
unfolding pathfinish_def pathstart_def shiftpath_def 

1117 
by auto 

36583  1118 

1119 
lemma path_image_shiftpath: 

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

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

49653  1123 
proof  
1124 
{ fix x 

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

49654  1129 
then show ?thesis 
49653  1130 
apply (rule_tac x="1 + x  a" in bexI) 
36583  1131 
using as(1,2) and as(3)[THEN bspec[where x="1 + x  a"]] and assms(1) 
49653  1132 
apply (auto simp add: field_simps atomize_not) 
1133 
done 

1134 
next 

1135 
case True 

53640  1136 
then show ?thesis 
1137 
using as(12) and assms(1) 

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

1139 
apply (auto simp add: field_simps) 

1140 
done 

49653  1141 
qed 
1142 
} 

49654  1143 
then show ?thesis 
53640  1144 
using assms 
1145 
unfolding shiftpath_def path_image_def pathfinish_def pathstart_def 

1146 
by (auto simp add: image_iff) 

49653  1147 
qed 
1148 

36583  1149 

60420  1150 
subsection \<open>Special case of straightline paths\<close> 
36583  1151 

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

36583  1154 

53640  1155 
lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a" 