author  wenzelm 
Tue, 31 Mar 2015 22:31:05 +0200  
changeset 59886  e0dc738eb08c 
parent 59360  b1e5d552e8cc 
child 62222  54a7b9422d3e 
permissions  rwrr 
47269  1 
(*<*) 
2 
theory Bool_nat_list 

3 
imports Main 

4 
begin 

5 
(*>*) 

6 

7 
text{* 

8 
\vspace{4ex} 

9 
\section{\texorpdfstring{Types @{typ bool}, @{typ nat} and @{text list}}{Types bool, nat and list}} 

10 

11 
These are the most important predefined types. We go through them one by one. 

12 
Based on examples we learn how to define (possibly recursive) functions and 

13 
prove theorems about them by induction and simplification. 

14 

55317  15 
\subsection{Type \indexed{@{typ bool}}{bool}} 
47269  16 

17 
The type of boolean values is a predefined datatype 

18 
@{datatype[display] bool} 

55317  19 
with the two values \indexed{@{const True}}{True} and \indexed{@{const False}}{False} and 
47269  20 
with many predefined functions: @{text "\<not>"}, @{text "\<and>"}, @{text "\<or>"}, @{text 
56989  21 
"\<longrightarrow>"}, etc. Here is how conjunction could be defined by pattern matching: 
47269  22 
*} 
23 

24 
fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where 

25 
"conj True True = True"  

26 
"conj _ _ = False" 

27 

28 
text{* Both the datatype and function definitions roughly follow the syntax 

29 
of functional programming languages. 

30 

55317  31 
\subsection{Type \indexed{@{typ nat}}{nat}} 
47269  32 

33 
Natural numbers are another predefined datatype: 

55317  34 
@{datatype[display] nat}\index{Suc@@{const Suc}} 
47269  35 
All values of type @{typ nat} are generated by the constructors 
36 
@{text 0} and @{const Suc}. Thus the values of type @{typ nat} are 

56989  37 
@{text 0}, @{term"Suc 0"}, @{term"Suc(Suc 0)"}, etc. 
47269  38 
There are many predefined functions: @{text "+"}, @{text "*"}, @{text 
39 
"\<le>"}, etc. Here is how you could define your own addition: 

40 
*} 

41 

42 
fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where 

43 
"add 0 n = n"  

44 
"add (Suc m) n = Suc(add m n)" 

45 

46 
text{* And here is a proof of the fact that @{prop"add m 0 = m"}: *} 

47 

48 
lemma add_02: "add m 0 = m" 

49 
apply(induction m) 

50 
apply(auto) 

51 
done 

52 
(*<*) 

53 
lemma "add m 0 = m" 

54 
apply(induction m) 

55 
(*>*) 

56 
txt{* The \isacom{lemma} command starts the proof and gives the lemma 

57 
a name, @{text add_02}. Properties of recursively defined functions 

58 
need to be established by induction in most cases. 

59 
Command \isacom{apply}@{text"(induction m)"} instructs Isabelle to 

60 
start a proof by induction on @{text m}. In response, it will show the 

61 
following proof state: 

62 
@{subgoals[display,indent=0]} 

63 
The numbered lines are known as \emph{subgoals}. 

64 
The first subgoal is the base case, the second one the induction step. 

65 
The prefix @{text"\<And>m."} is Isabelle's way of saying ``for an arbitrary but fixed @{text m}''. The @{text"\<Longrightarrow>"} separates assumptions from the conclusion. 

66 
The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try 

67 
and prove all subgoals automatically, essentially by simplifying them. 

68 
Because both subgoals are easy, Isabelle can do it. 

69 
The base case @{prop"add 0 0 = 0"} holds by definition of @{const add}, 

70 
and the induction step is almost as simple: 

71 
@{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"} 

72 
using first the definition of @{const add} and then the induction hypothesis. 

73 
In summary, both subproofs rely on simplification with function definitions and 

74 
the induction hypothesis. 

75 
As a result of that final \isacom{done}, Isabelle associates the lemma 

76 
just proved with its name. You can now inspect the lemma with the command 

77 
*} 

78 

79 
thm add_02 

80 

81 
txt{* which displays @{thm[show_question_marks,display] add_02} The free 

82 
variable @{text m} has been replaced by the \concept{unknown} 

56989  83 
@{text"?m"}. There is no logical difference between the two but there is an 
47269  84 
operational one: unknowns can be instantiated, which is what you want after 
85 
some lemma has been proved. 

86 

87 
Note that there is also a proof method @{text induct}, which behaves almost 

88 
like @{text induction}; the difference is explained in \autoref{ch:Isar}. 

89 

90 
\begin{warn} 

91 
Terminology: We use \concept{lemma}, \concept{theorem} and \concept{rule} 

92 
interchangeably for propositions that have been proved. 

93 
\end{warn} 

94 
\begin{warn} 

95 
Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard 

96 
arithmetic operations (@{text "+"}, @{text ""}, @{text "*"}, @{text"\<le>"}, 

58521  97 
@{text"<"}, etc.) are overloaded: they are available 
47269  98 
not just for natural numbers but for other types as well. 
99 
For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate 

100 
that you are talking about natural numbers. Hence Isabelle can only infer 

101 
that @{term x} is of some arbitrary type where @{text 0} and @{text"+"} 

54508  102 
exist. As a consequence, you will be unable to prove the goal. 
103 
% To alert you to such pitfalls, Isabelle flags numerals without a 

104 
% fixed type in its output: @ {prop"x+0 = x"}. 

105 
In this particular example, you need to include 

47269  106 
an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there 
107 
is enough contextual information this may not be necessary: @{prop"Suc x = 

108 
x"} automatically implies @{text"x::nat"} because @{term Suc} is not 

109 
overloaded. 

110 
\end{warn} 

111 

52361  112 
\subsubsection{An Informal Proof} 
47269  113 

114 
Above we gave some terse informal explanation of the proof of 

115 
@{prop"add m 0 = m"}. A more detailed informal exposition of the lemma 

116 
might look like this: 

117 
\bigskip 

118 

119 
\noindent 

120 
\textbf{Lemma} @{prop"add m 0 = m"} 

121 

122 
\noindent 

123 
\textbf{Proof} by induction on @{text m}. 

124 
\begin{itemize} 

125 
\item Case @{text 0} (the base case): @{prop"add 0 0 = 0"} 

126 
holds by definition of @{const add}. 

127 
\item Case @{term"Suc m"} (the induction step): 

128 
We assume @{prop"add m 0 = m"}, the induction hypothesis (IH), 

129 
and we need to show @{text"add (Suc m) 0 = Suc m"}. 

130 
The proof is as follows:\smallskip 

131 

132 
\begin{tabular}{@ {}rcl@ {\quad}l@ {}} 

133 
@{term "add (Suc m) 0"} &@{text"="}& @{term"Suc(add m 0)"} 

134 
& by definition of @{text add}\\ 

135 
&@{text"="}& @{term "Suc m"} & by IH 

136 
\end{tabular} 

137 
\end{itemize} 

138 
Throughout this book, \concept{IH} will stand for ``induction hypothesis''. 

139 

140 
We have now seen three proofs of @{prop"add m 0 = 0"}: the Isabelle one, the 

47711  141 
terse four lines explaining the base case and the induction step, and just now a 
47269  142 
model of a traditional inductive proof. The three proofs differ in the level 
143 
of detail given and the intended reader: the Isabelle proof is for the 

144 
machine, the informal proofs are for humans. Although this book concentrates 

47711  145 
on Isabelle proofs, it is important to be able to rephrase those proofs 
47269  146 
as informal text comprehensible to a reader familiar with traditional 
147 
mathematical proofs. Later on we will introduce an Isabelle proof language 

148 
that is closer to traditional informal mathematical language and is often 

149 
directly readable. 

150 

55317  151 
\subsection{Type \indexed{@{text list}}{list}} 
47269  152 

58521  153 
Although lists are already predefined, we define our own copy for 
47269  154 
demonstration purposes: 
155 
*} 

156 
(*<*) 

157 
apply(auto) 

158 
done 

159 
declare [[names_short]] 

160 
(*>*) 

47302  161 
datatype 'a list = Nil  Cons 'a "'a list" 
59204
0cbe0a56d3fa
update map definition in Prog_Prove for new datatype package
kleing
parents:
58521
diff
changeset

162 
(*<*) 
0cbe0a56d3fa
update map definition in Prog_Prove for new datatype package
kleing
parents:
58521
diff
changeset

163 
for map: map 
0cbe0a56d3fa
update map definition in Prog_Prove for new datatype package
kleing
parents:
58521
diff
changeset

164 
(*>*) 
47269  165 

47302  166 
text{* 
167 
\begin{itemize} 

47711  168 
\item Type @{typ "'a list"} is the type of lists over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type). 
47302  169 
\item Lists have two constructors: @{const Nil}, the empty list, and @{const Cons}, which puts an element (of type @{typ 'a}) in front of a list (of type @{typ "'a list"}). 
170 
Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"}, 

56989  171 
or @{term"Cons x (Cons y Nil)"}, etc. 
47302  172 
\item \isacom{datatype} requires no quotation marks on the 
173 
lefthand side, but on the righthand side each of the argument 

174 
types of a constructor needs to be enclosed in quotation marks, unless 

58504  175 
it is just an identifier (e.g., @{typ nat} or @{typ 'a}). 
47302  176 
\end{itemize} 
47269  177 
We also define two standard functions, append and reverse: *} 
178 

179 
fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

180 
"app Nil ys = ys"  

181 
"app (Cons x xs) ys = Cons x (app xs ys)" 

182 

183 
fun rev :: "'a list \<Rightarrow> 'a list" where 

184 
"rev Nil = Nil"  

185 
"rev (Cons x xs) = app (rev xs) (Cons x Nil)" 

186 

187 
text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of 

188 
@{text list} type. 

189 

55320  190 
Command \indexed{\isacommand{value}}{value} evaluates a term. For example, *} 
47269  191 

192 
value "rev(Cons True (Cons False Nil))" 

193 

194 
text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *} 

195 

196 
value "rev(Cons a (Cons b Nil))" 

197 

198 
text{* yields @{value "rev(Cons a (Cons b Nil))"}. 

199 
\medskip 

200 

47302  201 
Figure~\ref{fig:MyList} shows the theory created so far. 
56989  202 
Because @{text list}, @{const Nil}, @{const Cons}, etc.\ are already predefined, 
47719
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

203 
Isabelle prints qualified (long) names when executing this theory, for example, @{text MyList.Nil} 
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

204 
instead of @{const Nil}. 
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

205 
To suppress the qualified names you can insert the command 
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

206 
\texttt{declare [[names\_short]]}. 
56989  207 
This is not recommended in general but is convenient for this unusual example. 
47302  208 
% Notice where the 
209 
%quotations marks are needed that we mostly sweep under the carpet. In 

210 
%particular, notice that \isacom{datatype} requires no quotation marks on the 

211 
%lefthand side, but that on the righthand side each of the argument 

212 
%types of a constructor needs to be enclosed in quotation marks. 

47269  213 

214 
\begin{figure}[htbp] 

215 
\begin{alltt} 

48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47719
diff
changeset

216 
\input{MyList.thy}\end{alltt} 
58521  217 
\caption{A theory of lists} 
47269  218 
\label{fig:MyList} 
57805  219 
\index{comment} 
47269  220 
\end{figure} 
221 

222 
\subsubsection{Structural Induction for Lists} 

223 

224 
Just as for natural numbers, there is a proof principle of induction for 

225 
lists. Induction over a list is essentially induction over the length of 

226 
the list, although the length remains implicit. To prove that some property 

58504  227 
@{text P} holds for all lists @{text xs}, i.e., \mbox{@{prop"P(xs)"}}, 
47269  228 
you need to prove 
229 
\begin{enumerate} 

230 
\item the base case @{prop"P(Nil)"} and 

47711  231 
\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}. 
47269  232 
\end{enumerate} 
55318  233 
This is often called \concept{structural induction} for lists. 
47269  234 

235 
\subsection{The Proof Process} 

236 

237 
We will now demonstrate the typical proof process, which involves 

238 
the formulation and proof of auxiliary lemmas. 

239 
Our goal is to show that reversing a list twice produces the original 

240 
list. *} 

241 

242 
theorem rev_rev [simp]: "rev(rev xs) = xs" 

243 

244 
txt{* Commands \isacom{theorem} and \isacom{lemma} are 

245 
interchangeable and merely indicate the importance we attach to a 

246 
proposition. Via the bracketed attribute @{text simp} we also tell Isabelle 

55317  247 
to make the eventual theorem a \conceptnoidx{simplification rule}: future proofs 
47269  248 
involving simplification will replace occurrences of @{term"rev(rev xs)"} by 
249 
@{term"xs"}. The proof is by induction: *} 

250 

251 
apply(induction xs) 

252 

253 
txt{* 

254 
As explained above, we obtain two subgoals, namely the base case (@{const Nil}) and the induction step (@{const Cons}): 

255 
@{subgoals[display,indent=0,margin=65]} 

256 
Let us try to solve both goals automatically: 

257 
*} 

258 

259 
apply(auto) 

260 

261 
txt{*Subgoal~1 is proved, and disappears; the simplified version 

262 
of subgoal~2 becomes the new subgoal~1: 

263 
@{subgoals[display,indent=0,margin=70]} 

264 
In order to simplify this subgoal further, a lemma suggests itself. 

265 

266 
\subsubsection{A First Lemma} 

267 

268 
We insert the following lemma in front of the main theorem: 

269 
*} 

270 
(*<*) 

271 
oops 

272 
(*>*) 

273 
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)" 

274 

275 
txt{* There are two variables that we could induct on: @{text xs} and 

276 
@{text ys}. Because @{const app} is defined by recursion on 

277 
the first argument, @{text xs} is the correct one: 

278 
*} 

279 

280 
apply(induction xs) 

281 

282 
txt{* This time not even the base case is solved automatically: *} 

283 
apply(auto) 

284 
txt{* 

285 
\vspace{5ex} 

286 
@{subgoals[display,goals_limit=1]} 

287 
Again, we need to abandon this proof attempt and prove another simple lemma 

288 
first. 

289 

290 
\subsubsection{A Second Lemma} 

291 

292 
We again try the canonical proof procedure: 

293 
*} 

294 
(*<*) 

295 
oops 

296 
(*>*) 

297 
lemma app_Nil2 [simp]: "app xs Nil = xs" 

298 
apply(induction xs) 

299 
apply(auto) 

300 
done 

301 

302 
text{* 

303 
Thankfully, this worked. 

304 
Now we can continue with our stuck proof attempt of the first lemma: 

305 
*} 

306 

307 
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)" 

308 
apply(induction xs) 

309 
apply(auto) 

310 

311 
txt{* 

312 
We find that this time @{text"auto"} solves the base case, but the 

313 
induction step merely simplifies to 

314 
@{subgoals[display,indent=0,goals_limit=1]} 

47711  315 
The missing lemma is associativity of @{const app}, 
47269  316 
which we insert in front of the failed lemma @{text rev_app}. 
317 

318 
\subsubsection{Associativity of @{const app}} 

319 

320 
The canonical proof procedure succeeds without further ado: 

321 
*} 

322 
(*<*)oops(*>*) 

323 
lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)" 

324 
apply(induction xs) 

325 
apply(auto) 

326 
done 

327 
(*<*) 

328 
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys)(rev xs)" 

329 
apply(induction xs) 

330 
apply(auto) 

331 
done 

332 

333 
theorem rev_rev [simp]: "rev(rev xs) = xs" 

334 
apply(induction xs) 

335 
apply(auto) 

336 
done 

337 
(*>*) 

338 
text{* 

339 
Finally the proofs of @{thm[source] rev_app} and @{thm[source] rev_rev} 

340 
succeed, too. 

341 

52361  342 
\subsubsection{Another Informal Proof} 
47269  343 

344 
Here is the informal proof of associativity of @{const app} 

345 
corresponding to the Isabelle proof above. 

346 
\bigskip 

347 

348 
\noindent 

349 
\textbf{Lemma} @{prop"app (app xs ys) zs = app xs (app ys zs)"} 

350 

351 
\noindent 

352 
\textbf{Proof} by induction on @{text xs}. 

353 
\begin{itemize} 

354 
\item Case @{text Nil}: \ @{prop"app (app Nil ys) zs = app ys zs"} @{text"="} 

355 
\mbox{@{term"app Nil (app ys zs)"}} \ holds by definition of @{text app}. 

356 
\item Case @{text"Cons x xs"}: We assume 

357 
\begin{center} \hfill @{term"app (app xs ys) zs"} @{text"="} 

358 
@{term"app xs (app ys zs)"} \hfill (IH) \end{center} 

359 
and we need to show 

360 
\begin{center} @{prop"app (app (Cons x xs) ys) zs = app (Cons x xs) (app ys zs)"}.\end{center} 

361 
The proof is as follows:\smallskip 

362 

363 
\begin{tabular}{@ {}l@ {\quad}l@ {}} 

364 
@{term"app (app (Cons x xs) ys) zs"}\\ 

365 
@{text"= app (Cons x (app xs ys)) zs"} & by definition of @{text app}\\ 

366 
@{text"= Cons x (app (app xs ys) zs)"} & by definition of @{text app}\\ 

367 
@{text"= Cons x (app xs (app ys zs))"} & by IH\\ 

368 
@{text"= app (Cons x xs) (app ys zs)"} & by definition of @{text app} 

369 
\end{tabular} 

370 
\end{itemize} 

371 
\medskip 

372 

373 
\noindent Didn't we say earlier that all proofs are by simplification? But 

374 
in both cases, going from left to right, the last equality step is not a 

375 
simplification at all! In the base case it is @{prop"app ys zs = app Nil (app 

376 
ys zs)"}. It appears almost mysterious because we suddenly complicate the 

377 
term by appending @{text Nil} on the left. What is really going on is this: 

378 
when proving some equality \mbox{@{prop"s = t"}}, both @{text s} and @{text t} are 

54467  379 
simplified until they ``meet in the middle''. This heuristic for equality proofs 
47269  380 
works well for a functional programming context like ours. In the base case 
54467  381 
both @{term"app (app Nil ys) zs"} and @{term"app Nil (app 
382 
ys zs)"} are simplified to @{term"app ys zs"}, the term in the middle. 

47269  383 

52361  384 
\subsection{Predefined Lists} 
47269  385 
\label{sec:predeflists} 
386 

387 
Isabelle's predefined lists are the same as the ones above, but with 

388 
more syntactic sugar: 

389 
\begin{itemize} 

55317  390 
\item @{text "[]"} is \indexed{@{const Nil}}{Nil}, 
391 
\item @{term"x # xs"} is @{term"Cons x xs"}\index{Cons@@{const Cons}}, 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52842
diff
changeset

392 
\item @{text"[x\<^sub>1, \<dots>, x\<^sub>n]"} is @{text"x\<^sub>1 # \<dots> # x\<^sub>n # []"}, and 
47269  393 
\item @{term "xs @ ys"} is @{term"app xs ys"}. 
394 
\end{itemize} 

395 
There is also a large library of predefined functions. 

396 
The most important ones are the length function 

55317  397 
@{text"length :: 'a list \<Rightarrow> nat"}\index{length@@{const length}} (with the obvious definition), 
398 
and the \indexed{@{const map}}{map} function that applies a function to all elements of a list: 

47269  399 
\begin{isabelle} 
59360  400 
\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \isacom{where}\\ 
59204
0cbe0a56d3fa
update map definition in Prog_Prove for new datatype package
kleing
parents:
58521
diff
changeset

401 
@{text"\""}@{thm list.map(1) [of f]}@{text"\" "}\\ 
0cbe0a56d3fa
update map definition in Prog_Prove for new datatype package
kleing
parents:
58521
diff
changeset

402 
@{text"\""}@{thm list.map(2) [of f x xs]}@{text"\""} 
47269  403 
\end{isabelle} 
52782  404 

405 
\ifsem 

47269  406 
Also useful are the \concept{head} of a list, its first element, 
407 
and the \concept{tail}, the rest of the list: 

55317  408 
\begin{isabelle}\index{hd@@{const hd}} 
47269  409 
\isacom{fun} @{text"hd :: 'a list \<Rightarrow> 'a"}\\ 
410 
@{prop"hd(x#xs) = x"} 

411 
\end{isabelle} 

55317  412 
\begin{isabelle}\index{tl@@{const tl}} 
47269  413 
\isacom{fun} @{text"tl :: 'a list \<Rightarrow> 'a list"}\\ 
414 
@{prop"tl [] = []"} @{text""}\\ 

415 
@{prop"tl(x#xs) = xs"} 

416 
\end{isabelle} 

417 
Note that since HOL is a logic of total functions, @{term"hd []"} is defined, 

418 
but we do now know what the result is. That is, @{term"hd []"} is not undefined 

419 
but underdefined. 

52782  420 
\fi 
47306  421 
% 
52593  422 

52842  423 
From now on lists are always the predefined lists. 
424 

425 

54436  426 
\subsection*{Exercises} 
52593  427 

428 
\begin{exercise} 

54121  429 
Use the \isacom{value} command to evaluate the following expressions: 
430 
@{term[source] "1 + (2::nat)"}, @{term[source] "1 + (2::int)"}, 

431 
@{term[source] "1  (2::nat)"} and @{term[source] "1  (2::int)"}. 

432 
\end{exercise} 

433 

434 
\begin{exercise} 

52842  435 
Start from the definition of @{const add} given above. 
54467  436 
Prove that @{const add} is associative and commutative. 
54121  437 
Define a recursive function @{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"} 
438 
and prove @{prop"double m = add m m"}. 

52593  439 
\end{exercise} 
52718  440 

52593  441 
\begin{exercise} 
52842  442 
Define a function @{text"count ::"} @{typ"'a \<Rightarrow> 'a list \<Rightarrow> nat"} 
443 
that counts the number of occurrences of an element in a list. Prove 

444 
@{prop"count x xs \<le> length xs"}. 

445 
\end{exercise} 

446 

447 
\begin{exercise} 

448 
Define a recursive function @{text "snoc ::"} @{typ"'a list \<Rightarrow> 'a \<Rightarrow> 'a list"} 

54121  449 
that appends an element to the end of a list. With the help of @{text snoc} 
450 
define a recursive function @{text "reverse ::"} @{typ"'a list \<Rightarrow> 'a list"} 

451 
that reverses a list. Prove @{prop"reverse(reverse xs) = xs"}. 

452 
\end{exercise} 

453 

454 
\begin{exercise} 

455 
Define a recursive function @{text "sum ::"} @{typ"nat \<Rightarrow> nat"} such that 

456 
\mbox{@{text"sum n"}} @{text"="} @{text"0 + ... + n"} and prove 

457 
@{prop" sum(n::nat) = n * (n+1) div 2"}. 

52593  458 
\end{exercise} 
47269  459 
*} 
460 
(*<*) 

461 
end 

462 
(*>*) 