1.1 --- a/src/HOL/SetInterval.thy	Tue Apr 25 22:23:58 2006 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Apr 26 07:01:33 2006 +0200
     1.3 @@ -762,6 +762,67 @@
     1.4    done
     1.5  
     1.6  
     1.7 +subsection {* The formula for arithmetic sums *}
     1.8 +
     1.9 +lemma gauss_sum:
    1.10 +  "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
    1.11 +   of_nat n*((of_nat n)+1)"
    1.12 +proof (induct n)
    1.13 +  case 0
    1.14 +  show ?case by simp
    1.15 +next
    1.16 +  case (Suc n)
    1.17 +  then show ?case by (simp add: right_distrib add_assoc mult_ac)
    1.18 +qed
    1.19 +
    1.20 +theorem arith_series_general:
    1.21 +  "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.22 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
    1.23 +proof cases
    1.24 +  assume ngt1: "n > 1"
    1.25 +  let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
    1.26 +  have
    1.27 +    "(\<Sum>i\<in>{..<n}. a+?I i*d) =
    1.28 +     ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
    1.29 +    by (rule setsum_addf)
    1.30 +  also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
    1.31 +  also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
    1.32 +    by (simp add: setsum_right_distrib setsum_head_upt mult_ac)
    1.33 +  also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
    1.34 +    by (simp add: left_distrib right_distrib)
    1.35 +  also from ngt1 have "{1..<n} = {1..n - 1}"
    1.36 +    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)    
    1.37 +  also from ngt1 
    1.38 +  have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
    1.39 +    by (simp only: mult_ac gauss_sum [of "n - 1"])
    1.40 +       (simp add:  mult_ac of_nat_Suc [symmetric])
    1.41 +  finally show ?thesis by (simp add: mult_ac add_ac right_distrib)
    1.42 +next
    1.43 +  assume "\<not>(n > 1)"
    1.44 +  hence "n = 1 \<or> n = 0" by auto
    1.45 +  thus ?thesis by (auto simp: mult_ac right_distrib)
    1.46 +qed
    1.47 +
    1.48 +lemma arith_series_nat:
    1.49 +  "Suc (Suc 0) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
    1.50 +proof -
    1.51 +  have
    1.52 +    "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
    1.53 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    1.54 +    by (rule arith_series_general)
    1.55 +  thus ?thesis by (auto simp add: of_nat_id)
    1.56 +qed
    1.57 +
    1.58 +lemma arith_series_int:
    1.59 +  "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.60 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
    1.61 +proof -
    1.62 +  have
    1.63 +    "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.64 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    1.65 +    by (rule arith_series_general)
    1.66 +  thus ?thesis by simp
    1.67 +qed
    1.68  
    1.69  lemma sum_diff_distrib:
    1.70    fixes P::"nat\<Rightarrow>nat"