no longer declare .psimps rules as [simp].
This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.
(* Title: HOL/ex/NatSum.thy
Author: Tobias Nipkow
*)
header {* Summing natural numbers *}
theory NatSum imports Main Parity begin
text {*
Summing natural numbers, squares, cubes, etc.
Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
\url{http://www.research.att.com/~njas/sequences/}.
*}
lemmas [simp] =
ring_distribs
diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
text {*
\medskip The sum of the first @{text n} odd numbers equals @{text n}
squared.
*}
lemma sum_of_odds: "(\<Sum>i=0..<n. Suc (i + i)) = n * n"
by (induct n) auto
text {*
\medskip The sum of the first @{text n} odd squares.
*}
lemma sum_of_odd_squares:
"3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
by (induct n) auto
text {*
\medskip The sum of the first @{text n} odd cubes
*}
lemma sum_of_odd_cubes:
"(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
n * n * (2 * n * n - 1)"
by (induct n) auto
text {*
\medskip The sum of the first @{text n} positive integers equals
@{text "n (n + 1) / 2"}.*}
lemma sum_of_naturals:
"2 * (\<Sum>i=0..n. i) = n * Suc n"
by (induct n) auto
lemma sum_of_squares:
"6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
by (induct n) auto
lemma sum_of_cubes:
"4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
by (induct n) auto
text{* \medskip A cute identity: *}
lemma sum_squared: "(\<Sum>i=0..n. i)^2 = (\<Sum>i=0..n::nat. i^3)"
proof(induct n)
case 0 show ?case by simp
next
case (Suc n)
have "(\<Sum>i = 0..Suc n. i)^2 =
(\<Sum>i = 0..n. i^3) + (2*(\<Sum>i = 0..n. i)*(n+1) + (n+1)^2)"
(is "_ = ?A + ?B")
using Suc by(simp add:nat_number)
also have "?B = (n+1)^3"
using sum_of_naturals by(simp add:nat_number)
also have "?A + (n+1)^3 = (\<Sum>i=0..Suc n. i^3)" by simp
finally show ?case .
qed
text {*
\medskip Sum of fourth powers: three versions.
*}
lemma sum_of_fourth_powers:
"30 * (\<Sum>i=0..n. i * i * i * i) =
n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
apply (induct n)
apply simp_all
apply (case_tac n) -- {* eliminates the subtraction *}
apply (simp_all (no_asm_simp))
done
text {*
Two alternative proofs, with a change of variables and much more
subtraction, performed using the integers. *}
lemma int_sum_of_fourth_powers:
"30 * int (\<Sum>i=0..<m. i * i * i * i) =
int m * (int m - 1) * (int(2 * m) - 1) *
(int(3 * m * m) - int(3 * m) - 1)"
by (induct m) (simp_all add: int_mult)
lemma of_nat_sum_of_fourth_powers:
"30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
(of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
by (induct m) (simp_all add: of_nat_mult)
text {*
\medskip Sums of geometric series: @{text 2}, @{text 3} and the
general case.
*}
lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
by (induct n) (auto split: nat_diff_split)
lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
by (induct n) auto
lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
by (induct n) auto
end