doc-src/TutorialI/fp.tex
author paulson
Thu Jul 26 16:43:02 2001 +0200 (2001-07-26)
changeset 11456 7eb63f63e6c6
parent 11450 1b02a6c4032f
child 11457 279da0358aa9
permissions -rw-r--r--
revisions and indexing
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@11450
    34
\index{*ToyList (example)|(}
paulson@11419
    35
{\makeatother\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
paulson@11419
    40
\texttt{ToyList.thy}. It is good practice to present all declarations and
paulson@11450
    41
definitions at the beginning of a theory to facilitate browsing.%
paulson@11450
    42
\index{*ToyList (example)|)}
paulson@11419
    43
paulson@11419
    44
\begin{figure}[htbp]
paulson@11419
    45
\begin{ttbox}\makeatother
paulson@11419
    46
\input{ToyList2/ToyList2}\end{ttbox}
paulson@11450
    47
\caption{Proofs about Lists}
paulson@11419
    48
\label{fig:ToyList-proofs}
paulson@11419
    49
\end{figure}
paulson@11419
    50
paulson@11419
    51
\subsubsection*{Review}
paulson@11419
    52
paulson@11419
    53
This is the end of our toy proof. It should have familiarized you with
paulson@11419
    54
\begin{itemize}
paulson@11419
    55
\item the standard theorem proving procedure:
nipkow@8743
    56
state a goal (lemma or theorem); proceed with proof until a separate lemma is
nipkow@8743
    57
required; prove that lemma; come back to the original goal.
nipkow@8743
    58
\item a specific procedure that works well for functional programs:
nipkow@8743
    59
induction followed by all-out simplification via \isa{auto}.
nipkow@8743
    60
\item a basic repertoire of proof commands.
nipkow@8743
    61
\end{itemize}
nipkow@8743
    62
nipkow@8743
    63
paulson@10885
    64
\section{Some Helpful Commands}
nipkow@8743
    65
\label{sec:commands-and-hints}
nipkow@8743
    66
nipkow@8743
    67
This section discusses a few basic commands for manipulating the proof state
nipkow@8743
    68
and can be skipped by casual readers.
nipkow@8743
    69
nipkow@8743
    70
There are two kinds of commands used during a proof: the actual proof
nipkow@8743
    71
commands and auxiliary commands for examining the proof state and controlling
nipkow@8743
    72
the display. Simple proof commands are of the form
paulson@11456
    73
\commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically 
paulson@11419
    74
\isa{induct_tac} or \isa{auto}.  All such theorem proving operations
paulson@11419
    75
are referred to as \bfindex{methods}, and further ones are
paulson@11419
    76
introduced throughout the tutorial.  Unless stated otherwise, you may
paulson@11419
    77
assume that a method attacks merely the first subgoal. An exception is
paulson@11419
    78
\isa{auto}, which tries to solve all subgoals.
nipkow@8743
    79
paulson@11419
    80
The most useful auxiliary commands are as follows:
nipkow@8743
    81
\begin{description}
paulson@11419
    82
\item[Undoing:] \commdx{undo} undoes the effect of
paulson@11419
    83
the
nipkow@8743
    84
  last command; \isacommand{undo} can be undone by
paulson@11419
    85
  \commdx{redo}.  Both are only needed at the shell
nipkow@8743
    86
  level and should not occur in the final theory.
paulson@11419
    87
\item[Printing the current state:] \commdx{pr}
paulson@11419
    88
redisplays
paulson@11302
    89
  the current proof state, for example when it has scrolled past the top of
paulson@11302
    90
  the screen.
nipkow@8743
    91
\item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
nipkow@8743
    92
  print only the first $n$ subgoals from now on and redisplays the current
nipkow@8743
    93
  proof state. This is helpful when there are many subgoals.
nipkow@8743
    94
\item[Modifying the order of subgoals:]
paulson@11419
    95
\commdx{defer} moves the first subgoal to the end and
paulson@11419
    96
\commdx{prefer}~$n$ moves subgoal $n$ to the front.
nipkow@8743
    97
\item[Printing theorems:]
paulson@11419
    98
  \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
nipkow@8743
    99
  prints the named theorems.
nipkow@8743
   100
\item[Displaying types:] We have already mentioned the flag
paulson@11456
   101
  \texttt{show_types} above.\index{*show_types (flag)}
paulson@11456
   102
  It can also be useful for detecting misspellings in
paulson@11456
   103
  formulae. For example, if \texttt{show_types} is set and the goal
nipkow@8743
   104
  \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
nipkow@8743
   105
\par\noindent
nipkow@8743
   106
\begin{isabelle}%
nipkow@8743
   107
Variables:\isanewline
nipkow@8743
   108
~~xs~::~'a~list
nipkow@8743
   109
\end{isabelle}%
nipkow@8743
   110
\par\noindent
nipkow@8743
   111
which tells us that Isabelle has correctly inferred that
nipkow@8743
   112
\isa{xs} is a variable of list type. On the other hand, had we
nipkow@8743
   113
made a typo as in \isa{rev(re xs) = xs}, the response
nipkow@8743
   114
\par\noindent
nipkow@8743
   115
\begin{isabelle}%
nipkow@8743
   116
Variables:\isanewline
nipkow@8743
   117
~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
nipkow@8743
   118
~~xs~::~'a~list%
nipkow@8743
   119
\end{isabelle}%
nipkow@8743
   120
\par\noindent
nipkow@8743
   121
would have alerted us because of the unexpected variable \isa{re}.
paulson@11419
   122
\item[Reading terms and types:] \commdx{term}
nipkow@8743
   123
  \textit{string} reads, type-checks and prints the given string as a term in
nipkow@8743
   124
  the current context; the inferred type is output as well.
paulson@11419
   125
  \commdx{typ} \textit{string} reads and prints the given
nipkow@8743
   126
  string as a type in the current context.
nipkow@8743
   127
\item[(Re)loading theories:] When you start your interaction you must open a
paulson@11456
   128
  named theory with the line \commdx{theory}~\isa{T~=~\dots~:}. Isabelle
nipkow@8771
   129
  automatically loads all the required parent theories from their respective
nipkow@8771
   130
  files (which may take a moment, unless the theories are already loaded and
nipkow@9541
   131
  the files have not been modified).
nipkow@8743
   132
  
nipkow@8743
   133
  If you suddenly discover that you need to modify a parent theory of your
paulson@11428
   134
  current theory, you must first abandon your current theory%
paulson@11428
   135
  \indexbold{abandoning a theory}\indexbold{theories!abandoning} 
paulson@11428
   136
  (at the shell
paulson@11419
   137
  level type \commdx{kill}). After the parent theory has
nipkow@10971
   138
  been modified, you go back to your original theory. When its first line
nipkow@10971
   139
  \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
nipkow@8743
   140
  modified parent is reloaded automatically.
nipkow@9541
   141
  
nipkow@10978
   142
%  The only time when you need to load a theory by hand is when you simply
nipkow@10978
   143
%  want to check if it loads successfully without wanting to make use of the
nipkow@10978
   144
%  theory itself. This you can do by typing
paulson@11419
   145
%  \isa{\commdx{use\_thy}~"T"}.
nipkow@8743
   146
\end{description}
nipkow@8743
   147
Further commands are found in the Isabelle/Isar Reference Manual.
nipkow@8743
   148
nipkow@8771
   149
We now examine Isabelle's functional programming constructs systematically,
nipkow@8771
   150
starting with inductive datatypes.
nipkow@8771
   151
nipkow@8743
   152
nipkow@8743
   153
\section{Datatypes}
nipkow@8743
   154
\label{sec:datatype}
nipkow@8743
   155
paulson@11456
   156
\index{datatypes|(}%
nipkow@8743
   157
Inductive datatypes are part of almost every non-trivial application of HOL.
nipkow@8743
   158
First we take another look at a very important example, the datatype of
nipkow@8743
   159
lists, before we turn to datatypes in general. The section closes with a
nipkow@8743
   160
case study.
nipkow@8743
   161
nipkow@8743
   162
nipkow@8743
   163
\subsection{Lists}
nipkow@8743
   164
paulson@11428
   165
\index{*list (type)}%
paulson@11456
   166
Lists are one of the essential datatypes in computing.  You need to be familiar with their basic operations.
nipkow@8771
   167
Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
paulson@11428
   168
\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
nipkow@8743
   169
The latter contains many further operations. For example, the functions
paulson@11419
   170
\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
nipkow@8743
   171
element and the remainder of a list. (However, pattern-matching is usually
paulson@10795
   172
preferable to \isa{hd} and \isa{tl}.)  
nipkow@10800
   173
Also available are higher-order functions like \isa{map} and \isa{filter}.
paulson@10795
   174
Theory \isa{List} also contains
nipkow@8743
   175
more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
nipkow@8743
   176
$x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
nipkow@8743
   177
always use HOL's predefined lists.
nipkow@8743
   178
nipkow@8743
   179
paulson@10885
   180
\subsection{The General Format}
nipkow@8743
   181
\label{sec:general-datatype}
nipkow@8743
   182
nipkow@8743
   183
The general HOL \isacommand{datatype} definition is of the form
nipkow@8743
   184
\[
nipkow@8743
   185
\isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
nipkow@8743
   186
C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
nipkow@8743
   187
C@m~\tau@{m1}~\dots~\tau@{mk@m}
nipkow@8743
   188
\]
nipkow@8771
   189
where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct
nipkow@8743
   190
constructor names and $\tau@{ij}$ are types; it is customary to capitalize
nipkow@8743
   191
the first letter in constructor names. There are a number of
nipkow@8743
   192
restrictions (such as that the type should not be empty) detailed
nipkow@8743
   193
elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
nipkow@8743
   194
nipkow@8743
   195
Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and
nipkow@8743
   196
\isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically
nipkow@8743
   197
during proofs by simplification.  The same is true for the equations in
nipkow@8743
   198
primitive recursive function definitions.
nipkow@8743
   199
nipkow@9644
   200
Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
nipkow@10538
   201
the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
nipkow@9644
   202
just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
paulson@11456
   203
  1}.  In general, \cdx{size} returns 
paulson@11456
   204
\begin{itemize}
paulson@11456
   205
\item \isa{0} for all constructors
paulson@11456
   206
that do not have an argument of type $t$\\
paulson@11456
   207
\item for all other constructors,
paulson@11456
   208
one plus the sum of the sizes of all arguments of type~$t$.
paulson@11456
   209
\end{itemize}
paulson@11456
   210
Note that because
nipkow@9644
   211
\isa{size} is defined on every datatype, it is overloaded; on lists
paulson@11419
   212
\isa{size} is also called \sdx{length}, which is not overloaded.
paulson@10795
   213
Isabelle will always show \isa{size} on lists as \isa{length}.
nipkow@9644
   214
nipkow@9644
   215
paulson@10885
   216
\subsection{Primitive Recursion}
nipkow@8743
   217
paulson@11456
   218
\index{recursion!primitive}%
nipkow@8743
   219
Functions on datatypes are usually defined by recursion. In fact, most of the
paulson@11428
   220
time they are defined by what is called \textbf{primitive recursion}.
paulson@11428
   221
The keyword \commdx{primrec} is followed by a list of
nipkow@8743
   222
equations
nipkow@8743
   223
\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
nipkow@8743
   224
such that $C$ is a constructor of the datatype $t$ and all recursive calls of
nipkow@8743
   225
$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
nipkow@8743
   226
Isabelle immediately sees that $f$ terminates because one (fixed!) argument
nipkow@10654
   227
becomes smaller with every recursive call. There must be at most one equation
nipkow@8743
   228
for each constructor.  Their order is immaterial.
nipkow@8771
   229
A more general method for defining total recursive functions is introduced in
nipkow@10538
   230
{\S}\ref{sec:recdef}.
nipkow@8743
   231
nipkow@9493
   232
\begin{exercise}\label{ex:Tree}
nipkow@8743
   233
\input{Misc/document/Tree.tex}%
nipkow@8743
   234
\end{exercise}
nipkow@8743
   235
nipkow@9721
   236
\input{Misc/document/case_exprs.tex}
nipkow@8743
   237
nipkow@8743
   238
\input{Ifexpr/document/Ifexpr.tex}
paulson@11456
   239
\index{datatypes|)}
paulson@11456
   240
nipkow@8743
   241
paulson@10885
   242
\section{Some Basic Types}
nipkow@8743
   243
nipkow@8743
   244
paulson@10885
   245
\subsection{Natural Numbers}
paulson@11456
   246
\label{sec:nat}\index{natural numbers}%
paulson@11428
   247
\index{linear arithmetic|(}
nipkow@8743
   248
nipkow@8743
   249
\input{Misc/document/fakenat.tex}
nipkow@8743
   250
\input{Misc/document/natsum.tex}
nipkow@8743
   251
paulson@11428
   252
\index{linear arithmetic|)}
nipkow@8743
   253
nipkow@8743
   254
nipkow@10396
   255
\subsection{Pairs}
nipkow@9541
   256
\input{Misc/document/pairs.tex}
nipkow@8743
   257
nipkow@10608
   258
\subsection{Datatype {\tt\slshape option}}
nipkow@10543
   259
\label{sec:option}
nipkow@10543
   260
\input{Misc/document/Option2.tex}
nipkow@10543
   261
nipkow@8743
   262
\section{Definitions}
nipkow@8743
   263
\label{sec:Definitions}
nipkow@8743
   264
nipkow@8743
   265
A definition is simply an abbreviation, i.e.\ a new name for an existing
nipkow@8743
   266
construction. In particular, definitions cannot be recursive. Isabelle offers
nipkow@8743
   267
definitions on the level of types and terms. Those on the type level are
paulson@11456
   268
called \textbf{type synonyms}; those on the term level are simply called 
nipkow@8743
   269
definitions.
nipkow@8743
   270
nipkow@8743
   271
paulson@10885
   272
\subsection{Type Synonyms}
nipkow@8743
   273
paulson@11456
   274
\index{type synonyms|(}%
paulson@11456
   275
Type synonyms are similar to those found in ML\@. They are created by a 
paulson@11428
   276
\commdx{types} command:
nipkow@8743
   277
nipkow@8743
   278
\input{Misc/document/types.tex}%
nipkow@8743
   279
paulson@11456
   280
Pattern-matching is not allowed, i.e.\ each definition must be of
nipkow@8743
   281
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
nipkow@11215
   282
Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
paulson@11428
   283
in proofs.%
paulson@11456
   284
\index{type synonyms|)}
nipkow@8743
   285
nipkow@9844
   286
\input{Misc/document/prime_def.tex}
nipkow@8743
   287
nipkow@11203
   288
\input{Misc/document/Translations.tex}
nipkow@11203
   289
nipkow@8743
   290
nipkow@11201
   291
\section{The Definitional Approach}
nipkow@11201
   292
\label{sec:definitional}
nipkow@11201
   293
nipkow@11201
   294
As we pointed out at the beginning of the chapter, asserting arbitrary
paulson@11456
   295
axioms such as $f(n) = f(n) + 1$ can easily lead to contradictions. In order
nipkow@11201
   296
to avoid this danger, this tutorial advocates the definitional rather than
paulson@11456
   297
the axiomatic approach: introduce new concepts by definitions. However,  Isabelle/HOL seems to
paulson@11456
   298
support many richer definitional constructs, such as
paulson@11456
   299
\isacommand{primrec}. The point is that Isabelle reduces such constructs to first principles. For example, each
paulson@11456
   300
\isacommand{primrec} function definition is turned into a proper
paulson@11456
   301
(nonrecursive!) definition from which the user-supplied recursion equations are
paulson@11456
   302
derived as theorems.  This process is
paulson@11456
   303
hidden from the user, who does not have to understand the details.  Other commands described
paulson@11456
   304
later, like \isacommand{recdef} and \isacommand{inductive}, are treated similarly.  This strict adherence to the definitional approach reduces the risk of soundness errors.
nipkow@11201
   305
nipkow@8743
   306
\chapter{More Functional Programming}
nipkow@8743
   307
nipkow@8743
   308
The purpose of this chapter is to deepen the reader's understanding of the
nipkow@8771
   309
concepts encountered so far and to introduce advanced forms of datatypes and
nipkow@8771
   310
recursive functions. The first two sections give a structured presentation of
nipkow@10538
   311
theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss
nipkow@10538
   312
important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). They can
nipkow@8771
   313
be skipped by readers less interested in proofs. They are followed by a case
nipkow@10538
   314
study, a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
nipkow@8771
   315
datatypes, including those involving function spaces, are covered in
nipkow@10538
   316
{\S}\ref{sec:advanced-datatypes}, which closes with another case study, search
nipkow@8771
   317
trees (``tries'').  Finally we introduce \isacommand{recdef}, a very general
nipkow@8771
   318
form of recursive function definition which goes well beyond what
nipkow@10538
   319
\isacommand{primrec} allows ({\S}\ref{sec:recdef}).
nipkow@8743
   320
nipkow@8743
   321
nipkow@8743
   322
\section{Simplification}
nipkow@8743
   323
\label{sec:Simplification}
nipkow@8743
   324
\index{simplification|(}
nipkow@8743
   325
paulson@10795
   326
So far we have proved our theorems by \isa{auto}, which simplifies
nipkow@9541
   327
\emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
nipkow@9541
   328
that it did not need to so far. However, when you go beyond toy examples, you
nipkow@9541
   329
need to understand the ingredients of \isa{auto}.  This section covers the
nipkow@10971
   330
method that \isa{auto} always applies first, simplification.
nipkow@8743
   331
nipkow@8743
   332
Simplification is one of the central theorem proving tools in Isabelle and
nipkow@8743
   333
many other systems. The tool itself is called the \bfindex{simplifier}. The
nipkow@11159
   334
purpose of this section is to introduce the many features of the simplifier.
nipkow@10971
   335
Anybody intending to perform proofs in HOL should read this section. Later on
nipkow@10538
   336
({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
nipkow@9754
   337
little bit of how the simplifier works. The serious student should read that
nipkow@9754
   338
section as well, in particular in order to understand what happened if things
nipkow@9754
   339
do not simplify as expected.
nipkow@8743
   340
nipkow@11214
   341
\subsection{What is Simplification}
nipkow@9458
   342
nipkow@8743
   343
In its most basic form, simplification means repeated application of
nipkow@8743
   344
equations from left to right. For example, taking the rules for \isa{\at}
nipkow@8743
   345
and applying them to the term \isa{[0,1] \at\ []} results in a sequence of
nipkow@8743
   346
simplification steps:
nipkow@8743
   347
\begin{ttbox}\makeatother
nipkow@8743
   348
(0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
nipkow@8743
   349
\end{ttbox}
nipkow@9933
   350
This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
nipkow@9933
   351
equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.
nipkow@9933
   352
``Rewriting'' is more honest than ``simplification'' because the terms do not
nipkow@9933
   353
necessarily become simpler in the process.
nipkow@8743
   354
nipkow@9844
   355
\input{Misc/document/simp.tex}
nipkow@8743
   356
nipkow@8743
   357
\index{simplification|)}
nipkow@8743
   358
nipkow@9844
   359
\input{Misc/document/Itrev.tex}
nipkow@8743
   360
nipkow@9493
   361
\begin{exercise}
nipkow@9493
   362
\input{Misc/document/Tree2.tex}%
nipkow@9493
   363
\end{exercise}
nipkow@8743
   364
nipkow@9844
   365
\input{CodeGen/document/CodeGen.tex}
nipkow@8743
   366
nipkow@8743
   367
paulson@10885
   368
\section{Advanced Datatypes}
nipkow@8743
   369
\label{sec:advanced-datatypes}
paulson@11428
   370
\index{datatype@\isacommand {datatype} (command)|(}
paulson@11428
   371
\index{primrec@\isacommand {primrec} (command)|(}
nipkow@8743
   372
%|)
nipkow@8743
   373
paulson@11428
   374
This section presents advanced forms of datatypes: mutual and nested
paulson@11428
   375
recursion.  A series of examples will culminate in a treatment of the trie
paulson@11428
   376
data structure.
paulson@11428
   377
nipkow@8743
   378
paulson@10885
   379
\subsection{Mutual Recursion}
nipkow@8743
   380
\label{sec:datatype-mut-rec}
nipkow@8743
   381
nipkow@8743
   382
\input{Datatype/document/ABexpr.tex}
nipkow@8743
   383
paulson@10885
   384
\subsection{Nested Recursion}
nipkow@9644
   385
\label{sec:nested-datatype}
nipkow@8743
   386
nipkow@9644
   387
{\makeatother\input{Datatype/document/Nested.tex}}
nipkow@8743
   388
nipkow@8743
   389
paulson@11419
   390
\subsection{The Limits of Nested Recursion}
paulson@11419
   391
paulson@11419
   392
How far can we push nested recursion? By the unfolding argument above, we can
paulson@11419
   393
reduce nested to mutual recursion provided the nested recursion only involves
paulson@11419
   394
previously defined datatypes. This does not include functions:
paulson@11419
   395
\begin{isabelle}
paulson@11419
   396
\isacommand{datatype} t = C "t \isasymRightarrow\ bool"
paulson@11419
   397
\end{isabelle}
paulson@11419
   398
This declaration is a real can of worms.
paulson@11419
   399
In HOL it must be ruled out because it requires a type
paulson@11419
   400
\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
paulson@11419
   401
same cardinality --- an impossibility. For the same reason it is not possible
paulson@11419
   402
to allow recursion involving the type \isa{set}, which is isomorphic to
paulson@11419
   403
\isa{t \isasymFun\ bool}.
paulson@11419
   404
paulson@11419
   405
Fortunately, a limited form of recursion
paulson@11419
   406
involving function spaces is permitted: the recursive type may occur on the
paulson@11419
   407
right of a function arrow, but never on the left. Hence the above can of worms
paulson@11419
   408
is ruled out but the following example of a potentially infinitely branching tree is
paulson@11419
   409
accepted:
paulson@11419
   410
\smallskip
paulson@11419
   411
paulson@11419
   412
\input{Datatype/document/Fundata.tex}
paulson@11419
   413
\bigskip
paulson@11419
   414
paulson@11419
   415
If you need nested recursion on the left of a function arrow, there are
paulson@11419
   416
alternatives to pure HOL\@.  In the Logic for Computable Functions 
paulson@11419
   417
(LCF), types like
paulson@11419
   418
\begin{isabelle}
paulson@11419
   419
\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
paulson@11419
   420
\end{isabelle}
paulson@11419
   421
do indeed make sense~\cite{paulson87}.  Note the different arrow,
paulson@11419
   422
\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
paulson@11419
   423
expressing the type of \emph{continuous} functions. 
paulson@11419
   424
There is even a version of LCF on top of HOL,
paulson@11419
   425
called HOLCF~\cite{MuellerNvOS99}.
paulson@11428
   426
\index{datatype@\isacommand {datatype} (command)|)}
paulson@11428
   427
\index{primrec@\isacommand {primrec} (command)|)}
paulson@11419
   428
paulson@11419
   429
paulson@11419
   430
\subsection{Case Study: Tries}
paulson@11419
   431
\label{sec:Trie}
paulson@11419
   432
paulson@11419
   433
Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
paulson@11419
   434
indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
paulson@11419
   435
trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
paulson@11419
   436
``cat''.  When searching a string in a trie, the letters of the string are
paulson@11419
   437
examined sequentially. Each letter determines which subtrie to search next.
paulson@11419
   438
In this case study we model tries as a datatype, define a lookup and an
paulson@11419
   439
update function, and prove that they behave as expected.
paulson@11419
   440
paulson@11419
   441
\begin{figure}[htbp]
paulson@11419
   442
\begin{center}
nipkow@8743
   443
\unitlength1mm
nipkow@8743
   444
\begin{picture}(60,30)
nipkow@8743
   445
\put( 5, 0){\makebox(0,0)[b]{l}}
nipkow@8743
   446
\put(25, 0){\makebox(0,0)[b]{e}}
nipkow@8743
   447
\put(35, 0){\makebox(0,0)[b]{n}}
nipkow@8743
   448
\put(45, 0){\makebox(0,0)[b]{r}}
nipkow@8743
   449
\put(55, 0){\makebox(0,0)[b]{t}}
nipkow@8743
   450
%
nipkow@8743
   451
\put( 5, 9){\line(0,-1){5}}
nipkow@8743
   452
\put(25, 9){\line(0,-1){5}}
nipkow@8743
   453
\put(44, 9){\line(-3,-2){9}}
nipkow@8743
   454
\put(45, 9){\line(0,-1){5}}
nipkow@8743
   455
\put(46, 9){\line(3,-2){9}}
nipkow@8743
   456
%
nipkow@8743
   457
\put( 5,10){\makebox(0,0)[b]{l}}
nipkow@8743
   458
\put(15,10){\makebox(0,0)[b]{n}}
paulson@11419
   459
\put(25,10){\makebox(0,0)[b]{p}}
paulson@11419
   460
\put(45,10){\makebox(0,0)[b]{a}}
paulson@11419
   461
%
paulson@11419
   462
\put(14,19){\line(-3,-2){9}}
paulson@11419
   463
\put(15,19){\line(0,-1){5}}
paulson@11419
   464
\put(16,19){\line(3,-2){9}}
paulson@11419
   465
\put(45,19){\line(0,-1){5}}
paulson@11419
   466
%
paulson@11419
   467
\put(15,20){\makebox(0,0)[b]{a}}
paulson@11419
   468
\put(45,20){\makebox(0,0)[b]{c}}
paulson@11419
   469
%
paulson@11419
   470
\put(30,30){\line(-3,-2){13}}
paulson@11419
   471
\put(30,30){\line(3,-2){13}}
paulson@11419
   472
\end{picture}
paulson@11419
   473
\end{center}
paulson@11450
   474
\caption{A Sample Trie}
paulson@11419
   475
\label{fig:trie}
paulson@11419
   476
\end{figure}
paulson@11419
   477
paulson@11419
   478
Proper tries associate some value with each string. Since the
paulson@11419
   479
information is stored only in the final node associated with the string, many
paulson@11419
   480
nodes do not carry any value. This distinction is modeled with the help
paulson@11419
   481
of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
paulson@11419
   482
\input{Trie/document/Trie.tex}
paulson@11419
   483
paulson@11419
   484
\section{Total Recursive Functions}
paulson@11419
   485
\label{sec:recdef}
paulson@11428
   486
\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
paulson@11419
   487
paulson@11419
   488
Although many total functions have a natural primitive recursive definition,
paulson@11419
   489
this is not always the case. Arbitrary total recursive functions can be
paulson@11419
   490
defined by means of \isacommand{recdef}: you can use full pattern-matching,
paulson@11419
   491
recursion need not involve datatypes, and termination is proved by showing
paulson@11419
   492
that the arguments of all recursive calls are smaller in a suitable (user
paulson@11419
   493
supplied) sense. In this section we restrict ourselves to measure functions;
paulson@11419
   494
more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
paulson@11419
   495
paulson@11419
   496
\subsection{Defining Recursive Functions}
paulson@11419
   497
\label{sec:recdef-examples}
paulson@11419
   498
\input{Recdef/document/examples.tex}
paulson@11419
   499
paulson@11419
   500
\subsection{Proving Termination}
paulson@11419
   501
paulson@11419
   502
\input{Recdef/document/termination.tex}
paulson@11419
   503
paulson@11419
   504
\subsection{Simplification with Recdef}
paulson@11419
   505
\label{sec:recdef-simplification}
paulson@11419
   506
paulson@11419
   507
\input{Recdef/document/simplification.tex}
paulson@11419
   508
paulson@11419
   509
\subsection{Induction}
paulson@11419
   510
\index{induction!recursion|(}
nipkow@8743
   511
\index{recursion induction|(}
nipkow@8743
   512
nipkow@8743
   513
\input{Recdef/document/Induction.tex}
nipkow@9644
   514
\label{sec:recdef-induction}
nipkow@8743
   515
nipkow@8743
   516
\index{induction!recursion|)}
nipkow@8743
   517
\index{recursion induction|)}
paulson@11428
   518
\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}