Theory NatSum
theory NatSum imports ZF 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