25 |
25 |
26 declare zadd_zmult_distrib [simp] zadd_zmult_distrib2 [simp] |
26 declare zadd_zmult_distrib [simp] zadd_zmult_distrib2 [simp] |
27 declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp] |
27 declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp] |
28 |
28 |
29 (*The sum of the first n odd numbers equals n squared.*) |
29 (*The sum of the first n odd numbers equals n squared.*) |
30 lemma sum_of_odds: "n \<in> nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n" |
30 lemma sum_of_odds: "n \<in> nat \<Longrightarrow> sum (%i. i $+ i $+ #1, n) = $#n $* $#n" |
31 by (induct_tac "n", auto) |
31 by (induct_tac "n", auto) |
32 |
32 |
33 (*The sum of the first n odd squares*) |
33 (*The sum of the first n odd squares*) |
34 lemma sum_of_odd_squares: |
34 lemma sum_of_odd_squares: |
35 "n \<in> nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = |
35 "n \<in> nat \<Longrightarrow> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = |
36 $#n $* (#4 $* $#n $* $#n $- #1)" |
36 $#n $* (#4 $* $#n $* $#n $- #1)" |
37 by (induct_tac "n", auto) |
37 by (induct_tac "n", auto) |
38 |
38 |
39 (*The sum of the first n odd cubes*) |
39 (*The sum of the first n odd cubes*) |
40 lemma sum_of_odd_cubes: |
40 lemma sum_of_odd_cubes: |
41 "n \<in> nat |
41 "n \<in> nat |
42 ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = |
42 \<Longrightarrow> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = |
43 $#n $* $#n $* (#2 $* $#n $* $#n $- #1)" |
43 $#n $* $#n $* (#2 $* $#n $* $#n $- #1)" |
44 by (induct_tac "n", auto) |
44 by (induct_tac "n", auto) |
45 |
45 |
46 (*The sum of the first n positive integers equals n(n+1)/2.*) |
46 (*The sum of the first n positive integers equals n(n+1)/2.*) |
47 lemma sum_of_naturals: |
47 lemma sum_of_naturals: |
48 "n \<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)" |
48 "n \<in> nat \<Longrightarrow> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)" |
49 by (induct_tac "n", auto) |
49 by (induct_tac "n", auto) |
50 |
50 |
51 lemma sum_of_squares: |
51 lemma sum_of_squares: |
52 "n \<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) = |
52 "n \<in> nat \<Longrightarrow> #6 $* sum (%i. i$*i, succ(n)) = |
53 $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)" |
53 $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)" |
54 by (induct_tac "n", auto) |
54 by (induct_tac "n", auto) |
55 |
55 |
56 lemma sum_of_cubes: |
56 lemma sum_of_cubes: |
57 "n \<in> nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = |
57 "n \<in> nat \<Longrightarrow> #4 $* sum (%i. i$*i$*i, succ(n)) = |
58 $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)" |
58 $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)" |
59 by (induct_tac "n", auto) |
59 by (induct_tac "n", auto) |
60 |
60 |
61 (** Sum of fourth powers **) |
61 (** Sum of fourth powers **) |
62 |
62 |
63 lemma sum_of_fourth_powers: |
63 lemma sum_of_fourth_powers: |
64 "n \<in> nat ==> #30 $* sum (%i. i$*i$*i$*i, succ(n)) = |
64 "n \<in> nat \<Longrightarrow> #30 $* sum (%i. i$*i$*i$*i, succ(n)) = |
65 $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* |
65 $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* |
66 (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)" |
66 (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)" |
67 by (induct_tac "n", auto) |
67 by (induct_tac "n", auto) |
68 |
68 |
69 end |
69 end |