# HG changeset patch
# User immler
# Date 1572906380 18000
# Node ID 12cbcd00b651e918b54c9eed39c2c406052b0836
# Parent  be8cec1abcbb113fd3e6c41413da9f82a47a0f29
betweenness is a property on line segments

diff -r be8cec1abcbb -r 12cbcd00b651 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Nov 04 17:18:25 2019 -0500
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Nov 04 17:26:20 2019 -0500
@@ -3126,4 +3126,162 @@
     IVT'[of "-f" b "-y" a] assms
   by (cases "a \<le> b"; cases "f b \<ge> 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 \<le> u" "u \<le> 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 \<le> u" "u \<le> 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 \<noteq> 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 "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
+    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 \<longleftrightarrow> x \<in> closed_segment a b"
+  unfolding between_def by auto
+
+lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> 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) \<noteq> 0" and Fal2: "norm (a - b) > 0"
+    by auto
+  have *: "\<And>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 \<le> u" "u \<le> 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 "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b" 
+  proof -
+    let ?\<beta> = "norm (a - x) / norm (a - b)"
+    show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
+    proof (intro exI conjI)
+      show "?\<beta> \<le> 1"
+        using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto
+      show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b"
+      proof (subst euclidean_eq_iff; intro ballI)
+        fix i :: 'a
+        assume i: "i \<in> Basis"
+        have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> 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 "\<dots> = x\<bullet>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 \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> 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 *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y"
+    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 \<longleftrightarrow> x \<in> convex hull {a,b}"
+  unfolding between_mem_segment segment_convex_hull ..
+
+lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> 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 "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
+by (auto simp: between dist_commute)
+
+lemma between_trans:
+    fixes a :: "'a :: euclidean_space"
+    shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> between (A, Y) X"
+using assms by (auto simp add: between)
+
+lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
+  by (auto simp: between_def)
+
+lemma between_trans_2:
+  fixes a :: "'a :: euclidean_space"
+  shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> 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) \<longleftrightarrow> v = 0 \<or> 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 \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
+  by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
+
+
 end
diff -r be8cec1abcbb -r 12cbcd00b651 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Nov 04 17:18:25 2019 -0500
+++ b/src/HOL/Analysis/Starlike.thy	Mon Nov 04 17:26:20 2019 -0500
@@ -296,164 +296,6 @@
 lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
 
 
-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 \<le> u" "u \<le> 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 \<le> u" "u \<le> 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 \<noteq> 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 "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
-    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 \<longleftrightarrow> x \<in> closed_segment a b"
-  unfolding between_def by auto
-
-lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> 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) \<noteq> 0" and Fal2: "norm (a - b) > 0"
-    by auto
-  have *: "\<And>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 \<le> u" "u \<le> 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 "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b" 
-  proof -
-    let ?\<beta> = "norm (a - x) / norm (a - b)"
-    show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
-    proof (intro exI conjI)
-      show "?\<beta> \<le> 1"
-        using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto
-      show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b"
-      proof (subst euclidean_eq_iff; intro ballI)
-        fix i :: 'a
-        assume i: "i \<in> Basis"
-        have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> 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 "\<dots> = x\<bullet>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 \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> 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 *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y"
-    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 \<longleftrightarrow> x \<in> convex hull {a,b}"
-  unfolding between_mem_segment segment_convex_hull ..
-
-lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> 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 "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
-by (auto simp: between dist_commute)
-
-lemma between_trans:
-    fixes a :: "'a :: euclidean_space"
-    shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> between (A, Y) X"
-using assms by (auto simp add: between)
-
-lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
-  by (auto simp: between_def)
-
-lemma between_trans_2:
-  fixes a :: "'a :: euclidean_space"
-  shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> 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) \<longleftrightarrow> v = 0 \<or> 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 \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
-  by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
-
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>
 
 lemma mem_interior_convex_shrink: