--- 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
--- 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: