1 \chapter{Functional Programming in HOL}
3 Although on the surface this chapter is mainly concerned with how to write
4 functional programs in HOL and how to verify them, most of the
5 constructs and proof procedures introduced are general purpose and recur in
6 any specification or verification task.
8 The dedicated functional programmer should be warned: HOL offers only
9 \emph{total functional programming} --- all functions in HOL must be total;
10 lazy data structures are not directly available. On the positive side,
11 functions in HOL need not be computable: HOL is a specification language that
12 goes well beyond what can be expressed as a program. However, for the time
13 being we concentrate on the computable.
15 \section{An introductory theory}
16 \label{sec:intro-theory}
18 Functional programming needs datatypes and functions. Both of them can be
19 defined in a theory with a syntax reminiscent of languages like ML or
20 Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.
21 We will now examine it line by line.
24 \begin{ttbox}\makeatother
25 \input{ToyList2/ToyList1}\end{ttbox}
26 \caption{A theory of lists}
30 {\makeatother\input{ToyList/document/ToyList.tex}}
32 The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The
33 concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs}
34 constitutes the complete theory \texttt{ToyList} and should reside in file
35 \texttt{ToyList.thy}. It is good practice to present all declarations and
36 definitions at the beginning of a theory to facilitate browsing.
39 \begin{ttbox}\makeatother
40 \input{ToyList2/ToyList2}\end{ttbox}
41 \caption{Proofs about lists}
42 \label{fig:ToyList-proofs}
45 \subsubsection*{Review}
47 This is the end of our toy proof. It should have familiarized you with
49 \item the standard theorem proving procedure:
50 state a goal (lemma or theorem); proceed with proof until a separate lemma is
51 required; prove that lemma; come back to the original goal.
52 \item a specific procedure that works well for functional programs:
53 induction followed by all-out simplification via \isa{auto}.
54 \item a basic repertoire of proof commands.
58 \section{Some helpful commands}
59 \label{sec:commands-and-hints}
61 This section discusses a few basic commands for manipulating the proof state
62 and can be skipped by casual readers.
64 There are two kinds of commands used during a proof: the actual proof
65 commands and auxiliary commands for examining the proof state and controlling
66 the display. Simple proof commands are of the form
67 \isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a
68 synonym for ``theorem proving function''. Typical examples are
69 \isa{induct_tac} and \isa{auto}. Further methods are introduced throughout
70 the tutorial. Unless stated otherwise you may assume that a method attacks
71 merely the first subgoal. An exception is \isa{auto} which tries to solve all
74 The most useful auxiliary commands are:
76 \item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the
77 last command; \isacommand{undo} can be undone by
78 \isacommand{redo}\indexbold{*redo}. Both are only needed at the shell
79 level and should not occur in the final theory.
80 \item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays
81 the current proof state, for example when it has disappeared off the
83 \item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
84 print only the first $n$ subgoals from now on and redisplays the current
85 proof state. This is helpful when there are many subgoals.
86 \item[Modifying the order of subgoals:]
87 \isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and
88 \isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front.
89 \item[Printing theorems:]
90 \isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
91 prints the named theorems.
92 \item[Displaying types:] We have already mentioned the flag
93 \ttindex{show_types} above. It can also be useful for detecting typos in
94 formulae early on. For example, if \texttt{show_types} is set and the goal
95 \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
102 which tells us that Isabelle has correctly inferred that
103 \isa{xs} is a variable of list type. On the other hand, had we
104 made a typo as in \isa{rev(re xs) = xs}, the response
107 Variables:\isanewline
108 ~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
112 would have alerted us because of the unexpected variable \isa{re}.
113 \item[Reading terms and types:] \isacommand{term}\indexbold{*term}
114 \textit{string} reads, type-checks and prints the given string as a term in
115 the current context; the inferred type is output as well.
116 \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given
117 string as a type in the current context.
118 \item[(Re)loading theories:] When you start your interaction you must open a
119 named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
120 automatically loads all the required parent theories from their respective
121 files (which may take a moment, unless the theories are already loaded and
122 the files have not been modified).
124 If you suddenly discover that you need to modify a parent theory of your
125 current theory you must first abandon your current theory\indexbold{abandon
126 theory}\indexbold{theory!abandon} (at the shell
127 level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
128 been modified you go back to your original theory. When its first line
129 \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
130 modified parent is reloaded automatically.
132 The only time when you need to load a theory by hand is when you simply
133 want to check if it loads successfully without wanting to make use of the
134 theory itself. This you can do by typing
135 \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
137 Further commands are found in the Isabelle/Isar Reference Manual.
139 We now examine Isabelle's functional programming constructs systematically,
140 starting with inductive datatypes.
146 Inductive datatypes are part of almost every non-trivial application of HOL.
147 First we take another look at a very important example, the datatype of
148 lists, before we turn to datatypes in general. The section closes with a
155 Lists are one of the essential datatypes in computing. Readers of this
156 tutorial and users of HOL need to be familiar with their basic operations.
157 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
158 \isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
159 The latter contains many further operations. For example, the functions
160 \isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
161 element and the remainder of a list. (However, pattern-matching is usually
162 preferable to \isa{hd} and \isa{tl}.) Theory \isa{List} also contains
163 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
164 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we
165 always use HOL's predefined lists.
168 \subsection{The general format}
169 \label{sec:general-datatype}
171 The general HOL \isacommand{datatype} definition is of the form
173 \isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
174 C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
175 C@m~\tau@{m1}~\dots~\tau@{mk@m}
177 where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct
178 constructor names and $\tau@{ij}$ are types; it is customary to capitalize
179 the first letter in constructor names. There are a number of
180 restrictions (such as that the type should not be empty) detailed
181 elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
183 Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and
184 \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically
185 during proofs by simplification. The same is true for the equations in
186 primitive recursive function definitions.
188 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
189 the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is
190 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
191 1}. In general, \isa{size} returns \isa{0} for all constructors that do
192 not have an argument of type $t$, and for all other constructors \isa{1 +}
193 the sum of the sizes of all arguments of type $t$. Note that because
194 \isa{size} is defined on every datatype, it is overloaded; on lists
195 \isa{size} is also called \isa{length}, which is not overloaded.
198 \subsection{Primitive recursion}
200 Functions on datatypes are usually defined by recursion. In fact, most of the
201 time they are defined by what is called \bfindex{primitive recursion}.
202 The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of
204 \[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
205 such that $C$ is a constructor of the datatype $t$ and all recursive calls of
206 $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
207 Isabelle immediately sees that $f$ terminates because one (fixed!) argument
208 becomes smaller with every recursive call. There must be exactly one equation
209 for each constructor. Their order is immaterial.
210 A more general method for defining total recursive functions is introduced in
213 \begin{exercise}\label{ex:Tree}
214 \input{Misc/document/Tree.tex}%
217 \input{Misc/document/case_exprs.tex}
220 Induction is only allowed on free (or \isasymAnd-bound) variables that
221 should not occur among the assumptions of the subgoal; see
222 \S\ref{sec:ind-var-in-prems} for details. Case distinction
223 (\isa{case_tac}) works for arbitrary terms, which need to be
224 quoted if they are non-atomic.
228 \subsection{Case study: boolean expressions}
231 The aim of this case study is twofold: it shows how to model boolean
232 expressions and some algorithms for manipulating them, and it demonstrates
233 the constructs introduced above.
235 \input{Ifexpr/document/Ifexpr.tex}
238 How does one come up with the required lemmas? Try to prove the main theorems
239 without them and study carefully what \isa{auto} leaves unproved. This has
240 to provide the clue. The necessity of universal quantification
241 (\isa{\isasymforall{}t e}) in the two lemmas is explained in
242 \S\ref{sec:InductionHeuristics}
245 We strengthen the definition of a \isa{normal} If-expression as follows:
246 the first argument of all \isa{IF}s must be a variable. Adapt the above
247 development to this changed requirement. (Hint: you may need to formulate
248 some of the goals as implications (\isasymimp) rather than equalities
252 \section{Some basic types}
255 \subsection{Natural numbers}
259 \input{Misc/document/fakenat.tex}
260 \input{Misc/document/natsum.tex}
262 The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
263 \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},
264 \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
265 \isaindexbold{max} are predefined, as are the relations
266 \indexboldpos{\isasymle}{$HOL2arithrel} and
267 \ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
268 \isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although
269 Isabelle does not prove this completely automatically. Note that \isa{1} and
270 \isa{2} are available as abbreviations for the corresponding
271 \isa{Suc}-expressions. If you need the full set of numerals,
272 see~\S\ref{nat-numerals}.
275 The constant \ttindexbold{0} and the operations
276 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
277 \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max},
278 \indexboldpos{\isasymle}{$HOL2arithrel} and
279 \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
280 not just for natural numbers but at other types as well (see
281 \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there
282 is nothing to indicate that you are talking about natural numbers. Hence
283 Isabelle can only infer that \isa{x} is of some arbitrary type where
284 \isa{0} and \isa{+} are declared. As a consequence, you will be unable to
285 prove the goal (although it may take you some time to realize what has
286 happened if \texttt{show_types} is not set). In this particular example,
287 you need to include an explicit type constraint, for example \isa{x+0 =
288 (x::nat)}. If there is enough contextual information this may not be
289 necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because
290 \isa{Suc} is not overloaded.
293 Simple arithmetic goals are proved automatically by both \isa{auto}
294 and the simplification methods introduced in \S\ref{sec:Simplification}. For
297 \input{Misc/document/arith1.tex}%
298 is proved automatically. The main restriction is that only addition is taken
299 into account; other arithmetic operations and quantified formulae are ignored.
301 For more complex goals, there is the special method
302 \isaindexbold{arith} (which attacks the first subgoal). It proves
303 arithmetic goals involving the usual logical connectives (\isasymnot,
304 \isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and
305 the operations \isa{+}, \isa{-}, \isa{min} and \isa{max}. For example,
307 \input{Misc/document/arith2.tex}%
308 succeeds because \isa{k*k} can be treated as atomic.
311 \input{Misc/document/arith3.tex}%
312 is not even proved by \isa{arith} because the proof relies essentially
313 on properties of multiplication.
316 The running time of \isa{arith} is exponential in the number of occurrences
317 of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
318 \isaindexbold{max} because they are first eliminated by case distinctions.
320 \isa{arith} is incomplete even for the restricted class of formulae
321 described above (known as ``linear arithmetic''). If divisibility plays a
322 role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$.
323 Fortunately, such examples are rare in practice.
329 \subsection{Products}
330 \input{Misc/document/pairs.tex}
332 %FIXME move stuff below into section on proofs about products?
334 Abstraction over pairs and tuples is merely a convenient shorthand for a
335 more complex internal representation. Thus the internal and external form
336 of a term may differ, which can affect proofs. If you want to avoid this
337 complication, use \isa{fst} and \isa{snd}, i.e.\ write
338 \isa{\isasymlambda{}p.~fst p + snd p} instead of
339 \isa{\isasymlambda(x,y).~x + y}. See~\S\ref{proofs-about-products} for
340 theorem proving with tuple patterns.
343 Note that products, like natural numbers, are datatypes, which means
344 in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
345 products (see \S\ref{proofs-about-products}).
347 Instead of tuples with many components (where ``many'' is not much above 2),
348 it is far preferable to use record types (see \S\ref{sec:records}).
350 \section{Definitions}
351 \label{sec:Definitions}
353 A definition is simply an abbreviation, i.e.\ a new name for an existing
354 construction. In particular, definitions cannot be recursive. Isabelle offers
355 definitions on the level of types and terms. Those on the type level are
356 called type synonyms, those on the term level are called (constant)
360 \subsection{Type synonyms}
361 \indexbold{type synonym}
363 Type synonyms are similar to those found in ML. Their syntax is fairly self
366 \input{Misc/document/types.tex}%
368 Note that pattern-matching is not allowed, i.e.\ each definition must be of
369 the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
370 Section~\S\ref{sec:Simplification} explains how definitions are used
374 A common mistake when writing definitions is to introduce extra free
375 variables on the right-hand side as in the following fictitious definition:
376 \input{Misc/document/prime_def.tex}%
380 \chapter{More Functional Programming}
382 The purpose of this chapter is to deepen the reader's understanding of the
383 concepts encountered so far and to introduce advanced forms of datatypes and
384 recursive functions. The first two sections give a structured presentation of
385 theorem proving by simplification (\S\ref{sec:Simplification}) and discuss
386 important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can
387 be skipped by readers less interested in proofs. They are followed by a case
388 study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced
389 datatypes, including those involving function spaces, are covered in
390 \S\ref{sec:advanced-datatypes}, which closes with another case study, search
391 trees (``tries''). Finally we introduce \isacommand{recdef}, a very general
392 form of recursive function definition which goes well beyond what
393 \isacommand{primrec} allows (\S\ref{sec:recdef}).
396 \section{Simplification}
397 \label{sec:Simplification}
398 \index{simplification|(}
400 So far we have proved our theorems by \isa{auto}, which ``simplifies''
401 \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
402 that it did not need to so far. However, when you go beyond toy examples, you
403 need to understand the ingredients of \isa{auto}. This section covers the
404 method that \isa{auto} always applies first, namely simplification.
406 Simplification is one of the central theorem proving tools in Isabelle and
407 many other systems. The tool itself is called the \bfindex{simplifier}. The
408 purpose of this section is twofold: to introduce the many features of the
409 simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the
410 simplifier works (\S\ref{sec:SimpHow}). Anybody intending to use HOL should
411 read \S\ref{sec:SimpFeatures}, and the serious student should read
412 \S\ref{sec:SimpHow} as well in order to understand what happened in case
413 things do not simplify as expected.
416 \subsection{Using the simplifier}
417 \label{sec:SimpFeatures}
419 \subsubsection{What is simplification}
421 In its most basic form, simplification means repeated application of
422 equations from left to right. For example, taking the rules for \isa{\at}
423 and applying them to the term \isa{[0,1] \at\ []} results in a sequence of
424 simplification steps:
425 \begin{ttbox}\makeatother
426 (0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[]
428 This is also known as \bfindex{term rewriting} and the equations are referred
429 to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
430 because the terms do not necessarily become simpler in the process.
432 \subsubsection{Simplification rules}
433 \indexbold{simplification rules}
435 To facilitate simplification, theorems can be declared to be simplification
436 rules (with the help of the attribute \isa{[simp]}\index{*simp
437 (attribute)}), in which case proofs by simplification make use of these
438 rules automatically. In addition the constructs \isacommand{datatype} and
439 \isacommand{primrec} (and a few others) invisibly declare useful
440 simplification rules. Explicit definitions are \emph{not} declared
441 simplification rules automatically!
443 Not merely equations but pretty much any theorem can become a simplification
444 rule. The simplifier will try to make sense of it. For example, a theorem
445 \isasymnot$P$ is automatically turned into \isa{$P$ = False}. The details
446 are explained in \S\ref{sec:SimpHow}.
448 The simplification attribute of theorems can be turned on and off as follows:
450 lemmas [simp] = \(list of theorem names\);
451 lemmas [simp del] = \(list of theorem names\);
453 As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) =
454 xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification
455 rules. Those of a more specific nature (e.g.\ distributivity laws, which
456 alter the structure of terms considerably) should only be used selectively,
457 i.e.\ they should not be default simplification rules. Conversely, it may
458 also happen that a simplification rule needs to be disabled in certain
459 proofs. Frequent changes in the simplification status of a theorem may
460 indicate a badly designed theory.
462 Simplification may not terminate, for example if both $f(x) = g(x)$ and
463 $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
464 to include simplification rules that can lead to nontermination, either on
465 their own or in combination with other simplification rules.
468 \subsubsection{The simplification method}
469 \index{*simp (method)|bold}
471 The general format of the simplification method is
473 simp \(list of modifiers\)
475 where the list of \emph{modifiers} helps to fine tune the behaviour and may
476 be empty. Most if not all of the proofs seen so far could have been performed
477 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
478 only the first subgoal and may thus need to be repeated---use \isaindex{simp_all}
479 to simplify all subgoals.
480 Note that \isa{simp} fails if nothing changes.
482 \subsubsection{Adding and deleting simplification rules}
484 If a certain theorem is merely needed in a few proofs by simplification,
485 we do not need to make it a global simplification rule. Instead we can modify
486 the set of simplification rules used in a simplification step by adding rules
487 to it and/or deleting rules from it. The two modifiers for this are
489 add: \(list of theorem names\)
490 del: \(list of theorem names\)
492 In case you want to use only a specific list of theorems and ignore all
495 only: \(list of theorem names\)
499 \subsubsection{Assumptions}
500 \index{simplification!with/of assumptions}
502 {\makeatother\input{Misc/document/asm_simp.tex}}
504 \subsubsection{Rewriting with definitions}
505 \index{simplification!with definitions}
507 \input{Misc/document/def_rewr.tex}
510 If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
511 occurrences of $f$ with at least two arguments. Thus it is safer to define
512 $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
515 \subsubsection{Simplifying let-expressions}
516 \index{simplification!of let-expressions}
518 Proving a goal containing \isaindex{let}-expressions almost invariably
519 requires the \isa{let}-con\-structs to be expanded at some point. Since
520 \isa{let}-\isa{in} is just syntactic sugar for a predefined constant (called
521 \isa{Let}), expanding \isa{let}-constructs means rewriting with
524 {\makeatother\input{Misc/document/let_rewr.tex}}
526 \subsubsection{Conditional equations}
528 \input{Misc/document/cond_rewr.tex}
531 \subsubsection{Automatic case splits}
532 \indexbold{case splits}
535 {\makeatother\input{Misc/document/case_splits.tex}}
539 The simplifier merely simplifies the condition of an \isa{if} but not the
540 \isa{then} or \isa{else} parts. The latter are simplified only after the
541 condition reduces to \isa{True} or \isa{False}, or after splitting. The
542 same is true for \isaindex{case}-expressions: only the selector is
543 simplified at first, until either the expression reduces to one of the
544 cases or it is split.
547 \subsubsection{Arithmetic}
550 The simplifier routinely solves a small class of linear arithmetic formulae
551 (over type \isa{nat} and other numeric types): it only takes into account
552 assumptions and conclusions that are (possibly negated) (in)equalities
553 (\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus
555 \input{Misc/document/arith1.tex}%
556 is proved by simplification, whereas the only slightly more complex
558 \input{Misc/document/arith4.tex}%
559 is not proved by simplification and requires \isa{arith}.
561 \subsubsection{Tracing}
562 \indexbold{tracing the simplifier}
564 {\makeatother\input{Misc/document/trace_simp.tex}}
566 \index{simplification|)}
568 \section{Induction heuristics}
569 \label{sec:InductionHeuristics}
571 The purpose of this section is to illustrate some simple heuristics for
572 inductive proofs. The first one we have already mentioned in our initial
575 {\em 1. Theorems about recursive functions are proved by induction.}
577 In case the function has more than one argument
579 {\em 2. Do induction on argument number $i$ if the function is defined by
580 recursion in argument number $i$.}
582 When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
583 zs)}} in \S\ref{sec:intro-proof} we find (a) \isa{\at} is recursive in
584 the first argument, (b) \isa{xs} occurs only as the first argument of
585 \isa{\at}, and (c) both \isa{ys} and \isa{zs} occur at least once as
586 the second argument of \isa{\at}. Hence it is natural to perform induction
589 The key heuristic, and the main point of this section, is to
590 generalize the goal before induction. The reason is simple: if the goal is
591 too specific, the induction hypothesis is too weak to allow the induction
592 step to go through. Let us now illustrate the idea with an example.
594 {\makeatother\input{Misc/document/Itrev.tex}}
596 A final point worth mentioning is the orientation of the equation we just
597 proved: the more complex notion (\isa{itrev}) is on the left-hand
598 side, the simpler \isa{rev} on the right-hand side. This constitutes
599 another, albeit weak heuristic that is not restricted to induction:
601 {\em 5. The right-hand side of an equation should (in some sense) be
602 simpler than the left-hand side.}
604 The heuristic is tricky to apply because it is not obvious that
605 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
606 happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
609 \input{Misc/document/Tree2.tex}%
612 \section{Case study: compiling expressions}
613 \label{sec:ExprCompiler}
615 {\makeatother\input{CodeGen/document/CodeGen.tex}}
618 \section{Advanced datatypes}
619 \label{sec:advanced-datatypes}
624 This section presents advanced forms of \isacommand{datatype}s.
626 \subsection{Mutual recursion}
627 \label{sec:datatype-mut-rec}
629 \input{Datatype/document/ABexpr.tex}
631 \subsection{Nested recursion}
632 \label{sec:nested-datatype}
634 {\makeatother\input{Datatype/document/Nested.tex}}
637 \subsection{The limits of nested recursion}
639 How far can we push nested recursion? By the unfolding argument above, we can
640 reduce nested to mutual recursion provided the nested recursion only involves
641 previously defined datatypes. This does not include functions:
643 datatype t = C (t => bool)
645 is a real can of worms: in HOL it must be ruled out because it requires a type
646 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
647 same cardinality---an impossibility. For the same reason it is not possible
648 to allow recursion involving the type \isa{set}, which is isomorphic to
649 \isa{t \isasymFun\ bool}.
651 Fortunately, a limited form of recursion
652 involving function spaces is permitted: the recursive type may occur on the
653 right of a function arrow, but never on the left. Hence the above can of worms
654 is ruled out but the following example of a potentially infinitely branching tree is
658 \input{Datatype/document/Fundata.tex}
661 If you need nested recursion on the left of a function arrow,
662 there are alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like
664 datatype lam = C (lam -> lam)
666 do indeed make sense (note the intentionally different arrow \isa{->}).
667 There is even a version of LCF on top of HOL, called
668 HOLCF~\cite{MuellerNvOS99}.
673 \subsection{Case study: Tries}
675 Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
676 indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
677 trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
678 ``cat''. When searching a string in a trie, the letters of the string are
679 examined sequentially. Each letter determines which subtrie to search next.
680 In this case study we model tries as a datatype, define a lookup and an
681 update function, and prove that they behave as expected.
686 \begin{picture}(60,30)
687 \put( 5, 0){\makebox(0,0)[b]{l}}
688 \put(25, 0){\makebox(0,0)[b]{e}}
689 \put(35, 0){\makebox(0,0)[b]{n}}
690 \put(45, 0){\makebox(0,0)[b]{r}}
691 \put(55, 0){\makebox(0,0)[b]{t}}
693 \put( 5, 9){\line(0,-1){5}}
694 \put(25, 9){\line(0,-1){5}}
695 \put(44, 9){\line(-3,-2){9}}
696 \put(45, 9){\line(0,-1){5}}
697 \put(46, 9){\line(3,-2){9}}
699 \put( 5,10){\makebox(0,0)[b]{l}}
700 \put(15,10){\makebox(0,0)[b]{n}}
701 \put(25,10){\makebox(0,0)[b]{p}}
702 \put(45,10){\makebox(0,0)[b]{a}}
704 \put(14,19){\line(-3,-2){9}}
705 \put(15,19){\line(0,-1){5}}
706 \put(16,19){\line(3,-2){9}}
707 \put(45,19){\line(0,-1){5}}
709 \put(15,20){\makebox(0,0)[b]{a}}
710 \put(45,20){\makebox(0,0)[b]{c}}
712 \put(30,30){\line(-3,-2){13}}
713 \put(30,30){\line(3,-2){13}}
716 \caption{A sample trie}
720 Proper tries associate some value with each string. Since the
721 information is stored only in the final node associated with the string, many
722 nodes do not carry any value. This distinction is captured by the
723 following predefined datatype (from theory \isa{Option}, which is a parent
726 \input{Trie/document/Option2.tex}
727 \indexbold{*option}\indexbold{*None}\indexbold{*Some}%
728 \input{Trie/document/Trie.tex}
731 Write an improved version of \isa{update} that does not suffer from the
732 space leak in the version above. Prove the main theorem for your improved
737 Write a function to \emph{delete} entries from a trie. An easy solution is
738 a clever modification of \isa{update} which allows both insertion and
739 deletion with a single function. Prove (a modified version of) the main
740 theorem above. Optimize you function such that it shrinks tries after
741 deletion, if possible.
744 \section{Total recursive functions}
748 Although many total functions have a natural primitive recursive definition,
749 this is not always the case. Arbitrary total recursive functions can be
750 defined by means of \isacommand{recdef}: you can use full pattern-matching,
751 recursion need not involve datatypes, and termination is proved by showing
752 that the arguments of all recursive calls are smaller in a suitable (user
755 \subsection{Defining recursive functions}
757 \input{Recdef/document/examples.tex}
759 \subsection{Proving termination}
761 \input{Recdef/document/termination.tex}
763 \subsection{Simplification with recdef}
765 \input{Recdef/document/simplification.tex}
767 \subsection{Induction}
768 \index{induction!recursion|(}
769 \index{recursion induction|(}
771 \input{Recdef/document/Induction.tex}
772 \label{sec:recdef-induction}
774 \index{induction!recursion|)}
775 \index{recursion induction|)}
777 \subsection{Advanced forms of recursion}
778 \label{sec:advanced-recdef}
780 \input{Recdef/document/Nested0.tex}
781 \input{Recdef/document/Nested1.tex}
782 \input{Recdef/document/Nested2.tex}