6526
|
1 |
(* Title: HOL/Isar_examples/NatSum.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow and Markus Wenzel
|
|
4 |
*)
|
|
5 |
|
|
6 |
theory NatSum = Main:;
|
|
7 |
|
6746
|
8 |
section {* Summing natural numbers *};
|
6526
|
9 |
|
6746
|
10 |
text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *};
|
6526
|
11 |
|
|
12 |
consts
|
|
13 |
sum :: "[nat => nat, nat] => nat";
|
|
14 |
|
|
15 |
primrec
|
|
16 |
"sum f 0 = 0"
|
|
17 |
"sum f (Suc n) = f n + sum f n";
|
|
18 |
|
|
19 |
|
|
20 |
(*theorems [simp] = add_assoc add_commute add_left_commute add_mult_distrib add_mult_distrib2;*)
|
|
21 |
|
|
22 |
|
6746
|
23 |
subsection {* The sum of the first n positive integers equals n(n+1)/2 *};
|
6526
|
24 |
|
6746
|
25 |
text {* Emulate Isabelle proof script: *};
|
6526
|
26 |
|
|
27 |
(*
|
|
28 |
Goal "2*sum (%i. i) (Suc n) = n*Suc(n)";
|
|
29 |
by (Simp_tac 1);
|
|
30 |
by (induct_tac "n" 1);
|
|
31 |
by (Simp_tac 1);
|
|
32 |
by (Asm_simp_tac 1);
|
|
33 |
qed "sum_of_naturals";
|
|
34 |
*)
|
|
35 |
|
|
36 |
theorem "2 * sum (%i. i) (Suc n) = n * Suc n";
|
|
37 |
proof same;
|
|
38 |
refine simp_tac;
|
|
39 |
refine (induct n);
|
|
40 |
refine simp_tac;
|
|
41 |
refine asm_simp_tac;
|
|
42 |
qed_with sum_of_naturals;
|
|
43 |
|
|
44 |
|
6746
|
45 |
text {* Proper Isabelle/Isar proof expressing the same reasoning (which
|
|
46 |
is apparently not the most natural one): *};
|
6526
|
47 |
|
|
48 |
theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n";
|
|
49 |
proof simp;
|
|
50 |
show "n + (sum (%i. i) n + sum (%i. i) n) = n * n" (is "??P n");
|
|
51 |
proof (induct ??P n);
|
|
52 |
show "??P 0"; by simp;
|
|
53 |
fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp);
|
|
54 |
qed;
|
|
55 |
qed;
|
|
56 |
|
|
57 |
|
6746
|
58 |
subsection {* The sum of the first n odd numbers equals n squared *};
|
6526
|
59 |
|
6746
|
60 |
text {* First version: `proof-by-induction' *};
|
6526
|
61 |
|
|
62 |
theorem sum_of_odds: "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
|
|
63 |
proof (induct n);
|
|
64 |
show "??P 0"; by simp;
|
6559
|
65 |
fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp);
|
6526
|
66 |
qed;
|
|
67 |
|
6746
|
68 |
text {* The second version tells more about what is going on during the
|
|
69 |
induction. *};
|
6526
|
70 |
|
|
71 |
theorem sum_of_odds': "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
|
|
72 |
proof (induct n);
|
|
73 |
show "??P 0" (is "sum (%i. Suc (i + i)) 0 = 0 * 0"); by simp;
|
|
74 |
fix m; assume hyp: "??P m";
|
|
75 |
show "??P (Suc m)" (is "sum (%i. Suc (i + i)) (Suc m) = Suc m * Suc m");
|
|
76 |
by (simp, rule hyp);
|
|
77 |
qed;
|
|
78 |
|
|
79 |
|
|
80 |
end;
|