author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8976  340d306f0118 
child 10698  dc5e984dfe13 
permissions  rwrr 
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 

8836  6 
Summing natural numbers, squares, cubes, etc. 
8415  7 

8 
Originally demonstrated permutative rewriting, but add_ac is no longer needed 

9 
thanks to new simprocs. 

8842  10 

11 
Thanks to Sloane's OnLine Encyclopedia of Integer Sequences, 

12 
http://www.research.att.com/~njas/sequences/ 

969  13 
*) 
14 

8976  15 
Addsimps [lessThan_Suc, atMost_Suc]; 
8842  16 
Addsimps [add_mult_distrib, add_mult_distrib2]; 
8869
9ba7ef8a765b
new simprules needed because of new subtraction rewriting
paulson
parents:
8842
diff
changeset

17 
Addsimps [diff_mult_distrib, diff_mult_distrib2]; 
8842  18 

8493  19 
(*The sum of the first n odd numbers equals n squared.*) 
8976  20 
Goal "setsum (%i. Suc(i+i)) (lessThan n) = n*n"; 
8493  21 
by (induct_tac "n" 1); 
22 
by Auto_tac; 

23 
qed "sum_of_odds"; 

969  24 

8842  25 
(*The sum of the first n odd squares*) 
8976  26 
Goal "#3 * setsum (%i. Suc(i+i)*Suc(i+i)) (lessThan n) = n * (#4*n*n  #1)"; 
8842  27 
by (induct_tac "n" 1); 
28 
(*This removes the #1 from the inductive step*) 

29 
by (case_tac "n" 2); 

30 
by Auto_tac; 

31 
qed "sum_of_odd_squares"; 

32 

33 
(*The sum of the first n odd cubes*) 

8976  34 
Goal "setsum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) (lessThan n) = n * n * (#2*n*n  #1)"; 
8842  35 
by (induct_tac "n" 1); 
36 
(*This removes the #1 from the inductive step*) 

37 
by (case_tac "n" 2); 

38 
by Auto_tac; 

39 
qed "sum_of_odd_cubes"; 

8493  40 

8770  41 
(*The sum of the first n positive integers equals n(n+1)/2.*) 
8976  42 
Goal "#2 * setsum id (atMost n) = n*Suc(n)"; 
8770  43 
by (induct_tac "n" 1); 
44 
by Auto_tac; 

45 
qed "sum_of_naturals"; 

46 

8976  47 
Goal "#6 * setsum (%i. i*i) (atMost n) = n * Suc(n) * Suc(#2*n)"; 
8770  48 
by (induct_tac "n" 1); 
49 
by Auto_tac; 

50 
qed "sum_of_squares"; 

51 

8976  52 
Goal "#4 * setsum (%i. i*i*i) (atMost n) = n * n * Suc(n) * Suc(n)"; 
8770  53 
by (induct_tac "n" 1); 
54 
by Auto_tac; 

55 
qed "sum_of_cubes"; 

8836  56 

8842  57 
(** Sum of fourth powers: two versions **) 
8836  58 

8976  59 
Goal "#30 * setsum (%i. i*i*i*i) (atMost n) = \ 
8836  60 
\ n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n  #1)"; 
61 
by (induct_tac "n" 1); 

8976  62 
by Auto_tac; 
8842  63 
(*Eliminates the subtraction*) 
64 
by (case_tac "n" 1); 

65 
by (ALLGOALS Asm_simp_tac); 

8836  66 
qed "sum_of_fourth_powers"; 
67 

8976  68 
(*Alternative proof, with a change of variables and much more subtraction, 
69 
performed using the integers.*) 

8836  70 

8837  71 
Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, 
72 
zdiff_zmult_distrib, zdiff_zmult_distrib2]; 

73 

8976  74 
Goal "#30 * int (setsum (%i. i*i*i*i) (lessThan m)) = \ 
8842  75 
\ int m * (int m  #1) * (int (#2*m)  #1) * \ 
76 
\ (int (#3*m*m)  int(#3*m)  #1)"; 

77 
by (induct_tac "m" 1); 

78 
by (ALLGOALS Asm_simp_tac); 

8837  79 
qed "int_sum_of_fourth_powers"; 
8932  80 

81 
(** Sums of geometric series: 2, 3 and the general case **) 

82 

8976  83 
Goal "setsum (%i. #2^i) (lessThan n) = #2^n  1"; 
8932  84 
by (induct_tac "n" 1); 
85 
by Auto_tac; 

86 
qed "sum_of_2_powers"; 

87 

8976  88 
Goal "#2 * setsum (%i. #3^i) (lessThan n) = #3^n  1"; 
8932  89 
by (induct_tac "n" 1); 
90 
by Auto_tac; 

91 
qed "sum_of_3_powers"; 

92 

8976  93 
Goal "0<k ==> (k1) * setsum (%i. k^i) (lessThan n) = k^n  1"; 
8932  94 
by (induct_tac "n" 1); 
95 
by Auto_tac; 

96 
by (subgoal_tac "1*k^n <= k * k^n" 1); 

97 
by (Asm_full_simp_tac 1); 

98 
by (rtac mult_le_mono1 1); 

99 
by Auto_tac; 

100 
qed "sum_of_powers"; 