Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: continuous_linear.prf Sprache: Isabelle

Original von: 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 (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 \ (*\<^sub>R) c ` S = S)"
    using cone_iff[of S] assms by auto
  then have "0 \ closure S \ (\c. c > 0 \ (*\<^sub>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 \<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>
    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) *\<^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"
    unfolding mem_ball dist_norm
    unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>]
    unfolding dist_norm[symmetric]
    using u
    unfolding pos_less_divide_eq[OF xy]
    by auto
  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
    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 *\<^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
      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 *\<^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) = 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')
     \<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)"
    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 "\\<^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
    from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
    have "closed_segment x0 x \ ball x0 e" .
    also note \<open>\<dots> \<subseteq> X0\<close>
    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) *\<^sub>R a + u *\<^sub>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<..
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) *\<^sub>R a + u *\<^sub>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 \<open>0 \<le> u\<close> 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) *\<^sub>R a - (1-u) *\<^sub>R b)"
    by (simp add: dist_norm algebra_simps x)
  also have "... = (1-u) * dist a b"
  proof -
    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
      using \<open>u \<le> 1\<close> 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) *\<^sub>R a + u *\<^sub>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 \<open>0 < u\<close>)
  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) *\<^sub>R a - (1-u) *\<^sub>R b)"
    by (simp add: dist_norm algebra_simps x)
  also have "... = (1-u) * dist a b"
  proof -
    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
      using \<open>u < 1\<close> 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 \<open>0 < u\<close> 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 *\<^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"
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, hide_lams) 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\<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"
proof -
  { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
    then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>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) *\<^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 (metis (no_types, hide_lams) 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) *\<^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"
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) *\<^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"
  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) *\<^sub>R a + u *\<^sub>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 *\<^sub>R (b - a)) ` {0<..<1}) = (\u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
    apply (rule closure_injective_linear_image [symmetric])
     apply (use False in \<open>auto intro!: injI\<close>)
    done
  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"
  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)

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 (metis \<open>ua \<noteq> ub\<close> 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 \<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 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"
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) *\<^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)"
  proof -
    from X Y have "X - Y = u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp
    also have "\ = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>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\<^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 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

¤ Dauer der Verarbeitung: 0.55 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.