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