# Theory NatSum

Up to index of Isabelle/ZF/ex

theory NatSum
imports Main
begin

    (*  Title:      ZF/ex/Natsum.thy
        ID:         $Id: NatSum.thy,v 1.3 2005/06/17 14:15:11 haftmann Exp $
        Author:     Tobias Nipkow & Lawrence C Paulson

    A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.

    Note: n is a natural number but the sum is an integer,
                                and f maps integers to integers

    Summing natural numbers, squares, cubes, etc.

    Originally demonstrated permutative rewriting, but add_ac is no longer needed
      thanks to new simprocs.

    Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
      http://www.research.att.com/~njas/sequences/
    *)

    theory NatSum imports Main begin

    consts sum :: "[i=>i, i] => i"
    primrec
      "sum (f,0) = #0"
      "sum (f, succ(n)) = f($#n) $+ sum(f,n)"

    declare zadd_zmult_distrib [simp]  zadd_zmult_distrib2 [simp]
    declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp]

    (*The sum of the first n odd numbers equals n squared.*)
    lemma sum_of_odds: "n ∈ nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n"
    by (induct_tac "n", auto)

    (*The sum of the first n odd squares*)
    lemma sum_of_odd_squares:
         "n ∈ nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) =
          $#n $* (#4 $* $#n $* $#n $- #1)"
    by (induct_tac "n", auto)

    (*The sum of the first n odd cubes*)
    lemma sum_of_odd_cubes:
         "n ∈ nat
          ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) =
              $#n $* $#n $* (#2 $* $#n $* $#n $- #1)"
    by (induct_tac "n", auto)

    (*The sum of the first n positive integers equals n(n+1)/2.*)
    lemma sum_of_naturals:
         "n ∈ nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)"
    by (induct_tac "n", auto)

    lemma sum_of_squares:
         "n ∈ nat ==> #6 $* sum (%i. i$*i, succ(n)) =
                      $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)"
    by (induct_tac "n", auto)

    lemma sum_of_cubes:
         "n ∈ nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) =
                      $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)"
    by (induct_tac "n", auto)

    (** Sum of fourth powers **)

    lemma sum_of_fourth_powers:
         "n ∈ nat ==> #30 $* sum (%i. i$*i$*i$*i, succ(n)) =
                        $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $*
                        (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)"
    by (induct_tac "n", auto)

    end

lemma sum_of_odds:

      n ∈ nat ==> NatSum.sum(%i. i $+ i $+ #1, n) = $# n $× $# n

lemma sum_of_odd_squares:

      n ∈ nat
      ==> #3 $× NatSum.sum(%i. (i $+ i $+ #1) $× (i $+ i $+ #1), n) =
          $# n $× (#4 $× $# n $× $# n $- #1)

lemma sum_of_odd_cubes:

      n ∈ nat
      ==> NatSum.sum(%i. (i $+ i $+ #1) $× (i $+ i $+ #1) $× (i $+ i $+ #1), n) =
          $# n $× $# n $× (#2 $× $# n $× $# n $- #1)

lemma sum_of_naturals:

      n ∈ nat ==> #2 $× NatSum.sum(%i. i, succ(n)) = $# n $× $# succ(n)

lemma sum_of_squares:

      n ∈ nat
      ==> #6 $× NatSum.sum(%i. i $× i, succ(n)) =
          $# n $× ($# n $+ #1) $× (#2 $× $# n $+ #1)

lemma sum_of_cubes:

      n ∈ nat
      ==> #4 $× NatSum.sum(%i. i $× i $× i, succ(n)) =
          $# n $× $# n $× ($# n $+ #1) $× ($# n $+ #1)

lemma sum_of_fourth_powers:

      n ∈ nat
      ==> #30 $× NatSum.sum(%i. i $× i $× i $× i, succ(n)) =
          $# n $× ($# n $+ #1) $× (#2 $× $# n $+ #1) $×
          (#3 $× $# n $× $# n $+ #3 $× $# n $- #1)