src/ZF/ex/NatSum.thy
 author wenzelm Fri Feb 18 16:22:27 2011 +0100 (2011-02-18) changeset 41777 1f7cbe39d425 parent 35762 af3ff2ba4c54 child 65449 c82e63b11b8b permissions -rw-r--r--
1 (*  Title:      ZF/ex/NatSum.thy
2     Author:     Tobias Nipkow & Lawrence C Paulson
4 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
6 Note: n is a natural number but the sum is an integer,
7                             and f maps integers to integers
9 Summing natural numbers, squares, cubes, etc.
11 Originally demonstrated permutative rewriting, but add_ac is no longer needed
12   thanks to new simprocs.
14 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
15   http://www.research.att.com/~njas/sequences/
16 *)
19 theory NatSum imports Main begin
21 consts sum :: "[i=>i, i] => i"
22 primrec
23   "sum (f,0) = #0"
24   "sum (f, succ(n)) = f(\$#n) \$+ sum(f,n)"
27 declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp]
29 (*The sum of the first n odd numbers equals n squared.*)
30 lemma sum_of_odds: "n \<in> nat ==> sum (%i. i \$+ i \$+ #1, n) = \$#n \$* \$#n"
31 by (induct_tac "n", auto)
33 (*The sum of the first n odd squares*)
34 lemma sum_of_odd_squares:
35      "n \<in> nat ==> #3 \$* sum (%i. (i \$+ i \$+ #1) \$* (i \$+ i \$+ #1), n) =
36       \$#n \$* (#4 \$* \$#n \$* \$#n \$- #1)"
37 by (induct_tac "n", auto)
39 (*The sum of the first n odd cubes*)
40 lemma sum_of_odd_cubes:
41      "n \<in> nat
42       ==> sum (%i. (i \$+ i \$+ #1) \$* (i \$+ i \$+ #1) \$* (i \$+ i \$+ #1), n) =
43           \$#n \$* \$#n \$* (#2 \$* \$#n \$* \$#n \$- #1)"
44 by (induct_tac "n", auto)
46 (*The sum of the first n positive integers equals n(n+1)/2.*)
47 lemma sum_of_naturals:
48      "n \<in> nat ==> #2 \$* sum(%i. i, succ(n)) = \$#n \$* \$#succ(n)"
49 by (induct_tac "n", auto)
51 lemma sum_of_squares:
52      "n \<in> nat ==> #6 \$* sum (%i. i\$*i, succ(n)) =
53                   \$#n \$* (\$#n \$+ #1) \$* (#2 \$* \$#n \$+ #1)"
54 by (induct_tac "n", auto)
56 lemma sum_of_cubes:
57      "n \<in> nat ==> #4 \$* sum (%i. i\$*i\$*i, succ(n)) =
58                   \$#n \$* \$#n \$* (\$#n \$+ #1) \$* (\$#n \$+ #1)"
59 by (induct_tac "n", auto)
61 (** Sum of fourth powers **)
63 lemma sum_of_fourth_powers:
64      "n \<in> nat ==> #30 \$* sum (%i. i\$*i\$*i\$*i, succ(n)) =
65                     \$#n \$* (\$#n \$+ #1) \$* (#2 \$* \$#n \$+ #1) \$*
66                     (#3 \$* \$#n \$* \$#n \$+ #3 \$* \$#n \$- #1)"
67 by (induct_tac "n", auto)
69 end