src/HOL/SetInterval.thy
 changeset 19469 958d2f2dd8d4 parent 19376 529b735edbf2 child 19538 ae6d01fa2d8a
```     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.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.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.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.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"
```