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
```
```     3
```
```     4 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
```
```     5
```
```     6 Note: n is a natural number but the sum is an integer,
```
```     7                             and f maps integers to integers
```
```     8
```
```     9 Summing natural numbers, squares, cubes, etc.
```
```    10
```
```    11 Originally demonstrated permutative rewriting, but add_ac is no longer needed
```
```    12   thanks to new simprocs.
```
```    13
```
```    14 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
```
```    15   http://www.research.att.com/~njas/sequences/
```
```    16 *)
```
```    17
```
```    18
```
```    19 theory NatSum imports Main begin
```
```    20
```
```    21 consts sum :: "[i=>i, i] => i"
```
```    22 primrec
```
```    23   "sum (f,0) = #0"
```
```    24   "sum (f, succ(n)) = f(\$#n) \$+ sum(f,n)"
```
```    25
```
```    26 declare zadd_zmult_distrib [simp]  zadd_zmult_distrib2 [simp]
```
```    27 declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp]
```
```    28
```
```    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)
```
```    32
```
```    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)
```
```    38
```
```    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)
```
```    45
```
```    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)
```
```    50
```
```    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)
```
```    55
```
```    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)
```
```    60
```
```    61 (** Sum of fourth powers **)
```
```    62
```
```    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)
```
```    68
```
```    69 end
```