src/HOL/Inequalities.thy
changeset 66936 cf8d8fc23891
parent 66804 3f9bb52082c4
     1.1 --- a/src/HOL/Inequalities.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Inequalities.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -7,49 +7,6 @@
     1.4    imports Real_Vector_Spaces
     1.5  begin
     1.6  
     1.7 -lemma Sum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
     1.8 -proof(induct i == "nat(n-m)" arbitrary: m n)
     1.9 -  case 0
    1.10 -  hence "m = n" by arith
    1.11 -  thus ?case by (simp add: algebra_simps)
    1.12 -next
    1.13 -  case (Suc i)
    1.14 -  have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
    1.15 -  have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
    1.16 -  also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
    1.17 -    by(subst atLeastAtMostPlus1_int_conv) simp_all
    1.18 -  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
    1.19 -    by(simp add: Suc(1)[OF 0])
    1.20 -  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
    1.21 -  also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps)
    1.22 -  finally show ?case .
    1.23 -qed
    1.24 -
    1.25 -lemma Sum_Icc_nat: assumes "(m::nat) \<le> n"
    1.26 -shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    1.27 -proof -
    1.28 -  have "m*(m-1) \<le> n*(n + 1)"
    1.29 -   using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
    1.30 -  hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
    1.31 -    by (auto simp: Sum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_sum
    1.32 -          split: zdiff_int_split)
    1.33 -  thus ?thesis
    1.34 -    using of_nat_eq_iff by blast
    1.35 -qed
    1.36 -
    1.37 -lemma Sum_Ico_nat: assumes "(m::nat) \<le> n"
    1.38 -shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
    1.39 -proof cases
    1.40 -  assume "m < n"
    1.41 -  hence "{m..<n} = {m..n-1}" by auto
    1.42 -  hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
    1.43 -  also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
    1.44 -    using assms \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute)
    1.45 -  finally show ?thesis .
    1.46 -next
    1.47 -  assume "\<not> m < n" with assms show ?thesis by simp
    1.48 -qed
    1.49 -
    1.50  lemma Chebyshev_sum_upper:
    1.51    fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
    1.52    assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"