doc-src/TutorialI/fp.tex
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 44049 9f9a40e778d6
child 48522 708278fc2dff
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
paulson@11419
     1
\chapter{Functional Programming in HOL}
paulson@11419
     2
paulson@11450
     3
This chapter describes how to write
paulson@11450
     4
functional programs in HOL and how to verify them.  However, 
paulson@11450
     5
most of the constructs and
paulson@11450
     6
proof procedures introduced are general and recur in any specification
paulson@11450
     7
or verification task.  We really should speak of functional
paulson@11450
     8
\emph{modelling} rather than functional \emph{programming}: 
paulson@11450
     9
our primary aim is not
paulson@11419
    10
to write programs but to design abstract models of systems.  HOL is
paulson@11419
    11
a specification language that goes well beyond what can be expressed as a
paulson@11419
    12
program. However, for the time being we concentrate on the computable.
paulson@11419
    13
paulson@11450
    14
If you are a purist functional programmer, please note that all functions
paulson@11450
    15
in HOL must be total:
paulson@11450
    16
they must terminate for all inputs.  Lazy data structures are not
paulson@11419
    17
directly available.
paulson@11419
    18
paulson@11419
    19
\section{An Introductory Theory}
paulson@11419
    20
\label{sec:intro-theory}
paulson@11419
    21
paulson@11419
    22
Functional programming needs datatypes and functions. Both of them can be
paulson@11419
    23
defined in a theory with a syntax reminiscent of languages like ML or
paulson@11419
    24
Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.
paulson@11419
    25
We will now examine it line by line.
paulson@11419
    26
paulson@11419
    27
\begin{figure}[htbp]
paulson@11419
    28
\begin{ttbox}\makeatother
paulson@11419
    29
\input{ToyList2/ToyList1}\end{ttbox}
paulson@11450
    30
\caption{A Theory of Lists}
paulson@11419
    31
\label{fig:ToyList}
paulson@11419
    32
\end{figure}
paulson@11419
    33
paulson@11457
    34
\index{*ToyList example|(}
wenzelm@17182
    35
{\makeatother\medskip\input{ToyList/document/ToyList.tex}}
paulson@11419
    36
paulson@11419
    37
The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
paulson@11419
    38
concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
paulson@11419
    39
constitutes the complete theory \texttt{ToyList} and should reside in file
nipkow@12327
    40
\texttt{ToyList.thy}.
nipkow@12327
    41
% It is good practice to present all declarations and
nipkow@12327
    42
%definitions at the beginning of a theory to facilitate browsing.%
paulson@11457
    43
\index{*ToyList example|)}
paulson@11419
    44
paulson@11419
    45
\begin{figure}[htbp]
paulson@11419
    46
\begin{ttbox}\makeatother
paulson@11419
    47
\input{ToyList2/ToyList2}\end{ttbox}
paulson@11450
    48
\caption{Proofs about Lists}
paulson@11419
    49
\label{fig:ToyList-proofs}
paulson@11419
    50
\end{figure}
paulson@11419
    51
paulson@11419
    52
\subsubsection*{Review}
paulson@11419
    53
paulson@11419
    54
This is the end of our toy proof. It should have familiarized you with
paulson@11419
    55
\begin{itemize}
paulson@11419
    56
\item the standard theorem proving procedure:
nipkow@8743
    57
state a goal (lemma or theorem); proceed with proof until a separate lemma is
nipkow@8743
    58
required; prove that lemma; come back to the original goal.
nipkow@8743
    59
\item a specific procedure that works well for functional programs:
nipkow@8743
    60
induction followed by all-out simplification via \isa{auto}.
nipkow@8743
    61
\item a basic repertoire of proof commands.
nipkow@8743
    62
\end{itemize}
nipkow@8743
    63
nipkow@12332
    64
\begin{warn}
nipkow@12332
    65
It is tempting to think that all lemmas should have the \isa{simp} attribute
nipkow@12332
    66
just because this was the case in the example above. However, in that example
nipkow@12332
    67
all lemmas were equations, and the right-hand side was simpler than the
nipkow@12332
    68
left-hand side --- an ideal situation for simplification purposes. Unless
nipkow@12332
    69
this is clearly the case, novices should refrain from awarding a lemma the
nipkow@12332
    70
\isa{simp} attribute, which has a global effect. Instead, lemmas can be
nipkow@12332
    71
applied locally where they are needed, which is discussed in the following
nipkow@12332
    72
chapter.
nipkow@12332
    73
\end{warn}
nipkow@8743
    74
paulson@10885
    75
\section{Some Helpful Commands}
nipkow@8743
    76
\label{sec:commands-and-hints}
nipkow@8743
    77
nipkow@8743
    78
This section discusses a few basic commands for manipulating the proof state
nipkow@8743
    79
and can be skipped by casual readers.
nipkow@8743
    80
nipkow@8743
    81
There are two kinds of commands used during a proof: the actual proof
nipkow@8743
    82
commands and auxiliary commands for examining the proof state and controlling
nipkow@8743
    83
the display. Simple proof commands are of the form
nipkow@12327
    84
\commdx{apply}(\textit{method}), where \textit{method} is typically 
paulson@11419
    85
\isa{induct_tac} or \isa{auto}.  All such theorem proving operations
paulson@11419
    86
are referred to as \bfindex{methods}, and further ones are
paulson@11419
    87
introduced throughout the tutorial.  Unless stated otherwise, you may
paulson@11419
    88
assume that a method attacks merely the first subgoal. An exception is
paulson@11419
    89
\isa{auto}, which tries to solve all subgoals.
nipkow@8743
    90
paulson@11419
    91
The most useful auxiliary commands are as follows:
nipkow@8743
    92
\begin{description}
nipkow@8743
    93
\item[Modifying the order of subgoals:]
paulson@11419
    94
\commdx{defer} moves the first subgoal to the end and
paulson@11419
    95
\commdx{prefer}~$n$ moves subgoal $n$ to the front.
nipkow@8743
    96
\item[Printing theorems:]
paulson@11419
    97
  \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
nipkow@8743
    98
  prints the named theorems.
paulson@11419
    99
\item[Reading terms and types:] \commdx{term}
nipkow@8743
   100
  \textit{string} reads, type-checks and prints the given string as a term in
nipkow@8743
   101
  the current context; the inferred type is output as well.
paulson@11419
   102
  \commdx{typ} \textit{string} reads and prints the given
nipkow@8743
   103
  string as a type in the current context.
nipkow@8743
   104
\end{description}
nipkow@12327
   105
Further commands are found in the Isabelle/Isar Reference
nipkow@12327
   106
Manual~\cite{isabelle-isar-ref}.
nipkow@8743
   107
nipkow@16412
   108
\begin{pgnote}
nipkow@16523
   109
Clicking on the \pgmenu{State} button redisplays the current proof state.
nipkow@16412
   110
This is helpful in case commands like \isacommand{thm} have overwritten it.
nipkow@16412
   111
\end{pgnote}
nipkow@16412
   112
nipkow@8771
   113
We now examine Isabelle's functional programming constructs systematically,
nipkow@8771
   114
starting with inductive datatypes.
nipkow@8771
   115
nipkow@8743
   116
nipkow@8743
   117
\section{Datatypes}
nipkow@8743
   118
\label{sec:datatype}
nipkow@8743
   119
paulson@11456
   120
\index{datatypes|(}%
nipkow@8743
   121
Inductive datatypes are part of almost every non-trivial application of HOL.
paulson@11458
   122
First we take another look at an important example, the datatype of
nipkow@8743
   123
lists, before we turn to datatypes in general. The section closes with a
nipkow@8743
   124
case study.
nipkow@8743
   125
nipkow@8743
   126
nipkow@8743
   127
\subsection{Lists}
nipkow@8743
   128
paulson@11428
   129
\index{*list (type)}%
paulson@11457
   130
Lists are one of the essential datatypes in computing.  We expect that you
paulson@11457
   131
are already familiar with their basic operations.
nipkow@8771
   132
Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
paulson@11428
   133
\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
nipkow@8743
   134
The latter contains many further operations. For example, the functions
paulson@11419
   135
\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
nipkow@25263
   136
element and the remainder of a list. (However, pattern matching is usually
paulson@10795
   137
preferable to \isa{hd} and \isa{tl}.)  
nipkow@10800
   138
Also available are higher-order functions like \isa{map} and \isa{filter}.
paulson@10795
   139
Theory \isa{List} also contains
nipkow@8743
   140
more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
nipkow@8743
   141
$x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
nipkow@12327
   142
always use HOL's predefined lists by building on theory \isa{Main}.
nipkow@27712
   143
\begin{warn}
nipkow@27712
   144
Looking ahead to sets and quanifiers in Part II:
nipkow@27712
   145
The best way to express that some element \isa{x} is in a list \isa{xs} is
nipkow@27712
   146
\isa{x $\in$ set xs}, where \isa{set} is a function that turns a list into the
nipkow@27712
   147
set of its elements.
nipkow@27712
   148
By the same device you can also write bounded quantifiers like
nipkow@27712
   149
\isa{$\forall$x $\in$ set xs} or embed lists in other set expressions.
nipkow@27712
   150
\end{warn}
nipkow@8743
   151
nipkow@8743
   152
paulson@10885
   153
\subsection{The General Format}
nipkow@8743
   154
\label{sec:general-datatype}
nipkow@8743
   155
nipkow@8743
   156
The general HOL \isacommand{datatype} definition is of the form
nipkow@8743
   157
\[
nipkow@8743
   158
\isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
nipkow@8743
   159
C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
nipkow@8743
   160
C@m~\tau@{m1}~\dots~\tau@{mk@m}
nipkow@8743
   161
\]
nipkow@8771
   162
where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct
nipkow@8743
   163
constructor names and $\tau@{ij}$ are types; it is customary to capitalize
nipkow@8743
   164
the first letter in constructor names. There are a number of
nipkow@8743
   165
restrictions (such as that the type should not be empty) detailed
nipkow@8743
   166
elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
nipkow@8743
   167
nipkow@8743
   168
Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and
nipkow@8743
   169
\isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically
nipkow@8743
   170
during proofs by simplification.  The same is true for the equations in
nipkow@8743
   171
primitive recursive function definitions.
nipkow@8743
   172
nipkow@12327
   173
Every\footnote{Except for advanced datatypes where the recursion involves
nipkow@12327
   174
``\isasymRightarrow'' as in {\S}\ref{sec:nested-fun-datatype}.} datatype $t$
nipkow@12327
   175
comes equipped with a \isa{size} function from $t$ into the natural numbers
nipkow@12327
   176
(see~{\S}\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\
nipkow@12327
   177
\isa{size [] = 0} and \isa{size(x \# xs) = size xs + 1}.  In general,
nipkow@12327
   178
\cdx{size} returns
paulson@11456
   179
\begin{itemize}
nipkow@27015
   180
\item zero for all constructors that do not have an argument of type $t$,
paulson@11457
   181
\item one plus the sum of the sizes of all arguments of type~$t$,
nipkow@27015
   182
for all other constructors.
paulson@11456
   183
\end{itemize}
paulson@11456
   184
Note that because
nipkow@9644
   185
\isa{size} is defined on every datatype, it is overloaded; on lists
paulson@11419
   186
\isa{size} is also called \sdx{length}, which is not overloaded.
paulson@10795
   187
Isabelle will always show \isa{size} on lists as \isa{length}.
nipkow@9644
   188
nipkow@9644
   189
paulson@10885
   190
\subsection{Primitive Recursion}
nipkow@8743
   191
paulson@11456
   192
\index{recursion!primitive}%
nipkow@8743
   193
Functions on datatypes are usually defined by recursion. In fact, most of the
nipkow@27015
   194
time they are defined by what is called \textbf{primitive recursion} over some
nipkow@27015
   195
datatype $t$. This means that the recursion equations must be of the form
nipkow@8743
   196
\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
nipkow@27015
   197
such that $C$ is a constructor of $t$ and all recursive calls of
nipkow@8743
   198
$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
nipkow@8743
   199
Isabelle immediately sees that $f$ terminates because one (fixed!) argument
nipkow@10654
   200
becomes smaller with every recursive call. There must be at most one equation
nipkow@8743
   201
for each constructor.  Their order is immaterial.
nipkow@8771
   202
A more general method for defining total recursive functions is introduced in
nipkow@25258
   203
{\S}\ref{sec:fun}.
nipkow@8743
   204
nipkow@9493
   205
\begin{exercise}\label{ex:Tree}
nipkow@8743
   206
\input{Misc/document/Tree.tex}%
nipkow@8743
   207
\end{exercise}
nipkow@8743
   208
nipkow@9721
   209
\input{Misc/document/case_exprs.tex}
nipkow@8743
   210
nipkow@8743
   211
\input{Ifexpr/document/Ifexpr.tex}
paulson@11456
   212
\index{datatypes|)}
paulson@11456
   213
nipkow@8743
   214
paulson@10885
   215
\section{Some Basic Types}
nipkow@8743
   216
paulson@11457
   217
This section introduces the types of natural numbers and ordered pairs.  Also
paulson@11457
   218
described is type \isa{option}, which is useful for modelling exceptional
paulson@11457
   219
cases. 
nipkow@8743
   220
paulson@10885
   221
\subsection{Natural Numbers}
paulson@11456
   222
\label{sec:nat}\index{natural numbers}%
paulson@11428
   223
\index{linear arithmetic|(}
nipkow@8743
   224
wenzelm@17182
   225
\input{Misc/document/fakenat.tex}\medskip
nipkow@8743
   226
\input{Misc/document/natsum.tex}
nipkow@8743
   227
paulson@11428
   228
\index{linear arithmetic|)}
nipkow@8743
   229
nipkow@8743
   230
nipkow@10396
   231
\subsection{Pairs}
nipkow@9541
   232
\input{Misc/document/pairs.tex}
nipkow@8743
   233
nipkow@10608
   234
\subsection{Datatype {\tt\slshape option}}
nipkow@10543
   235
\label{sec:option}
nipkow@10543
   236
\input{Misc/document/Option2.tex}
nipkow@10543
   237
nipkow@8743
   238
\section{Definitions}
nipkow@8743
   239
\label{sec:Definitions}
nipkow@8743
   240
nipkow@8743
   241
A definition is simply an abbreviation, i.e.\ a new name for an existing
nipkow@8743
   242
construction. In particular, definitions cannot be recursive. Isabelle offers
nipkow@8743
   243
definitions on the level of types and terms. Those on the type level are
paulson@11456
   244
called \textbf{type synonyms}; those on the term level are simply called 
nipkow@8743
   245
definitions.
nipkow@8743
   246
nipkow@8743
   247
paulson@10885
   248
\subsection{Type Synonyms}
nipkow@8743
   249
nipkow@12327
   250
\index{type synonyms}%
paulson@11456
   251
Type synonyms are similar to those found in ML\@. They are created by a 
nipkow@44049
   252
\commdx{type\protect\_synonym} command:
nipkow@8743
   253
wenzelm@17182
   254
\medskip
nipkow@12327
   255
\input{Misc/document/types.tex}
nipkow@8743
   256
nipkow@9844
   257
\input{Misc/document/prime_def.tex}
nipkow@8743
   258
nipkow@8743
   259
nipkow@11201
   260
\section{The Definitional Approach}
nipkow@11201
   261
\label{sec:definitional}
nipkow@11201
   262
paulson@11457
   263
\index{Definitional Approach}%
nipkow@11201
   264
As we pointed out at the beginning of the chapter, asserting arbitrary
paulson@11456
   265
axioms such as $f(n) = f(n) + 1$ can easily lead to contradictions. In order
paulson@11457
   266
to avoid this danger, we advocate the definitional rather than
paulson@11456
   267
the axiomatic approach: introduce new concepts by definitions. However,  Isabelle/HOL seems to
paulson@11456
   268
support many richer definitional constructs, such as
paulson@11456
   269
\isacommand{primrec}. The point is that Isabelle reduces such constructs to first principles. For example, each
paulson@11456
   270
\isacommand{primrec} function definition is turned into a proper
paulson@11456
   271
(nonrecursive!) definition from which the user-supplied recursion equations are
paulson@11457
   272
automatically proved.  This process is
paulson@11456
   273
hidden from the user, who does not have to understand the details.  Other commands described
nipkow@25258
   274
later, like \isacommand{fun} and \isacommand{inductive}, work similarly.  
paulson@11457
   275
This strict adherence to the definitional approach reduces the risk of 
paulson@11457
   276
soundness errors.
nipkow@11201
   277
nipkow@8743
   278
\chapter{More Functional Programming}
nipkow@8743
   279
paulson@11458
   280
The purpose of this chapter is to deepen your understanding of the
nipkow@8771
   281
concepts encountered so far and to introduce advanced forms of datatypes and
nipkow@8771
   282
recursive functions. The first two sections give a structured presentation of
nipkow@10538
   283
theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss
paulson@11458
   284
important heuristics for induction ({\S}\ref{sec:InductionHeuristics}).  You can
paulson@11458
   285
skip them if you are not planning to perform proofs yourself.
paulson@11458
   286
We then present a case
paulson@11458
   287
study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
nipkow@8771
   288
datatypes, including those involving function spaces, are covered in
paulson@11458
   289
{\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
nipkow@25258
   290
trees (``tries'').  Finally we introduce \isacommand{fun}, a general
paulson@11458
   291
form of recursive function definition that goes well beyond 
nipkow@25258
   292
\isacommand{primrec} ({\S}\ref{sec:fun}).
nipkow@8743
   293
nipkow@8743
   294
nipkow@8743
   295
\section{Simplification}
nipkow@8743
   296
\label{sec:Simplification}
nipkow@8743
   297
\index{simplification|(}
nipkow@8743
   298
paulson@10795
   299
So far we have proved our theorems by \isa{auto}, which simplifies
paulson@11458
   300
all subgoals. In fact, \isa{auto} can do much more than that. 
paulson@11458
   301
To go beyond toy examples, you
nipkow@9541
   302
need to understand the ingredients of \isa{auto}.  This section covers the
nipkow@10971
   303
method that \isa{auto} always applies first, simplification.
nipkow@8743
   304
nipkow@8743
   305
Simplification is one of the central theorem proving tools in Isabelle and
paulson@11458
   306
many other systems. The tool itself is called the \textbf{simplifier}. 
paulson@11458
   307
This section introduces the many features of the simplifier
paulson@11458
   308
and is required reading if you intend to perform proofs.  Later on,
paulson@11458
   309
{\S}\ref{sec:simplification-II} explains some more advanced features and a
nipkow@9754
   310
little bit of how the simplifier works. The serious student should read that
paulson@11458
   311
section as well, in particular to understand why the simplifier did
paulson@11458
   312
something unexpected.
nipkow@8743
   313
paulson@11458
   314
\subsection{What is Simplification?}
nipkow@9458
   315
nipkow@8743
   316
In its most basic form, simplification means repeated application of
nipkow@8743
   317
equations from left to right. For example, taking the rules for \isa{\at}
nipkow@8743
   318
and applying them to the term \isa{[0,1] \at\ []} results in a sequence of
nipkow@8743
   319
simplification steps:
nipkow@8743
   320
\begin{ttbox}\makeatother
nipkow@8743
   321
(0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
nipkow@8743
   322
\end{ttbox}
nipkow@9933
   323
This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
paulson@11458
   324
equations are referred to as \bfindex{rewrite rules}.
nipkow@9933
   325
``Rewriting'' is more honest than ``simplification'' because the terms do not
nipkow@9933
   326
necessarily become simpler in the process.
nipkow@8743
   327
paulson@11458
   328
The simplifier proves arithmetic goals as described in
paulson@11458
   329
{\S}\ref{sec:nat} above.  Arithmetic expressions are simplified using built-in
paulson@11458
   330
procedures that go beyond mere rewrite rules.  New simplification procedures
paulson@11458
   331
can be coded and installed, but they are definitely not a matter for this
paulson@11458
   332
tutorial. 
paulson@11458
   333
nipkow@9844
   334
\input{Misc/document/simp.tex}
nipkow@8743
   335
nipkow@8743
   336
\index{simplification|)}
nipkow@8743
   337
nipkow@9844
   338
\input{Misc/document/Itrev.tex}
nipkow@13305
   339
\begin{exercise}
nipkow@13305
   340
\input{Misc/document/Plus.tex}%
nipkow@13305
   341
\end{exercise}
nipkow@9493
   342
\begin{exercise}
nipkow@9493
   343
\input{Misc/document/Tree2.tex}%
nipkow@9493
   344
\end{exercise}
nipkow@8743
   345
nipkow@9844
   346
\input{CodeGen/document/CodeGen.tex}
nipkow@8743
   347
nipkow@8743
   348
paulson@10885
   349
\section{Advanced Datatypes}
nipkow@8743
   350
\label{sec:advanced-datatypes}
paulson@11428
   351
\index{datatype@\isacommand {datatype} (command)|(}
paulson@11428
   352
\index{primrec@\isacommand {primrec} (command)|(}
nipkow@8743
   353
%|)
nipkow@8743
   354
paulson@11428
   355
This section presents advanced forms of datatypes: mutual and nested
paulson@11428
   356
recursion.  A series of examples will culminate in a treatment of the trie
paulson@11428
   357
data structure.
paulson@11428
   358
nipkow@8743
   359
paulson@10885
   360
\subsection{Mutual Recursion}
nipkow@8743
   361
\label{sec:datatype-mut-rec}
nipkow@8743
   362
nipkow@8743
   363
\input{Datatype/document/ABexpr.tex}
nipkow@8743
   364
paulson@10885
   365
\subsection{Nested Recursion}
nipkow@9644
   366
\label{sec:nested-datatype}
nipkow@8743
   367
nipkow@9644
   368
{\makeatother\input{Datatype/document/Nested.tex}}
nipkow@8743
   369
nipkow@8743
   370
paulson@11419
   371
\subsection{The Limits of Nested Recursion}
nipkow@12327
   372
\label{sec:nested-fun-datatype}
paulson@11419
   373
paulson@11419
   374
How far can we push nested recursion? By the unfolding argument above, we can
paulson@11419
   375
reduce nested to mutual recursion provided the nested recursion only involves
paulson@11419
   376
previously defined datatypes. This does not include functions:
paulson@11419
   377
\begin{isabelle}
paulson@11419
   378
\isacommand{datatype} t = C "t \isasymRightarrow\ bool"
paulson@11419
   379
\end{isabelle}
paulson@11419
   380
This declaration is a real can of worms.
paulson@11419
   381
In HOL it must be ruled out because it requires a type
paulson@11419
   382
\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
paulson@11419
   383
same cardinality --- an impossibility. For the same reason it is not possible
nipkow@12328
   384
to allow recursion involving the type \isa{t set}, which is isomorphic to
paulson@11419
   385
\isa{t \isasymFun\ bool}.
paulson@11419
   386
paulson@11419
   387
Fortunately, a limited form of recursion
paulson@11419
   388
involving function spaces is permitted: the recursive type may occur on the
paulson@11419
   389
right of a function arrow, but never on the left. Hence the above can of worms
paulson@11458
   390
is ruled out but the following example of a potentially 
paulson@11458
   391
\index{infinitely branching trees}%
paulson@11458
   392
infinitely branching tree is accepted:
paulson@11419
   393
\smallskip
paulson@11419
   394
paulson@11419
   395
\input{Datatype/document/Fundata.tex}
paulson@11419
   396
paulson@11419
   397
If you need nested recursion on the left of a function arrow, there are
paulson@11419
   398
alternatives to pure HOL\@.  In the Logic for Computable Functions 
paulson@11458
   399
(\rmindex{LCF}), types like
paulson@11419
   400
\begin{isabelle}
paulson@11419
   401
\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
paulson@11419
   402
\end{isabelle}
paulson@11419
   403
do indeed make sense~\cite{paulson87}.  Note the different arrow,
paulson@11419
   404
\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
paulson@11419
   405
expressing the type of \emph{continuous} functions. 
paulson@11419
   406
There is even a version of LCF on top of HOL,
paulson@11458
   407
called \rmindex{HOLCF}~\cite{MuellerNvOS99}.
paulson@11428
   408
\index{datatype@\isacommand {datatype} (command)|)}
paulson@11428
   409
\index{primrec@\isacommand {primrec} (command)|)}
paulson@11419
   410
paulson@11419
   411
paulson@11419
   412
\subsection{Case Study: Tries}
paulson@11419
   413
\label{sec:Trie}
paulson@11419
   414
paulson@11458
   415
\index{tries|(}%
paulson@11419
   416
Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
paulson@11419
   417
indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
paulson@11419
   418
trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
paulson@11419
   419
``cat''.  When searching a string in a trie, the letters of the string are
paulson@11419
   420
examined sequentially. Each letter determines which subtrie to search next.
paulson@11419
   421
In this case study we model tries as a datatype, define a lookup and an
paulson@11419
   422
update function, and prove that they behave as expected.
paulson@11419
   423
paulson@11419
   424
\begin{figure}[htbp]
paulson@11419
   425
\begin{center}
nipkow@8743
   426
\unitlength1mm
nipkow@8743
   427
\begin{picture}(60,30)
nipkow@8743
   428
\put( 5, 0){\makebox(0,0)[b]{l}}
nipkow@8743
   429
\put(25, 0){\makebox(0,0)[b]{e}}
nipkow@8743
   430
\put(35, 0){\makebox(0,0)[b]{n}}
nipkow@8743
   431
\put(45, 0){\makebox(0,0)[b]{r}}
nipkow@8743
   432
\put(55, 0){\makebox(0,0)[b]{t}}
nipkow@8743
   433
%
nipkow@8743
   434
\put( 5, 9){\line(0,-1){5}}
nipkow@8743
   435
\put(25, 9){\line(0,-1){5}}
nipkow@8743
   436
\put(44, 9){\line(-3,-2){9}}
nipkow@8743
   437
\put(45, 9){\line(0,-1){5}}
nipkow@8743
   438
\put(46, 9){\line(3,-2){9}}
nipkow@8743
   439
%
nipkow@8743
   440
\put( 5,10){\makebox(0,0)[b]{l}}
nipkow@8743
   441
\put(15,10){\makebox(0,0)[b]{n}}
paulson@11419
   442
\put(25,10){\makebox(0,0)[b]{p}}
paulson@11419
   443
\put(45,10){\makebox(0,0)[b]{a}}
paulson@11419
   444
%
paulson@11419
   445
\put(14,19){\line(-3,-2){9}}
paulson@11419
   446
\put(15,19){\line(0,-1){5}}
paulson@11419
   447
\put(16,19){\line(3,-2){9}}
paulson@11419
   448
\put(45,19){\line(0,-1){5}}
paulson@11419
   449
%
paulson@11419
   450
\put(15,20){\makebox(0,0)[b]{a}}
paulson@11419
   451
\put(45,20){\makebox(0,0)[b]{c}}
paulson@11419
   452
%
paulson@11419
   453
\put(30,30){\line(-3,-2){13}}
paulson@11419
   454
\put(30,30){\line(3,-2){13}}
paulson@11419
   455
\end{picture}
paulson@11419
   456
\end{center}
paulson@11450
   457
\caption{A Sample Trie}
paulson@11419
   458
\label{fig:trie}
paulson@11419
   459
\end{figure}
paulson@11419
   460
paulson@11419
   461
Proper tries associate some value with each string. Since the
paulson@11419
   462
information is stored only in the final node associated with the string, many
paulson@11419
   463
nodes do not carry any value. This distinction is modeled with the help
paulson@11419
   464
of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
paulson@11419
   465
\input{Trie/document/Trie.tex}
paulson@11458
   466
\index{tries|)}
paulson@11419
   467
nipkow@25261
   468
\section{Total Recursive Functions: \isacommand{fun}}
nipkow@25258
   469
\label{sec:fun}
nipkow@25258
   470
\index{fun@\isacommand {fun} (command)|(}\index{functions!total|(}
paulson@11419
   471
paulson@11419
   472
Although many total functions have a natural primitive recursive definition,
paulson@11419
   473
this is not always the case. Arbitrary total recursive functions can be
nipkow@25263
   474
defined by means of \isacommand{fun}: you can use full pattern matching,
paulson@11419
   475
recursion need not involve datatypes, and termination is proved by showing
nipkow@25258
   476
that the arguments of all recursive calls are smaller in a suitable sense.
nipkow@25258
   477
In this section we restrict ourselves to functions where Isabelle can prove
nipkow@25281
   478
termination automatically. More advanced function definitions, including user
nipkow@25281
   479
supplied termination proofs, nested recursion and partiality, are discussed
nipkow@25281
   480
in a separate tutorial~\cite{isabelle-function}.
paulson@11419
   481
nipkow@25258
   482
\input{Fun/document/fun0.tex}
paulson@11419
   483
nipkow@25258
   484
\index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}