(* Title: HOL/Analysis/Line_Segment.thy Author: L C Paulson, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Bogdan Grechuk, University of Edinburgh Author: Armin Heller, TU Muenchen Author: Johannes Hoelzl, TU Muenchen *) section ‹Line Segment› theory Line_Segment imports Convex Topology_Euclidean_Space begin subsection✐‹tag unimportant› ‹Topological Properties of Convex Sets, Metric Spaces and Functions› lemma convex_supp_sum: assumes "convex S" and 1: "supp_sum u I = 1" and "⋀i. i ∈ I ⟹ 0 ≤ u i ∧ (u i = 0 ∨ f i ∈ S)" shows "supp_sum (λi. u i *⇩_{R}f i) I ∈ S" proof - have fin: "finite {i ∈ I. u i ≠ 0}" using 1 sum.infinite by (force simp: supp_sum_def support_on_def) then have "supp_sum (λi. u i *⇩_{R}f i) I = sum (λi. u i *⇩_{R}f i) {i ∈ I. u i ≠ 0}" by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def) also have "... ∈ S" using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin ‹convex S›]) finally show ?thesis . qed lemma sphere_eq_empty [simp]: fixes a :: "'a::{real_normed_vector, perfect_space}" shows "sphere a r = {} ⟷ r < 0" by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist) lemma cone_closure: fixes S :: "'a::real_normed_vector set" assumes "cone S" shows "cone (closure S)" proof (cases "S = {}") case True then show ?thesis by auto next case False then have "0 ∈ S ∧ (∀c. c > 0 ⟶ (*⇩_{R}) c ` S = S)" using cone_iff[of S] assms by auto then have "0 ∈ closure S ∧ (∀c. c > 0 ⟶ (*⇩_{R}) c ` closure S = closure S)" using closure_subset by (auto simp: closure_scaleR) then show ?thesis using False cone_iff[of "closure S"] by auto qed corollary component_complement_connected: fixes S :: "'a::real_normed_vector set" assumes "connected S" "C ∈ components (-S)" shows "connected(-C)" using component_diff_connected [of S UNIV] assms by (auto simp: Compl_eq_Diff_UNIV) proposition clopen: fixes S :: "'a :: real_normed_vector set" shows "closed S ∧ open S ⟷ S = {} ∨ S = UNIV" by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format]) corollary compact_open: fixes S :: "'a :: euclidean_space set" shows "compact S ∧ open S ⟷ S = {}" by (auto simp: compact_eq_bounded_closed clopen) corollary finite_imp_not_open: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "⟦finite S; open S⟧ ⟹ S={}" using clopen [of S] finite_imp_closed not_bounded_UNIV by blast corollary empty_interior_finite: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "finite S ⟹ interior S = {}" by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open) text ‹Balls, being convex, are connected.› lemma convex_local_global_minimum: fixes s :: "'a::real_normed_vector set" assumes "e > 0" and "convex_on s f" and "ball x e ⊆ s" and "∀y∈ball x e. f x ≤ f y" shows "∀y∈s. f x ≤ f y" proof (rule ccontr) have "x ∈ s" using assms(1,3) by auto assume "¬ ?thesis" then obtain y where "y∈s" and y: "f x > f y" by auto then have xy: "0 < dist x y" by auto then obtain u where "0 < u" "u ≤ 1" and u: "u < e / dist x y" using field_lbound_gt_zero[of 1 "e / dist x y"] xy ‹e>0› by auto then have "f ((1-u) *⇩_{R}x + u *⇩_{R}y) ≤ (1-u) * f x + u * f y" using ‹x∈s› ‹y∈s› using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto moreover have *: "x - ((1 - u) *⇩_{R}x + u *⇩_{R}y) = u *⇩_{R}(x - y)" by (simp add: algebra_simps) have "(1 - u) *⇩_{R}x + u *⇩_{R}y ∈ ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF ‹0<u›] unfolding dist_norm[symmetric] using u unfolding pos_less_divide_eq[OF xy] by auto then have "f x ≤ f ((1 - u) *⇩_{R}x + u *⇩_{R}y)" using assms(4) by auto ultimately show False using mult_strict_left_mono[OF y ‹u>0›] unfolding left_diff_distrib by auto qed lemma convex_ball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (ball x e)" proof (auto simp: convex_def) fix y z assume yz: "dist x y < e" "dist x z < e" fix u v :: real assume uv: "0 ≤ u" "0 ≤ v" "u + v = 1" have "dist x (u *⇩_{R}y + v *⇩_{R}z) ≤ u * dist x y + v * dist x z" using uv yz using convex_on_dist [of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto then show "dist x (u *⇩_{R}y + v *⇩_{R}z) < e" using convex_bound_lt[OF yz uv] by auto qed lemma convex_cball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (cball x e)" proof - { fix y z assume yz: "dist x y ≤ e" "dist x z ≤ e" fix u v :: real assume uv: "0 ≤ u" "0 ≤ v" "u + v = 1" have "dist x (u *⇩_{R}y + v *⇩_{R}z) ≤ u * dist x y + v * dist x z" using uv yz using convex_on_dist [of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto then have "dist x (u *⇩_{R}y + v *⇩_{R}z) ≤ e" using convex_bound_le[OF yz uv] by auto } then show ?thesis by (auto simp: convex_def Ball_def) qed lemma connected_ball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (ball x e)" using convex_connected convex_ball by auto lemma connected_cball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (cball x e)" using convex_connected convex_cball by auto lemma bounded_convex_hull: fixes s :: "'a::real_normed_vector set" assumes "bounded s" shows "bounded (convex hull s)" proof - from assms obtain B where B: "∀x∈s. norm x ≤ B" unfolding bounded_iff by auto show ?thesis by (simp add: bounded_subset[OF bounded_cball, of _ 0 B] B subsetI subset_hull) qed lemma finite_imp_bounded_convex_hull: fixes s :: "'a::real_normed_vector set" shows "finite s ⟹ bounded (convex hull s)" using bounded_convex_hull finite_imp_bounded by auto subsection ‹Midpoint› definition✐‹tag important› midpoint :: "'a::real_vector ⇒ 'a ⇒ 'a" where "midpoint a b = (inverse (2::real)) *⇩_{R}(a + b)" lemma midpoint_idem [simp]: "midpoint x x = x" unfolding midpoint_def by simp lemma midpoint_sym: "midpoint a b = midpoint b a" unfolding midpoint_def by (auto simp add: scaleR_right_distrib) lemma midpoint_eq_iff: "midpoint a b = c ⟷ a + b = c + c" proof - have "midpoint a b = c ⟷ scaleR 2 (midpoint a b) = scaleR 2 c" by simp then show ?thesis unfolding midpoint_def scaleR_2 [symmetric] by simp qed lemma fixes a::real assumes "a ≤ b" shows ge_midpoint_1: "a ≤ midpoint a b" and le_midpoint_1: "midpoint a b ≤ b" by (simp_all add: midpoint_def assms) lemma dist_midpoint: fixes a b :: "'a::real_normed_vector" shows "dist a (midpoint a b) = (dist a b) / 2" (is ?t1) "dist b (midpoint a b) = (dist a b) / 2" (is ?t2) "dist (midpoint a b) a = (dist a b) / 2" (is ?t3) "dist (midpoint a b) b = (dist a b) / 2" (is ?t4) proof - have *: "⋀x y::'a. 2 *⇩_{R}x = - y ⟹ norm x = (norm y) / 2" unfolding equation_minus_iff by auto have **: "⋀x y::'a. 2 *⇩_{R}x = y ⟹ norm x = (norm y) / 2" by auto note scaleR_right_distrib [simp] show ?t1 unfolding midpoint_def dist_norm apply (rule **) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t2 unfolding midpoint_def dist_norm apply (rule *) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t3 unfolding midpoint_def dist_norm apply (rule *) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t4 unfolding midpoint_def dist_norm apply (rule **) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done qed lemma midpoint_eq_endpoint [simp]: "midpoint a b = a ⟷ a = b" "midpoint a b = b ⟷ a = b" unfolding midpoint_eq_iff by auto lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" using midpoint_eq_iff by metis lemma midpoint_linear_image: "linear f ⟹ midpoint(f a)(f b) = f(midpoint a b)" by (simp add: linear_iff midpoint_def) subsection ‹Open and closed segments› definition✐‹tag important› closed_segment :: "'a::real_vector ⇒ 'a ⇒ 'a set" where "closed_segment a b = {(1 - u) *⇩_{R}a + u *⇩_{R}b | u::real. 0 ≤ u ∧ u ≤ 1}" definition✐‹tag important› open_segment :: "'a::real_vector ⇒ 'a ⇒ 'a set" where "open_segment a b ≡ closed_segment a b - {a,b}" lemmas segment = open_segment_def closed_segment_def lemma in_segment: "x ∈ closed_segment a b ⟷ (∃u. 0 ≤ u ∧ u ≤ 1 ∧ x = (1 - u) *⇩_{R}a + u *⇩_{R}b)" "x ∈ open_segment a b ⟷ a ≠ b ∧ (∃u. 0 < u ∧ u < 1 ∧ x = (1 - u) *⇩_{R}a + u *⇩_{R}b)" using less_eq_real_def by (auto simp: segment algebra_simps) lemma closed_segment_linear_image: "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f" proof - interpret linear f by fact show ?thesis by (force simp add: in_segment add scale) qed lemma open_segment_linear_image: "⟦linear f; inj f⟧ ⟹ open_segment (f a) (f b) = f ` (open_segment a b)" by (force simp: open_segment_def closed_segment_linear_image inj_on_def) lemma closed_segment_translation: "closed_segment (c + a) (c + b) = image (λx. c + x) (closed_segment a b)" apply safe apply (rule_tac x="x-c" in image_eqI) apply (auto simp: in_segment algebra_simps) done lemma open_segment_translation: "open_segment (c + a) (c + b) = image (λx. c + x) (open_segment a b)" by (simp add: open_segment_def closed_segment_translation translation_diff) lemma closed_segment_of_real: "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" apply (auto simp: image_iff in_segment scaleR_conv_of_real) apply (rule_tac x="(1-u)*x + u*y" in bexI) apply (auto simp: in_segment) done lemma open_segment_of_real: "open_segment (of_real x) (of_real y) = of_real ` open_segment x y" apply (auto simp: image_iff in_segment scaleR_conv_of_real) apply (rule_tac x="(1-u)*x + u*y" in bexI) apply (auto simp: in_segment) done lemma closed_segment_Reals: "⟦x ∈ Reals; y ∈ Reals⟧ ⟹ closed_segment x y = of_real ` closed_segment (Re x) (Re y)" by (metis closed_segment_of_real of_real_Re) lemma open_segment_Reals: "⟦x ∈ Reals; y ∈ Reals⟧ ⟹ open_segment x y = of_real ` open_segment (Re x) (Re y)" by (metis open_segment_of_real of_real_Re) lemma open_segment_PairD: "(x, x') ∈ open_segment (a, a') (b, b') ⟹ (x ∈ open_segment a b ∨ a = b) ∧ (x' ∈ open_segment a' b' ∨ a' = b')" by (auto simp: in_segment) lemma closed_segment_PairD: "(x, x') ∈ closed_segment (a, a') (b, b') ⟹ x ∈ closed_segment a b ∧ x' ∈ closed_segment a' b'" by (auto simp: closed_segment_def) lemma closed_segment_translation_eq [simp]: "d + x ∈ closed_segment (d + a) (d + b) ⟷ x ∈ closed_segment a b" proof - have *: "⋀d x a b. x ∈ closed_segment a b ⟹ d + x ∈ closed_segment (d + a) (d + b)" apply (simp add: closed_segment_def) apply (erule ex_forward) apply (simp add: algebra_simps) done show ?thesis using * [where d = "-d"] * by (fastforce simp add:) qed lemma open_segment_translation_eq [simp]: "d + x ∈ open_segment (d + a) (d + b) ⟷ x ∈ open_segment a b" by (simp add: open_segment_def) lemma of_real_closed_segment [simp]: "of_real x ∈ closed_segment (of_real a) (of_real b) ⟷ x ∈ closed_segment a b" apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) using of_real_eq_iff by fastforce lemma of_real_open_segment [simp]: "of_real x ∈ open_segment (of_real a) (of_real b) ⟷ x ∈ open_segment a b" apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) using of_real_eq_iff by fastforce lemma convex_contains_segment: "convex S ⟷ (∀a∈S. ∀b∈S. closed_segment a b ⊆ S)" unfolding convex_alt closed_segment_def by auto lemma closed_segment_in_Reals: "⟦x ∈ closed_segment a b; a ∈ Reals; b ∈ Reals⟧ ⟹ x ∈ Reals" by (meson subsetD convex_Reals convex_contains_segment) lemma open_segment_in_Reals: "⟦x ∈ open_segment a b; a ∈ Reals; b ∈ Reals⟧ ⟹ x ∈ Reals" by (metis Diff_iff closed_segment_in_Reals open_segment_def) lemma closed_segment_subset: "⟦x ∈ S; y ∈ S; convex S⟧ ⟹ closed_segment x y ⊆ S" by (simp add: convex_contains_segment) lemma closed_segment_subset_convex_hull: "⟦x ∈ convex hull S; y ∈ convex hull S⟧ ⟹ closed_segment x y ⊆ convex hull S" using convex_contains_segment by blast lemma segment_convex_hull: "closed_segment a b = convex hull {a,b}" proof - have *: "⋀x. {x} ≠ {}" by auto show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton by (safe; rule_tac x="1 - u" in exI; force) qed lemma open_closed_segment: "u ∈ open_segment w z ⟹ u ∈ closed_segment w z" by (auto simp add: closed_segment_def open_segment_def) lemma segment_open_subset_closed: "open_segment a b ⊆ closed_segment a b" by (auto simp: closed_segment_def open_segment_def) lemma bounded_closed_segment: fixes a :: "'a::real_normed_vector" shows "bounded (closed_segment a b)" by (rule boundedI[where B="max (norm a) (norm b)"]) (auto simp: closed_segment_def max_def convex_bound_le intro!: norm_triangle_le) lemma bounded_open_segment: fixes a :: "'a::real_normed_vector" shows "bounded (open_segment a b)" by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) lemmas bounded_segment = bounded_closed_segment open_closed_segment lemma ends_in_segment [iff]: "a ∈ closed_segment a b" "b ∈ closed_segment a b" unfolding segment_convex_hull by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) lemma eventually_closed_segment: fixes x0::"'a::real_normed_vector" assumes "open X0" "x0 ∈ X0" shows "∀⇩_{F}x in at x0 within U. closed_segment x0 x ⊆ X0" proof - from openE[OF assms] obtain e where e: "0 < e" "ball x0 e ⊆ X0" . then have "∀⇩_{F}x in at x0 within U. x ∈ ball x0 e" by (auto simp: dist_commute eventually_at) then show ?thesis proof eventually_elim case (elim x) have "x0 ∈ ball x0 e" using ‹e > 0› by simp from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] have "closed_segment x0 x ⊆ ball x0 e" . also note ‹… ⊆ X0› finally show ?case . qed qed lemma closed_segment_commute: "closed_segment a b = closed_segment b a" proof - have "{a, b} = {b, a}" by auto thus ?thesis by (simp add: segment_convex_hull) qed lemma segment_bound1: assumes "x ∈ closed_segment a b" shows "norm (x - a) ≤ norm (b - a)" proof - obtain u where "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" "0 ≤ u" "u ≤ 1" using assms by (auto simp add: closed_segment_def) then show "norm (x - a) ≤ norm (b - a)" apply clarify apply (auto simp: algebra_simps) apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) done qed lemma segment_bound: assumes "x ∈ closed_segment a b" shows "norm (x - a) ≤ norm (b - a)" "norm (x - b) ≤ norm (b - a)" by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)+ lemma open_segment_commute: "open_segment a b = open_segment b a" proof - have "{a, b} = {b, a}" by auto thus ?thesis by (simp add: closed_segment_commute open_segment_def) qed lemma closed_segment_idem [simp]: "closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps) lemma open_segment_idem [simp]: "open_segment a a = {}" by (simp add: open_segment_def) lemma closed_segment_eq_open: "closed_segment a b = open_segment a b ∪ {a,b}" using open_segment_def by auto lemma convex_contains_open_segment: "convex s ⟷ (∀a∈s. ∀b∈s. open_segment a b ⊆ s)" by (simp add: convex_contains_segment closed_segment_eq_open) lemma closed_segment_eq_real_ivl1: fixes a b::real assumes "a ≤ b" shows "closed_segment a b = {a .. b}" proof safe fix x assume "x ∈ closed_segment a b" then obtain u where u: "0 ≤ u" "u ≤ 1" and x_def: "x = (1 - u) * a + u * b" by (auto simp: closed_segment_def) have "u * a ≤ u * b" "(1 - u) * a ≤ (1 - u) * b" by (auto intro!: mult_left_mono u assms) then show "x ∈ {a .. b}" unfolding x_def by (auto simp: algebra_simps) next show "⋀x. x ∈ {a..b} ⟹ x ∈ closed_segment a b" by (force simp: closed_segment_def divide_simps algebra_simps intro: exI[where x="(x - a) / (b - a)" for x]) qed lemma closed_segment_eq_real_ivl: fixes a b::real shows "closed_segment a b = (if a ≤ b then {a .. b} else {b .. a})" using closed_segment_eq_real_ivl1[of a b] closed_segment_eq_real_ivl1[of b a] by (auto simp: closed_segment_commute) lemma open_segment_eq_real_ivl: fixes a b::real shows "open_segment a b = (if a ≤ b then {a<..<b} else {b<..<a})" by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm) lemma closed_segment_real_eq: fixes u::real shows "closed_segment u v = (λx. (v - u) * x + u) ` {0..1}" by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) lemma closed_segment_same_Re: assumes "Re a = Re b" shows "closed_segment a b = {z. Re z = Re a ∧ Im z ∈ closed_segment (Im a) (Im b)}" proof safe fix z assume "z ∈ closed_segment a b" then obtain u where u: "u ∈ {0..1}" "z = a + of_real u * (b - a)" by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) from assms show "Re z = Re a" by (auto simp: u) from u(1) show "Im z ∈ closed_segment (Im a) (Im b)" by (force simp: u closed_segment_def algebra_simps) next fix z assume [simp]: "Re z = Re a" and "Im z ∈ closed_segment (Im a) (Im b)" then obtain u where u: "u ∈ {0..1}" "Im z = Im a + of_real u * (Im b - Im a)" by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) from u(1) show "z ∈ closed_segment a b" using assms by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff) qed lemma closed_segment_same_Im: assumes "Im a = Im b" shows "closed_segment a b = {z. Im z = Im a ∧ Re z ∈ closed_segment (Re a) (Re b)}" proof safe fix z assume "z ∈ closed_segment a b" then obtain u where u: "u ∈ {0..1}" "z = a + of_real u * (b - a)" by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) from assms show "Im z = Im a" by (auto simp: u) from u(1) show "Re z ∈ closed_segment (Re a) (Re b)" by (force simp: u closed_segment_def algebra_simps) next fix z assume [simp]: "Im z = Im a" and "Re z ∈ closed_segment (Re a) (Re b)" then obtain u where u: "u ∈ {0..1}" "Re z = Re a + of_real u * (Re b - Re a)" by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps) from u(1) show "z ∈ closed_segment a b" using assms by (force simp: u closed_segment_def algebra_simps scaleR_conv_of_real complex_eq_iff) qed lemma dist_in_closed_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ closed_segment a b" shows "dist x a ≤ dist a b ∧ dist x b ≤ dist a b" proof (intro conjI) obtain u where u: "0 ≤ u" "u ≤ 1" and x: "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" using assms by (force simp: in_segment algebra_simps) have "dist x a = u * dist a b" apply (simp add: dist_norm algebra_simps x) by (metis ‹0 ≤ u› abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) also have "... ≤ dist a b" by (simp add: mult_left_le_one_le u) finally show "dist x a ≤ dist a b" . have "dist x b = norm ((1-u) *⇩_{R}a - (1-u) *⇩_{R}b)" by (simp add: dist_norm algebra_simps x) also have "... = (1-u) * dist a b" proof - have "norm ((1 - 1 * u) *⇩_{R}(a - b)) = (1 - 1 * u) * norm (a - b)" using ‹u ≤ 1› by force then show ?thesis by (simp add: dist_norm real_vector.scale_right_diff_distrib) qed also have "... ≤ dist a b" by (simp add: mult_left_le_one_le u) finally show "dist x b ≤ dist a b" . qed lemma dist_in_open_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ open_segment a b" shows "dist x a < dist a b ∧ dist x b < dist a b" proof (intro conjI) obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" using assms by (force simp: in_segment algebra_simps) have "dist x a = u * dist a b" apply (simp add: dist_norm algebra_simps x) by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib ‹0 < u›) also have *: "... < dist a b" using assms mult_less_cancel_right2 u(2) by fastforce finally show "dist x a < dist a b" . have ab_ne0: "dist a b ≠ 0" using * by fastforce have "dist x b = norm ((1-u) *⇩_{R}a - (1-u) *⇩_{R}b)" by (simp add: dist_norm algebra_simps x) also have "... = (1-u) * dist a b" proof - have "norm ((1 - 1 * u) *⇩_{R}(a - b)) = (1 - 1 * u) * norm (a - b)" using ‹u < 1› by force then show ?thesis by (simp add: dist_norm real_vector.scale_right_diff_distrib) qed also have "... < dist a b" using ab_ne0 ‹0 < u› by simp finally show "dist x b < dist a b" . qed lemma dist_decreases_open_segment_0: fixes x :: "'a :: euclidean_space" assumes "x ∈ open_segment 0 b" shows "dist c x < dist c 0 ∨ dist c x < dist c b" proof (rule ccontr, clarsimp simp: not_less) obtain u where u: "0 ≠ b" "0 < u" "u < 1" and x: "x = u *⇩_{R}b" using assms by (auto simp: in_segment) have xb: "x ∙ b < b ∙ b" using u x by auto assume "norm c ≤ dist c x" then have "c ∙ c ≤ (c - x) ∙ (c - x)" by (simp add: dist_norm norm_le) moreover have "0 < x ∙ b" using u x by auto ultimately have less: "c ∙ b < x ∙ b" by (simp add: x algebra_simps inner_commute u) assume "dist c b ≤ dist c x" then have "(c - b) ∙ (c - b) ≤ (c - x) ∙ (c - x)" by (simp add: dist_norm norm_le) then have "(b ∙ b) * (1 - u*u) ≤ 2 * (b ∙ c) * (1-u)" by (simp add: x algebra_simps inner_commute) then have "(1+u) * (b ∙ b) * (1-u) ≤ 2 * (b ∙ c) * (1-u)" by (simp add: algebra_simps) then have "(1+u) * (b ∙ b) ≤ 2 * (b ∙ c)" using ‹u < 1› by auto with xb have "c ∙ b ≥ x ∙ b" by (auto simp: x algebra_simps inner_commute) with less show False by auto qed proposition dist_decreases_open_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ open_segment a b" shows "dist c x < dist c a ∨ dist c x < dist c b" proof - have *: "x - a ∈ open_segment 0 (b - a)" using assms by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) show ?thesis using dist_decreases_open_segment_0 [OF *, of "c-a"] assms by (simp add: dist_norm) qed corollary open_segment_furthest_le: fixes a b x y :: "'a::euclidean_space" assumes "x ∈ open_segment a b" shows "norm (y - x) < norm (y - a) ∨ norm (y - x) < norm (y - b)" by (metis assms dist_decreases_open_segment dist_norm) corollary dist_decreases_closed_segment: fixes a :: "'a :: euclidean_space" assumes "x ∈ closed_segment a b" shows "dist c x ≤ dist c a ∨ dist c x ≤ dist c b" apply (cases "x ∈ open_segment a b") using dist_decreases_open_segment less_eq_real_def apply blast by (metis DiffI assms empty_iff insertE open_segment_def order_refl) corollary segment_furthest_le: fixes a b x y :: "'a::euclidean_space" assumes "x ∈ closed_segment a b" shows "norm (y - x) ≤ norm (y - a) ∨ norm (y - x) ≤ norm (y - b)" by (metis assms dist_decreases_closed_segment dist_norm) lemma convex_intermediate_ball: fixes a :: "'a :: euclidean_space" shows "⟦ball a r ⊆ T; T ⊆ cball a r⟧ ⟹ convex T" apply (simp add: convex_contains_open_segment, clarify) by (metis (no_types, opaque_lifting) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b ⊆ closed_segment a b" apply (clarsimp simp: midpoint_def in_segment) apply (rule_tac x="(1 + u) / 2" in exI) apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) by (metis field_sum_of_halves scaleR_left.add) lemma notin_segment_midpoint: fixes a :: "'a :: euclidean_space" shows "a ≠ b ⟹ a ∉ closed_segment (midpoint a b) b" by (auto simp: dist_midpoint dest!: dist_in_closed_segment) subsubsection‹More lemmas, especially for working with the underlying formula› lemma segment_eq_compose: fixes a :: "'a :: real_vector" shows "(λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) = (λx. a + x) o (λu. u *⇩_{R}(b - a))" by (simp add: o_def algebra_simps) lemma segment_degen_1: fixes a :: "'a :: real_vector" shows "(1 - u) *⇩_{R}a + u *⇩_{R}b = b ⟷ a=b ∨ u=1" proof - { assume "(1 - u) *⇩_{R}a + u *⇩_{R}b = b" then have "(1 - u) *⇩_{R}a = (1 - u) *⇩_{R}b" by (simp add: algebra_simps) then have "a=b ∨ u=1" by simp } then show ?thesis by (auto simp: algebra_simps) qed lemma segment_degen_0: fixes a :: "'a :: real_vector" shows "(1 - u) *⇩_{R}a + u *⇩_{R}b = a ⟷ a=b ∨ u=0" using segment_degen_1 [of "1-u" b a] by (auto simp: algebra_simps) lemma add_scaleR_degen: fixes a b ::"'a::real_vector" assumes "(u *⇩_{R}b + v *⇩_{R}a) = (u *⇩_{R}a + v *⇩_{R}b)" "u ≠ v" shows "a=b" by (metis (no_types, opaque_lifting) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms) lemma closed_segment_image_interval: "closed_segment a b = (λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) ` {0..1}" by (auto simp: set_eq_iff image_iff closed_segment_def) lemma open_segment_image_interval: "open_segment a b = (if a=b then {} else (λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) ` {0<..<1})" by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval lemma closed_segment_neq_empty [simp]: "closed_segment a b ≠ {}" by auto lemma open_segment_eq_empty [simp]: "open_segment a b = {} ⟷ a = b" proof - { assume a1: "open_segment a b = {}" have "{} ≠ {0::real<..<1}" by simp then have "a = b" using a1 open_segment_image_interval by fastforce } then show ?thesis by auto qed lemma open_segment_eq_empty' [simp]: "{} = open_segment a b ⟷ a = b" using open_segment_eq_empty by blast lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty lemma inj_segment: fixes a :: "'a :: real_vector" assumes "a ≠ b" shows "inj_on (λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) I" proof fix x y assume "(1 - x) *⇩_{R}a + x *⇩_{R}b = (1 - y) *⇩_{R}a + y *⇩_{R}b" then have "x *⇩_{R}(b - a) = y *⇩_{R}(b - a)" by (simp add: algebra_simps) with assms show "x = y" by (simp add: real_vector.scale_right_imp_eq) qed lemma finite_closed_segment [simp]: "finite(closed_segment a b) ⟷ a = b" apply auto apply (rule ccontr) apply (simp add: segment_image_interval) using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast done lemma finite_open_segment [simp]: "finite(open_segment a b) ⟷ a = b" by (auto simp: open_segment_def) lemmas finite_segment = finite_closed_segment finite_open_segment lemma closed_segment_eq_sing: "closed_segment a b = {c} ⟷ a = c ∧ b = c" by auto lemma open_segment_eq_sing: "open_segment a b ≠ {c}" by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval) lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing lemma open_segment_bound1: assumes "x ∈ open_segment a b" shows "norm (x - a) < norm (b - a)" proof - obtain u where "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" "0 < u" "u < 1" "a ≠ b" using assms by (auto simp add: open_segment_image_interval split: if_split_asm) then show "norm (x - a) < norm (b - a)" apply clarify apply (auto simp: algebra_simps) apply (simp add: scaleR_diff_right [symmetric]) done qed lemma compact_segment [simp]: fixes a :: "'a::real_normed_vector" shows "compact (closed_segment a b)" by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) lemma closed_segment [simp]: fixes a :: "'a::real_normed_vector" shows "closed (closed_segment a b)" by (simp add: compact_imp_closed) lemma closure_closed_segment [simp]: fixes a :: "'a::real_normed_vector" shows "closure(closed_segment a b) = closed_segment a b" by simp lemma open_segment_bound: assumes "x ∈ open_segment a b" shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" apply (simp add: assms open_segment_bound1) by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) lemma closure_open_segment [simp]: "closure (open_segment a b) = (if a = b then {} else closed_segment a b)" for a :: "'a::euclidean_space" proof (cases "a = b") case True then show ?thesis by simp next case False have "closure ((λu. u *⇩_{R}(b - a)) ` {0<..<1}) = (λu. u *⇩_{R}(b - a)) ` closure {0<..<1}" apply (rule closure_injective_linear_image [symmetric]) apply (use False in ‹auto intro!: injI›) done then have "closure ((λu. (1 - u) *⇩_{R}a + u *⇩_{R}b) ` {0<..<1}) = (λx. (1 - x) *⇩_{R}a + x *⇩_{R}b) ` closure {0<..<1}" using closure_translation [of a "((λx. x *⇩_{R}b - x *⇩_{R}a) ` {0<..<1})"] by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image) then show ?thesis by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan) qed lemma closed_open_segment_iff [simp]: fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) ⟷ a = b" by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) lemma compact_open_segment_iff [simp]: fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) ⟷ a = b" by (simp add: bounded_open_segment compact_eq_bounded_closed) lemma convex_closed_segment [iff]: "convex (closed_segment a b)" unfolding segment_convex_hull by(rule convex_convex_hull) lemma convex_open_segment [iff]: "convex (open_segment a b)" proof - have "convex ((λu. u *⇩_{R}(b - a)) ` {0<..<1})" by (rule convex_linear_image) auto then have "convex ((+) a ` (λu. u *⇩_{R}(b - a)) ` {0<..<1})" by (rule convex_translation) then show ?thesis by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right) qed lemmas convex_segment = convex_closed_segment convex_open_segment lemma subset_closed_segment: "closed_segment a b ⊆ closed_segment c d ⟷ a ∈ closed_segment c d ∧ b ∈ closed_segment c d" by auto (meson contra_subsetD convex_closed_segment convex_contains_segment) lemma subset_co_segment: "closed_segment a b ⊆ open_segment c d ⟷ a ∈ open_segment c d ∧ b ∈ open_segment c d" using closed_segment_subset by blast lemma subset_open_segment: fixes a :: "'a::euclidean_space" shows "open_segment a b ⊆ open_segment c d ⟷ a = b ∨ a ∈ closed_segment c d ∧ b ∈ closed_segment c d" (is "?lhs = ?rhs") proof (cases "a = b") case True then show ?thesis by simp next case False show ?thesis proof assume rhs: ?rhs with ‹a ≠ b› have "c ≠ d" using closed_segment_idem singleton_iff by auto have "∃uc. (1 - u) *⇩_{R}((1 - ua) *⇩_{R}c + ua *⇩_{R}d) + u *⇩_{R}((1 - ub) *⇩_{R}c + ub *⇩_{R}d) = (1 - uc) *⇩_{R}c + uc *⇩_{R}d ∧ 0 < uc ∧ uc < 1" if neq: "(1 - ua) *⇩_{R}c + ua *⇩_{R}d ≠ (1 - ub) *⇩_{R}c + ub *⇩_{R}d" "c ≠ d" and "a = (1 - ua) *⇩_{R}c + ua *⇩_{R}d" "b = (1 - ub) *⇩_{R}c + ub *⇩_{R}d" and u: "0 < u" "u < 1" and uab: "0 ≤ ua" "ua ≤ 1" "0 ≤ ub" "ub ≤ 1" for u ua ub proof - have "ua ≠ ub" using neq by auto moreover have "(u - 1) * ua ≤ 0" using u uab by (simp add: mult_nonpos_nonneg) ultimately have lt: "(u - 1) * ua < u * ub" using u uab by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less) have "p * ua + q * ub < p+q" if p: "0 < p" and q: "0 < q" for p q proof - have "¬ p ≤ 0" "¬ q ≤ 0" using p q not_less by blast+ then show ?thesis by (metis ‹ua ≠ ub› add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5) less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4)) qed then have "(1 - u) * ua + u * ub < 1" using u ‹ua ≠ ub› by (metis diff_add_cancel diff_gt_0_iff_gt) with lt show ?thesis by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps) qed with rhs ‹a ≠ b› ‹c ≠ d› show ?lhs unfolding open_segment_image_interval closed_segment_def by (fastforce simp add:) next assume lhs: ?lhs with ‹a ≠ b› have "c ≠ d" by (meson finite_open_segment rev_finite_subset) have "closure (open_segment a b) ⊆ closure (open_segment c d)" using lhs closure_mono by blast then have "closed_segment a b ⊆ closed_segment c d" by (simp add: ‹a ≠ b› ‹c ≠ d›) then show ?rhs by (force simp: ‹a ≠ b›) qed qed lemma subset_oc_segment: fixes a :: "'a::euclidean_space" shows "open_segment a b ⊆ closed_segment c d ⟷ a = b ∨ a ∈ closed_segment c d ∧ b ∈ closed_segment c d" apply (simp add: subset_open_segment [symmetric]) apply (rule iffI) apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment) apply (meson dual_order.trans segment_open_subset_closed) done lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment lemma dist_half_times2: fixes a :: "'a :: real_normed_vector" shows "dist ((1 / 2) *⇩_{R}(a + b)) x * 2 = dist (a+b) (2 *⇩_{R}x)" proof - have "norm ((1 / 2) *⇩_{R}(a + b) - x) * 2 = norm (2 *⇩_{R}((1 / 2) *⇩_{R}(a + b) - x))" by simp also have "... = norm ((a + b) - 2 *⇩_{R}x)" by (simp add: real_vector.scale_right_diff_distrib) finally show ?thesis by (simp only: dist_norm) qed lemma closed_segment_as_ball: "closed_segment a b = affine hull {a,b} ∩ cball(inverse 2 *⇩_{R}(a + b))(norm(b - a) / 2)" proof (cases "b = a") case True then show ?thesis by (auto simp: hull_inc) next case False then have *: "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 ≤ norm (b - a)) = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1)" for x proof - have "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 ≤ norm (b - a)) = ((∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 ≤ norm (b - a))" unfolding eq_diff_eq [symmetric] by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}x)) ≤ norm (b - a))" by (simp add: dist_half_times2) (simp add: dist_norm) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}((1 - u) *⇩_{R}a + u *⇩_{R}b))) ≤ norm (b - a))" by auto also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((1 - u * 2) *⇩_{R}(b - a)) ≤ norm (b - a))" by (simp add: algebra_simps scaleR_2) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ * norm (b - a) ≤ norm (b - a))" by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ ≤ 1)" by (simp add: mult_le_cancel_right2 False) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1)" by auto finally show ?thesis . qed show ?thesis by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *) qed lemma open_segment_as_ball: "open_segment a b = affine hull {a,b} ∩ ball(inverse 2 *⇩_{R}(a + b))(norm(b - a) / 2)" proof (cases "b = a") case True then show ?thesis by (auto simp: hull_inc) next case False then have *: "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 < norm (b - a)) = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 < u ∧ u < 1)" for x proof - have "((∃u v. x = u *⇩_{R}a + v *⇩_{R}b ∧ u + v = 1) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 < norm (b - a)) = ((∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b) ∧ dist ((1 / 2) *⇩_{R}(a + b)) x * 2 < norm (b - a))" unfolding eq_diff_eq [symmetric] by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}x)) < norm (b - a))" by (simp add: dist_half_times2) (simp add: dist_norm) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((a+b) - (2 *⇩_{R}((1 - u) *⇩_{R}a + u *⇩_{R}b))) < norm (b - a))" by auto also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ norm ((1 - u * 2) *⇩_{R}(b - a)) < norm (b - a))" by (simp add: algebra_simps scaleR_2) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ * norm (b - a) < norm (b - a))" by simp also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ ¦1 - u * 2¦ < 1)" by (simp add: mult_le_cancel_right2 False) also have "... = (∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 < u ∧ u < 1)" by auto finally show ?thesis . qed show ?thesis using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *) qed lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball lemma connected_segment [iff]: fixes x :: "'a :: real_normed_vector" shows "connected (closed_segment x y)" by (simp add: convex_connected) lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real unfolding closed_segment_eq_real_ivl by (auto simp: is_interval_def) lemma IVT'_closed_segment_real: fixes f :: "real ⇒ real" assumes "y ∈ closed_segment (f a) (f b)" assumes "continuous_on (closed_segment a b) f" shows "∃x ∈ closed_segment a b. f x = y" using IVT'[of f a y b] IVT'[of "-f" a "-y" b] IVT'[of f b y a] IVT'[of "-f" b "-y" a] assms by (cases "a ≤ b"; cases "f b ≥ f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus) subsection ‹Betweenness› definition✐‹tag important› "between = (λ(a,b) x. x ∈ closed_segment a b)" lemma betweenI: assumes "0 ≤ u" "u ≤ 1" "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" shows "between (a, b) x" using assms unfolding between_def closed_segment_def by auto lemma betweenE: assumes "between (a, b) x" obtains u where "0 ≤ u" "u ≤ 1" "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" using assms unfolding between_def closed_segment_def by auto lemma between_implies_scaled_diff: assumes "between (S, T) X" "between (S, T) Y" "S ≠ Y" obtains c where "(X - Y) = c *⇩_{R}(S - Y)" proof - from ‹between (S, T) X› obtain u⇩_{X}where X: "X = u⇩_{X}*⇩_{R}S + (1 - u⇩_{X}) *⇩_{R}T" by (metis add.commute betweenE eq_diff_eq) from ‹between (S, T) Y› obtain u⇩_{Y}where Y: "Y = u⇩_{Y}*⇩_{R}S + (1 - u⇩_{Y}) *⇩_{R}T" by (metis add.commute betweenE eq_diff_eq) have "X - Y = (u⇩_{X}- u⇩_{Y}) *⇩_{R}(S - T)" proof - from X Y have "X - Y = u⇩_{X}*⇩_{R}S - u⇩_{Y}*⇩_{R}S + ((1 - u⇩_{X}) *⇩_{R}T - (1 - u⇩_{Y}) *⇩_{R}T)" by simp also have "… = (u⇩_{X}- u⇩_{Y}) *⇩_{R}S - (u⇩_{X}- u⇩_{Y}) *⇩_{R}T" by (simp add: scaleR_left.diff) finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib) qed moreover from Y have "S - Y = (1 - u⇩_{Y}) *⇩_{R}(S - T)" by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) moreover note ‹S ≠ Y› ultimately have "(X - Y) = ((u⇩_{X}- u⇩_{Y}) / (1 - u⇩_{Y})) *⇩_{R}(S - Y)" by auto from this that show thesis by blast qed lemma between_mem_segment: "between (a,b) x ⟷ x ∈ closed_segment a b" unfolding between_def by auto lemma between: "between (a, b) (x::'a::euclidean_space) ⟷ dist a b = (dist a x) + (dist x b)" proof (cases "a = b") case True then show ?thesis by (auto simp add: between_def dist_commute) next case False then have Fal: "norm (a - b) ≠ 0" and Fal2: "norm (a - b) > 0" by auto have *: "⋀u. a - ((1 - u) *⇩_{R}a + u *⇩_{R}b) = u *⇩_{R}(a - b)" by (auto simp add: algebra_simps) have "norm (a - x) *⇩_{R}(x - b) = norm (x - b) *⇩_{R}(a - x)" if "x = (1 - u) *⇩_{R}a + u *⇩_{R}b" "0 ≤ u" "u ≤ 1" for u proof - have *: "a - x = u *⇩_{R}(a - b)" "x - b = (1 - u) *⇩_{R}(a - b)" unfolding that(1) by (auto simp add:algebra_simps) show "norm (a - x) *⇩_{R}(x - b) = norm (x - b) *⇩_{R}(a - x)" unfolding norm_minus_commute[of x a] * using ‹0 ≤ u› ‹u ≤ 1› by simp qed moreover have "∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1" if "dist a b = dist a x + dist x b" proof - let ?β = "norm (a - x) / norm (a - b)" show "∃u. x = (1 - u) *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ u ∧ u ≤ 1" proof (intro exI conjI) show "?β ≤ 1" using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto show "x = (1 - ?β) *⇩_{R}a + (?β) *⇩_{R}b" proof (subst euclidean_eq_iff; intro ballI) fix i :: 'a assume i: "i ∈ Basis" have "((1 - ?β) *⇩_{R}a + (?β) *⇩_{R}b) ∙ i = ((norm (a - b) - norm (a - x)) * (a ∙ i) + norm (a - x) * (b ∙ i)) / norm (a - b)" using Fal by (auto simp add: field_simps inner_simps) also have "… = x∙i" apply (rule divide_eq_imp[OF Fal]) unfolding that[unfolded dist_norm] using that[unfolded dist_triangle_eq] i apply (subst (asm) euclidean_eq_iff) apply (auto simp add: field_simps inner_simps) done finally show "x ∙ i = ((1 - ?β) *⇩_{R}a + (?β) *⇩_{R}b) ∙ i" by auto qed qed (use Fal2 in auto) qed ultimately show ?thesis by (force simp add: between_def closed_segment_def dist_triangle_eq) qed lemma between_midpoint: fixes a :: "'a::euclidean_space" shows "between (a,b) (midpoint a b)" (is ?t1) and "between (b,a) (midpoint a b)" (is ?t2) proof - have *: "⋀x y z. x = (1/2::real) *⇩_{R}z ⟹ y = (1/2) *⇩_{R}z ⟹ norm z = norm x + norm y" by auto show ?t1 ?t2 unfolding between midpoint_def dist_norm by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *) qed lemma between_mem_convex_hull: "between (a,b) x ⟷ x ∈ convex hull {a,b}" unfolding between_mem_segment segment_convex_hull .. lemma between_triv_iff [simp]: "between (a,a) b ⟷ a=b" by (auto simp: between_def) lemma between_triv1 [simp]: "between (a,b) a" by (auto simp: between_def) lemma between_triv2 [simp]: "between (a,b) b" by (auto simp: between_def) lemma between_commute: "between (a,b) = between (b,a)" by (auto simp: between_def closed_segment_commute) lemma between_antisym: fixes a :: "'a :: euclidean_space" shows "⟦between (b,c) a; between (a,c) b⟧ ⟹ a = b" by (auto simp: between dist_commute) lemma between_trans: fixes a :: "'a :: euclidean_space" shows "⟦between (b,c) a; between (a,c) d⟧ ⟹ between (b,c) d" using dist_triangle2 [of b c d] dist_triangle3 [of b d a] by (auto simp: between dist_commute) lemma between_norm: fixes a :: "'a :: euclidean_space" shows "between (a,b) x ⟷ norm(x - a) *⇩_{R}(b - x) = norm(b - x) *⇩_{R}(x - a)" by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps) lemma between_swap: fixes A B X Y :: "'a::euclidean_space" assumes "between (A, B) X" assumes "between (A, B) Y" shows "between (X, B) Y ⟷ between (A, Y) X" using assms by (auto simp add: between) lemma between_translation [simp]: "between (a + y,a + z) (a + x) ⟷ between (y,z) x" by (auto simp: between_def) lemma between_trans_2: fixes a :: "'a :: euclidean_space" shows "⟦between (b,c) a; between (a,b) d⟧ ⟹ between (c,d) a" by (metis between_commute between_swap between_trans) lemma between_scaleR_lift [simp]: fixes v :: "'a::euclidean_space" shows "between (a *⇩_{R}v, b *⇩_{R}v) (c *⇩_{R}v) ⟷ v = 0 ∨ between (a, b) c" by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric]) lemma between_1: fixes x::real shows "between (a,b) x ⟷ (a ≤ x ∧ x ≤ b) ∨ (b ≤ x ∧ x ≤ a)" by (auto simp: between_mem_segment closed_segment_eq_real_ivl) end