src/HOL/Library/Convex.thy
changeset 36778 739a9379e29b
parent 36648 43b66dcd9266
child 38642 8fa437809c67
     1.1 --- a/src/HOL/Library/Convex.thy	Sun May 09 17:47:43 2010 -0700
     1.2 +++ b/src/HOL/Library/Convex.thy	Sun May 09 22:51:11 2010 -0700
     1.3 @@ -362,8 +362,7 @@
     1.4    { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
     1.5      hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
     1.6      hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
     1.7 -      using add_nonneg_pos[of "\<mu> *\<^sub>R x" "(1 - \<mu>) *\<^sub>R y"]
     1.8 -        real_mult_order by auto fastsimp }
     1.9 +      by (auto simp add: add_pos_pos mult_pos_pos) }
    1.10    ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
    1.11  qed
    1.12  
    1.13 @@ -426,7 +425,7 @@
    1.14      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.15        using scaleR_right.setsum[of "inverse (1 - a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps)
    1.16      also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)"
    1.17 -      by (auto simp:real_divide_def)
    1.18 +      by (auto simp: divide_inverse)
    1.19      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.20        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.21        by (auto simp add:add_commute)
    1.22 @@ -555,7 +554,7 @@
    1.23      from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
    1.24      from mult_right_mono_neg[OF this le(2)]
    1.25      have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
    1.26 -      unfolding diff_def using real_add_mult_distrib by auto
    1.27 +      by (simp add: algebra_simps)
    1.28      hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
    1.29      hence res: "f' y * (x - y) \<le> f x - f y" by auto
    1.30      have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
    1.31 @@ -570,7 +569,7 @@
    1.32      from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
    1.33      from mult_right_mono[OF this ge(2)]
    1.34      have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
    1.35 -      unfolding diff_def using real_add_mult_distrib by auto
    1.36 +      by (simp add: algebra_simps)
    1.37      hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
    1.38      hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
    1.39        using res by auto } note less_imp = this
    1.40 @@ -606,9 +605,9 @@
    1.41    have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
    1.42      by auto
    1.43    hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
    1.44 -    unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
    1.45 +    unfolding inverse_eq_divide by (auto simp add: mult_assoc)
    1.46    have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
    1.47 -    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
    1.48 +    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] mult_pos_pos)
    1.49    from f''_ge0_imp_convex[OF pos_is_convex,
    1.50      unfolded greaterThan_iff, OF f' f''0 f''_ge0]
    1.51    show ?thesis by auto