simplified statement and proof
authornipkow
Fri May 01 20:25:57 2015 +0200 (2015-05-01)
changeset 601679a97407488cd
parent 60165 29c826137153
child 60168 0305c511a821
simplified statement and proof
src/HOL/Inequalities.thy
     1.1 --- a/src/HOL/Inequalities.thy	Fri May 01 11:36:16 2015 +0100
     1.2 +++ b/src/HOL/Inequalities.thy	Fri May 01 20:25:57 2015 +0200
     1.3 @@ -7,30 +7,22 @@
     1.4    imports Real_Vector_Spaces
     1.5  begin
     1.6  
     1.7 -lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
     1.8 -  setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
     1.9 -using gauss_sum[where n=n and 'a = 'a,symmetric] by auto
    1.10 -
    1.11 -lemma Setsum_Icc_int: assumes "0 \<le> m" and "(m::int) \<le> n"
    1.12 -shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    1.13 -proof-
    1.14 -  { fix k::int assume "k\<ge>0"
    1.15 -    hence "\<Sum> {1..k::int} = k * (k+1) div 2"
    1.16 -      by (rule gauss_sum_div2[where 'a = int, transferred]) simp
    1.17 -  } note 1 = this
    1.18 -  have "{m..n} = {0..n} - {0..m-1}" using `m\<ge>0` by auto
    1.19 -  hence "\<Sum>{m..n} = \<Sum>{0..n} - \<Sum>{0..m-1}" using assms
    1.20 -    by (force intro!: setsum_diff)
    1.21 -  also have "{0..n} = {0} Un {1..n}" using assms by auto
    1.22 -  also have "\<Sum>({0} \<union> {1..n}) = \<Sum>{1..n}" by(simp add: setsum.union_disjoint)
    1.23 -  also have "\<dots> = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]])
    1.24 -  also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})"
    1.25 -    using assms by auto
    1.26 -  also have "\<Sum> \<dots> = m*(m-1) div 2" using `m\<ge>0` by(simp add: 1 mult.commute)
    1.27 -  also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2"
    1.28 -    apply(subgoal_tac "even(n*(n+1)) \<and> even(m*(m-1))")
    1.29 -    by (auto (*simp: even_def[symmetric]*))
    1.30 -  finally show ?thesis .
    1.31 +lemma Setsum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    1.32 +proof(induct i == "nat(n-m)" arbitrary: m n)
    1.33 +  case 0
    1.34 +  hence "m = n" by arith
    1.35 +  thus ?case by (simp add: algebra_simps)
    1.36 +next
    1.37 +  case (Suc i)
    1.38 +  have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
    1.39 +  have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
    1.40 +  also have "\<dots> = \<Sum> {m..n-1} + n" using `m \<le> n`
    1.41 +    by(subst atLeastAtMostPlus1_int_conv) simp_all
    1.42 +  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
    1.43 +    by(simp add: Suc(1)[OF 0])
    1.44 +  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
    1.45 +  also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps)
    1.46 +  finally show ?case .
    1.47  qed
    1.48  
    1.49  lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n"
    1.50 @@ -39,7 +31,7 @@
    1.51    have "m*(m-1) \<le> n*(n + 1)"
    1.52     using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
    1.53    hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
    1.54 -    by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult
    1.55 +    by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult
    1.56        split: zdiff_int_split)
    1.57    thus ?thesis by simp
    1.58  qed