src/HOL/Library/Convex.thy
changeset 57512 cc97b347b301
parent 57418 6ab1c7cb0b8d
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Convex.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4      have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
     1.5        by auto
     1.6      then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s"
     1.7 -      using s by (auto simp:add_commute)
     1.8 +      using s by (auto simp:add.commute)
     1.9    }
    1.10    then show "convex s"
    1.11      unfolding convex_alt by auto
    1.12 @@ -525,7 +525,7 @@
    1.13        using a_nonneg a1 asms by blast
    1.14      have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) = f ((\<Sum> j \<in> s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
    1.15        using setsum.insert[of s i "\<lambda> j. a j *\<^sub>R y j", OF `finite s` `i \<notin> s`] asms
    1.16 -      by (auto simp only:add_commute)
    1.17 +      by (auto simp only:add.commute)
    1.18      also have "\<dots> = f (((1 - a i) * inverse (1 - a i)) *\<^sub>R (\<Sum> j \<in> s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
    1.19        using i0 by auto
    1.20      also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)"
    1.21 @@ -535,7 +535,7 @@
    1.22        by (auto simp: divide_inverse)
    1.23      also have "\<dots> \<le> (1 - a i) *\<^sub>R f ((\<Sum> j \<in> s. ?a j *\<^sub>R y j)) + a i * f (y i)"
    1.24        using conv[of "y i" "(\<Sum> j \<in> s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1]
    1.25 -      by (auto simp add:add_commute)
    1.26 +      by (auto simp add:add.commute)
    1.27      also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)"
    1.28        using add_right_mono[OF mult_left_mono[of _ _ "1 - a i",
    1.29          OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp
    1.30 @@ -768,7 +768,7 @@
    1.31      by auto
    1.32    then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
    1.33      DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
    1.34 -    unfolding inverse_eq_divide by (auto simp add: mult_assoc)
    1.35 +    unfolding inverse_eq_divide by (auto simp add: mult.assoc)
    1.36    have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
    1.37      using `b > 1` by (auto intro!:less_imp_le)
    1.38    from f''_ge0_imp_convex[OF pos_is_convex,