equal
deleted
inserted
replaced
1 (* Title: HOL/ex/NatSum.ML |
1 (* Title: HOL/ex/NatSum.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 Summing natural numbers, squares and cubes. Could be continued... |
6 Summing natural numbers, squares and cubes. Could be continued... |
|
7 Demonstrates permutative rewriting. |
7 *) |
8 *) |
8 |
9 |
9 Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac); |
10 Addsimps add_ac; |
10 Addsimps [add_mult_distrib,add_mult_distrib2]; |
11 Addsimps [add_mult_distrib, add_mult_distrib2]; |
11 |
12 |
12 (*The sum of the first n positive integers equals n(n+1)/2.*) |
13 (*The sum of the first n positive integers equals n(n+1)/2.*) |
13 goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)"; |
14 goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)"; |
14 by (Simp_tac 1); |
15 by (Simp_tac 1); |
15 by (nat_ind_tac "n" 1); |
16 by (nat_ind_tac "n" 1); |