src/HOL/Analysis/Polytope.thy
changeset 63918 6bf55e6e0b75
parent 63807 5f77017055a3
child 63967 2aa42596edc3
     1.1 --- a/src/HOL/Analysis/Polytope.thy	Mon Sep 19 12:53:30 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Polytope.thy	Mon Sep 19 20:06:21 2016 +0200
     1.3 @@ -303,7 +303,7 @@
     1.4      have cge0: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> c i"
     1.5        using a b u01 by (simp add: c_def)
     1.6      have sumc1: "setsum c S = 1"
     1.7 -      by (simp add: c_def setsum.distrib setsum_right_distrib [symmetric] asum bsum)
     1.8 +      by (simp add: c_def setsum.distrib setsum_distrib_left [symmetric] asum bsum)
     1.9      have sumci_xy: "(\<Sum>i\<in>S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y"
    1.10        apply (simp add: c_def setsum.distrib scaleR_left_distrib)
    1.11        by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.setsum [symmetric] aeqx beqy)
    1.12 @@ -357,7 +357,7 @@
    1.13            apply (rule_tac x="\<lambda>i. inverse (1-k) * c i" in exI)
    1.14            apply auto
    1.15            apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) setsum_nonneg subsetCE)
    1.16 -          apply (metis False mult.commute right_inverse right_minus_eq setsum_right_distrib sumcf)
    1.17 +          apply (metis False mult.commute right_inverse right_minus_eq setsum_distrib_left sumcf)
    1.18            by (metis (mono_tags, lifting) scaleR_right.setsum scaleR_scaleR setsum.cong)
    1.19          with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
    1.20            by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
    1.21 @@ -365,7 +365,7 @@
    1.22            apply (simp add: weq_sumsum convex_hull_finite fin)
    1.23            apply (rule_tac x="\<lambda>i. inverse k * c i" in exI)
    1.24            using \<open>k > 0\<close> cge0
    1.25 -          apply (auto simp: scaleR_right.setsum setsum_right_distrib [symmetric] k_def [symmetric])
    1.26 +          apply (auto simp: scaleR_right.setsum setsum_distrib_left [symmetric] k_def [symmetric])
    1.27            done
    1.28          ultimately show ?thesis
    1.29            using disj by blast