src/HOL/Library/Convex.thy
changeset 56571 f4635657d66f
parent 56544 b60d5d119489
child 56796 9f84219715a7
     1.1 --- a/src/HOL/Library/Convex.thy	Mon Apr 14 10:55:56 2014 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Mon Apr 14 13:08:17 2014 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4      with `0 \<le> setsum a s` have "0 < setsum a s" by simp
     1.5      then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
     1.6        using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
     1.7 -      by (simp add: IH divide_nonneg_pos setsum_divide_distrib [symmetric])
     1.8 +      by (simp add: IH setsum_divide_distrib [symmetric])
     1.9      from `convex C` and `y i \<in> C` and this and `0 \<le> a i`
    1.10        and `0 \<le> setsum a s` and `a i + setsum a s = 1`
    1.11      have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
    1.12 @@ -432,9 +432,7 @@
    1.13      then have "a i < 1" using asm by auto
    1.14      then have i0: "1 - a i > 0" by auto
    1.15      let ?a = "\<lambda>j. a j / (1 - a i)"
    1.16 -    { fix j assume "j \<in> s"
    1.17 -      then have "?a j \<ge> 0"
    1.18 -        using i0 asms divide_nonneg_pos
    1.19 +    { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
    1.20          by fastforce }
    1.21      note a_nonneg = this
    1.22      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto