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