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