34 text {* |
34 text {* |
35 \medskip The sum of the first @{text n} odd squares. |
35 \medskip The sum of the first @{text n} odd squares. |
36 *} |
36 *} |
37 |
37 |
38 lemma sum_of_odd_squares: |
38 lemma sum_of_odd_squares: |
39 "#3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) = |
39 "# 3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) = |
40 n * (#4 * n * n - #1)" |
40 n * (# 4 * n * n - Numeral1)" |
41 apply (induct n) |
41 apply (induct n) |
42 txt {* This removes the @{term "-#1"} from the inductive step *} |
42 txt {* This removes the @{term "-Numeral1"} from the inductive step *} |
43 apply (case_tac [2] n) |
43 apply (case_tac [2] n) |
44 apply auto |
44 apply auto |
45 done |
45 done |
46 |
46 |
47 |
47 |
49 \medskip The sum of the first @{term n} odd cubes |
49 \medskip The sum of the first @{term n} odd cubes |
50 *} |
50 *} |
51 |
51 |
52 lemma sum_of_odd_cubes: |
52 lemma sum_of_odd_cubes: |
53 "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) = |
53 "setsum (\<lambda>i. Suc (i + i) * Suc (i + i) * Suc (i + i)) (lessThan n) = |
54 n * n * (#2 * n * n - #1)" |
54 n * n * (# 2 * n * n - Numeral1)" |
55 apply (induct "n") |
55 apply (induct "n") |
56 txt {* This removes the @{term "-#1"} from the inductive step *} |
56 txt {* This removes the @{term "-Numeral1"} from the inductive step *} |
57 apply (case_tac [2] "n") |
57 apply (case_tac [2] "n") |
58 apply auto |
58 apply auto |
59 done |
59 done |
60 |
60 |
61 text {* |
61 text {* |
62 \medskip The sum of the first @{term n} positive integers equals |
62 \medskip The sum of the first @{term n} positive integers equals |
63 @{text "n (n + 1) / 2"}.*} |
63 @{text "n (n + 1) / 2"}.*} |
64 |
64 |
65 lemma sum_of_naturals: |
65 lemma sum_of_naturals: |
66 "#2 * setsum id (atMost n) = n * Suc n" |
66 "# 2 * setsum id (atMost n) = n * Suc n" |
67 apply (induct n) |
67 apply (induct n) |
68 apply auto |
68 apply auto |
69 done |
69 done |
70 |
70 |
71 lemma sum_of_squares: |
71 lemma sum_of_squares: |
72 "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)" |
72 "# 6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (# 2 * n)" |
73 apply (induct n) |
73 apply (induct n) |
74 apply auto |
74 apply auto |
75 done |
75 done |
76 |
76 |
77 lemma sum_of_cubes: |
77 lemma sum_of_cubes: |
78 "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n" |
78 "# 4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n" |
79 apply (induct n) |
79 apply (induct n) |
80 apply auto |
80 apply auto |
81 done |
81 done |
82 |
82 |
83 |
83 |
84 text {* |
84 text {* |
85 \medskip Sum of fourth powers: two versions. |
85 \medskip Sum of fourth powers: two versions. |
86 *} |
86 *} |
87 |
87 |
88 lemma sum_of_fourth_powers: |
88 lemma sum_of_fourth_powers: |
89 "#30 * setsum (\<lambda>i. i * i * i * i) (atMost n) = |
89 "# 30 * setsum (\<lambda>i. i * i * i * i) (atMost n) = |
90 n * Suc n * Suc (#2 * n) * (#3 * n * n + #3 * n - #1)" |
90 n * Suc n * Suc (# 2 * n) * (# 3 * n * n + # 3 * n - Numeral1)" |
91 apply (induct n) |
91 apply (induct n) |
92 apply auto |
92 apply auto |
93 txt {* Eliminates the subtraction *} |
93 txt {* Eliminates the subtraction *} |
94 apply (case_tac n) |
94 apply (case_tac n) |
95 apply simp_all |
95 apply simp_all |
105 zadd_zmult_distrib2 [simp] |
105 zadd_zmult_distrib2 [simp] |
106 zdiff_zmult_distrib [simp] |
106 zdiff_zmult_distrib [simp] |
107 zdiff_zmult_distrib2 [simp] |
107 zdiff_zmult_distrib2 [simp] |
108 |
108 |
109 lemma int_sum_of_fourth_powers: |
109 lemma int_sum_of_fourth_powers: |
110 "#30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) = |
110 "# 30 * int (setsum (\<lambda>i. i * i * i * i) (lessThan m)) = |
111 int m * (int m - #1) * (int (#2 * m) - #1) * |
111 int m * (int m - Numeral1) * (int (# 2 * m) - Numeral1) * |
112 (int (#3 * m * m) - int (#3 * m) - #1)" |
112 (int (# 3 * m * m) - int (# 3 * m) - Numeral1)" |
113 apply (induct m) |
113 apply (induct m) |
114 apply simp_all |
114 apply simp_all |
115 done |
115 done |
116 |
116 |
117 |
117 |
118 text {* |
118 text {* |
119 \medskip Sums of geometric series: 2, 3 and the general case *} |
119 \medskip Sums of geometric series: 2, 3 and the general case *} |
120 |
120 |
121 lemma sum_of_2_powers: "setsum (\<lambda>i. #2^i) (lessThan n) = #2^n - 1" |
121 lemma sum_of_2_powers: "setsum (\<lambda>i. # 2^i) (lessThan n) = # 2^n - (1::nat)" |
122 apply (induct n) |
122 apply (induct n) |
123 apply (auto split: nat_diff_split) |
123 apply (auto split: nat_diff_split) |
124 done |
124 done |
125 |
125 |
126 lemma sum_of_3_powers: "#2 * setsum (\<lambda>i. #3^i) (lessThan n) = #3^n - 1" |
126 lemma sum_of_3_powers: "# 2 * setsum (\<lambda>i. # 3^i) (lessThan n) = # 3^n - (1::nat)" |
127 apply (induct n) |
127 apply (induct n) |
128 apply auto |
128 apply auto |
129 done |
129 done |
130 |
130 |
131 lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\<lambda>i. k^i) (lessThan n) = k^n - 1" |
131 lemma sum_of_powers: "0 < k ==> (k - 1) * setsum (\<lambda>i. k^i) (lessThan n) = k^n - (1::nat)" |
132 apply (induct n) |
132 apply (induct n) |
133 apply auto |
133 apply auto |
134 done |
134 done |
135 |
135 |
136 end |
136 end |