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