|
1 (* Author: John Harrison |
|
2 Translation from HOL light: Robert Himmelmann, TU Muenchen *) |
|
3 |
|
4 header {* Fashoda meet theorem. *} |
|
5 |
|
6 theory Fashoda |
|
7 imports Brouwer_Fixpoint Vec1 |
|
8 begin |
|
9 |
|
10 subsection {*Fashoda meet theorem. *} |
|
11 |
|
12 lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))" |
|
13 unfolding infnorm_def UNIV_2 apply(rule Sup_eq) by auto |
|
14 |
|
15 lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow> |
|
16 (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))" |
|
17 unfolding infnorm_2 by auto |
|
18 |
|
19 lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1" |
|
20 using assms unfolding infnorm_eq_1_2 by auto |
|
21 |
|
22 lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2" |
|
23 assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}" |
|
24 "continuous_on {- 1..1} f" "continuous_on {- 1..1} g" |
|
25 "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1" |
|
26 shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr) |
|
27 case goal1 note as = this[unfolded bex_simps,rule_format] |
|
28 def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" |
|
29 def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" |
|
30 have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z" |
|
31 unfolding negatex_def infnorm_2 vector_2 by auto |
|
32 have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def |
|
33 unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm |
|
34 unfolding infnorm_eq_0[THEN sym] by auto |
|
35 let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)" |
|
36 have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}" |
|
37 apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer |
|
38 apply(rule_tac x="vec x" in exI) by auto |
|
39 { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}" |
|
40 then guess w unfolding image_iff .. note w = this |
|
41 hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval by auto} note x0=this |
|
42 have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto |
|
43 have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto |
|
44 have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ |
|
45 prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding * |
|
46 apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def) |
|
47 apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def]) |
|
48 apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof- |
|
49 show "bounded_linear negatex" apply(rule bounded_linearI') unfolding Cart_eq proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real |
|
50 show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *s x) $ i = (c *s negatex x) $ i" |
|
51 apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) |
|
52 unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto) |
|
53 have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof- |
|
54 case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto |
|
55 hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format]) |
|
56 have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format]) |
|
57 thus "x\<in>{- 1..1}" unfolding mem_interval infnorm_2 apply- apply rule |
|
58 proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed |
|
59 guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"]) |
|
60 apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval |
|
61 apply(rule 1 2 3)+ . note x=this |
|
62 have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto |
|
63 hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format]) |
|
64 have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format]) |
|
65 have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)" |
|
66 apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0" |
|
67 have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto |
|
68 thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)" |
|
69 unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def |
|
70 unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed |
|
71 note lem3 = this[rule_format] |
|
72 have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval by auto |
|
73 hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto |
|
74 have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto |
|
75 thus False proof- fix P Q R S |
|
76 presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto |
|
77 next assume as:"x$1 = 1" |
|
78 hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto |
|
79 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" |
|
80 using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]] |
|
81 unfolding as negatex_def vector_2 by auto moreover |
|
82 from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto |
|
83 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval |
|
84 apply(erule_tac x=1 in allE) by auto |
|
85 next assume as:"x$1 = -1" |
|
86 hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto |
|
87 have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" |
|
88 using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]] |
|
89 unfolding as negatex_def vector_2 by auto moreover |
|
90 from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto |
|
91 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval |
|
92 apply(erule_tac x=1 in allE) by auto |
|
93 next assume as:"x$2 = 1" |
|
94 hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto |
|
95 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
|
96 using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]] |
|
97 unfolding as negatex_def vector_2 by auto moreover |
|
98 from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto |
|
99 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval |
|
100 apply(erule_tac x=2 in allE) by auto |
|
101 next assume as:"x$2 = -1" |
|
102 hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto |
|
103 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
|
104 using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]] |
|
105 unfolding as negatex_def vector_2 by auto moreover |
|
106 from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto |
|
107 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval |
|
108 apply(erule_tac x=2 in allE) by auto qed(auto) qed |
|
109 |
|
110 lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2" |
|
111 assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}" |
|
112 "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1" |
|
113 obtains z where "z \<in> path_image f" "z \<in> path_image g" proof- |
|
114 note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] |
|
115 def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)" |
|
116 have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto) |
|
117 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) |
|
118 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" |
|
119 using isc and assms(3-4) unfolding image_compose by auto |
|
120 have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+ |
|
121 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)" |
|
122 apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc]) |
|
123 by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding Cart_eq by auto |
|
124 show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1" |
|
125 unfolding o_def iscale_def using assms by(auto simp add:*) qed |
|
126 then guess s .. from this(2) guess t .. note st=this |
|
127 show thesis apply(rule_tac z="f (iscale s)" in that) |
|
128 using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply- |
|
129 apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI) |
|
130 using isc[unfolded subset_eq, rule_format] by auto qed |
|
131 |
|
132 lemma fashoda: fixes b::"real^2" |
|
133 assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}" |
|
134 "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1" |
|
135 "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2" |
|
136 obtains z where "z \<in> path_image f" "z \<in> path_image g" proof- |
|
137 fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto |
|
138 next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto |
|
139 hence "a \<le> b" unfolding interval_eq_empty vector_le_def by(auto simp add: not_less) |
|
140 thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_le_def forall_2 by auto |
|
141 next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component) |
|
142 apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image) |
|
143 unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"] |
|
144 unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this |
|
145 have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast |
|
146 hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def |
|
147 using assms(3)[unfolded path_image_def subset_eq mem_interval,rule_format,of "f 0" 1] |
|
148 unfolding mem_interval apply(erule_tac x=1 in allE) using as by auto |
|
149 thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto |
|
150 next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component) |
|
151 apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image) |
|
152 unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"] |
|
153 unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this |
|
154 have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast |
|
155 hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def |
|
156 using assms(4)[unfolded path_image_def subset_eq mem_interval,rule_format,of "g 0" 2] |
|
157 unfolding mem_interval apply(erule_tac x=2 in allE) using as by auto |
|
158 thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto |
|
159 next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2" |
|
160 have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto |
|
161 guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) |
|
162 unfolding path_def path_image_def pathstart_def pathfinish_def |
|
163 apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+ |
|
164 unfolding subset_eq apply(rule_tac[1-2] ballI) |
|
165 proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
|
166 then guess y unfolding image_iff .. note y=this |
|
167 show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij) |
|
168 using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto |
|
169 next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
|
170 then guess y unfolding image_iff .. note y=this |
|
171 show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij) |
|
172 using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto |
|
173 next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1" |
|
174 "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1" |
|
175 "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1" |
|
176 "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" unfolding interval_bij_def Cart_lambda_beta vector_component_simps o_def split_conv |
|
177 unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this |
|
178 from z(1) guess zf unfolding image_iff .. note zf=this |
|
179 from z(2) guess zg unfolding image_iff .. note zg=this |
|
180 have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto |
|
181 show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that) |
|
182 apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij[OF *] path_image_def |
|
183 using zf(1) zg(1) by auto qed |
|
184 |
|
185 subsection {*Some slightly ad hoc lemmas I use below*} |
|
186 |
|
187 lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1" |
|
188 shows "x \<in> closed_segment a b \<longleftrightarrow> (x$1 = a$1 \<and> x$1 = b$1 \<and> |
|
189 (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2))" (is "_ = ?R") |
|
190 proof- |
|
191 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" |
|
192 { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq |
|
193 unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } |
|
194 { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this |
|
195 { fix b a assume "b + u * a > a + u * b" |
|
196 hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps) |
|
197 hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto |
|
198 hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) |
|
199 using u(3-4) by(auto simp add:field_simps) } note * = this |
|
200 { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono) |
|
201 apply(drule mult_less_imp_less_left) using u by auto |
|
202 hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this |
|
203 thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) } |
|
204 { assume ?R thus ?L proof(cases "x$2 = b$2") |
|
205 case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True |
|
206 using `?R` by(auto simp add:field_simps) |
|
207 next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R` |
|
208 by(auto simp add:field_simps) |
|
209 qed } qed |
|
210 |
|
211 lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2" |
|
212 shows "x \<in> closed_segment a b \<longleftrightarrow> (x$2 = a$2 \<and> x$2 = b$2 \<and> |
|
213 (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1))" (is "_ = ?R") |
|
214 proof- |
|
215 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" |
|
216 { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq |
|
217 unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } |
|
218 { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this |
|
219 { fix b a assume "b + u * a > a + u * b" |
|
220 hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps) |
|
221 hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto |
|
222 hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) |
|
223 using u(3-4) by(auto simp add:field_simps) } note * = this |
|
224 { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono) |
|
225 apply(drule mult_less_imp_less_left) using u by auto |
|
226 hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this |
|
227 thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) } |
|
228 { assume ?R thus ?L proof(cases "x$1 = b$1") |
|
229 case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True |
|
230 using `?R` by(auto simp add:field_simps) |
|
231 next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R` |
|
232 by(auto simp add:field_simps) |
|
233 qed } qed |
|
234 |
|
235 subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *} |
|
236 |
|
237 lemma fashoda_interlace: fixes a::"real^2" |
|
238 assumes "path f" "path g" |
|
239 "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}" |
|
240 "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2" |
|
241 "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2" |
|
242 "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1" |
|
243 "(pathfinish f)$1 < (pathfinish g)$1" |
|
244 obtains z where "z \<in> path_image f" "z \<in> path_image g" |
|
245 proof- |
|
246 have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto |
|
247 note ab=this[unfolded interval_eq_empty not_ex forall_2 not_less] |
|
248 have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}" |
|
249 using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto |
|
250 note startfin = this[unfolded mem_interval forall_2] |
|
251 let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++ |
|
252 linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++ |
|
253 linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++ |
|
254 linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])" |
|
255 let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++ |
|
256 linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++ |
|
257 linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++ |
|
258 linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])" |
|
259 let ?a = "vector[a$1 - 2, a$2 - 3]" |
|
260 let ?b = "vector[b$1 + 2, b$2 + 3]" |
|
261 have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union> |
|
262 path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union> |
|
263 path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union> |
|
264 path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))" |
|
265 "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union> |
|
266 path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union> |
|
267 path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union> |
|
268 path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2) |
|
269 by(auto simp add: path_image_join path_linepath) |
|
270 have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2) |
|
271 guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b]) |
|
272 unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof- |
|
273 show "path ?P1" "path ?P2" using assms by auto |
|
274 have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3 |
|
275 apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format]) |
|
276 unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(3) |
|
277 using assms(9-) unfolding assms by(auto simp add:field_simps) |
|
278 thus "path_image ?P1 \<subseteq> {?a .. ?b}" . |
|
279 have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2 |
|
280 apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format]) |
|
281 unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(4) |
|
282 using assms(9-) unfolding assms by(auto simp add:field_simps) |
|
283 thus "path_image ?P2 \<subseteq> {?a .. ?b}" . |
|
284 show "a $ 1 - 2 = a $ 1 - 2" "b $ 1 + 2 = b $ 1 + 2" "pathstart g $ 2 - 3 = a $ 2 - 3" "b $ 2 + 3 = b $ 2 + 3" |
|
285 by(auto simp add: assms) |
|
286 qed note z=this[unfolded P1P2 path_image_linepath] |
|
287 show thesis apply(rule that[of z]) proof- |
|
288 have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or> |
|
289 z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or> |
|
290 z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or> |
|
291 z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow> |
|
292 (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or> |
|
293 z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or> |
|
294 z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or> |
|
295 z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False" |
|
296 apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this |
|
297 have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto |
|
298 hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto |
|
299 hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps) |
|
300 moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto |
|
301 hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto |
|
302 hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps) |
|
303 ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto |
|
304 have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *) |
|
305 moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto |
|
306 note this[unfolded mem_interval forall_2] |
|
307 hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *) |
|
308 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" |
|
309 using as(2) unfolding * assms by(auto simp add:field_simps) |
|
310 thus False unfolding * using ab by auto |
|
311 qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast |
|
312 hence z':"z\<in>{a..b}" using assms(3-4) by auto |
|
313 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> (z = pathstart f \<or> z = pathfinish f)" |
|
314 unfolding Cart_eq forall_2 assms by auto |
|
315 with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval forall_2 apply- |
|
316 apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto |
|
317 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> (z = pathstart g \<or> z = pathfinish g)" |
|
318 unfolding Cart_eq forall_2 assms by auto |
|
319 with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval forall_2 apply- |
|
320 apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto |
|
321 qed qed |
|
322 |
|
323 (** The Following still needs to be translated. Maybe I will do that later. |
|
324 |
|
325 (* ------------------------------------------------------------------------- *) |
|
326 (* Complement in dimension N >= 2 of set homeomorphic to any interval in *) |
|
327 (* any dimension is (path-)connected. This naively generalizes the argument *) |
|
328 (* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer *) |
|
329 (* fixed point theorem", American Mathematical Monthly 1984. *) |
|
330 (* ------------------------------------------------------------------------- *) |
|
331 |
|
332 let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove |
|
333 (`!p:real^M->real^N a b. |
|
334 ~(interval[a,b] = {}) /\ |
|
335 p continuous_on interval[a,b] /\ |
|
336 (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y) |
|
337 ==> ?f. f continuous_on (:real^N) /\ |
|
338 IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\ |
|
339 (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`, |
|
340 REPEAT STRIP_TAC THEN |
|
341 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN |
|
342 DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN |
|
343 SUBGOAL_THEN `(q:real^N->real^M) continuous_on |
|
344 (IMAGE p (interval[a:real^M,b]))` |
|
345 ASSUME_TAC THENL |
|
346 [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]; |
|
347 ALL_TAC] THEN |
|
348 MP_TAC(ISPECL [`q:real^N->real^M`; |
|
349 `IMAGE (p:real^M->real^N) |
|
350 (interval[a,b])`; |
|
351 `a:real^M`; `b:real^M`] |
|
352 TIETZE_CLOSED_INTERVAL) THEN |
|
353 ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE; |
|
354 COMPACT_IMP_CLOSED] THEN |
|
355 ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN |
|
356 DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN |
|
357 EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN |
|
358 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN |
|
359 CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN |
|
360 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN |
|
361 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ] |
|
362 CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);; |
|
363 |
|
364 let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove |
|
365 (`!s:real^N->bool a b:real^M. |
|
366 s homeomorphic (interval[a,b]) |
|
367 ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`, |
|
368 REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN |
|
369 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN |
|
370 MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN |
|
371 DISCH_TAC THEN |
|
372 SUBGOAL_THEN |
|
373 `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ |
|
374 (p:real^M->real^N) x = p y ==> x = y` |
|
375 ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN |
|
376 FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN |
|
377 DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN |
|
378 ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN |
|
379 ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV; |
|
380 NOT_BOUNDED_UNIV] THEN |
|
381 ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN |
|
382 X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN |
|
383 SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN |
|
384 SUBGOAL_THEN `bounded((path_component s c) UNION |
|
385 (IMAGE (p:real^M->real^N) (interval[a,b])))` |
|
386 MP_TAC THENL |
|
387 [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED; |
|
388 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; |
|
389 ALL_TAC] THEN |
|
390 DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN |
|
391 REWRITE_TAC[UNION_SUBSET] THEN |
|
392 DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN |
|
393 MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`] |
|
394 RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN |
|
395 ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN |
|
396 DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN |
|
397 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC |
|
398 (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN |
|
399 REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN |
|
400 ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN |
|
401 SUBGOAL_THEN |
|
402 `(q:real^N->real^N) continuous_on |
|
403 (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))` |
|
404 MP_TAC THENL |
|
405 [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN |
|
406 REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN |
|
407 REPEAT CONJ_TAC THENL |
|
408 [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN |
|
409 ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED; |
|
410 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; |
|
411 ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; |
|
412 ALL_TAC] THEN |
|
413 X_GEN_TAC `z:real^N` THEN |
|
414 REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN |
|
415 STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN |
|
416 MP_TAC(ISPECL |
|
417 [`path_component s (z:real^N)`; `path_component s (c:real^N)`] |
|
418 OPEN_INTER_CLOSURE_EQ_EMPTY) THEN |
|
419 ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL |
|
420 [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN |
|
421 ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED; |
|
422 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; |
|
423 REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN |
|
424 DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN |
|
425 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN |
|
426 REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]]; |
|
427 ALL_TAC] THEN |
|
428 SUBGOAL_THEN |
|
429 `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) = |
|
430 (:real^N)` |
|
431 SUBST1_TAC THENL |
|
432 [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN |
|
433 REWRITE_TAC[CLOSURE_SUBSET]; |
|
434 DISCH_TAC] THEN |
|
435 MP_TAC(ISPECL |
|
436 [`(\x. &2 % c - x) o |
|
437 (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`; |
|
438 `cball(c:real^N,B)`] |
|
439 BROUWER) THEN |
|
440 REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN |
|
441 ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN |
|
442 SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL |
|
443 [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN |
|
444 REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN |
|
445 ASM SET_TAC[PATH_COMPONENT_REFL_EQ]; |
|
446 ALL_TAC] THEN |
|
447 REPEAT CONJ_TAC THENL |
|
448 [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN |
|
449 SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN |
|
450 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL |
|
451 [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN |
|
452 MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN |
|
453 MATCH_MP_TAC CONTINUOUS_ON_MUL THEN |
|
454 SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN |
|
455 REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN |
|
456 MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN |
|
457 MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN |
|
458 ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN |
|
459 SUBGOAL_THEN |
|
460 `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)` |
|
461 SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN |
|
462 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN |
|
463 ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST; |
|
464 CONTINUOUS_ON_LIFT_NORM]; |
|
465 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN |
|
466 X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN |
|
467 REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN |
|
468 REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN |
|
469 ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN |
|
470 ASM_REAL_ARITH_TAC; |
|
471 REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN |
|
472 REWRITE_TAC[IN_CBALL; o_THM; dist] THEN |
|
473 X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN |
|
474 REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN |
|
475 ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL |
|
476 [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN |
|
477 REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN |
|
478 ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN |
|
479 ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN |
|
480 UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN |
|
481 REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB]; |
|
482 EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN |
|
483 REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN |
|
484 ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN |
|
485 SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL |
|
486 [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN |
|
487 ASM_REWRITE_TAC[] THEN |
|
488 MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN |
|
489 ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);; |
|
490 |
|
491 let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove |
|
492 (`!s:real^N->bool a b:real^M. |
|
493 2 <= dimindex(:N) /\ s homeomorphic interval[a,b] |
|
494 ==> path_connected((:real^N) DIFF s)`, |
|
495 REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN |
|
496 FIRST_ASSUM(MP_TAC o MATCH_MP |
|
497 UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN |
|
498 ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN |
|
499 ABBREV_TAC `t = (:real^N) DIFF s` THEN |
|
500 DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN |
|
501 STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN |
|
502 REWRITE_TAC[COMPACT_INTERVAL] THEN |
|
503 DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN |
|
504 REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN |
|
505 X_GEN_TAC `B:real` THEN STRIP_TAC THEN |
|
506 SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\ |
|
507 (?v:real^N. v IN path_component t y /\ B < norm(v))` |
|
508 STRIP_ASSUME_TAC THENL |
|
509 [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN |
|
510 MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN |
|
511 CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN |
|
512 MATCH_MP_TAC PATH_COMPONENT_SYM THEN |
|
513 MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN |
|
514 CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN |
|
515 MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN |
|
516 EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL |
|
517 [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE |
|
518 `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN |
|
519 ASM_REWRITE_TAC[SUBSET; IN_CBALL_0]; |
|
520 MP_TAC(ISPEC `cball(vec 0:real^N,B)` |
|
521 PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN |
|
522 ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN |
|
523 REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN |
|
524 DISCH_THEN MATCH_MP_TAC THEN |
|
525 ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);; |
|
526 |
|
527 (* ------------------------------------------------------------------------- *) |
|
528 (* In particular, apply all these to the special case of an arc. *) |
|
529 (* ------------------------------------------------------------------------- *) |
|
530 |
|
531 let RETRACTION_ARC = prove |
|
532 (`!p. arc p |
|
533 ==> ?f. f continuous_on (:real^N) /\ |
|
534 IMAGE f (:real^N) SUBSET path_image p /\ |
|
535 (!x. x IN path_image p ==> f x = x)`, |
|
536 REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN |
|
537 MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN |
|
538 ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);; |
|
539 |
|
540 let PATH_CONNECTED_ARC_COMPLEMENT = prove |
|
541 (`!p. 2 <= dimindex(:N) /\ arc p |
|
542 ==> path_connected((:real^N) DIFF path_image p)`, |
|
543 REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN |
|
544 MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`] |
|
545 PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN |
|
546 ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN |
|
547 ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN |
|
548 MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN |
|
549 EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);; |
|
550 |
|
551 let CONNECTED_ARC_COMPLEMENT = prove |
|
552 (`!p. 2 <= dimindex(:N) /\ arc p |
|
553 ==> connected((:real^N) DIFF path_image p)`, |
|
554 SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *) |
|
555 |
|
556 end |