107 define negatex :: "real^2 \<Rightarrow> real^2" |
107 define negatex :: "real^2 \<Rightarrow> real^2" |
108 where "negatex x = (vector [-(x$1), x$2])" for x |
108 where "negatex x = (vector [-(x$1), x$2])" for x |
109 have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z" |
109 have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z" |
110 unfolding negatex_def infnorm_2 vector_2 by auto |
110 unfolding negatex_def infnorm_2 vector_2 by auto |
111 have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1" |
111 have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1" |
112 unfolding sqprojection_def |
112 unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR] |
113 unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] |
113 by (simp add: real_abs_infnorm infnorm_eq_0) |
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" |
114 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}" |
115 have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1..1}" |
120 apply (rule set_eqI) |
116 proof |
121 unfolding image_iff Bex_def mem_box_cart interval_cbox_cart |
117 show "(\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 \<subseteq> {-1..1}" for i |
122 apply rule |
118 by (auto simp: mem_box_cart) |
123 defer |
119 show "{-1..1} \<subseteq> (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1" for i |
124 apply (rule_tac x="vec x" in exI) |
120 by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, hide_lams) vec_component) |
125 apply auto |
121 qed |
126 done |
|
127 { |
122 { |
128 fix x |
123 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))" |
124 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: |
125 then obtain w :: "real^2" where w: |
131 "w \<in> cbox (- 1) 1" |
126 "w \<in> cbox (- 1) 1" |
134 then have "x \<noteq> 0" |
129 then have "x \<noteq> 0" |
135 using as[of "w$1" "w$2"] |
130 using as[of "w$1" "w$2"] |
136 unfolding mem_box_cart atLeastAtMost_iff |
131 unfolding mem_box_cart atLeastAtMost_iff |
137 by auto |
132 by auto |
138 } note x0 = this |
133 } 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> {}" |
134 have 1: "box (- 1) (1::real^2) \<noteq> {}" |
142 unfolding interval_eq_empty_cart by auto |
135 unfolding interval_eq_empty_cart by auto |
143 have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)" |
136 have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" |
|
137 for i x y c |
|
138 using exhaust_2 [of i] by (auto simp: negatex_def) |
|
139 then have "bounded_linear negatex" |
|
140 by (simp add: bounded_linearI' vec_eq_iff) |
|
141 then have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)" |
144 apply (intro continuous_intros continuous_on_component) |
142 apply (intro continuous_intros continuous_on_component) |
145 unfolding * |
143 unfolding * sqprojection_def |
146 apply (rule assms)+ |
144 apply (intro assms continuous_intros)+ |
147 apply (subst sqprojection_def) |
145 apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on) |
148 apply (intro continuous_intros) |
146 done |
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" |
147 have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1" |
171 unfolding subset_eq |
148 unfolding subset_eq |
172 proof (rule, goal_cases) |
149 proof (rule, goal_cases) |
173 case (1 x) |
150 case (1 x) |
174 then obtain y :: "real^2" where y: |
151 then obtain y :: "real^2" where y: |
175 "y \<in> cbox (- 1) 1" |
152 "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" |
153 "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 .. |
154 unfolding image_iff .. |
178 have "?F y \<noteq> 0" |
155 have "?F y \<noteq> 0" |
179 apply (rule x0) |
156 by (rule x0) (use y in auto) |
180 using y(1) |
|
181 apply auto |
|
182 done |
|
183 then have *: "infnorm (sqprojection (?F y)) = 1" |
157 then have *: "infnorm (sqprojection (?F y)) = 1" |
184 unfolding y o_def |
158 unfolding y o_def |
185 by - (rule lem2[rule_format]) |
159 by - (rule lem2[rule_format]) |
186 have "infnorm x = 1" |
160 have inf1: "infnorm x = 1" |
187 unfolding *[symmetric] y o_def |
161 unfolding *[symmetric] y o_def |
188 by (rule lem1[rule_format]) |
162 by (rule lem1[rule_format]) |
189 then show "x \<in> cbox (-1) 1" |
163 show "x \<in> cbox (-1) 1" |
190 unfolding mem_box_cart interval_cbox_cart infnorm_2 |
164 unfolding mem_box_cart interval_cbox_cart infnorm_2 |
191 apply - |
165 proof |
192 apply rule |
|
193 proof - |
|
194 fix i |
166 fix i |
195 assume "max \<bar>x $ 1\<bar> \<bar>x $ 2\<bar> = 1" |
167 show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i" |
196 then show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i" |
168 using exhaust_2 [of i] inf1 by (auto simp: infnorm_2) |
197 apply (cases "i = 1") |
|
198 defer |
|
199 apply (drule 21) |
|
200 apply auto |
|
201 done |
|
202 qed |
169 qed |
203 qed |
170 qed |
204 obtain x :: "real^2" where x: |
171 obtain x :: "real^2" where x: |
205 "x \<in> cbox (- 1) 1" |
172 "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" |
173 "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x" |
209 unfolding interior_cbox |
176 unfolding interior_cbox |
210 apply (rule 1 2 3)+ |
177 apply (rule 1 2 3)+ |
211 apply blast |
178 apply blast |
212 done |
179 done |
213 have "?F x \<noteq> 0" |
180 have "?F x \<noteq> 0" |
214 apply (rule x0) |
181 by (rule x0) (use x in auto) |
215 using x(1) |
|
216 apply auto |
|
217 done |
|
218 then have *: "infnorm (sqprojection (?F x)) = 1" |
182 then have *: "infnorm (sqprojection (?F x)) = 1" |
219 unfolding o_def |
183 unfolding o_def |
220 by (rule lem2[rule_format]) |
184 by (rule lem2[rule_format]) |
221 have nx: "infnorm x = 1" |
185 have nx: "infnorm x = 1" |
222 apply (subst x(2)[symmetric]) |
186 apply (subst x(2)[symmetric]) |
223 unfolding *[symmetric] o_def |
187 unfolding *[symmetric] o_def |
224 apply (rule lem1[rule_format]) |
188 apply (rule lem1[rule_format]) |
225 done |
189 done |
226 have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" |
190 have iff: "0 < sqprojection x$i \<longleftrightarrow> 0 < x$i" "sqprojection x$i < 0 \<longleftrightarrow> x$i < 0" if "x \<noteq> 0" for 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 - |
191 proof - |
231 fix x :: "real^2" |
|
232 fix i :: 2 |
|
233 assume x: "x \<noteq> 0" |
|
234 have "inverse (infnorm x) > 0" |
192 have "inverse (infnorm x) > 0" |
235 using x[unfolded infnorm_pos_lt[symmetric]] by auto |
193 by (simp add: infnorm_pos_lt that) |
236 then show "(0 < sqprojection x $ i) = (0 < x $ i)" |
194 then show "(0 < sqprojection x $ i) = (0 < x $ i)" |
237 and "(sqprojection x $ i < 0) = (x $ i < 0)" |
195 and "(sqprojection x $ i < 0) = (x $ i < 0)" |
238 unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def |
196 unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def |
239 unfolding zero_less_mult_iff mult_less_0_iff |
197 unfolding zero_less_mult_iff mult_less_0_iff |
240 by (auto simp add: field_simps) |
198 by (auto simp add: field_simps) |
241 qed |
199 qed |
242 note lem3 = this[rule_format] |
|
243 have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" |
200 have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" |
244 using x(1) unfolding mem_box_cart by auto |
201 using x(1) unfolding mem_box_cart by auto |
245 then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0" |
202 then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0" |
246 unfolding right_minus_eq |
203 using as by auto |
247 apply - |
204 consider "x $ 1 = -1" | "x $ 1 = 1" | "x $ 2 = -1" | "x $ 2 = 1" |
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 |
205 using nx unfolding infnorm_eq_1_2 by auto |
253 then show False |
206 then show False |
254 proof - |
207 proof cases |
255 fix P Q R S |
208 case 1 |
256 presume "P \<or> Q \<or> R \<or> S" |
209 then have *: "f (x $ 1) $ 1 = - 1" |
257 and "P \<Longrightarrow> False" |
210 using assms(5) by auto |
258 and "Q \<Longrightarrow> False" |
211 have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" |
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]] |
212 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
268 unfolding as negatex_def vector_2 |
213 by (auto simp: negatex_def 1) |
269 by auto |
|
270 moreover |
214 moreover |
271 from x1 have "g (x $ 2) \<in> cbox (-1) 1" |
215 from x1 have "g (x $ 2) \<in> cbox (-1) 1" |
272 using assms(2) by blast |
216 using assms(2) by blast |
273 ultimately show False |
217 ultimately show False |
274 unfolding lem3[OF nz] vector_component_simps * mem_box_cart |
218 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
275 using not_le by auto |
219 using not_le by auto |
276 next |
220 next |
277 assume as: "x$1 = -1" |
221 case 2 |
278 then have *: "f (x $ 1) $ 1 = - 1" |
222 then have *: "f (x $ 1) $ 1 = 1" |
279 using assms(5) by auto |
223 using assms(6) by auto |
280 have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" |
224 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" |
281 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
225 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2 |
282 unfolding as negatex_def vector_2 |
226 by (auto simp: negatex_def) |
283 by auto |
227 moreover have "g (x $ 2) \<in> cbox (-1) 1" |
284 moreover |
228 using assms(2) x1 by blast |
285 from x1 have "g (x $ 2) \<in> cbox (-1) 1" |
|
286 using assms(2) by blast |
|
287 ultimately show False |
229 ultimately show False |
288 unfolding lem3[OF nz] vector_component_simps * mem_box_cart |
230 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
289 using not_le by auto |
231 using not_le by auto |
290 next |
232 next |
291 assume as: "x$2 = 1" |
233 case 3 |
|
234 then have *: "g (x $ 2) $ 2 = - 1" |
|
235 using assms(7) by auto |
|
236 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
|
237 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def) |
|
238 moreover |
|
239 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
|
240 using assms(1) by blast |
|
241 ultimately show False |
|
242 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
|
243 by (erule_tac x=2 in allE) auto |
|
244 next |
|
245 case 4 |
292 then have *: "g (x $ 2) $ 2 = 1" |
246 then have *: "g (x $ 2) $ 2 = 1" |
293 using assms(8) by auto |
247 using assms(8) by auto |
294 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
248 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
295 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
249 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def) |
296 unfolding as negatex_def vector_2 |
|
297 by auto |
|
298 moreover |
250 moreover |
299 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
251 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
300 apply - |
252 using assms(1) by blast |
301 apply (rule assms(1)[unfolded subset_eq,rule_format]) |
|
302 apply auto |
|
303 done |
|
304 ultimately show False |
253 ultimately show False |
305 unfolding lem3[OF nz] vector_component_simps * mem_box_cart |
254 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
306 apply (erule_tac x=2 in allE) |
255 by (erule_tac x=2 in allE) auto |
307 apply auto |
256 qed |
308 done |
|
309 next |
|
310 assume as: "x$2 = -1" |
|
311 then have *: "g (x $ 2) $ 2 = - 1" |
|
312 using assms(7) by auto |
|
313 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
|
314 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
|
315 unfolding as negatex_def vector_2 |
|
316 by auto |
|
317 moreover |
|
318 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
|
319 apply - |
|
320 apply (rule assms(1)[unfolded subset_eq,rule_format]) |
|
321 apply auto |
|
322 done |
|
323 ultimately show False |
|
324 unfolding lem3[OF nz] vector_component_simps * mem_box_cart |
|
325 apply (erule_tac x=2 in allE) |
|
326 apply auto |
|
327 done |
|
328 qed auto |
|
329 qed |
257 qed |
330 |
258 |
331 lemma fashoda_unit_path: |
259 lemma fashoda_unit_path: |
332 fixes f g :: "real \<Rightarrow> real^2" |
260 fixes f g :: "real \<Rightarrow> real^2" |
333 assumes "path f" |
261 assumes "path f" |
774 apply (rule fashoda[of ?P1 ?P2 ?a ?b]) |
700 apply (rule fashoda[of ?P1 ?P2 ?a ?b]) |
775 unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 |
701 unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 |
776 proof - |
702 proof - |
777 show "path ?P1" and "path ?P2" |
703 show "path ?P1" and "path ?P2" |
778 using assms by auto |
704 using assms by auto |
779 have "path_image ?P1 \<subseteq> cbox ?a ?b" |
705 show "path_image ?P1 \<subseteq> cbox ?a ?b" "path_image ?P2 \<subseteq> cbox ?a ?b" |
780 unfolding P1P2 path_image_linepath |
706 unfolding P1P2 path_image_linepath using startfin paf pag |
781 apply (rule Un_least)+ |
707 by (auto simp: mem_box_cart segment_horizontal segment_vertical forall_2) |
782 defer 3 |
|
783 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
|
784 unfolding mem_box_cart forall_2 vector_2 |
|
785 using ab startfin abab assms(3) |
|
786 using assms(9-) |
|
787 unfolding assms |
|
788 apply (auto simp add: field_simps box_def) |
|
789 done |
|
790 then show "path_image ?P1 \<subseteq> cbox ?a ?b" . |
|
791 have "path_image ?P2 \<subseteq> cbox ?a ?b" |
|
792 unfolding P1P2 path_image_linepath |
|
793 apply (rule Un_least)+ |
|
794 defer 2 |
|
795 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
|
796 unfolding mem_box_cart forall_2 vector_2 |
|
797 using ab startfin abab assms(4) |
|
798 using assms(9-) |
|
799 unfolding assms |
|
800 apply (auto simp add: field_simps box_def) |
|
801 done |
|
802 then show "path_image ?P2 \<subseteq> cbox ?a ?b" . |
|
803 show "a $ 1 - 2 = a $ 1 - 2" |
708 show "a $ 1 - 2 = a $ 1 - 2" |
804 and "b $ 1 + 2 = b $ 1 + 2" |
709 and "b $ 1 + 2 = b $ 1 + 2" |
805 and "pathstart g $ 2 - 3 = a $ 2 - 3" |
710 and "pathstart g $ 2 - 3 = a $ 2 - 3" |
806 and "b $ 2 + 3 = b $ 2 + 3" |
711 and "b $ 2 + 3 = b $ 2 + 3" |
807 by (auto simp add: assms) |
712 by (auto simp add: assms) |
808 qed |
713 qed |
809 note z=this[unfolded P1P2 path_image_linepath] |
714 note z=this[unfolded P1P2 path_image_linepath] |
810 show thesis |
715 show thesis |
811 apply (rule that[of z]) |
716 proof (rule that[of z]) |
812 proof - |
|
813 have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or> |
717 have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or> |
814 z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or> |
718 z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or> |
815 z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or> |
719 z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or> |
816 z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow> |
720 z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow> |
817 (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or> |
721 (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or> |
836 by auto |
740 by auto |
837 then have "z$1 \<noteq> pathstart f$1" |
741 then have "z$1 \<noteq> pathstart f$1" |
838 using prems(2) using assms ab |
742 using prems(2) using assms ab |
839 by (auto simp add: field_simps) |
743 by (auto simp add: field_simps) |
840 ultimately have *: "z$2 = a$2 - 2" |
744 ultimately have *: "z$2 = a$2 - 2" |
841 using prems(1) |
745 using prems(1) by auto |
842 by auto |
|
843 have "z$1 \<noteq> pathfinish g$1" |
746 have "z$1 \<noteq> pathfinish g$1" |
844 using prems(2) |
747 using prems(2) assms ab |
845 using assms ab |
|
846 by (auto simp add: field_simps *) |
748 by (auto simp add: field_simps *) |
847 moreover have "pathstart g \<in> cbox a b" |
749 moreover have "pathstart g \<in> cbox a b" |
848 using assms(4) pathstart_in_path_image[of g] |
750 using assms(4) pathstart_in_path_image[of g] |
849 by auto |
751 by auto |
850 note this[unfolded mem_box_cart forall_2] |
752 note this[unfolded mem_box_cart forall_2] |
851 then have "z$1 \<noteq> pathstart g$1" |
753 then have "z$1 \<noteq> pathstart g$1" |
852 using prems(1) |
754 using prems(1) assms ab |
853 using assms ab |
|
854 by (auto simp add: field_simps *) |
755 by (auto simp add: field_simps *) |
855 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" |
756 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" |
856 using prems(2) |
757 using prems(2) unfolding * assms by (auto simp add: field_simps) |
857 unfolding * assms |
|
858 by (auto simp add: field_simps) |
|
859 then show False |
758 then show False |
860 unfolding * using ab by auto |
759 unfolding * using ab by auto |
861 qed |
760 qed |
862 then have "z \<in> path_image f \<or> z \<in> path_image g" |
761 then have "z \<in> path_image f \<or> z \<in> path_image g" |
863 using z unfolding Un_iff by blast |
762 using z unfolding Un_iff by blast |
864 then have z': "z \<in> cbox a b" |
763 then have z': "z \<in> cbox a b" |
865 using assms(3-4) |
764 using assms(3-4) by auto |
866 by auto |
|
867 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> |
765 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> |
868 z = pathstart f \<or> z = pathfinish f" |
766 z = pathstart f \<or> z = pathfinish f" |
869 unfolding vec_eq_iff forall_2 assms |
767 unfolding vec_eq_iff forall_2 assms |
870 by auto |
768 by auto |
871 with z' show "z \<in> path_image f" |
769 with z' show "z \<in> path_image f" |
872 using z(1) |
770 using z(1) |
873 unfolding Un_iff mem_box_cart forall_2 |
771 unfolding Un_iff mem_box_cart forall_2 |
874 apply - |
772 by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms) |
875 apply (simp only: segment_vertical segment_horizontal vector_2) |
|
876 unfolding assms |
|
877 apply auto |
|
878 done |
|
879 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> |
773 have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> |
880 z = pathstart g \<or> z = pathfinish g" |
774 z = pathstart g \<or> z = pathfinish g" |
881 unfolding vec_eq_iff forall_2 assms |
775 unfolding vec_eq_iff forall_2 assms |
882 by auto |
776 by auto |
883 with z' show "z \<in> path_image g" |
777 with z' show "z \<in> path_image g" |
884 using z(2) |
778 using z(2) |
885 unfolding Un_iff mem_box_cart forall_2 |
779 unfolding Un_iff mem_box_cart forall_2 |
886 apply (simp only: segment_vertical segment_horizontal vector_2) |
780 by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms) |
887 unfolding assms |
|
888 apply auto |
|
889 done |
|
890 qed |
781 qed |
891 qed |
782 qed |
892 |
783 |
893 end |
784 end |