Theory HOL-Analysis.Line_Segment

(* 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

subsectiontag 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 (metis empty_iff linorder_not_less mem_sphere sphere_empty vector_choose_dist)

lemma cone_closure:
  fixes S :: "'a::real_normed_vector set"
  assumes "cone S"
  shows "cone (closure S)"
  by (metis UnCI assms closure_Un_frontier closure_eq_empty closure_scaleR cone_iff)


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"
  using  connected_UNIV by (force simp add: connected_clopen)

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 "yball x e. f x  f y"
  shows "ys. f x  f y"
proof (rule ccontr)
  have "x  s" using assms(1,3) by auto
  assume "¬ ?thesis"
  then obtain y where "ys" 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 xs ys by (smt (verit) assms(2) convex_on_def)
  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"
    by (smt (verit) "*" 0 < u dist_norm mem_ball norm_scaleR pos_less_divide_eq u xy)
  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 by (meson UNIV_I convex_def convex_on_def convex_on_dist)
  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 by (meson UNIV_I convex_def convex_on_def convex_on_dist)
    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: "xs. 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›

definitiontag 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›

definitiontag 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}"

definitiontag 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) = (λx. c + x) ` (closed_segment a b)" (is "?L = _ ` ?R")
proof -
  have "x. x  ?L  x - c  ?R" "x. x  ?R  c + x  ?L"
    by (auto simp: in_segment algebra_simps)
  then show ?thesis by force
qed

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"
  by (simp add: closed_segment_linear_image linearI scaleR_conv_of_real)

lemma open_segment_of_real:
    "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
  by (simp add: closed_segment_of_real image_set_diff inj_of_real open_segment_def)

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)"
    using closed_segment_translation by blast
  show ?thesis
    using * [where d = "-d"] * by fastforce
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"
  by (simp add: closed_segment_of_real image_iff)

lemma of_real_open_segment [simp]:
  "of_real x  open_segment (of_real a) (of_real b)  x  open_segment a b"
  by (simp add: image_iff open_segment_of_real)

lemma convex_contains_segment:
  "convex S  (aS. bS. 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 (simp add: open_closed_segment subsetI)

lemma bounded_closed_segment:
  fixes a :: "'a::real_normed_vector" shows "bounded (closed_segment a b)"
  by (simp add: bounded_convex_hull segment_convex_hull)

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"
  by (simp_all add: hull_inc segment_convex_hull)


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
    then have "closed_segment x0 x  ball x0 e"
      using closed_segment_subset elim by blast 
    then show ?case
      using e(2) by auto 
  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 u: "x = (1 - u) *R a + u *R b" "0  u" "u  1"
    using assms by (auto simp add: closed_segment_def)
  then have "norm (u *R b - u *R a)  norm (b - a)"
    by (simp add: mult_left_le_one_le flip: scaleR_diff_right)
  with u show ?thesis
    by (metis add_diff_cancel_left scaleR_collapse)
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_bound1:
  assumes "x  open_segment a b"
  shows "norm (x - a) < norm (b - a)"
proof -
  obtain u where u: "x = (1 - u) *R a + u *R b" "0 < u" "u < 1"
    by (meson assms in_segment)
  then have "norm (u *R b - u *R a) < norm (b - a)"
    using assms in_segment(2) less_eq_real_def by (fastforce simp flip: scaleR_diff_right)
  with u show ?thesis
    by (metis add_diff_cancel_left scaleR_collapse)
qed

lemma open_segment_commute: "open_segment a b = open_segment b a"
  by (simp add: closed_segment_commute insert_commute open_segment_def)

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  (as. bs. 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})"
  by (metis closed_segment_commute closed_segment_eq_real_ivl1 nle_le)

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: closed_segment_eq_real_ivl image_affinity_atLeastAtMost)

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"
  by (metis assms dist_commute dist_norm segment_bound(2) segment_bound1)

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"
  by (metis assms dist_commute dist_norm open_segment_bound1 open_segment_commute)

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"
  by (smt (verit, ccfv_threshold) Un_iff assms closed_segment_eq_open dist_norm empty_iff insertE open_segment_furthest_le)

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"
  by (smt (verit) convex_contains_open_segment dist_decreases_open_segment mem_ball mem_cball subset_eq)

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 (simp add: 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"
  by (smt (verit, best) add_right_cancel scaleR_cancel_left scaleR_collapse)

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 (smt (verit) add_diff_cancel_left' add_diff_eq assms scaleR_cancel_left scaleR_left.diff)
  
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"
  by (simp add: segment_image_interval(2))

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"
  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment [of a b]]
  unfolding segment_image_interval
  by (smt (verit, del_insts) finite.emptyI finite_insert finite_subset image_subset_iff insertCI segment_degen_0)

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 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)"
  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}"
  proof (rule closure_injective_linear_image [symmetric])
  qed (use False in auto intro!: injI)
  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"
  using closed_segment_subset convex_closed_segment ends_in_segment in_mono by blast

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 (smt (verit) ua  ub mult_cancel_left1 mult_left_le 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 closed_segment_same_fst:
  "fst a = fst b  closed_segment a b = {fst a} × closed_segment (snd a) (snd b)"
  by (auto simp: closed_segment_def scaleR_prod_def)

lemma closed_segment_same_snd:
  "snd a = snd b  closed_segment a b = closed_segment (fst a) (fst b) × {snd a}"
  by (auto simp: closed_segment_def scaleR_prod_def)

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" 
    (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    by (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment)
  show "?rhs  ?lhs"
    by (meson dual_order.trans segment_open_subset_closed subset_open_segment)
qed

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›

definitiontag 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 uX where X: "X = uX *R S + (1 - uX) *R T"
    by (metis add.commute betweenE eq_diff_eq)
  from between (S, T) Y obtain uY where Y: "Y = uY *R S + (1 - uY) *R T"
    by (metis add.commute betweenE eq_diff_eq)
  have "X - Y = (uX - uY) *R (S - T)"
    by (simp add: X Y scaleR_left.diff scaleR_right_diff_distrib)
  moreover from Y have "S - Y = (1 - uY) *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) = ((uX - uY) / (1 - uY)) *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 " = xi"
          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 flip: scaleR_left_diff_distrib distrib_right)

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