# HG changeset patch
# User paulson
# Date 957286499 -7200
# Node ID b0c32189b2c140dbc11d9898668d04de8ef353c5
# Parent  2d4afbc468010b7b35f5fb7869625fb8444939cf
now using binary naturals

diff -r 2d4afbc46801 -r b0c32189b2c1 src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Tue May 02 18:54:38 2000 +0200
+++ b/src/HOL/ex/NatSum.ML	Tue May 02 18:54:59 2000 +0200
@@ -15,43 +15,20 @@
 by Auto_tac;
 qed "sum_of_odds";
 
-(*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 "Suc(Suc(Suc(Suc 2))) * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(2*n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "sum_of_squares";
-
-Goal "Suc(Suc 2) * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)";
-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";