1 \chapter{Functional Programming in HOL}
3 This chapter describes how to write
4 functional programs in HOL and how to verify them. However,
5 most of the constructs and
6 proof procedures introduced are general and recur in any specification
7 or verification task. We really should speak of functional
8 \emph{modelling} rather than functional \emph{programming}:
10 to write programs but to design abstract models of systems. HOL is
11 a specification language that goes well beyond what can be expressed as a
12 program. However, for the time being we concentrate on the computable.
14 If you are a purist functional programmer, please note that all functions
16 they must terminate for all inputs. Lazy data structures are not
19 \section{An Introductory Theory}
20 \label{sec:intro-theory}
22 Functional programming needs datatypes and functions. Both of them can be
23 defined in a theory with a syntax reminiscent of languages like ML or
24 Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.
25 We will now examine it line by line.
28 \begin{ttbox}\makeatother
29 \input{ToyList2/ToyList1}\end{ttbox}
30 \caption{A Theory of Lists}
34 \index{*ToyList example|(}
35 {\makeatother\input{ToyList/document/ToyList.tex}}
37 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
38 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
39 constitutes the complete theory \texttt{ToyList} and should reside in file
40 \texttt{ToyList.thy}. It is good practice to present all declarations and
41 definitions at the beginning of a theory to facilitate browsing.%
42 \index{*ToyList example|)}
45 \begin{ttbox}\makeatother
46 \input{ToyList2/ToyList2}\end{ttbox}
47 \caption{Proofs about Lists}
48 \label{fig:ToyList-proofs}
51 \subsubsection*{Review}
53 This is the end of our toy proof. It should have familiarized you with
55 \item the standard theorem proving procedure:
56 state a goal (lemma or theorem); proceed with proof until a separate lemma is
57 required; prove that lemma; come back to the original goal.
58 \item a specific procedure that works well for functional programs:
59 induction followed by all-out simplification via \isa{auto}.
60 \item a basic repertoire of proof commands.
64 \section{Some Helpful Commands}
65 \label{sec:commands-and-hints}
67 This section discusses a few basic commands for manipulating the proof state
68 and can be skipped by casual readers.
70 There are two kinds of commands used during a proof: the actual proof
71 commands and auxiliary commands for examining the proof state and controlling
72 the display. Simple proof commands are of the form
73 \commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically
74 \isa{induct_tac} or \isa{auto}. All such theorem proving operations
75 are referred to as \bfindex{methods}, and further ones are
76 introduced throughout the tutorial. Unless stated otherwise, you may
77 assume that a method attacks merely the first subgoal. An exception is
78 \isa{auto}, which tries to solve all subgoals.
80 The most useful auxiliary commands are as follows:
82 \item[Undoing:] \commdx{undo} undoes the effect of
84 last command; \isacommand{undo} can be undone by
85 \commdx{redo}. Both are only needed at the shell
86 level and should not occur in the final theory.
87 \item[Printing the current state:] \commdx{pr}
89 the current proof state, for example when it has scrolled past the top of
91 \item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
92 print only the first $n$ subgoals from now on and redisplays the current
93 proof state. This is helpful when there are many subgoals.
94 \item[Modifying the order of subgoals:]
95 \commdx{defer} moves the first subgoal to the end and
96 \commdx{prefer}~$n$ moves subgoal $n$ to the front.
97 \item[Printing theorems:]
98 \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
99 prints the named theorems.
100 \item[Displaying types:] We have already mentioned the flag
101 \texttt{show_types} above.\index{*show_types (flag)}
102 It can also be useful for detecting misspellings in
103 formulae. For example, if \texttt{show_types} is set and the goal
104 \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
107 Variables:\isanewline
111 which tells us that Isabelle has correctly inferred that
112 \isa{xs} is a variable of list type. On the other hand, had we
113 made a typo as in \isa{rev(re xs) = xs}, the response
116 Variables:\isanewline
117 ~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
121 would have alerted us because of the unexpected variable \isa{re}.
122 \item[Reading terms and types:] \commdx{term}
123 \textit{string} reads, type-checks and prints the given string as a term in
124 the current context; the inferred type is output as well.
125 \commdx{typ} \textit{string} reads and prints the given
126 string as a type in the current context.
127 \item[(Re)loading theories:] When you start your interaction you must open a
128 named theory with the line \commdx{theory}~\isa{T~=~\dots~:}. Isabelle
129 automatically loads all the required parent theories from their respective
130 files (which may take a moment, unless the theories are already loaded and
131 the files have not been modified).
133 If you suddenly discover that you need to modify a parent theory of your
134 current theory, you must first abandon your current theory%
135 \indexbold{abandoning a theory}\indexbold{theories!abandoning}
137 level type \commdx{kill}). After the parent theory has
138 been modified, you go back to your original theory. When its first line
139 \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
140 modified parent is reloaded automatically.
142 % The only time when you need to load a theory by hand is when you simply
143 % want to check if it loads successfully without wanting to make use of the
144 % theory itself. This you can do by typing
145 % \isa{\commdx{use\_thy}~"T"}.
147 Further commands are found in the Isabelle/Isar Reference Manual.
149 We now examine Isabelle's functional programming constructs systematically,
150 starting with inductive datatypes.
157 Inductive datatypes are part of almost every non-trivial application of HOL.
158 First we take another look at an important example, the datatype of
159 lists, before we turn to datatypes in general. The section closes with a
165 \index{*list (type)}%
166 Lists are one of the essential datatypes in computing. We expect that you
167 are already familiar with their basic operations.
168 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
169 \thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
170 The latter contains many further operations. For example, the functions
171 \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
172 element and the remainder of a list. (However, pattern-matching is usually
173 preferable to \isa{hd} and \isa{tl}.)
174 Also available are higher-order functions like \isa{map} and \isa{filter}.
175 Theory \isa{List} also contains
176 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
177 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we
178 always use HOL's predefined lists.
181 \subsection{The General Format}
182 \label{sec:general-datatype}
184 The general HOL \isacommand{datatype} definition is of the form
186 \isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
187 C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
188 C@m~\tau@{m1}~\dots~\tau@{mk@m}
190 where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct
191 constructor names and $\tau@{ij}$ are types; it is customary to capitalize
192 the first letter in constructor names. There are a number of
193 restrictions (such as that the type should not be empty) detailed
194 elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
196 Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and
197 \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically
198 during proofs by simplification. The same is true for the equations in
199 primitive recursive function definitions.
201 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
202 the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
203 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
204 1}. In general, \cdx{size} returns
206 \item zero for all constructors
207 that do not have an argument of type $t$\\
208 \item one plus the sum of the sizes of all arguments of type~$t$,
209 for all other constructors
212 \isa{size} is defined on every datatype, it is overloaded; on lists
213 \isa{size} is also called \sdx{length}, which is not overloaded.
214 Isabelle will always show \isa{size} on lists as \isa{length}.
217 \subsection{Primitive Recursion}
219 \index{recursion!primitive}%
220 Functions on datatypes are usually defined by recursion. In fact, most of the
221 time they are defined by what is called \textbf{primitive recursion}.
222 The keyword \commdx{primrec} is followed by a list of
224 \[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
225 such that $C$ is a constructor of the datatype $t$ and all recursive calls of
226 $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
227 Isabelle immediately sees that $f$ terminates because one (fixed!) argument
228 becomes smaller with every recursive call. There must be at most one equation
229 for each constructor. Their order is immaterial.
230 A more general method for defining total recursive functions is introduced in
231 {\S}\ref{sec:recdef}.
233 \begin{exercise}\label{ex:Tree}
234 \input{Misc/document/Tree.tex}%
237 \input{Misc/document/case_exprs.tex}
239 \input{Ifexpr/document/Ifexpr.tex}
243 \section{Some Basic Types}
245 This section introduces the types of natural numbers and ordered pairs. Also
246 described is type \isa{option}, which is useful for modelling exceptional
249 \subsection{Natural Numbers}
250 \label{sec:nat}\index{natural numbers}%
251 \index{linear arithmetic|(}
253 \input{Misc/document/fakenat.tex}
254 \input{Misc/document/natsum.tex}
256 \index{linear arithmetic|)}
260 \input{Misc/document/pairs.tex}
262 \subsection{Datatype {\tt\slshape option}}
264 \input{Misc/document/Option2.tex}
266 \section{Definitions}
267 \label{sec:Definitions}
269 A definition is simply an abbreviation, i.e.\ a new name for an existing
270 construction. In particular, definitions cannot be recursive. Isabelle offers
271 definitions on the level of types and terms. Those on the type level are
272 called \textbf{type synonyms}; those on the term level are simply called
276 \subsection{Type Synonyms}
278 \index{type synonyms|(}%
279 Type synonyms are similar to those found in ML\@. They are created by a
280 \commdx{types} command:
282 \input{Misc/document/types.tex}%
283 \index{type synonyms|)}
285 \input{Misc/document/prime_def.tex}
287 \input{Misc/document/Translations.tex}
290 \section{The Definitional Approach}
291 \label{sec:definitional}
293 \index{Definitional Approach}%
294 As we pointed out at the beginning of the chapter, asserting arbitrary
295 axioms such as $f(n) = f(n) + 1$ can easily lead to contradictions. In order
296 to avoid this danger, we advocate the definitional rather than
297 the axiomatic approach: introduce new concepts by definitions. However, Isabelle/HOL seems to
298 support many richer definitional constructs, such as
299 \isacommand{primrec}. The point is that Isabelle reduces such constructs to first principles. For example, each
300 \isacommand{primrec} function definition is turned into a proper
301 (nonrecursive!) definition from which the user-supplied recursion equations are
302 automatically proved. This process is
303 hidden from the user, who does not have to understand the details. Other commands described
304 later, like \isacommand{recdef} and \isacommand{inductive}, work similarly.
305 This strict adherence to the definitional approach reduces the risk of
308 \chapter{More Functional Programming}
310 The purpose of this chapter is to deepen your understanding of the
311 concepts encountered so far and to introduce advanced forms of datatypes and
312 recursive functions. The first two sections give a structured presentation of
313 theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss
314 important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). You can
315 skip them if you are not planning to perform proofs yourself.
316 We then present a case
317 study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
318 datatypes, including those involving function spaces, are covered in
319 {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
320 trees (``tries''). Finally we introduce \isacommand{recdef}, a general
321 form of recursive function definition that goes well beyond
322 \isacommand{primrec} ({\S}\ref{sec:recdef}).
325 \section{Simplification}
326 \label{sec:Simplification}
327 \index{simplification|(}
329 So far we have proved our theorems by \isa{auto}, which simplifies
330 all subgoals. In fact, \isa{auto} can do much more than that.
331 To go beyond toy examples, you
332 need to understand the ingredients of \isa{auto}. This section covers the
333 method that \isa{auto} always applies first, simplification.
335 Simplification is one of the central theorem proving tools in Isabelle and
336 many other systems. The tool itself is called the \textbf{simplifier}.
337 This section introduces the many features of the simplifier
338 and is required reading if you intend to perform proofs. Later on,
339 {\S}\ref{sec:simplification-II} explains some more advanced features and a
340 little bit of how the simplifier works. The serious student should read that
341 section as well, in particular to understand why the simplifier did
342 something unexpected.
344 \subsection{What is Simplification?}
346 In its most basic form, simplification means repeated application of
347 equations from left to right. For example, taking the rules for \isa{\at}
348 and applying them to the term \isa{[0,1] \at\ []} results in a sequence of
349 simplification steps:
350 \begin{ttbox}\makeatother
351 (0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[]
353 This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
354 equations are referred to as \bfindex{rewrite rules}.
355 ``Rewriting'' is more honest than ``simplification'' because the terms do not
356 necessarily become simpler in the process.
358 The simplifier proves arithmetic goals as described in
359 {\S}\ref{sec:nat} above. Arithmetic expressions are simplified using built-in
360 procedures that go beyond mere rewrite rules. New simplification procedures
361 can be coded and installed, but they are definitely not a matter for this
364 \input{Misc/document/simp.tex}
366 \index{simplification|)}
368 \input{Misc/document/Itrev.tex}
371 \input{Misc/document/Tree2.tex}%
374 \input{CodeGen/document/CodeGen.tex}
377 \section{Advanced Datatypes}
378 \label{sec:advanced-datatypes}
379 \index{datatype@\isacommand {datatype} (command)|(}
380 \index{primrec@\isacommand {primrec} (command)|(}
383 This section presents advanced forms of datatypes: mutual and nested
384 recursion. A series of examples will culminate in a treatment of the trie
388 \subsection{Mutual Recursion}
389 \label{sec:datatype-mut-rec}
391 \input{Datatype/document/ABexpr.tex}
393 \subsection{Nested Recursion}
394 \label{sec:nested-datatype}
396 {\makeatother\input{Datatype/document/Nested.tex}}
399 \subsection{The Limits of Nested Recursion}
401 How far can we push nested recursion? By the unfolding argument above, we can
402 reduce nested to mutual recursion provided the nested recursion only involves
403 previously defined datatypes. This does not include functions:
405 \isacommand{datatype} t = C "t \isasymRightarrow\ bool"
407 This declaration is a real can of worms.
408 In HOL it must be ruled out because it requires a type
409 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
410 same cardinality --- an impossibility. For the same reason it is not possible
411 to allow recursion involving the type \isa{set}, which is isomorphic to
412 \isa{t \isasymFun\ bool}.
414 Fortunately, a limited form of recursion
415 involving function spaces is permitted: the recursive type may occur on the
416 right of a function arrow, but never on the left. Hence the above can of worms
417 is ruled out but the following example of a potentially
418 \index{infinitely branching trees}%
419 infinitely branching tree is accepted:
422 \input{Datatype/document/Fundata.tex}
424 If you need nested recursion on the left of a function arrow, there are
425 alternatives to pure HOL\@. In the Logic for Computable Functions
426 (\rmindex{LCF}), types like
428 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
430 do indeed make sense~\cite{paulson87}. Note the different arrow,
431 \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
432 expressing the type of \emph{continuous} functions.
433 There is even a version of LCF on top of HOL,
434 called \rmindex{HOLCF}~\cite{MuellerNvOS99}.
435 \index{datatype@\isacommand {datatype} (command)|)}
436 \index{primrec@\isacommand {primrec} (command)|)}
439 \subsection{Case Study: Tries}
443 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
444 indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
445 trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
446 ``cat''. When searching a string in a trie, the letters of the string are
447 examined sequentially. Each letter determines which subtrie to search next.
448 In this case study we model tries as a datatype, define a lookup and an
449 update function, and prove that they behave as expected.
454 \begin{picture}(60,30)
455 \put( 5, 0){\makebox(0,0)[b]{l}}
456 \put(25, 0){\makebox(0,0)[b]{e}}
457 \put(35, 0){\makebox(0,0)[b]{n}}
458 \put(45, 0){\makebox(0,0)[b]{r}}
459 \put(55, 0){\makebox(0,0)[b]{t}}
461 \put( 5, 9){\line(0,-1){5}}
462 \put(25, 9){\line(0,-1){5}}
463 \put(44, 9){\line(-3,-2){9}}
464 \put(45, 9){\line(0,-1){5}}
465 \put(46, 9){\line(3,-2){9}}
467 \put( 5,10){\makebox(0,0)[b]{l}}
468 \put(15,10){\makebox(0,0)[b]{n}}
469 \put(25,10){\makebox(0,0)[b]{p}}
470 \put(45,10){\makebox(0,0)[b]{a}}
472 \put(14,19){\line(-3,-2){9}}
473 \put(15,19){\line(0,-1){5}}
474 \put(16,19){\line(3,-2){9}}
475 \put(45,19){\line(0,-1){5}}
477 \put(15,20){\makebox(0,0)[b]{a}}
478 \put(45,20){\makebox(0,0)[b]{c}}
480 \put(30,30){\line(-3,-2){13}}
481 \put(30,30){\line(3,-2){13}}
484 \caption{A Sample Trie}
488 Proper tries associate some value with each string. Since the
489 information is stored only in the final node associated with the string, many
490 nodes do not carry any value. This distinction is modeled with the help
491 of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
492 \input{Trie/document/Trie.tex}
495 \section{Total Recursive Functions}
497 \index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
499 Although many total functions have a natural primitive recursive definition,
500 this is not always the case. Arbitrary total recursive functions can be
501 defined by means of \isacommand{recdef}: you can use full pattern-matching,
502 recursion need not involve datatypes, and termination is proved by showing
503 that the arguments of all recursive calls are smaller in a suitable (user
504 supplied) sense. In this section we restrict ourselves to measure functions;
505 more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
507 \subsection{Defining Recursive Functions}
508 \label{sec:recdef-examples}
509 \input{Recdef/document/examples.tex}
511 \subsection{Proving Termination}
513 \input{Recdef/document/termination.tex}
515 \subsection{Simplification and Recursive Functions}
516 \label{sec:recdef-simplification}
518 \input{Recdef/document/simplification.tex}
520 \subsection{Induction and Recursive Functions}
521 \index{induction!recursion|(}
522 \index{recursion induction|(}
524 \input{Recdef/document/Induction.tex}
525 \label{sec:recdef-induction}
527 \index{induction!recursion|)}
528 \index{recursion induction|)}
529 \index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}