1.1 --- a/src/HOL/ex/NatSum.ML	Sun Apr 23 11:41:06 2000 +0200
     1.2 +++ b/src/HOL/ex/NatSum.ML	Sun Apr 23 11:41:45 2000 +0200
     1.3 @@ -32,3 +32,26 @@
     1.4  by (induct_tac "n" 1);
     1.5  by Auto_tac;
     1.6  qed "sum_of_cubes";
     1.7 +
     1.8 +
     1.9 +(** Repeating some of the previous examples using binary numerals **)
    1.10 +
    1.11 +(*The sum of the first n positive integers equals n(n+1)/2.*)
    1.12 +Goal "#2 * sum id (Suc n) = n*Suc(n)";
    1.13 +by (induct_tac "n" 1);
    1.14 +by Auto_tac;
    1.15 +qed "sum_of_naturals";
    1.16 +
    1.17 +Addsimps [add_mult_distrib, add_mult_distrib2];
    1.18 +
    1.19 +Goal "#6 * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(#2*n)";
    1.20 +by (induct_tac "n" 1);
    1.21 +by Auto_tac;
    1.22 +(*12.6 secs, down to 5.9 secs, down to 4 secs*)
    1.23 +qed "sum_of_squares";
    1.24 +
    1.25 +Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)";
    1.26 +by (induct_tac "n" 1);
    1.27 +by Auto_tac;
    1.28 +(*27.7 secs, down to 10.9 secs, down to 7.3 secs*)
    1.29 +qed "sum_of_cubes";