author | wenzelm |
Mon, 22 Jun 1998 17:26:46 +0200 | |
changeset 5069 | 3ea049f7979d |
parent 4558 | 31becfd8d329 |
child 5206 | a3f26b19cd7e |
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 |
||
4558 | 10 |
Delsimprocs nat_cancel; |
3269 | 11 |
Addsimps add_ac; |
12 |
Addsimps [add_mult_distrib, add_mult_distrib2]; |
|
969 | 13 |
|
14 |
(*The sum of the first n positive integers equals n(n+1)/2.*) |
|
5069 | 15 |
Goal "2*sum (%i. i) (Suc n) = n*Suc(n)"; |
1266 | 16 |
by (Simp_tac 1); |
4246 | 17 |
by (induct_tac "n" 1); |
1266 | 18 |
by (Simp_tac 1); |
19 |
by (Asm_simp_tac 1); |
|
969 | 20 |
qed "sum_of_naturals"; |
21 |
||
5069 | 22 |
Goal |
3842 | 23 |
"Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)"; |
1266 | 24 |
by (Simp_tac 1); |
4246 | 25 |
by (induct_tac "n" 1); |
1266 | 26 |
by (Simp_tac 1); |
27 |
by (Asm_simp_tac 1); |
|
969 | 28 |
qed "sum_of_squares"; |
29 |
||
5069 | 30 |
Goal |
3842 | 31 |
"Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; |
1266 | 32 |
by (Simp_tac 1); |
4246 | 33 |
by (induct_tac "n" 1); |
1266 | 34 |
by (Simp_tac 1); |
35 |
by (Asm_simp_tac 1); |
|
969 | 36 |
qed "sum_of_cubes"; |
37 |
||
38 |
(*The sum of the first n odd numbers equals n squared.*) |
|
5069 | 39 |
Goal "sum (%i. Suc(i+i)) n = n*n"; |
4246 | 40 |
by (induct_tac "n" 1); |
1266 | 41 |
by (Simp_tac 1); |
42 |
by (Asm_simp_tac 1); |
|
969 | 43 |
qed "sum_of_odds"; |
44 |