ex/NatSum.ML

--- a/ex/NatSum.ML	Fri Jun 17 14:16:50 1994 +0200
+++ b/ex/NatSum.ML	Fri Jun 17 18:28:36 1994 +0200
@@ -9,12 +9,13 @@
 val natsum_ss = arith_ss addsimps
   ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
 
+(*The sum of the first n positive integers equals n(n+1)/2.*)
 goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
 by (simp_tac natsum_ss 1);
 by (nat_ind_tac "n" 1);
 by (simp_tac natsum_ss 1);
 by (asm_simp_tac natsum_ss 1);
-result();
+val sum_of_naturals = result();
 
 goal NatSum.thy
   "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum(%i.i*i,Suc(n)) = \
@@ -23,7 +24,7 @@
 by (nat_ind_tac "n" 1);
 by (simp_tac natsum_ss 1);
 by (asm_simp_tac natsum_ss 1);
-result();
+val sum_of_squares = result();
 
 goal NatSum.thy
   "Suc(Suc(Suc(Suc(0))))*sum(%i.i*i*i,Suc(n)) = n*n*Suc(n)*Suc(n)";
@@ -31,4 +32,12 @@
 by (nat_ind_tac "n" 1);
 by (simp_tac natsum_ss 1);
 by (asm_simp_tac natsum_ss 1);
-result();
+val sum_of_cubes = result();
+
+(*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 natsum_ss 1);
+by (asm_simp_tac natsum_ss 1);
+val sum_of_odds = result();
+