# 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";