src/HOL/ex/NatSum.ML
 author paulson Mon, 03 Jun 1996 11:41:26 +0200 changeset 1783 173ce86b4c22 parent 1465 5d7a7e439cec child 1805 10494d0241cd permissions -rw-r--r--
Used 2 instead of Suc(Suc 0)

(*  Title:      HOL/ex/natsum.ML
ID:         \$Id\$
Author:     Tobias Nipkow

Summing natural numbers, squares and cubes. Could be continued...
*)

(*The sum of the first n positive integers equals n(n+1)/2.*)
goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
by (Simp_tac 1);
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "sum_of_naturals";

goal NatSum.thy
"Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = \
\  n*Suc(n)*Suc(Suc(Suc(0))*n)";
by (Simp_tac 1);
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "sum_of_squares";

goal NatSum.thy
"Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
by (Simp_tac 1);
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "sum_of_cubes";

(*The sum of the first n odd numbers equals n squared.*)
goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n";
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "sum_of_odds";