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--
more precise headers;
     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