src/HOL/ex/NatSum.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 3842 b55686a7b22c
child 4246 c539e702e1d2
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/NatSum.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 Summing natural numbers, squares and cubes.  Could be continued...
     7 Demonstrates permutative rewriting.
     8 *)
     9 
    10 Addsimps add_ac;
    11 Addsimps [add_mult_distrib, add_mult_distrib2];
    12 
    13 (*The sum of the first n positive integers equals n(n+1)/2.*)
    14 goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";
    15 by (Simp_tac 1);
    16 by (nat_ind_tac "n" 1);
    17 by (Simp_tac 1);
    18 by (Asm_simp_tac 1);
    19 qed "sum_of_naturals";
    20 
    21 goal NatSum.thy
    22   "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
    23 by (Simp_tac 1);
    24 by (nat_ind_tac "n" 1);
    25 by (Simp_tac 1);
    26 by (Asm_simp_tac 1);
    27 qed "sum_of_squares";
    28 
    29 goal NatSum.thy
    30   "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
    31 by (Simp_tac 1);
    32 by (nat_ind_tac "n" 1);
    33 by (Simp_tac 1);
    34 by (Asm_simp_tac 1);
    35 qed "sum_of_cubes";
    36 
    37 (*The sum of the first n odd numbers equals n squared.*)
    38 goal NatSum.thy "sum (%i. Suc(i+i)) n = n*n";
    39 by (nat_ind_tac "n" 1);
    40 by (Simp_tac 1);
    41 by (Asm_simp_tac 1);
    42 qed "sum_of_odds";
    43