author | berghofe |
Tue, 25 Jun 1996 13:11:29 +0200 | |
changeset 1824 | 44254696843a |
parent 1805 | 10494d0241cd |
child 3269 | eca2a3634acd |
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 |
||
6 |
Summing natural numbers, squares and cubes. Could be continued... |
|
7 |
*) |
|
8 |
||
1266 | 9 |
Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac); |
1805
10494d0241cd
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1783
diff
changeset
|
10 |
Addsimps [add_mult_distrib,add_mult_distrib2]; |
969 | 11 |
|
12 |
(*The sum of the first n positive integers equals n(n+1)/2.*) |
|
1783 | 13 |
goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)"; |
1266 | 14 |
by (Simp_tac 1); |
969 | 15 |
by (nat_ind_tac "n" 1); |
1266 | 16 |
by (Simp_tac 1); |
17 |
by (Asm_simp_tac 1); |
|
969 | 18 |
qed "sum_of_naturals"; |
19 |
||
20 |
goal NatSum.thy |
|
1805
10494d0241cd
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1783
diff
changeset
|
21 |
"Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = n*Suc(n)*Suc(2*n)"; |
1266 | 22 |
by (Simp_tac 1); |
969 | 23 |
by (nat_ind_tac "n" 1); |
1266 | 24 |
by (Simp_tac 1); |
25 |
by (Asm_simp_tac 1); |
|
969 | 26 |
qed "sum_of_squares"; |
27 |
||
28 |
goal NatSum.thy |
|
29 |
"Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; |
|
1266 | 30 |
by (Simp_tac 1); |
969 | 31 |
by (nat_ind_tac "n" 1); |
1266 | 32 |
by (Simp_tac 1); |
33 |
by (Asm_simp_tac 1); |
|
969 | 34 |
qed "sum_of_cubes"; |
35 |
||
36 |
(*The sum of the first n odd numbers equals n squared.*) |
|
37 |
goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n"; |
|
38 |
by (nat_ind_tac "n" 1); |
|
1266 | 39 |
by (Simp_tac 1); |
40 |
by (Asm_simp_tac 1); |
|
969 | 41 |
qed "sum_of_odds"; |
42 |