src/HOL/Inequalities.thy
changeset 61609 77b453bd616f
parent 60758 d8d85a8172b5
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Inequalities.thy	Tue Nov 03 11:20:21 2015 +0100
     1.2 +++ b/src/HOL/Inequalities.thy	Tue Nov 10 14:18:41 2015 +0000
     1.3 @@ -31,9 +31,10 @@
     1.4    have "m*(m-1) \<le> n*(n + 1)"
     1.5     using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
     1.6    hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
     1.7 -    by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult
     1.8 -      split: zdiff_int_split)
     1.9 -  thus ?thesis by simp
    1.10 +    by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum
    1.11 +          split: zdiff_int_split)
    1.12 +  thus ?thesis
    1.13 +    by blast 
    1.14  qed
    1.15  
    1.16  lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
    1.17 @@ -75,7 +76,6 @@
    1.18           (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
    1.19      n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
    1.20  using Chebyshev_sum_upper[where 'a=real, of n a b]
    1.21 -by (simp del: real_of_nat_mult real_of_nat_setsum
    1.22 -  add: real_of_nat_mult[symmetric] real_of_nat_setsum[symmetric] real_of_nat_def[symmetric])
    1.23 +by (simp del: of_nat_mult of_nat_setsum  add: of_nat_mult[symmetric] of_nat_setsum[symmetric])
    1.24  
    1.25  end