|
1 (* Title: HOL/ex/NatSum.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Lawrence C Paulson |
|
4 |
|
5 Summing natural numbers, squares, cubes, etc. |
|
6 |
|
7 Originally demonstrated permutative rewriting, but add_ac is no longer needed |
|
8 thanks to new simprocs. |
|
9 |
|
10 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
|
11 http://www.research.att.com/~njas/sequences/ |
|
12 *) |
|
13 |
|
14 Addsimps [zadd_zmult_distrib, zadd_zmult_distrib2]; |
|
15 Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2]; |
|
16 |
|
17 (*The sum of the first n odd numbers equals n squared.*) |
|
18 Goal "n: nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n"; |
|
19 by (induct_tac "n" 1); |
|
20 by Auto_tac; |
|
21 qed "sum_of_odds"; |
|
22 |
|
23 (*The sum of the first n odd squares*) |
|
24 Goal "n: nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \ |
|
25 \ $#n $* (#4 $* $#n $* $#n $- #1)"; |
|
26 by (induct_tac "n" 1); |
|
27 by Auto_tac; |
|
28 qed "sum_of_odd_squares"; |
|
29 |
|
30 (*The sum of the first n odd cubes*) |
|
31 Goal "n: nat \ |
|
32 \ ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \ |
|
33 \ $#n $* $#n $* (#2 $* $#n $* $#n $- #1)"; |
|
34 by (induct_tac "n" 1); |
|
35 by Auto_tac; |
|
36 qed "sum_of_odd_cubes"; |
|
37 |
|
38 (*The sum of the first n positive integers equals n(n+1)/2.*) |
|
39 Goal "n: nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)"; |
|
40 by (induct_tac "n" 1); |
|
41 by Auto_tac; |
|
42 qed "sum_of_naturals"; |
|
43 |
|
44 Goal "n: nat ==> #6 $* sum (%i. i$*i, succ(n)) = \ |
|
45 \ $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)"; |
|
46 by (induct_tac "n" 1); |
|
47 by Auto_tac; |
|
48 qed "sum_of_squares"; |
|
49 |
|
50 Goal "n: nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \ |
|
51 \ $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)"; |
|
52 by (induct_tac "n" 1); |
|
53 by Auto_tac; |
|
54 qed "sum_of_cubes"; |
|
55 |
|
56 (** Sum of fourth powers **) |
|
57 |
|
58 Goal "n: nat ==> \ |
|
59 \ #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \ |
|
60 \ $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \ |
|
61 \ (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)"; |
|
62 by (induct_tac "n" 1); |
|
63 by Auto_tac; |
|
64 qed "sum_of_fourth_powers"; |