src/HOL/Library/Convex.thy
changeset 44282 f0de18b62d63
parent 44142 8e27e0177518
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Library/Convex.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -129,7 +129,7 @@
     1.4      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     1.5      hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
     1.6      hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
     1.7 -    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
     1.8 +    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
     1.9      from this asms
    1.10      have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
    1.11      hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
    1.12 @@ -410,7 +410,7 @@
    1.13      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
    1.14      hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
    1.15      hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
    1.16 -    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp
    1.17 +    hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
    1.18      have "convex C" using asms by auto
    1.19      hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
    1.20        using asms convex_setsum[OF `finite s`
    1.21 @@ -433,7 +433,7 @@
    1.22        using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
    1.23          OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
    1.24      also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
    1.25 -      unfolding mult_right.setsum[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
    1.26 +      unfolding setsum_right_distrib[of "1 - a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto
    1.27      also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto
    1.28      also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto
    1.29      finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))"