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