equal
deleted
inserted
replaced
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) = n * (#4 * n * n - #1)" |
39 "#3 * setsum (\<lambda>i. Suc (i + i) * Suc (i + i)) (lessThan n) = |
|
40 n * (#4 * n * n - #1)" |
40 apply (induct n) |
41 apply (induct n) |
41 txt {* This removes the @{term "-#1"} from the inductive step *} |
42 txt {* This removes the @{term "-#1"} from the inductive step *} |
42 apply (case_tac [2] n) |
43 apply (case_tac [2] n) |
43 apply auto |
44 apply auto |
44 done |
45 done |
59 |
60 |
60 text {* |
61 text {* |
61 \medskip The sum of the first @{term n} positive integers equals |
62 \medskip The sum of the first @{term n} positive integers equals |
62 @{text "n (n + 1) / 2"}.*} |
63 @{text "n (n + 1) / 2"}.*} |
63 |
64 |
64 lemma sum_of_naturals: "#2 * setsum id (atMost n) = n * Suc n" |
65 lemma sum_of_naturals: |
|
66 "#2 * setsum id (atMost n) = n * Suc n" |
65 apply (induct n) |
67 apply (induct n) |
66 apply auto |
68 apply auto |
67 done |
69 done |
68 |
70 |
69 lemma sum_of_squares: "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)" |
71 lemma sum_of_squares: |
|
72 "#6 * setsum (\<lambda>i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)" |
70 apply (induct n) |
73 apply (induct n) |
71 apply auto |
74 apply auto |
72 done |
75 done |
73 |
76 |
74 lemma sum_of_cubes: "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n" |
77 lemma sum_of_cubes: |
|
78 "#4 * setsum (\<lambda>i. i * i * i) (atMost n) = n * n * Suc n * Suc n" |
75 apply (induct n) |
79 apply (induct n) |
76 apply auto |
80 apply auto |
77 done |
81 done |
78 |
82 |
79 |
83 |