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