Quelle Line_Segment.thy Sprache: Isabelle

(* 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 \<open>Line Segment\<close>

theory Line_Segment
imports
  Convex
  Topology_Euclidean_Space
begin

subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets, Metric Spaces and Functions\<close>

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 *\<^sub>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 *\<^sub>R f i) I = sum (\i. u i *\<^sub>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 \<open>convex S\<close>])
  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 \<open>Balls, being convex, are connected.\<close>

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 \<open>e>0\<close> by auto
  then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \ (1-u) * f x + u * f y"
    using \<open>x\<in>s\<close> \<open>y\<in>s\<close> by (smt (verit) assms(2) convex_on_def)
  moreover
  have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
    by (simp add: algebra_simps)
  have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ ball x e"
    by (smt (verit) "*" \<open>0 < u\<close> dist_norm mem_ball norm_scaleR pos_less_divide_eq u xy)
  then have "f x \ f ((1 - u) *\<^sub>R x + u *\<^sub>R y)"
    using assms(4) by auto
  ultimately show False
    using mult_strict_left_mono[OF y \<open>u>0\<close>]
    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 *\<^sub>R y + v *\<^sub>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 *\<^sub>R y + v *\<^sub>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 *\<^sub>R y + v *\<^sub>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 *\<^sub>R y + v *\<^sub>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 \<open>Midpoint\<close>

definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
  where "midpoint a b = (inverse (2::real)) *\<^sub>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 *\<^sub>R x = - y \ norm x = (norm y) / 2"
    unfolding equation_minus_iff by auto
  have **: "\x y::'a. 2 *\<^sub>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>Open and closed segments\<close>

definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
  where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}"

definition\<^marker>\<open>tag important\<close> open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> '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) *\<^sub>R a + u *\<^sub>R b)"
    "x \ open_segment a b \ a \ b \ (\u. 0 < u \ u < 1 \ x = (1 - u) *\<^sub>R a + u *\<^sub>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')
     \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> 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 \ (\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 (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 "\\<^sub>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 "\\<^sub>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) *\<^sub>R a + u *\<^sub>R b" "0 \ u" "u \ 1"
    using assms by (auto simp add: closed_segment_def)
  then have "norm (u *\<^sub>R b - u *\<^sub>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) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1"
    by (meson assms in_segment)
  then have "norm (u *\<^sub>R b - u *\<^sub>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 \ (\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})"
  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<..
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 *\<^sub>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 \<open>u < 1\<close> 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\<open>More lemmas, especially for working with the underlying formula\<close>

lemma segment_eq_compose:
  fixes a :: "'a :: real_vector"
  shows "(\u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\x. a + x) o (\u. u *\<^sub>R (b - a))"
    by (simp add: o_def algebra_simps)

lemma segment_degen_1:
  fixes a :: "'a :: real_vector"
  shows "(1 - u) *\<^sub>R a + u *\<^sub>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) *\<^sub>R a + u *\<^sub>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 *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>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) *\<^sub>R a + u *\<^sub>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) *\<^sub>R a + u *\<^sub>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) *\<^sub>R a + u *\<^sub>R b) I"
proof
  fix x y
  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
  then have "x *\<^sub>R (b - a) = y *\<^sub>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 *\<^sub>R (b - a)) ` {0<..<1}) = (\u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
  proof (rule closure_injective_linear_image [symmetric])
  qed (use False in \<open>auto intro!: injI\<close>)
  then have "closure
     ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
    using closure_translation [of a "((\x. x *\<^sub>R b - x *\<^sub>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 *\<^sub>R (b - a)) ` {0<..<1})"
    by (rule convex_linear_image) auto
  then have "convex ((+) a ` (\u. u *\<^sub>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 \<in> closed_segment c d \<and> b \<in> 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 \<in> open_segment c d \<and> b \<in> 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 \<or> a \<in> closed_segment c d \<and> b \<in> 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 \<open>a \<noteq> b\<close> have "c \<noteq> d"
      using closed_segment_idem singleton_iff by auto
    have "\uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \ (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \ d"
           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>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) \<open>ua \<noteq> ub\<close> mult_cancel_left1 mult_left_le uab(2) uab(4))
      qed
      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
        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 \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
      unfolding open_segment_image_interval closed_segment_def
      by (fastforce simp add:)
  next
    assume lhs: ?lhs
    with \<open>a \<noteq> b\<close> have "c \<noteq> 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: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
    then show ?rhs
      by (force simp: \<open>a \<noteq> b\<close>)
  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 \<or> a \<in> closed_segment c d \<and> b \<in> 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) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
proof -
  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
    by simp
  also have "... = norm ((a + b) - 2 *\<^sub>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 *\<^sub>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 *\<^sub>R a + v *\<^sub>R b \ u + v = 1) \
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
  proof -
    have "((\u v. x = u *\<^sub>R a + v *\<^sub>R b \ u + v = 1) \
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
      unfolding eq_diff_eq [symmetric] by simp
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
      by (simp add: dist_half_times2) (simp add: dist_norm)
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
      by auto
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
      by (simp add: algebra_simps scaleR_2)
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
      by simp
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ \1 - u * 2\ \ 1)"
      by (simp add: mult_le_cancel_right2 False)
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>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} \<inter> ball(inverse 2 *\<^sub>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 *\<^sub>R a + v *\<^sub>R b \ u + v = 1) \
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
  proof -
    have "((\u v. x = u *\<^sub>R a + v *\<^sub>R b \ u + v = 1) \
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
      unfolding eq_diff_eq [symmetric] by simp
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
      by (simp add: dist_half_times2) (simp add: dist_norm)
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
      by auto
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
      by (simp add: algebra_simps scaleR_2)
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \
                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
      by simp
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ \1 - u * 2\ < 1)"
      by (simp add: mult_le_cancel_right2 False)
    also have "... = (\u. x = (1 - u) *\<^sub>R a + u *\<^sub>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 \<open>Betweenness\<close>

definition\<^marker>\<open>tag important\<close> "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"

lemma betweenI:
  assumes "0 \ u" "u \ 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>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) *\<^sub>R a + u *\<^sub>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 *\<^sub>R (S - Y)"
proof -
  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"
    by (metis add.commute betweenE eq_diff_eq)
  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"
    by (metis add.commute betweenE eq_diff_eq)
  have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
    by (simp add: X Y scaleR_left.diff scaleR_right_diff_distrib)
  moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
  moreover note \<open>S \<noteq> Y\<close>
  ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>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) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)"
    by (auto simp add: algebra_simps)
  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 \ u" "u \ 1" for u
  proof -
    have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
      unfolding that(1) by (auto simp add:algebra_simps)
    show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
      unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
      by simp
  qed
  moreover have "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \ 0 \ u \ u \ 1" if "dist a b = dist a x + dist x b"
  proof -
    let ?\<beta> = "norm (a - x) / norm (a - b)"
    show "\u. x = (1 - u) *\<^sub>R a + u *\<^sub>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 - ?\) *\<^sub>R a + (?\) *\<^sub>R b"
      proof (subst euclidean_eq_iff; intro ballI)
        fix i :: 'a
        assume i: "i \ Basis"
        have "((1 - ?\) *\<^sub>R a + (?\) *\<^sub>R b) \ i
              = ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> 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 - ?\) *\<^sub>R a + (?\) *\<^sub>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) *\<^sub>R z \ y = (1/2) *\<^sub>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) *\<^sub>R (b - x) = norm(b - x) *\<^sub>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 *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>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

quality93%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.