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, cubes, etc. |
7 |
7 |
8 Originally demonstrated permutative rewriting, but add_ac is no longer needed |
8 Originally demonstrated permutative rewriting, but add_ac is no longer needed |
9 thanks to new simprocs. |
9 thanks to new simprocs. |
10 *) |
10 *) |
11 |
11 |
30 |
30 |
31 Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
31 Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
32 by (induct_tac "n" 1); |
32 by (induct_tac "n" 1); |
33 by Auto_tac; |
33 by Auto_tac; |
34 qed "sum_of_cubes"; |
34 qed "sum_of_cubes"; |
|
35 |
|
36 (** Sum of fourth powers requires lemmas **) |
|
37 |
|
38 Goal "[| #1 <= (j::nat); k <= m |] ==> k <= j*m"; |
|
39 by (dtac mult_le_mono 1); |
|
40 by Auto_tac; |
|
41 qed "mult_le_1_mono"; |
|
42 |
|
43 Addsimps [diff_mult_distrib, diff_mult_distrib2]; |
|
44 |
|
45 (*Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
|
46 http://www.research.att.com/~njas/sequences/*) |
|
47 Goal "#30 * sum (%i. i*i*i*i) (Suc n) = \ |
|
48 \ n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)"; |
|
49 by (induct_tac "n" 1); |
|
50 by (Simp_tac 1); |
|
51 (*Automating this inequality proof would make the proof trivial*) |
|
52 by (subgoal_tac "n <= #10 * (n * (n * n)) + (#15 * (n * (n * (n * n))) + \ |
|
53 \ #6 * (n * (n * (n * (n * n)))))" 1); |
|
54 (*In simplifying we want only the outer Suc argument to be unfolded. |
|
55 Thus the result matches the induction hypothesis (also with Suc). *) |
|
56 by (asm_simp_tac (simpset() delsimps [sum_Suc] |
|
57 addsimps [inst "n" "Suc ?m" sum_Suc]) 1); |
|
58 by (rtac ([mult_le_1_mono, le_add1] MRS le_trans) 1); |
|
59 by (rtac le_cube 2); |
|
60 by (Simp_tac 1); |
|
61 qed "sum_of_fourth_powers"; |
|
62 |
|
63 |