author | haftmann |
Thu, 11 Mar 2010 14:38:20 +0100 | |
changeset 35724 | 178ad68f93ed |
parent 33026 | 8f35633c4922 |
child 37671 | fa53d267dab3 |
permissions | -rw-r--r-- |
33026 | 1 |
(* Title: HOL/Isar_Examples/Summation.thy |
7443 | 2 |
Author: Markus Wenzel |
3 |
*) |
|
4 |
||
10007 | 5 |
header {* Summing natural numbers *} |
7443 | 6 |
|
15561 | 7 |
theory Summation |
8 |
imports Main |
|
9 |
begin |
|
10 |
||
7968 | 11 |
text_raw {* |
12 |
\footnote{This example is somewhat reminiscent of the |
|
13 |
\url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is |
|
14 |
discussed in \cite{isabelle-ref} in the context of permutative |
|
15 |
rewrite rules and ordered rewriting.} |
|
10007 | 16 |
*} |
7968 | 17 |
|
18 |
text {* |
|
19 |
Subsequently, we prove some summation laws of natural numbers |
|
7982 | 20 |
(including odds, squares, and cubes). These examples demonstrate how |
7968 | 21 |
plain natural deduction (including induction) may be combined with |
22 |
calculational proof. |
|
10007 | 23 |
*} |
7968 | 24 |
|
7761 | 25 |
|
10007 | 26 |
subsection {* Summation laws *} |
7443 | 27 |
|
7968 | 28 |
text {* |
29 |
The sum of natural numbers $0 + \cdots + n$ equals $n \times (n + |
|
7982 | 30 |
1)/2$. Avoiding formal reasoning about division we prove this |
31 |
equation multiplied by $2$. |
|
10007 | 32 |
*} |
7800 | 33 |
|
34 |
theorem sum_of_naturals: |
|
15561 | 35 |
"2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)" |
10007 | 36 |
(is "?P n" is "?S n = _") |
37 |
proof (induct n) |
|
38 |
show "?P 0" by simp |
|
10146 | 39 |
next |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
40 |
fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp |
10007 | 41 |
also assume "?S n = n * (n + 1)" |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
42 |
also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp |
10007 | 43 |
finally show "?P (Suc n)" by simp |
44 |
qed |
|
7443 | 45 |
|
7968 | 46 |
text {* |
47 |
The above proof is a typical instance of mathematical induction. The |
|
48 |
main statement is viewed as some $\var{P} \ap n$ that is split by the |
|
49 |
induction method into base case $\var{P} \ap 0$, and step case |
|
7982 | 50 |
$\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$. |
7968 | 51 |
|
52 |
The step case is established by a short calculation in forward |
|
53 |
manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of |
|
7982 | 54 |
the thesis, the final result is achieved by transformations involving |
55 |
basic arithmetic reasoning (using the Simplifier). The main point is |
|
56 |
where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is |
|
57 |
introduced in order to replace a certain subterm. So the |
|
7968 | 58 |
``transitivity'' rule involved here is actual \emph{substitution}. |
59 |
Also note how the occurrence of ``\dots'' in the subsequent step |
|
7982 | 60 |
documents the position where the right-hand side of the hypothesis |
7968 | 61 |
got filled in. |
62 |
||
63 |
\medskip A further notable point here is integration of calculations |
|
7982 | 64 |
with plain natural deduction. This works so well in Isar for two |
65 |
reasons. |
|
7968 | 66 |
\begin{enumerate} |
67 |
||
68 |
\item Facts involved in \isakeyword{also}~/ \isakeyword{finally} |
|
69 |
calculational chains may be just anything. There is nothing special |
|
70 |
about \isakeyword{have}, so the natural deduction element |
|
71 |
\isakeyword{assume} works just as well. |
|
72 |
||
73 |
\item There are two \emph{separate} primitives for building natural |
|
74 |
deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$. |
|
7982 | 75 |
Thus it is possible to start reasoning with some new ``arbitrary, but |
76 |
fixed'' elements before bringing in the actual assumption. In |
|
77 |
contrast, natural deduction is occasionally formalized with basic |
|
78 |
context elements of the form $x:A$ instead. |
|
7968 | 79 |
|
80 |
\end{enumerate} |
|
10007 | 81 |
*} |
7968 | 82 |
|
83 |
text {* |
|
7982 | 84 |
\medskip We derive further summation laws for odds, squares, and |
85 |
cubes as follows. The basic technique of induction plus calculation |
|
86 |
is the same as before. |
|
10007 | 87 |
*} |
7968 | 88 |
|
7800 | 89 |
theorem sum_of_odds: |
15561 | 90 |
"(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)" |
10007 | 91 |
(is "?P n" is "?S n = _") |
92 |
proof (induct n) |
|
93 |
show "?P 0" by simp |
|
10146 | 94 |
next |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
95 |
fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10672
diff
changeset
|
96 |
also assume "?S n = n^Suc (Suc 0)" |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
97 |
also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp |
10007 | 98 |
finally show "?P (Suc n)" by simp |
99 |
qed |
|
7443 | 100 |
|
8814 | 101 |
text {* |
102 |
Subsequently we require some additional tweaking of Isabelle built-in |
|
103 |
arithmetic simplifications, such as bringing in distributivity by |
|
104 |
hand. |
|
10007 | 105 |
*} |
8814 | 106 |
|
10007 | 107 |
lemmas distrib = add_mult_distrib add_mult_distrib2 |
8814 | 108 |
|
7761 | 109 |
theorem sum_of_squares: |
15561 | 110 |
"6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)" |
10007 | 111 |
(is "?P n" is "?S n = _") |
112 |
proof (induct n) |
|
113 |
show "?P 0" by simp |
|
10146 | 114 |
next |
18193 | 115 |
fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" |
116 |
by (simp add: distrib) |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
117 |
also assume "?S n = n * (n + 1) * (2 * n + 1)" |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
118 |
also have "... + 6 * (n + 1)^Suc (Suc 0) = |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
119 |
(n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib) |
10007 | 120 |
finally show "?P (Suc n)" by simp |
121 |
qed |
|
7443 | 122 |
|
7800 | 123 |
theorem sum_of_cubes: |
15561 | 124 |
"4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)" |
10007 | 125 |
(is "?P n" is "?S n = _") |
126 |
proof (induct n) |
|
127 |
show "?P 0" by (simp add: power_eq_if) |
|
10146 | 128 |
next |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
129 |
fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3" |
10007 | 130 |
by (simp add: power_eq_if distrib) |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10672
diff
changeset
|
131 |
also assume "?S n = (n * (n + 1))^Suc (Suc 0)" |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
132 |
also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)" |
10007 | 133 |
by (simp add: power_eq_if distrib) |
134 |
finally show "?P (Suc n)" by simp |
|
135 |
qed |
|
7443 | 136 |
|
7968 | 137 |
text {* |
138 |
Comparing these examples with the tactic script version |
|
139 |
\url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note |
|
7982 | 140 |
an important difference of how induction vs.\ simplification is |
7968 | 141 |
applied. While \cite[\S10]{isabelle-ref} advises for these examples |
142 |
that ``induction should not be applied until the goal is in the |
|
143 |
simplest form'' this would be a very bad idea in our setting. |
|
144 |
||
145 |
Simplification normalizes all arithmetic expressions involved, |
|
7982 | 146 |
producing huge intermediate goals. With applying induction |
147 |
afterwards, the Isar proof text would have to reflect the emerging |
|
148 |
configuration by appropriate sub-proofs. This would result in badly |
|
149 |
structured, low-level technical reasoning, without any good idea of |
|
150 |
the actual point. |
|
7968 | 151 |
|
152 |
\medskip As a general rule of good proof style, automatic methods |
|
7982 | 153 |
such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as |
7968 | 154 |
initial proof methods, but only as terminal ones, solving certain |
155 |
goals completely. |
|
10007 | 156 |
*} |
7968 | 157 |
|
10007 | 158 |
end |