src/HOL/Library/Convex.thy
 changeset 53676 476ef9b468d2 parent 53620 3c7f5e7926dc child 54230 b1d955791529
```     1.1 --- a/src/HOL/Library/Convex.thy	Tue Sep 17 00:39:51 2013 +0200
1.2 +++ b/src/HOL/Library/Convex.thy	Fri Sep 13 14:57:20 2013 -0700
1.3 @@ -14,6 +14,16 @@
1.4  definition convex :: "'a::real_vector set \<Rightarrow> bool"
1.5    where "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
1.6
1.7 +lemma convexI:
1.8 +  assumes "\<And>x y u v. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 \<le> u \<Longrightarrow> 0 \<le> v \<Longrightarrow> u + v = 1 \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
1.9 +  shows "convex s"
1.10 +  using assms unfolding convex_def by fast
1.11 +
1.12 +lemma convexD:
1.13 +  assumes "convex s" and "x \<in> s" and "y \<in> s" and "0 \<le> u" and "0 \<le> v" and "u + v = 1"
1.14 +  shows "u *\<^sub>R x + v *\<^sub>R y \<in> s"
1.15 +  using assms unfolding convex_def by fast
1.16 +
1.17  lemma convex_alt:
1.18    "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *\<^sub>R x + u *\<^sub>R y) \<in> s)"
1.19    (is "_ \<longleftrightarrow> ?alt")
1.20 @@ -140,7 +150,7 @@
1.21      then have a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
1.22      with asms have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastforce
1.23      then have "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
1.24 -      using asms[unfolded convex_def, rule_format] yai ai1 by auto
1.25 +      using asms yai ai1 by (auto intro: convexD)
1.26      then have "a i *\<^sub>R y i + (\<Sum> j \<in> s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \<in> C"
1.27        using scaleR_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j *\<^sub>R y j" s] by auto
1.28      then have "a i *\<^sub>R y i + (\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C" using i0 by auto
```