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]

lemma sum_of_odds: "n ∈ nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n"

by (induct_tac "n", auto)

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)

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)

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)

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