src/HOL/Library/Convex.thy
changeset 44142 8e27e0177518
parent 43337 57a1c19f8e3b
child 44282 f0de18b62d63
     1.1 --- a/src/HOL/Library/Convex.thy	Wed Aug 10 17:02:03 2011 -0700
     1.2 +++ b/src/HOL/Library/Convex.thy	Wed Aug 10 18:02:16 2011 -0700
     1.3 @@ -49,7 +49,7 @@
     1.4  
     1.5  lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
     1.6    unfolding convex_def
     1.7 -  by (auto simp: inner_add inner_scaleR intro!: convex_bound_le)
     1.8 +  by (auto simp: inner_add intro!: convex_bound_le)
     1.9  
    1.10  lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
    1.11  proof -
    1.12 @@ -209,7 +209,7 @@
    1.13    shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1
    1.14                        \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
    1.15    unfolding convex_explicit
    1.16 -proof (safe elim!: conjE)
    1.17 +proof (safe)
    1.18    fix t u assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
    1.19      and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
    1.20    have *:"s \<inter> t = t" using as(2) by auto
    1.21 @@ -480,9 +480,9 @@
    1.22    also have "\<dots> = a * (f x - f y) + f y" by (simp add: field_simps)
    1.23    finally have "f t - f y \<le> a * (f x - f y)" by simp
    1.24    with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
    1.25 -    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps a_def)
    1.26 +    by (simp add: le_divide_eq divide_le_eq field_simps a_def)
    1.27    with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
    1.28 -    by (simp add: times_divide_eq le_divide_eq divide_le_eq field_simps)
    1.29 +    by (simp add: le_divide_eq divide_le_eq field_simps)
    1.30  qed
    1.31  
    1.32  lemma pos_convex_function: