# HG changeset patch
# User paulson
# Date 956482905 -7200
# Node ID bfab4d4b7516963a6ed56f79d2b330692e8ea0e1
# Parent  981ebe7f1f103e3b381c85c64a314693bb7fb554
new, but still slow, proofs using binary numerals

diff -r 981ebe7f1f10 -r bfab4d4b7516 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Sun Apr 23 11:41:06 2000 +0200
+++ b/src/HOL/ex/NatSum.ML	Sun Apr 23 11:41:45 2000 +0200
@@ -32,3 +32,26 @@
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_cubes";
+
+
+(** Repeating some of the previous examples using binary numerals **)
+
+(*The sum of the first n positive integers equals n(n+1)/2.*)
+Goal "#2 * sum id (Suc n) = n*Suc(n)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "sum_of_naturals";
+
+Addsimps [add_mult_distrib, add_mult_distrib2];
+
+Goal "#6 * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(#2*n)";
+by (induct_tac "n" 1);
+by Auto_tac;
+(*12.6 secs, down to 5.9 secs, down to 4 secs*)
+qed "sum_of_squares";
+
+Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)";
+by (induct_tac "n" 1);
+by Auto_tac;
+(*27.7 secs, down to 10.9 secs, down to 7.3 secs*)
+qed "sum_of_cubes";