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