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