292 apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment) |
292 apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment) |
293 apply (meson dual_order.trans segment_open_subset_closed) |
293 apply (meson dual_order.trans segment_open_subset_closed) |
294 done |
294 done |
295 |
295 |
296 lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment |
296 lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment |
297 |
|
298 |
|
299 subsection\<open>Betweenness\<close> |
|
300 |
|
301 definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)" |
|
302 |
|
303 lemma betweenI: |
|
304 assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
305 shows "between (a, b) x" |
|
306 using assms unfolding between_def closed_segment_def by auto |
|
307 |
|
308 lemma betweenE: |
|
309 assumes "between (a, b) x" |
|
310 obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" |
|
311 using assms unfolding between_def closed_segment_def by auto |
|
312 |
|
313 lemma between_implies_scaled_diff: |
|
314 assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y" |
|
315 obtains c where "(X - Y) = c *\<^sub>R (S - Y)" |
|
316 proof - |
|
317 from \<open>between (S, T) X\<close> obtain u\<^sub>X where X: "X = u\<^sub>X *\<^sub>R S + (1 - u\<^sub>X) *\<^sub>R T" |
|
318 by (metis add.commute betweenE eq_diff_eq) |
|
319 from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T" |
|
320 by (metis add.commute betweenE eq_diff_eq) |
|
321 have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)" |
|
322 proof - |
|
323 from X Y have "X - Y = u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp |
|
324 also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff) |
|
325 finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib) |
|
326 qed |
|
327 moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)" |
|
328 by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) |
|
329 moreover note \<open>S \<noteq> Y\<close> |
|
330 ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto |
|
331 from this that show thesis by blast |
|
332 qed |
|
333 |
|
334 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b" |
|
335 unfolding between_def by auto |
|
336 |
|
337 lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)" |
|
338 proof (cases "a = b") |
|
339 case True |
|
340 then show ?thesis |
|
341 by (auto simp add: between_def dist_commute) |
|
342 next |
|
343 case False |
|
344 then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" |
|
345 by auto |
|
346 have *: "\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" |
|
347 by (auto simp add: algebra_simps) |
|
348 have "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" if "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" for u |
|
349 proof - |
|
350 have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" |
|
351 unfolding that(1) by (auto simp add:algebra_simps) |
|
352 show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" |
|
353 unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close> |
|
354 by simp |
|
355 qed |
|
356 moreover have "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b" |
|
357 proof - |
|
358 let ?\<beta> = "norm (a - x) / norm (a - b)" |
|
359 show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" |
|
360 proof (intro exI conjI) |
|
361 show "?\<beta> \<le> 1" |
|
362 using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto |
|
363 show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b" |
|
364 proof (subst euclidean_eq_iff; intro ballI) |
|
365 fix i :: 'a |
|
366 assume i: "i \<in> Basis" |
|
367 have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i |
|
368 = ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)" |
|
369 using Fal by (auto simp add: field_simps inner_simps) |
|
370 also have "\<dots> = x\<bullet>i" |
|
371 apply (rule divide_eq_imp[OF Fal]) |
|
372 unfolding that[unfolded dist_norm] |
|
373 using that[unfolded dist_triangle_eq] i |
|
374 apply (subst (asm) euclidean_eq_iff) |
|
375 apply (auto simp add: field_simps inner_simps) |
|
376 done |
|
377 finally show "x \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i" |
|
378 by auto |
|
379 qed |
|
380 qed (use Fal2 in auto) |
|
381 qed |
|
382 ultimately show ?thesis |
|
383 by (force simp add: between_def closed_segment_def dist_triangle_eq) |
|
384 qed |
|
385 |
|
386 lemma between_midpoint: |
|
387 fixes a :: "'a::euclidean_space" |
|
388 shows "between (a,b) (midpoint a b)" (is ?t1) |
|
389 and "between (b,a) (midpoint a b)" (is ?t2) |
|
390 proof - |
|
391 have *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" |
|
392 by auto |
|
393 show ?t1 ?t2 |
|
394 unfolding between midpoint_def dist_norm |
|
395 by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *) |
|
396 qed |
|
397 |
|
398 lemma between_mem_convex_hull: |
|
399 "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}" |
|
400 unfolding between_mem_segment segment_convex_hull .. |
|
401 |
|
402 lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b" |
|
403 by (auto simp: between_def) |
|
404 |
|
405 lemma between_triv1 [simp]: "between (a,b) a" |
|
406 by (auto simp: between_def) |
|
407 |
|
408 lemma between_triv2 [simp]: "between (a,b) b" |
|
409 by (auto simp: between_def) |
|
410 |
|
411 lemma between_commute: |
|
412 "between (a,b) = between (b,a)" |
|
413 by (auto simp: between_def closed_segment_commute) |
|
414 |
|
415 lemma between_antisym: |
|
416 fixes a :: "'a :: euclidean_space" |
|
417 shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b" |
|
418 by (auto simp: between dist_commute) |
|
419 |
|
420 lemma between_trans: |
|
421 fixes a :: "'a :: euclidean_space" |
|
422 shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d" |
|
423 using dist_triangle2 [of b c d] dist_triangle3 [of b d a] |
|
424 by (auto simp: between dist_commute) |
|
425 |
|
426 lemma between_norm: |
|
427 fixes a :: "'a :: euclidean_space" |
|
428 shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)" |
|
429 by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps) |
|
430 |
|
431 lemma between_swap: |
|
432 fixes A B X Y :: "'a::euclidean_space" |
|
433 assumes "between (A, B) X" |
|
434 assumes "between (A, B) Y" |
|
435 shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X" |
|
436 using assms by (auto simp add: between) |
|
437 |
|
438 lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x" |
|
439 by (auto simp: between_def) |
|
440 |
|
441 lemma between_trans_2: |
|
442 fixes a :: "'a :: euclidean_space" |
|
443 shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a" |
|
444 by (metis between_commute between_swap between_trans) |
|
445 |
|
446 lemma between_scaleR_lift [simp]: |
|
447 fixes v :: "'a::euclidean_space" |
|
448 shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c" |
|
449 by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric]) |
|
450 |
|
451 lemma between_1: |
|
452 fixes x::real |
|
453 shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)" |
|
454 by (auto simp: between_mem_segment closed_segment_eq_real_ivl) |
|
455 |
297 |
456 |
298 |
457 subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close> |
299 subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close> |
458 |
300 |
459 lemma mem_interior_convex_shrink: |
301 lemma mem_interior_convex_shrink: |