1 (* Author: John Harrison |
|
2 Author: Robert Himmelmann, TU Muenchen (translation from HOL light) |
|
3 *) |
|
4 |
|
5 section \<open>Fashoda meet theorem\<close> |
|
6 |
|
7 theory Fashoda |
|
8 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space |
|
9 begin |
|
10 |
|
11 subsection \<open>Bijections between intervals.\<close> |
|
12 |
|
13 definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space" |
|
14 where "interval_bij = |
|
15 (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))" |
|
16 |
|
17 lemma interval_bij_affine: |
|
18 "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) + |
|
19 (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))" |
|
20 by (auto simp: setsum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff |
|
21 field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum.cong) |
|
22 |
|
23 lemma continuous_interval_bij: |
|
24 fixes a b :: "'a::euclidean_space" |
|
25 shows "continuous (at x) (interval_bij (a, b) (u, v))" |
|
26 by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros) |
|
27 |
|
28 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))" |
|
29 apply(rule continuous_at_imp_continuous_on) |
|
30 apply (rule, rule continuous_interval_bij) |
|
31 done |
|
32 |
|
33 lemma in_interval_interval_bij: |
|
34 fixes a b u v x :: "'a::euclidean_space" |
|
35 assumes "x \<in> cbox a b" |
|
36 and "cbox u v \<noteq> {}" |
|
37 shows "interval_bij (a, b) (u, v) x \<in> cbox u v" |
|
38 apply (simp only: interval_bij_def split_conv mem_box inner_setsum_left_Basis cong: ball_cong) |
|
39 apply safe |
|
40 proof - |
|
41 fix i :: 'a |
|
42 assume i: "i \<in> Basis" |
|
43 have "cbox a b \<noteq> {}" |
|
44 using assms by auto |
|
45 with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i" |
|
46 using assms(2) by (auto simp add: box_eq_empty) |
|
47 have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i" |
|
48 using assms(1)[unfolded mem_box] using i by auto |
|
49 have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)" |
|
50 using * x by auto |
|
51 then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)" |
|
52 using * by auto |
|
53 have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)" |
|
54 apply (rule mult_right_mono) |
|
55 unfolding divide_le_eq_1 |
|
56 using * x |
|
57 apply auto |
|
58 done |
|
59 then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i" |
|
60 using * by auto |
|
61 qed |
|
62 |
|
63 lemma interval_bij_bij: |
|
64 "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow> |
|
65 interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x" |
|
66 by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a]) |
|
67 |
|
68 lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i" |
|
69 shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x" |
|
70 using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis) |
|
71 |
|
72 |
|
73 subsection \<open>Fashoda meet theorem\<close> |
|
74 |
|
75 lemma infnorm_2: |
|
76 fixes x :: "real^2" |
|
77 shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>" |
|
78 unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto |
|
79 |
|
80 lemma infnorm_eq_1_2: |
|
81 fixes x :: "real^2" |
|
82 shows "infnorm x = 1 \<longleftrightarrow> |
|
83 \<bar>x$1\<bar> \<le> 1 \<and> \<bar>x$2\<bar> \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)" |
|
84 unfolding infnorm_2 by auto |
|
85 |
|
86 lemma infnorm_eq_1_imp: |
|
87 fixes x :: "real^2" |
|
88 assumes "infnorm x = 1" |
|
89 shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1" |
|
90 using assms unfolding infnorm_eq_1_2 by auto |
|
91 |
|
92 lemma fashoda_unit: |
|
93 fixes f g :: "real \<Rightarrow> real^2" |
|
94 assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1" |
|
95 and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1" |
|
96 and "continuous_on {-1 .. 1} f" |
|
97 and "continuous_on {-1 .. 1} g" |
|
98 and "f (- 1)$1 = - 1" |
|
99 and "f 1$1 = 1" "g (- 1) $2 = -1" |
|
100 and "g 1 $2 = 1" |
|
101 shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t" |
|
102 proof (rule ccontr) |
|
103 assume "\<not> ?thesis" |
|
104 note as = this[unfolded bex_simps,rule_format] |
|
105 define sqprojection |
|
106 where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2" |
|
107 define negatex :: "real^2 \<Rightarrow> real^2" |
|
108 where "negatex x = (vector [-(x$1), x$2])" for x |
|
109 have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z" |
|
110 unfolding negatex_def infnorm_2 vector_2 by auto |
|
111 have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1" |
|
112 unfolding sqprojection_def |
|
113 unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] |
|
114 unfolding abs_inverse real_abs_infnorm |
|
115 apply (subst infnorm_eq_0[symmetric]) |
|
116 apply auto |
|
117 done |
|
118 let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w" |
|
119 have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1 .. 1}" |
|
120 apply (rule set_eqI) |
|
121 unfolding image_iff Bex_def mem_interval_cart interval_cbox_cart |
|
122 apply rule |
|
123 defer |
|
124 apply (rule_tac x="vec x" in exI) |
|
125 apply auto |
|
126 done |
|
127 { |
|
128 fix x |
|
129 assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` (cbox (- 1) (1::real^2))" |
|
130 then obtain w :: "real^2" where w: |
|
131 "w \<in> cbox (- 1) 1" |
|
132 "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w" |
|
133 unfolding image_iff .. |
|
134 then have "x \<noteq> 0" |
|
135 using as[of "w$1" "w$2"] |
|
136 unfolding mem_interval_cart atLeastAtMost_iff |
|
137 by auto |
|
138 } note x0 = this |
|
139 have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2" |
|
140 using UNIV_2 by auto |
|
141 have 1: "box (- 1) (1::real^2) \<noteq> {}" |
|
142 unfolding interval_eq_empty_cart by auto |
|
143 have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)" |
|
144 apply (intro continuous_intros continuous_on_component) |
|
145 unfolding * |
|
146 apply (rule assms)+ |
|
147 apply (subst sqprojection_def) |
|
148 apply (intro continuous_intros) |
|
149 apply (simp add: infnorm_eq_0 x0) |
|
150 apply (rule linear_continuous_on) |
|
151 proof - |
|
152 show "bounded_linear negatex" |
|
153 apply (rule bounded_linearI') |
|
154 unfolding vec_eq_iff |
|
155 proof (rule_tac[!] allI) |
|
156 fix i :: 2 |
|
157 fix x y :: "real^2" |
|
158 fix c :: real |
|
159 show "negatex (x + y) $ i = |
|
160 (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" |
|
161 apply - |
|
162 apply (case_tac[!] "i\<noteq>1") |
|
163 prefer 3 |
|
164 apply (drule_tac[1-2] 21) |
|
165 unfolding negatex_def |
|
166 apply (auto simp add:vector_2) |
|
167 done |
|
168 qed |
|
169 qed |
|
170 have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1" |
|
171 unfolding subset_eq |
|
172 proof (rule, goal_cases) |
|
173 case (1 x) |
|
174 then obtain y :: "real^2" where y: |
|
175 "y \<in> cbox (- 1) 1" |
|
176 "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y" |
|
177 unfolding image_iff .. |
|
178 have "?F y \<noteq> 0" |
|
179 apply (rule x0) |
|
180 using y(1) |
|
181 apply auto |
|
182 done |
|
183 then have *: "infnorm (sqprojection (?F y)) = 1" |
|
184 unfolding y o_def |
|
185 by - (rule lem2[rule_format]) |
|
186 have "infnorm x = 1" |
|
187 unfolding *[symmetric] y o_def |
|
188 by (rule lem1[rule_format]) |
|
189 then show "x \<in> cbox (-1) 1" |
|
190 unfolding mem_interval_cart interval_cbox_cart infnorm_2 |
|
191 apply - |
|
192 apply rule |
|
193 proof - |
|
194 fix i |
|
195 assume "max \<bar>x $ 1\<bar> \<bar>x $ 2\<bar> = 1" |
|
196 then show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i" |
|
197 apply (cases "i = 1") |
|
198 defer |
|
199 apply (drule 21) |
|
200 apply auto |
|
201 done |
|
202 qed |
|
203 qed |
|
204 obtain x :: "real^2" where x: |
|
205 "x \<in> cbox (- 1) 1" |
|
206 "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x" |
|
207 apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"]) |
|
208 apply (rule compact_cbox convex_box)+ |
|
209 unfolding interior_cbox |
|
210 apply (rule 1 2 3)+ |
|
211 apply blast |
|
212 done |
|
213 have "?F x \<noteq> 0" |
|
214 apply (rule x0) |
|
215 using x(1) |
|
216 apply auto |
|
217 done |
|
218 then have *: "infnorm (sqprojection (?F x)) = 1" |
|
219 unfolding o_def |
|
220 by (rule lem2[rule_format]) |
|
221 have nx: "infnorm x = 1" |
|
222 apply (subst x(2)[symmetric]) |
|
223 unfolding *[symmetric] o_def |
|
224 apply (rule lem1[rule_format]) |
|
225 done |
|
226 have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" |
|
227 and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)" |
|
228 apply - |
|
229 apply (rule_tac[!] allI impI)+ |
|
230 proof - |
|
231 fix x :: "real^2" |
|
232 fix i :: 2 |
|
233 assume x: "x \<noteq> 0" |
|
234 have "inverse (infnorm x) > 0" |
|
235 using x[unfolded infnorm_pos_lt[symmetric]] by auto |
|
236 then show "(0 < sqprojection x $ i) = (0 < x $ i)" |
|
237 and "(sqprojection x $ i < 0) = (x $ i < 0)" |
|
238 unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def |
|
239 unfolding zero_less_mult_iff mult_less_0_iff |
|
240 by (auto simp add: field_simps) |
|
241 qed |
|
242 note lem3 = this[rule_format] |
|
243 have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" |
|
244 using x(1) unfolding mem_interval_cart by auto |
|
245 then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0" |
|
246 unfolding right_minus_eq |
|
247 apply - |
|
248 apply (rule as) |
|
249 apply auto |
|
250 done |
|
251 have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" |
|
252 using nx unfolding infnorm_eq_1_2 by auto |
|
253 then show False |
|
254 proof - |
|
255 fix P Q R S |
|
256 presume "P \<or> Q \<or> R \<or> S" |
|
257 and "P \<Longrightarrow> False" |
|
258 and "Q \<Longrightarrow> False" |
|
259 and "R \<Longrightarrow> False" |
|
260 and "S \<Longrightarrow> False" |
|
261 then show False by auto |
|
262 next |
|
263 assume as: "x$1 = 1" |
|
264 then have *: "f (x $ 1) $ 1 = 1" |
|
265 using assms(6) by auto |
|
266 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" |
|
267 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
|
268 unfolding as negatex_def vector_2 |
|
269 by auto |
|
270 moreover |
|
271 from x1 have "g (x $ 2) \<in> cbox (-1) 1" |
|
272 apply - |
|
273 apply (rule assms(2)[unfolded subset_eq,rule_format]) |
|
274 apply auto |
|
275 done |
|
276 ultimately show False |
|
277 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
278 apply (erule_tac x=1 in allE) |
|
279 apply auto |
|
280 done |
|
281 next |
|
282 assume as: "x$1 = -1" |
|
283 then have *: "f (x $ 1) $ 1 = - 1" |
|
284 using assms(5) by auto |
|
285 have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" |
|
286 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
|
287 unfolding as negatex_def vector_2 |
|
288 by auto |
|
289 moreover |
|
290 from x1 have "g (x $ 2) \<in> cbox (-1) 1" |
|
291 apply - |
|
292 apply (rule assms(2)[unfolded subset_eq,rule_format]) |
|
293 apply auto |
|
294 done |
|
295 ultimately show False |
|
296 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
297 apply (erule_tac x=1 in allE) |
|
298 apply auto |
|
299 done |
|
300 next |
|
301 assume as: "x$2 = 1" |
|
302 then have *: "g (x $ 2) $ 2 = 1" |
|
303 using assms(8) by auto |
|
304 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
|
305 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
|
306 unfolding as negatex_def vector_2 |
|
307 by auto |
|
308 moreover |
|
309 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
|
310 apply - |
|
311 apply (rule assms(1)[unfolded subset_eq,rule_format]) |
|
312 apply auto |
|
313 done |
|
314 ultimately show False |
|
315 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
316 apply (erule_tac x=2 in allE) |
|
317 apply auto |
|
318 done |
|
319 next |
|
320 assume as: "x$2 = -1" |
|
321 then have *: "g (x $ 2) $ 2 = - 1" |
|
322 using assms(7) by auto |
|
323 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
|
324 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
|
325 unfolding as negatex_def vector_2 |
|
326 by auto |
|
327 moreover |
|
328 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
|
329 apply - |
|
330 apply (rule assms(1)[unfolded subset_eq,rule_format]) |
|
331 apply auto |
|
332 done |
|
333 ultimately show False |
|
334 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
335 apply (erule_tac x=2 in allE) |
|
336 apply auto |
|
337 done |
|
338 qed auto |
|
339 qed |
|
340 |
|
341 lemma fashoda_unit_path: |
|
342 fixes f g :: "real \<Rightarrow> real^2" |
|
343 assumes "path f" |
|
344 and "path g" |
|
345 and "path_image f \<subseteq> cbox (-1) 1" |
|
346 and "path_image g \<subseteq> cbox (-1) 1" |
|
347 and "(pathstart f)$1 = -1" |
|
348 and "(pathfinish f)$1 = 1" |
|
349 and "(pathstart g)$2 = -1" |
|
350 and "(pathfinish g)$2 = 1" |
|
351 obtains z where "z \<in> path_image f" and "z \<in> path_image g" |
|
352 proof - |
|
353 note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] |
|
354 define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real |
|
355 have isc: "iscale ` {- 1..1} \<subseteq> {0..1}" |
|
356 unfolding iscale_def by auto |
|
357 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" |
|
358 proof (rule fashoda_unit) |
|
359 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" |
|
360 using isc and assms(3-4) by (auto simp add: image_comp [symmetric]) |
|
361 have *: "continuous_on {- 1..1} iscale" |
|
362 unfolding iscale_def by (rule continuous_intros)+ |
|
363 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)" |
|
364 apply - |
|
365 apply (rule_tac[!] continuous_on_compose[OF *]) |
|
366 apply (rule_tac[!] continuous_on_subset[OF _ isc]) |
|
367 apply (rule assms)+ |
|
368 done |
|
369 have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" |
|
370 unfolding vec_eq_iff by auto |
|
371 show "(f \<circ> iscale) (- 1) $ 1 = - 1" |
|
372 and "(f \<circ> iscale) 1 $ 1 = 1" |
|
373 and "(g \<circ> iscale) (- 1) $ 2 = -1" |
|
374 and "(g \<circ> iscale) 1 $ 2 = 1" |
|
375 unfolding o_def iscale_def |
|
376 using assms |
|
377 by (auto simp add: *) |
|
378 qed |
|
379 then obtain s t where st: |
|
380 "s \<in> {- 1..1}" |
|
381 "t \<in> {- 1..1}" |
|
382 "(f \<circ> iscale) s = (g \<circ> iscale) t" |
|
383 by auto |
|
384 show thesis |
|
385 apply (rule_tac z = "f (iscale s)" in that) |
|
386 using st |
|
387 unfolding o_def path_image_def image_iff |
|
388 apply - |
|
389 apply (rule_tac x="iscale s" in bexI) |
|
390 prefer 3 |
|
391 apply (rule_tac x="iscale t" in bexI) |
|
392 using isc[unfolded subset_eq, rule_format] |
|
393 apply auto |
|
394 done |
|
395 qed |
|
396 |
|
397 lemma fashoda: |
|
398 fixes b :: "real^2" |
|
399 assumes "path f" |
|
400 and "path g" |
|
401 and "path_image f \<subseteq> cbox a b" |
|
402 and "path_image g \<subseteq> cbox a b" |
|
403 and "(pathstart f)$1 = a$1" |
|
404 and "(pathfinish f)$1 = b$1" |
|
405 and "(pathstart g)$2 = a$2" |
|
406 and "(pathfinish g)$2 = b$2" |
|
407 obtains z where "z \<in> path_image f" and "z \<in> path_image g" |
|
408 proof - |
|
409 fix P Q S |
|
410 presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis" |
|
411 then show thesis |
|
412 by auto |
|
413 next |
|
414 have "cbox a b \<noteq> {}" |
|
415 using assms(3) using path_image_nonempty[of f] by auto |
|
416 then have "a \<le> b" |
|
417 unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less) |
|
418 then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" |
|
419 unfolding less_eq_vec_def forall_2 by auto |
|
420 next |
|
421 assume as: "a$1 = b$1" |
|
422 have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" |
|
423 apply (rule connected_ivt_component_cart) |
|
424 apply (rule connected_path_image assms)+ |
|
425 apply (rule pathstart_in_path_image) |
|
426 apply (rule pathfinish_in_path_image) |
|
427 unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"] |
|
428 unfolding pathstart_def |
|
429 apply (auto simp add: less_eq_vec_def mem_interval_cart) |
|
430 done |
|
431 then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" .. |
|
432 have "z \<in> cbox a b" |
|
433 using z(1) assms(4) |
|
434 unfolding path_image_def |
|
435 by blast |
|
436 then have "z = f 0" |
|
437 unfolding vec_eq_iff forall_2 |
|
438 unfolding z(2) pathstart_def |
|
439 using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1] |
|
440 unfolding mem_interval_cart |
|
441 apply (erule_tac x=1 in allE) |
|
442 using as |
|
443 apply auto |
|
444 done |
|
445 then show thesis |
|
446 apply - |
|
447 apply (rule that[OF _ z(1)]) |
|
448 unfolding path_image_def |
|
449 apply auto |
|
450 done |
|
451 next |
|
452 assume as: "a$2 = b$2" |
|
453 have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" |
|
454 apply (rule connected_ivt_component_cart) |
|
455 apply (rule connected_path_image assms)+ |
|
456 apply (rule pathstart_in_path_image) |
|
457 apply (rule pathfinish_in_path_image) |
|
458 unfolding assms |
|
459 using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"] |
|
460 unfolding pathstart_def |
|
461 apply (auto simp add: less_eq_vec_def mem_interval_cart) |
|
462 done |
|
463 then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" .. |
|
464 have "z \<in> cbox a b" |
|
465 using z(1) assms(3) |
|
466 unfolding path_image_def |
|
467 by blast |
|
468 then have "z = g 0" |
|
469 unfolding vec_eq_iff forall_2 |
|
470 unfolding z(2) pathstart_def |
|
471 using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2] |
|
472 unfolding mem_interval_cart |
|
473 apply (erule_tac x=2 in allE) |
|
474 using as |
|
475 apply auto |
|
476 done |
|
477 then show thesis |
|
478 apply - |
|
479 apply (rule that[OF z(1)]) |
|
480 unfolding path_image_def |
|
481 apply auto |
|
482 done |
|
483 next |
|
484 assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2" |
|
485 have int_nem: "cbox (-1) (1::real^2) \<noteq> {}" |
|
486 unfolding interval_eq_empty_cart by auto |
|
487 obtain z :: "real^2" where z: |
|
488 "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
|
489 "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
|
490 apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) |
|
491 unfolding path_def path_image_def pathstart_def pathfinish_def |
|
492 apply (rule_tac[1-2] continuous_on_compose) |
|
493 apply (rule assms[unfolded path_def] continuous_on_interval_bij)+ |
|
494 unfolding subset_eq |
|
495 apply(rule_tac[1-2] ballI) |
|
496 proof - |
|
497 fix x |
|
498 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
|
499 then obtain y where y: |
|
500 "y \<in> {0..1}" |
|
501 "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y" |
|
502 unfolding image_iff .. |
|
503 show "x \<in> cbox (- 1) 1" |
|
504 unfolding y o_def |
|
505 apply (rule in_interval_interval_bij) |
|
506 using y(1) |
|
507 using assms(3)[unfolded path_image_def subset_eq] int_nem |
|
508 apply auto |
|
509 done |
|
510 next |
|
511 fix x |
|
512 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
|
513 then obtain y where y: |
|
514 "y \<in> {0..1}" |
|
515 "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y" |
|
516 unfolding image_iff .. |
|
517 show "x \<in> cbox (- 1) 1" |
|
518 unfolding y o_def |
|
519 apply (rule in_interval_interval_bij) |
|
520 using y(1) |
|
521 using assms(4)[unfolded path_image_def subset_eq] int_nem |
|
522 apply auto |
|
523 done |
|
524 next |
|
525 show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1" |
|
526 and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1" |
|
527 and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1" |
|
528 and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" |
|
529 using assms as |
|
530 by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def) |
|
531 (simp_all add: inner_axis) |
|
532 qed |
|
533 from z(1) obtain zf where zf: |
|
534 "zf \<in> {0..1}" |
|
535 "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf" |
|
536 unfolding image_iff .. |
|
537 from z(2) obtain zg where zg: |
|
538 "zg \<in> {0..1}" |
|
539 "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg" |
|
540 unfolding image_iff .. |
|
541 have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" |
|
542 unfolding forall_2 |
|
543 using as |
|
544 by auto |
|
545 show thesis |
|
546 apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that) |
|
547 apply (subst zf) |
|
548 defer |
|
549 apply (subst zg) |
|
550 unfolding o_def interval_bij_bij_cart[OF *] path_image_def |
|
551 using zf(1) zg(1) |
|
552 apply auto |
|
553 done |
|
554 qed |
|
555 |
|
556 |
|
557 subsection \<open>Some slightly ad hoc lemmas I use below\<close> |
|
558 |
|
559 lemma segment_vertical: |
|
560 fixes a :: "real^2" |
|
561 assumes "a$1 = b$1" |
|
562 shows "x \<in> closed_segment a b \<longleftrightarrow> |
|
563 x$1 = a$1 \<and> x$1 = b$1 \<and> (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2)" |
|
564 (is "_ = ?R") |
|
565 proof - |
|
566 let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1" |
|
567 { |
|
568 presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L" |
|
569 then show ?thesis |
|
570 unfolding closed_segment_def mem_Collect_eq |
|
571 unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps |
|
572 by blast |
|
573 } |
|
574 { |
|
575 assume ?L |
|
576 then obtain u where u: |
|
577 "x $ 1 = (1 - u) * a $ 1 + u * b $ 1" |
|
578 "x $ 2 = (1 - u) * a $ 2 + u * b $ 2" |
|
579 "0 \<le> u" |
|
580 "u \<le> 1" |
|
581 by blast |
|
582 { fix b a |
|
583 assume "b + u * a > a + u * b" |
|
584 then have "(1 - u) * b > (1 - u) * a" |
|
585 by (auto simp add:field_simps) |
|
586 then have "b \<ge> a" |
|
587 apply (drule_tac mult_left_less_imp_less) |
|
588 using u |
|
589 apply auto |
|
590 done |
|
591 then have "u * a \<le> u * b" |
|
592 apply - |
|
593 apply (rule mult_left_mono[OF _ u(3)]) |
|
594 using u(3-4) |
|
595 apply (auto simp add: field_simps) |
|
596 done |
|
597 } note * = this |
|
598 { |
|
599 fix a b |
|
600 assume "u * b > u * a" |
|
601 then have "(1 - u) * a \<le> (1 - u) * b" |
|
602 apply - |
|
603 apply (rule mult_left_mono) |
|
604 apply (drule mult_left_less_imp_less) |
|
605 using u |
|
606 apply auto |
|
607 done |
|
608 then have "a + u * b \<le> b + u * a" |
|
609 by (auto simp add: field_simps) |
|
610 } note ** = this |
|
611 then show ?R |
|
612 unfolding u assms |
|
613 using u |
|
614 by (auto simp add:field_simps not_le intro: * **) |
|
615 } |
|
616 { |
|
617 assume ?R |
|
618 then show ?L |
|
619 proof (cases "x$2 = b$2") |
|
620 case True |
|
621 then show ?L |
|
622 apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) |
|
623 unfolding assms True |
|
624 using \<open>?R\<close> |
|
625 apply (auto simp add: field_simps) |
|
626 done |
|
627 next |
|
628 case False |
|
629 then show ?L |
|
630 apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) |
|
631 unfolding assms |
|
632 using \<open>?R\<close> |
|
633 apply (auto simp add: field_simps) |
|
634 done |
|
635 qed |
|
636 } |
|
637 qed |
|
638 |
|
639 lemma segment_horizontal: |
|
640 fixes a :: "real^2" |
|
641 assumes "a$2 = b$2" |
|
642 shows "x \<in> closed_segment a b \<longleftrightarrow> |
|
643 x$2 = a$2 \<and> x$2 = b$2 \<and> (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1)" |
|
644 (is "_ = ?R") |
|
645 proof - |
|
646 let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1" |
|
647 { |
|
648 presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L" |
|
649 then show ?thesis |
|
650 unfolding closed_segment_def mem_Collect_eq |
|
651 unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps |
|
652 by blast |
|
653 } |
|
654 { |
|
655 assume ?L |
|
656 then obtain u where u: |
|
657 "x $ 1 = (1 - u) * a $ 1 + u * b $ 1" |
|
658 "x $ 2 = (1 - u) * a $ 2 + u * b $ 2" |
|
659 "0 \<le> u" |
|
660 "u \<le> 1" |
|
661 by blast |
|
662 { |
|
663 fix b a |
|
664 assume "b + u * a > a + u * b" |
|
665 then have "(1 - u) * b > (1 - u) * a" |
|
666 by (auto simp add: field_simps) |
|
667 then have "b \<ge> a" |
|
668 apply (drule_tac mult_left_less_imp_less) |
|
669 using u |
|
670 apply auto |
|
671 done |
|
672 then have "u * a \<le> u * b" |
|
673 apply - |
|
674 apply (rule mult_left_mono[OF _ u(3)]) |
|
675 using u(3-4) |
|
676 apply (auto simp add: field_simps) |
|
677 done |
|
678 } note * = this |
|
679 { |
|
680 fix a b |
|
681 assume "u * b > u * a" |
|
682 then have "(1 - u) * a \<le> (1 - u) * b" |
|
683 apply - |
|
684 apply (rule mult_left_mono) |
|
685 apply (drule mult_left_less_imp_less) |
|
686 using u |
|
687 apply auto |
|
688 done |
|
689 then have "a + u * b \<le> b + u * a" |
|
690 by (auto simp add: field_simps) |
|
691 } note ** = this |
|
692 then show ?R |
|
693 unfolding u assms |
|
694 using u |
|
695 by (auto simp add: field_simps not_le intro: * **) |
|
696 } |
|
697 { |
|
698 assume ?R |
|
699 then show ?L |
|
700 proof (cases "x$1 = b$1") |
|
701 case True |
|
702 then show ?L |
|
703 apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) |
|
704 unfolding assms True |
|
705 using \<open>?R\<close> |
|
706 apply (auto simp add: field_simps) |
|
707 done |
|
708 next |
|
709 case False |
|
710 then show ?L |
|
711 apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) |
|
712 unfolding assms |
|
713 using \<open>?R\<close> |
|
714 apply (auto simp add: field_simps) |
|
715 done |
|
716 qed |
|
717 } |
|
718 qed |
|
719 |
|
720 |
|
721 subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close> |
|
722 |
|
723 lemma fashoda_interlace: |
|
724 fixes a :: "real^2" |
|
725 assumes "path f" |
|
726 and "path g" |
|
727 and "path_image f \<subseteq> cbox a b" |
|
728 and "path_image g \<subseteq> cbox a b" |
|
729 and "(pathstart f)$2 = a$2" |
|
730 and "(pathfinish f)$2 = a$2" |
|
731 and "(pathstart g)$2 = a$2" |
|
732 and "(pathfinish g)$2 = a$2" |
|
733 and "(pathstart f)$1 < (pathstart g)$1" |
|
734 and "(pathstart g)$1 < (pathfinish f)$1" |
|
735 and "(pathfinish f)$1 < (pathfinish g)$1" |
|
736 obtains z where "z \<in> path_image f" and "z \<in> path_image g" |
|
737 proof - |
|
738 have "cbox a b \<noteq> {}" |
|
739 using path_image_nonempty[of f] using assms(3) by auto |
|
740 note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less] |
|
741 have "pathstart f \<in> cbox a b" |
|
742 and "pathfinish f \<in> cbox a b" |
|
743 and "pathstart g \<in> cbox a b" |
|
744 and "pathfinish g \<in> cbox a b" |
|
745 using pathstart_in_path_image pathfinish_in_path_image |
|
746 using assms(3-4) |
|
747 by auto |
|
748 note startfin = this[unfolded mem_interval_cart forall_2] |
|
749 let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++ |
|
750 linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++ |
|
751 linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++ |
|
752 linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])" |
|
753 let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++ |
|
754 linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++ |
|
755 linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++ |
|
756 linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])" |
|
757 let ?a = "vector[a$1 - 2, a$2 - 3]" |
|
758 let ?b = "vector[b$1 + 2, b$2 + 3]" |
|
759 have P1P2: "path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union> |
|
760 path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union> |
|
761 path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union> |
|
762 path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))" |
|
763 "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union> |
|
764 path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union> |
|
765 path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union> |
|
766 path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2) |
|
767 by(auto simp add: path_image_join path_linepath) |
|
768 have abab: "cbox a b \<subseteq> cbox ?a ?b" |
|
769 unfolding interval_cbox_cart[symmetric] |
|
770 by (auto simp add:less_eq_vec_def forall_2 vector_2) |
|
771 obtain z where |
|
772 "z \<in> path_image |
|
773 (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++ |
|
774 linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++ |
|
775 f +++ |
|
776 linepath (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) +++ |
|
777 linepath (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]))" |
|
778 "z \<in> path_image |
|
779 (linepath (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g) +++ |
|
780 g +++ |
|
781 linepath (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1]) +++ |
|
782 linepath (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1]) +++ |
|
783 linepath (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]))" |
|
784 apply (rule fashoda[of ?P1 ?P2 ?a ?b]) |
|
785 unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 |
|
786 proof - |
|
787 show "path ?P1" and "path ?P2" |
|
788 using assms by auto |
|
789 have "path_image ?P1 \<subseteq> cbox ?a ?b" |
|
790 unfolding P1P2 path_image_linepath |
|
791 apply (rule Un_least)+ |
|
792 defer 3 |
|
793 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
|
794 unfolding mem_interval_cart forall_2 vector_2 |
|
795 using ab startfin abab assms(3) |
|
796 using assms(9-) |
|
797 unfolding assms |
|
798 apply (auto simp add: field_simps box_def) |
|
799 done |
|
800 then show "path_image ?P1 \<subseteq> cbox ?a ?b" . |
|
801 have "path_image ?P2 \<subseteq> cbox ?a ?b" |
|
802 unfolding P1P2 path_image_linepath |
|
803 apply (rule Un_least)+ |
|
804 defer 2 |
|
805 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
|
806 unfolding mem_interval_cart forall_2 vector_2 |
|
807 using ab startfin abab assms(4) |
|
808 using assms(9-) |
|
809 unfolding assms |
|
810 apply (auto simp add: field_simps box_def) |
|
811 done |
|
812 then show "path_image ?P2 \<subseteq> cbox ?a ?b" . |
|
813 show "a $ 1 - 2 = a $ 1 - 2" |
|
814 and "b $ 1 + 2 = b $ 1 + 2" |
|
815 and "pathstart g $ 2 - 3 = a $ 2 - 3" |
|
816 and "b $ 2 + 3 = b $ 2 + 3" |
|
817 by (auto simp add: assms) |
|
818 qed |
|
819 note z=this[unfolded P1P2 path_image_linepath] |
|
820 show thesis |
|
821 apply (rule that[of z]) |
|
822 proof - |
|
823 have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or> |
|
824 z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or> |
|
825 z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or> |
|
826 z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow> |
|
827 (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or> |
|
828 z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or> |
|
829 z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or> |
|
830 z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False" |
|
831 proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases) |
|
832 case prems: 1 |
|
833 have "pathfinish f \<in> cbox a b" |
|
834 using assms(3) pathfinish_in_path_image[of f] by auto |
|
835 then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" |
|
836 unfolding mem_interval_cart forall_2 by auto |
|
837 then have "z$1 \<noteq> pathfinish f$1" |
|
838 using prems(2) |
|
839 using assms ab |
|
840 by (auto simp add: field_simps) |
|
841 moreover have "pathstart f \<in> cbox a b" |
|
842 using assms(3) pathstart_in_path_image[of f] |
|
843 by auto |
|
844 then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" |
|
845 unfolding mem_interval_cart forall_2 |
|
846 by auto |
|
847 then have "z$1 \<noteq> pathstart f$1" |
|
848 using prems(2) using assms ab |
|
849 by (auto simp add: field_simps) |
|
850 ultimately have *: "z$2 = a$2 - 2" |
|
851 using prems(1) |
|
852 by auto |
|
853 have "z$1 \<noteq> pathfinish g$1" |
|
854 using prems(2) |
|
855 using assms ab |
|
856 by (auto simp add: field_simps *) |
|
857 moreover have "pathstart g \<in> cbox a b" |
|
858 using assms(4) pathstart_in_path_image[of g] |
|
859 by auto |
|
860 note this[unfolded mem_interval_cart forall_2] |
|
861 then have "z$1 \<noteq> pathstart g$1" |
|
862 using prems(1) |
|
863 using assms ab |
|
864 by (auto simp add: field_simps *) |
|
865 ultimately have "a $ 2 - 1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2 - 1" |
|
866 using prems(2) |
|
867 unfolding * assms |
|
868 by (auto simp add: field_simps) |
|
869 then show False |
|
870 unfolding * using ab by auto |
|
871 qed |
|
872 then have "z \<in> path_image f \<or> z \<in> path_image g" |
|
873 using z unfolding Un_iff by blast |
|
874 then have z': "z \<in> cbox a b" |
|
875 using assms(3-4) |
|
876 by auto |
|
877 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> |
|
878 z = pathstart f \<or> z = pathfinish f" |
|
879 unfolding vec_eq_iff forall_2 assms |
|
880 by auto |
|
881 with z' show "z \<in> path_image f" |
|
882 using z(1) |
|
883 unfolding Un_iff mem_interval_cart forall_2 |
|
884 apply - |
|
885 apply (simp only: segment_vertical segment_horizontal vector_2) |
|
886 unfolding assms |
|
887 apply auto |
|
888 done |
|
889 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> |
|
890 z = pathstart g \<or> z = pathfinish g" |
|
891 unfolding vec_eq_iff forall_2 assms |
|
892 by auto |
|
893 with z' show "z \<in> path_image g" |
|
894 using z(2) |
|
895 unfolding Un_iff mem_interval_cart forall_2 |
|
896 apply (simp only: segment_vertical segment_horizontal vector_2) |
|
897 unfolding assms |
|
898 apply auto |
|
899 done |
|
900 qed |
|
901 qed |
|
902 |
|
903 (** The Following still needs to be translated. Maybe I will do that later. |
|
904 |
|
905 (* ------------------------------------------------------------------------- *) |
|
906 (* Complement in dimension N >= 2 of set homeomorphic to any interval in *) |
|
907 (* any dimension is (path-)connected. This naively generalizes the argument *) |
|
908 (* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer *) |
|
909 (* fixed point theorem", American Mathematical Monthly 1984. *) |
|
910 (* ------------------------------------------------------------------------- *) |
|
911 |
|
912 let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove |
|
913 (`!p:real^M->real^N a b. |
|
914 ~(interval[a,b] = {}) /\ |
|
915 p continuous_on interval[a,b] /\ |
|
916 (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y) |
|
917 ==> ?f. f continuous_on (:real^N) /\ |
|
918 IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\ |
|
919 (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`, |
|
920 REPEAT STRIP_TAC THEN |
|
921 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN |
|
922 DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN |
|
923 SUBGOAL_THEN `(q:real^N->real^M) continuous_on |
|
924 (IMAGE p (interval[a:real^M,b]))` |
|
925 ASSUME_TAC THENL |
|
926 [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]; |
|
927 ALL_TAC] THEN |
|
928 MP_TAC(ISPECL [`q:real^N->real^M`; |
|
929 `IMAGE (p:real^M->real^N) |
|
930 (interval[a,b])`; |
|
931 `a:real^M`; `b:real^M`] |
|
932 TIETZE_CLOSED_INTERVAL) THEN |
|
933 ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE; |
|
934 COMPACT_IMP_CLOSED] THEN |
|
935 ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN |
|
936 DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN |
|
937 EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN |
|
938 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN |
|
939 CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN |
|
940 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN |
|
941 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ] |
|
942 CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);; |
|
943 |
|
944 let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove |
|
945 (`!s:real^N->bool a b:real^M. |
|
946 s homeomorphic (interval[a,b]) |
|
947 ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`, |
|
948 REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN |
|
949 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN |
|
950 MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN |
|
951 DISCH_TAC THEN |
|
952 SUBGOAL_THEN |
|
953 `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ |
|
954 (p:real^M->real^N) x = p y ==> x = y` |
|
955 ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN |
|
956 FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN |
|
957 DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN |
|
958 ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN |
|
959 ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV; |
|
960 NOT_BOUNDED_UNIV] THEN |
|
961 ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN |
|
962 X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN |
|
963 SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN |
|
964 SUBGOAL_THEN `bounded((path_component s c) UNION |
|
965 (IMAGE (p:real^M->real^N) (interval[a,b])))` |
|
966 MP_TAC THENL |
|
967 [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED; |
|
968 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; |
|
969 ALL_TAC] THEN |
|
970 DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN |
|
971 REWRITE_TAC[UNION_SUBSET] THEN |
|
972 DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN |
|
973 MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`] |
|
974 RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN |
|
975 ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN |
|
976 DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN |
|
977 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC |
|
978 (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN |
|
979 REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN |
|
980 ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN |
|
981 SUBGOAL_THEN |
|
982 `(q:real^N->real^N) continuous_on |
|
983 (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))` |
|
984 MP_TAC THENL |
|
985 [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN |
|
986 REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN |
|
987 REPEAT CONJ_TAC THENL |
|
988 [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN |
|
989 ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED; |
|
990 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; |
|
991 ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; |
|
992 ALL_TAC] THEN |
|
993 X_GEN_TAC `z:real^N` THEN |
|
994 REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN |
|
995 STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN |
|
996 MP_TAC(ISPECL |
|
997 [`path_component s (z:real^N)`; `path_component s (c:real^N)`] |
|
998 OPEN_INTER_CLOSURE_EQ_EMPTY) THEN |
|
999 ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL |
|
1000 [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN |
|
1001 ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED; |
|
1002 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; |
|
1003 REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN |
|
1004 DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN |
|
1005 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN |
|
1006 REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]]; |
|
1007 ALL_TAC] THEN |
|
1008 SUBGOAL_THEN |
|
1009 `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) = |
|
1010 (:real^N)` |
|
1011 SUBST1_TAC THENL |
|
1012 [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN |
|
1013 REWRITE_TAC[CLOSURE_SUBSET]; |
|
1014 DISCH_TAC] THEN |
|
1015 MP_TAC(ISPECL |
|
1016 [`(\x. &2 % c - x) o |
|
1017 (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`; |
|
1018 `cball(c:real^N,B)`] |
|
1019 BROUWER) THEN |
|
1020 REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN |
|
1021 ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN |
|
1022 SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL |
|
1023 [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN |
|
1024 REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN |
|
1025 ASM SET_TAC[PATH_COMPONENT_REFL_EQ]; |
|
1026 ALL_TAC] THEN |
|
1027 REPEAT CONJ_TAC THENL |
|
1028 [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN |
|
1029 SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN |
|
1030 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL |
|
1031 [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN |
|
1032 MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN |
|
1033 MATCH_MP_TAC CONTINUOUS_ON_MUL THEN |
|
1034 SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN |
|
1035 REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN |
|
1036 MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN |
|
1037 MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN |
|
1038 ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN |
|
1039 SUBGOAL_THEN |
|
1040 `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)` |
|
1041 SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN |
|
1042 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN |
|
1043 ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST; |
|
1044 CONTINUOUS_ON_LIFT_NORM]; |
|
1045 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN |
|
1046 X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN |
|
1047 REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN |
|
1048 REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN |
|
1049 ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN |
|
1050 ASM_REAL_ARITH_TAC; |
|
1051 REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN |
|
1052 REWRITE_TAC[IN_CBALL; o_THM; dist] THEN |
|
1053 X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN |
|
1054 REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN |
|
1055 ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL |
|
1056 [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN |
|
1057 REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN |
|
1058 ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN |
|
1059 ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN |
|
1060 UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN |
|
1061 REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB]; |
|
1062 EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN |
|
1063 REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN |
|
1064 ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN |
|
1065 SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL |
|
1066 [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN |
|
1067 ASM_REWRITE_TAC[] THEN |
|
1068 MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN |
|
1069 ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);; |
|
1070 |
|
1071 let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove |
|
1072 (`!s:real^N->bool a b:real^M. |
|
1073 2 <= dimindex(:N) /\ s homeomorphic interval[a,b] |
|
1074 ==> path_connected((:real^N) DIFF s)`, |
|
1075 REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN |
|
1076 FIRST_ASSUM(MP_TAC o MATCH_MP |
|
1077 UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN |
|
1078 ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN |
|
1079 ABBREV_TAC `t = (:real^N) DIFF s` THEN |
|
1080 DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN |
|
1081 STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN |
|
1082 REWRITE_TAC[COMPACT_INTERVAL] THEN |
|
1083 DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN |
|
1084 REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN |
|
1085 X_GEN_TAC `B:real` THEN STRIP_TAC THEN |
|
1086 SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\ |
|
1087 (?v:real^N. v IN path_component t y /\ B < norm(v))` |
|
1088 STRIP_ASSUME_TAC THENL |
|
1089 [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN |
|
1090 MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN |
|
1091 CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN |
|
1092 MATCH_MP_TAC PATH_COMPONENT_SYM THEN |
|
1093 MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN |
|
1094 CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN |
|
1095 MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN |
|
1096 EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL |
|
1097 [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE |
|
1098 `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN |
|
1099 ASM_REWRITE_TAC[SUBSET; IN_CBALL_0]; |
|
1100 MP_TAC(ISPEC `cball(vec 0:real^N,B)` |
|
1101 PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN |
|
1102 ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN |
|
1103 REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN |
|
1104 DISCH_THEN MATCH_MP_TAC THEN |
|
1105 ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);; |
|
1106 |
|
1107 (* ------------------------------------------------------------------------- *) |
|
1108 (* In particular, apply all these to the special case of an arc. *) |
|
1109 (* ------------------------------------------------------------------------- *) |
|
1110 |
|
1111 let RETRACTION_ARC = prove |
|
1112 (`!p. arc p |
|
1113 ==> ?f. f continuous_on (:real^N) /\ |
|
1114 IMAGE f (:real^N) SUBSET path_image p /\ |
|
1115 (!x. x IN path_image p ==> f x = x)`, |
|
1116 REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN |
|
1117 MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN |
|
1118 ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);; |
|
1119 |
|
1120 let PATH_CONNECTED_ARC_COMPLEMENT = prove |
|
1121 (`!p. 2 <= dimindex(:N) /\ arc p |
|
1122 ==> path_connected((:real^N) DIFF path_image p)`, |
|
1123 REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN |
|
1124 MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`] |
|
1125 PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN |
|
1126 ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN |
|
1127 ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN |
|
1128 MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN |
|
1129 EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);; |
|
1130 |
|
1131 let CONNECTED_ARC_COMPLEMENT = prove |
|
1132 (`!p. 2 <= dimindex(:N) /\ arc p |
|
1133 ==> connected((:real^N) DIFF path_image p)`, |
|
1134 SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *) |
|
1135 |
|
1136 end |
|