moved segment lemmas where they belong
authornipkow
Wed Dec 04 18:28:24 2019 +0100 (2 days ago ago)
changeset 71433095cf95d7725
parent 71432 be2c2bfa54a0
child 71435 7b9ff966974f
moved segment lemmas where they belong
src/HOL/Analysis/Line_Segment.thy
src/HOL/Analysis/Starlike.thy
     1.1 --- a/src/HOL/Analysis/Line_Segment.thy	Wed Dec 04 15:36:58 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Line_Segment.thy	Wed Dec 04 18:28:24 2019 +0100
     1.3 @@ -789,6 +789,57 @@
     1.4  
     1.5  lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
     1.6  
     1.7 +lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
     1.8 +  by auto
     1.9 +
    1.10 +lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
    1.11 +proof -
    1.12 +  { assume a1: "open_segment a b = {}"
    1.13 +    have "{} \<noteq> {0::real<..<1}"
    1.14 +      by simp
    1.15 +    then have "a = b"
    1.16 +      using a1 open_segment_image_interval by fastforce
    1.17 +  } then show ?thesis by auto
    1.18 +qed
    1.19 +
    1.20 +lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
    1.21 +  using open_segment_eq_empty by blast
    1.22 +
    1.23 +lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
    1.24 +
    1.25 +lemma inj_segment:
    1.26 +  fixes a :: "'a :: real_vector"
    1.27 +  assumes "a \<noteq> b"
    1.28 +    shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
    1.29 +proof
    1.30 +  fix x y
    1.31 +  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
    1.32 +  then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
    1.33 +    by (simp add: algebra_simps)
    1.34 +  with assms show "x = y"
    1.35 +    by (simp add: real_vector.scale_right_imp_eq)
    1.36 +qed
    1.37 +
    1.38 +lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
    1.39 +  apply auto
    1.40 +  apply (rule ccontr)
    1.41 +  apply (simp add: segment_image_interval)
    1.42 +  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
    1.43 +  done
    1.44 +
    1.45 +lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
    1.46 +  by (auto simp: open_segment_def)
    1.47 +
    1.48 +lemmas finite_segment = finite_closed_segment finite_open_segment
    1.49 +
    1.50 +lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
    1.51 +  by auto
    1.52 +
    1.53 +lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
    1.54 +  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
    1.55 +
    1.56 +lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
    1.57 +
    1.58  lemma open_segment_bound1:
    1.59    assumes "x \<in> open_segment a b"
    1.60    shows "norm (x - a) < norm (b - a)"
    1.61 @@ -868,6 +919,172 @@
    1.62  
    1.63  lemmas convex_segment = convex_closed_segment convex_open_segment
    1.64  
    1.65 +lemma subset_closed_segment:
    1.66 +    "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
    1.67 +     a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
    1.68 +  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
    1.69 +
    1.70 +lemma subset_co_segment:
    1.71 +    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
    1.72 +     a \<in> open_segment c d \<and> b \<in> open_segment c d"
    1.73 +using closed_segment_subset by blast
    1.74 +
    1.75 +lemma subset_open_segment:
    1.76 +  fixes a :: "'a::euclidean_space"
    1.77 +  shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
    1.78 +         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
    1.79 +        (is "?lhs = ?rhs")
    1.80 +proof (cases "a = b")
    1.81 +  case True then show ?thesis by simp
    1.82 +next
    1.83 +  case False show ?thesis
    1.84 +  proof
    1.85 +    assume rhs: ?rhs
    1.86 +    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
    1.87 +      using closed_segment_idem singleton_iff by auto
    1.88 +    have "\<exists>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.89 +               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
    1.90 +        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
    1.91 +           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
    1.92 +           and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
    1.93 +        for u ua ub
    1.94 +    proof -
    1.95 +      have "ua \<noteq> ub"
    1.96 +        using neq by auto
    1.97 +      moreover have "(u - 1) * ua \<le> 0" using u uab
    1.98 +        by (simp add: mult_nonpos_nonneg)
    1.99 +      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
   1.100 +        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
   1.101 +      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
   1.102 +      proof -
   1.103 +        have "\<not> p \<le> 0" "\<not> q \<le> 0"
   1.104 +          using p q not_less by blast+
   1.105 +        then show ?thesis
   1.106 +          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
   1.107 +                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
   1.108 +      qed
   1.109 +      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
   1.110 +        by (metis diff_add_cancel diff_gt_0_iff_gt)
   1.111 +      with lt show ?thesis
   1.112 +        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
   1.113 +    qed
   1.114 +    with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
   1.115 +      unfolding open_segment_image_interval closed_segment_def
   1.116 +      by (fastforce simp add:)
   1.117 +  next
   1.118 +    assume lhs: ?lhs
   1.119 +    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
   1.120 +      by (meson finite_open_segment rev_finite_subset)
   1.121 +    have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
   1.122 +      using lhs closure_mono by blast
   1.123 +    then have "closed_segment a b \<subseteq> closed_segment c d"
   1.124 +      by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
   1.125 +    then show ?rhs
   1.126 +      by (force simp: \<open>a \<noteq> b\<close>)
   1.127 +  qed
   1.128 +qed
   1.129 +
   1.130 +lemma subset_oc_segment:
   1.131 +  fixes a :: "'a::euclidean_space"
   1.132 +  shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
   1.133 +         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   1.134 +apply (simp add: subset_open_segment [symmetric])
   1.135 +apply (rule iffI)
   1.136 + apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
   1.137 +apply (meson dual_order.trans segment_open_subset_closed)
   1.138 +done
   1.139 +
   1.140 +lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
   1.141 +
   1.142 +lemma dist_half_times2:
   1.143 +  fixes a :: "'a :: real_normed_vector"
   1.144 +  shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
   1.145 +proof -
   1.146 +  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
   1.147 +    by simp
   1.148 +  also have "... = norm ((a + b) - 2 *\<^sub>R x)"
   1.149 +    by (simp add: real_vector.scale_right_diff_distrib)
   1.150 +  finally show ?thesis
   1.151 +    by (simp only: dist_norm)
   1.152 +qed
   1.153 +
   1.154 +lemma closed_segment_as_ball:
   1.155 +    "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
   1.156 +proof (cases "b = a")
   1.157 +  case True then show ?thesis by (auto simp: hull_inc)
   1.158 +next
   1.159 +  case False
   1.160 +  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
   1.161 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
   1.162 +                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
   1.163 +  proof -
   1.164 +    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
   1.165 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
   1.166 +          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
   1.167 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
   1.168 +      unfolding eq_diff_eq [symmetric] by simp
   1.169 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.170 +                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
   1.171 +      by (simp add: dist_half_times2) (simp add: dist_norm)
   1.172 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.173 +            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
   1.174 +      by auto
   1.175 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.176 +                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
   1.177 +      by (simp add: algebra_simps scaleR_2)
   1.178 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.179 +                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
   1.180 +      by simp
   1.181 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
   1.182 +      by (simp add: mult_le_cancel_right2 False)
   1.183 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
   1.184 +      by auto
   1.185 +    finally show ?thesis .
   1.186 +  qed
   1.187 +  show ?thesis
   1.188 +    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
   1.189 +qed
   1.190 +
   1.191 +lemma open_segment_as_ball:
   1.192 +    "open_segment a b =
   1.193 +     affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
   1.194 +proof (cases "b = a")
   1.195 +  case True then show ?thesis by (auto simp: hull_inc)
   1.196 +next
   1.197 +  case False
   1.198 +  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
   1.199 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
   1.200 +                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
   1.201 +  proof -
   1.202 +    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
   1.203 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
   1.204 +          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
   1.205 +                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
   1.206 +      unfolding eq_diff_eq [symmetric] by simp
   1.207 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.208 +                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
   1.209 +      by (simp add: dist_half_times2) (simp add: dist_norm)
   1.210 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.211 +            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
   1.212 +      by auto
   1.213 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.214 +                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
   1.215 +      by (simp add: algebra_simps scaleR_2)
   1.216 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
   1.217 +                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
   1.218 +      by simp
   1.219 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
   1.220 +      by (simp add: mult_le_cancel_right2 False)
   1.221 +    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
   1.222 +      by auto
   1.223 +    finally show ?thesis .
   1.224 +  qed
   1.225 +  show ?thesis
   1.226 +    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
   1.227 +qed
   1.228 +
   1.229 +lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
   1.230 +
   1.231  lemma connected_segment [iff]:
   1.232    fixes x :: "'a :: real_normed_vector"
   1.233    shows "connected (closed_segment x y)"
     2.1 --- a/src/HOL/Analysis/Starlike.thy	Wed Dec 04 15:36:58 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 18:28:24 2019 +0100
     2.3 @@ -79,226 +79,6 @@
     2.4      by (meson hull_mono inf_mono subset_insertI subset_refl)
     2.5  qed
     2.6  
     2.7 -subsection\<^marker>\<open>tag unimportant\<close>\<open>More results about segments\<close>
     2.8 -
     2.9 -lemma dist_half_times2:
    2.10 -  fixes a :: "'a :: real_normed_vector"
    2.11 -  shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
    2.12 -proof -
    2.13 -  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
    2.14 -    by simp
    2.15 -  also have "... = norm ((a + b) - 2 *\<^sub>R x)"
    2.16 -    by (simp add: real_vector.scale_right_diff_distrib)
    2.17 -  finally show ?thesis
    2.18 -    by (simp only: dist_norm)
    2.19 -qed
    2.20 -
    2.21 -lemma closed_segment_as_ball:
    2.22 -    "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
    2.23 -proof (cases "b = a")
    2.24 -  case True then show ?thesis by (auto simp: hull_inc)
    2.25 -next
    2.26 -  case False
    2.27 -  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    2.28 -                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
    2.29 -                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
    2.30 -  proof -
    2.31 -    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    2.32 -                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
    2.33 -          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
    2.34 -                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
    2.35 -      unfolding eq_diff_eq [symmetric] by simp
    2.36 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.37 -                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
    2.38 -      by (simp add: dist_half_times2) (simp add: dist_norm)
    2.39 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.40 -            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
    2.41 -      by auto
    2.42 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.43 -                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
    2.44 -      by (simp add: algebra_simps scaleR_2)
    2.45 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.46 -                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
    2.47 -      by simp
    2.48 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
    2.49 -      by (simp add: mult_le_cancel_right2 False)
    2.50 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
    2.51 -      by auto
    2.52 -    finally show ?thesis .
    2.53 -  qed
    2.54 -  show ?thesis
    2.55 -    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
    2.56 -qed
    2.57 -
    2.58 -lemma open_segment_as_ball:
    2.59 -    "open_segment a b =
    2.60 -     affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
    2.61 -proof (cases "b = a")
    2.62 -  case True then show ?thesis by (auto simp: hull_inc)
    2.63 -next
    2.64 -  case False
    2.65 -  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    2.66 -                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
    2.67 -                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
    2.68 -  proof -
    2.69 -    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
    2.70 -                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
    2.71 -          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
    2.72 -                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
    2.73 -      unfolding eq_diff_eq [symmetric] by simp
    2.74 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.75 -                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
    2.76 -      by (simp add: dist_half_times2) (simp add: dist_norm)
    2.77 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.78 -            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
    2.79 -      by auto
    2.80 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.81 -                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
    2.82 -      by (simp add: algebra_simps scaleR_2)
    2.83 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
    2.84 -                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
    2.85 -      by simp
    2.86 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
    2.87 -      by (simp add: mult_le_cancel_right2 False)
    2.88 -    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
    2.89 -      by auto
    2.90 -    finally show ?thesis .
    2.91 -  qed
    2.92 -  show ?thesis
    2.93 -    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
    2.94 -qed
    2.95 -
    2.96 -lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
    2.97 -
    2.98 -lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
    2.99 -  by auto
   2.100 -
   2.101 -lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
   2.102 -proof -
   2.103 -  { assume a1: "open_segment a b = {}"
   2.104 -    have "{} \<noteq> {0::real<..<1}"
   2.105 -      by simp
   2.106 -    then have "a = b"
   2.107 -      using a1 open_segment_image_interval by fastforce
   2.108 -  } then show ?thesis by auto
   2.109 -qed
   2.110 -
   2.111 -lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
   2.112 -  using open_segment_eq_empty by blast
   2.113 -
   2.114 -lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
   2.115 -
   2.116 -lemma inj_segment:
   2.117 -  fixes a :: "'a :: real_vector"
   2.118 -  assumes "a \<noteq> b"
   2.119 -    shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
   2.120 -proof
   2.121 -  fix x y
   2.122 -  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
   2.123 -  then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
   2.124 -    by (simp add: algebra_simps)
   2.125 -  with assms show "x = y"
   2.126 -    by (simp add: real_vector.scale_right_imp_eq)
   2.127 -qed
   2.128 -
   2.129 -lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
   2.130 -  apply auto
   2.131 -  apply (rule ccontr)
   2.132 -  apply (simp add: segment_image_interval)
   2.133 -  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
   2.134 -  done
   2.135 -
   2.136 -lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
   2.137 -  by (auto simp: open_segment_def)
   2.138 -
   2.139 -lemmas finite_segment = finite_closed_segment finite_open_segment
   2.140 -
   2.141 -lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
   2.142 -  by auto
   2.143 -
   2.144 -lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
   2.145 -  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
   2.146 -
   2.147 -lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
   2.148 -
   2.149 -lemma subset_closed_segment:
   2.150 -    "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
   2.151 -     a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   2.152 -  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
   2.153 -
   2.154 -lemma subset_co_segment:
   2.155 -    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
   2.156 -     a \<in> open_segment c d \<and> b \<in> open_segment c d"
   2.157 -using closed_segment_subset by blast
   2.158 -
   2.159 -lemma subset_open_segment:
   2.160 -  fixes a :: "'a::euclidean_space"
   2.161 -  shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
   2.162 -         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   2.163 -        (is "?lhs = ?rhs")
   2.164 -proof (cases "a = b")
   2.165 -  case True then show ?thesis by simp
   2.166 -next
   2.167 -  case False show ?thesis
   2.168 -  proof
   2.169 -    assume rhs: ?rhs
   2.170 -    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
   2.171 -      using closed_segment_idem singleton_iff by auto
   2.172 -    have "\<exists>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) =
   2.173 -               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
   2.174 -        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
   2.175 -           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
   2.176 -           and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
   2.177 -        for u ua ub
   2.178 -    proof -
   2.179 -      have "ua \<noteq> ub"
   2.180 -        using neq by auto
   2.181 -      moreover have "(u - 1) * ua \<le> 0" using u uab
   2.182 -        by (simp add: mult_nonpos_nonneg)
   2.183 -      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
   2.184 -        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
   2.185 -      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
   2.186 -      proof -
   2.187 -        have "\<not> p \<le> 0" "\<not> q \<le> 0"
   2.188 -          using p q not_less by blast+
   2.189 -        then show ?thesis
   2.190 -          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
   2.191 -                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
   2.192 -      qed
   2.193 -      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
   2.194 -        by (metis diff_add_cancel diff_gt_0_iff_gt)
   2.195 -      with lt show ?thesis
   2.196 -        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
   2.197 -    qed
   2.198 -    with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
   2.199 -      unfolding open_segment_image_interval closed_segment_def
   2.200 -      by (fastforce simp add:)
   2.201 -  next
   2.202 -    assume lhs: ?lhs
   2.203 -    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
   2.204 -      by (meson finite_open_segment rev_finite_subset)
   2.205 -    have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
   2.206 -      using lhs closure_mono by blast
   2.207 -    then have "closed_segment a b \<subseteq> closed_segment c d"
   2.208 -      by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
   2.209 -    then show ?rhs
   2.210 -      by (force simp: \<open>a \<noteq> b\<close>)
   2.211 -  qed
   2.212 -qed
   2.213 -
   2.214 -lemma subset_oc_segment:
   2.215 -  fixes a :: "'a::euclidean_space"
   2.216 -  shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
   2.217 -         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
   2.218 -apply (simp add: subset_open_segment [symmetric])
   2.219 -apply (rule iffI)
   2.220 - apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
   2.221 -apply (meson dual_order.trans segment_open_subset_closed)
   2.222 -done
   2.223 -
   2.224 -lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
   2.225 -
   2.226 -
   2.227  subsection\<^marker>\<open>tag unimportant\<close> \<open>Shrinking towards the interior of a convex set\<close>
   2.228  
   2.229  lemma mem_interior_convex_shrink: