nipkow@8743: \chapter{Functional Programming in HOL}
nipkow@8743: 
nipkow@8743: Although on the surface this chapter is mainly concerned with how to write
nipkow@8743: functional programs in HOL and how to verify them, most of the
nipkow@8743: constructs and proof procedures introduced are general purpose and recur in
nipkow@8743: any specification or verification task.
nipkow@8743: 
nipkow@9541: The dedicated functional programmer should be warned: HOL offers only
nipkow@9541: \emph{total functional programming} --- all functions in HOL must be total;
nipkow@9541: lazy data structures are not directly available. On the positive side,
nipkow@9541: functions in HOL need not be computable: HOL is a specification language that
nipkow@9541: goes well beyond what can be expressed as a program. However, for the time
nipkow@9541: being we concentrate on the computable.
nipkow@8743: 
nipkow@8743: \section{An introductory theory}
nipkow@8743: \label{sec:intro-theory}
nipkow@8743: 
nipkow@8743: Functional programming needs datatypes and functions. Both of them can be
nipkow@8743: defined in a theory with a syntax reminiscent of languages like ML or
nipkow@8743: Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.
nipkow@8743: We will now examine it line by line.
nipkow@8743: 
nipkow@8743: \begin{figure}[htbp]
nipkow@8743: \begin{ttbox}\makeatother
nipkow@8743: \input{ToyList2/ToyList1}\end{ttbox}
nipkow@8743: \caption{A theory of lists}
nipkow@8743: \label{fig:ToyList}
nipkow@8743: \end{figure}
nipkow@8743: 
nipkow@8743: {\makeatother\input{ToyList/document/ToyList.tex}}
nipkow@8743: 
nipkow@8743: The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The
nipkow@8743: concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs}
nipkow@8743: constitutes the complete theory \texttt{ToyList} and should reside in file
nipkow@8743: \texttt{ToyList.thy}. It is good practice to present all declarations and
nipkow@8743: definitions at the beginning of a theory to facilitate browsing.
nipkow@8743: 
nipkow@8743: \begin{figure}[htbp]
nipkow@8743: \begin{ttbox}\makeatother
nipkow@8743: \input{ToyList2/ToyList2}\end{ttbox}
nipkow@8743: \caption{Proofs about lists}
nipkow@8743: \label{fig:ToyList-proofs}
nipkow@8743: \end{figure}
nipkow@8743: 
nipkow@8743: \subsubsection*{Review}
nipkow@8743: 
nipkow@8743: This is the end of our toy proof. It should have familiarized you with
nipkow@8743: \begin{itemize}
nipkow@8743: \item the standard theorem proving procedure:
nipkow@8743: state a goal (lemma or theorem); proceed with proof until a separate lemma is
nipkow@8743: required; prove that lemma; come back to the original goal.
nipkow@8743: \item a specific procedure that works well for functional programs:
nipkow@8743: induction followed by all-out simplification via \isa{auto}.
nipkow@8743: \item a basic repertoire of proof commands.
nipkow@8743: \end{itemize}
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \section{Some helpful commands}
nipkow@8743: \label{sec:commands-and-hints}
nipkow@8743: 
nipkow@8743: This section discusses a few basic commands for manipulating the proof state
nipkow@8743: and can be skipped by casual readers.
nipkow@8743: 
nipkow@8743: There are two kinds of commands used during a proof: the actual proof
nipkow@8743: commands and auxiliary commands for examining the proof state and controlling
nipkow@8743: the display. Simple proof commands are of the form
nipkow@8743: \isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a
nipkow@8743: synonym for ``theorem proving function''. Typical examples are
nipkow@8743: \isa{induct_tac} and \isa{auto}. Further methods are introduced throughout
nipkow@8743: the tutorial.  Unless stated otherwise you may assume that a method attacks
nipkow@8743: merely the first subgoal. An exception is \isa{auto} which tries to solve all
nipkow@8743: subgoals.
nipkow@8743: 
nipkow@8743: The most useful auxiliary commands are:
nipkow@8743: \begin{description}
nipkow@8743: \item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the
nipkow@8743:   last command; \isacommand{undo} can be undone by
nipkow@8743:   \isacommand{redo}\indexbold{*redo}.  Both are only needed at the shell
nipkow@8743:   level and should not occur in the final theory.
nipkow@8743: \item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays
nipkow@8743:   the current proof state, for example when it has disappeared off the
nipkow@8743:   screen.
nipkow@8743: \item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
nipkow@8743:   print only the first $n$ subgoals from now on and redisplays the current
nipkow@8743:   proof state. This is helpful when there are many subgoals.
nipkow@8743: \item[Modifying the order of subgoals:]
nipkow@8743: \isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and
nipkow@8743: \isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front.
nipkow@8743: \item[Printing theorems:]
nipkow@8743:   \isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
nipkow@8743:   prints the named theorems.
nipkow@8743: \item[Displaying types:] We have already mentioned the flag
nipkow@8743:   \ttindex{show_types} above. It can also be useful for detecting typos in
nipkow@8743:   formulae early on. For example, if \texttt{show_types} is set and the goal
nipkow@8743:   \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
nipkow@8743: \par\noindent
nipkow@8743: \begin{isabelle}%
nipkow@8743: Variables:\isanewline
nipkow@8743: ~~xs~::~'a~list
nipkow@8743: \end{isabelle}%
nipkow@8743: \par\noindent
nipkow@8743: which tells us that Isabelle has correctly inferred that
nipkow@8743: \isa{xs} is a variable of list type. On the other hand, had we
nipkow@8743: made a typo as in \isa{rev(re xs) = xs}, the response
nipkow@8743: \par\noindent
nipkow@8743: \begin{isabelle}%
nipkow@8743: Variables:\isanewline
nipkow@8743: ~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
nipkow@8743: ~~xs~::~'a~list%
nipkow@8743: \end{isabelle}%
nipkow@8743: \par\noindent
nipkow@8743: would have alerted us because of the unexpected variable \isa{re}.
nipkow@8743: \item[Reading terms and types:] \isacommand{term}\indexbold{*term}
nipkow@8743:   \textit{string} reads, type-checks and prints the given string as a term in
nipkow@8743:   the current context; the inferred type is output as well.
nipkow@8743:   \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given
nipkow@8743:   string as a type in the current context.
nipkow@8743: \item[(Re)loading theories:] When you start your interaction you must open a
nipkow@8771:   named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
nipkow@8771:   automatically loads all the required parent theories from their respective
nipkow@8771:   files (which may take a moment, unless the theories are already loaded and
nipkow@9541:   the files have not been modified).
nipkow@8743:   
nipkow@8743:   If you suddenly discover that you need to modify a parent theory of your
nipkow@9494:   current theory you must first abandon your current theory\indexbold{abandon
nipkow@9494:   theory}\indexbold{theory!abandon} (at the shell
nipkow@8743:   level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
nipkow@8743:   been modified you go back to your original theory. When its first line
nipkow@8743:   \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
nipkow@8743:   modified parent is reloaded automatically.
nipkow@9541:   
nipkow@9541:   The only time when you need to load a theory by hand is when you simply
nipkow@9541:   want to check if it loads successfully without wanting to make use of the
nipkow@9541:   theory itself. This you can do by typing
nipkow@9541:   \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
nipkow@8743: \end{description}
nipkow@8743: Further commands are found in the Isabelle/Isar Reference Manual.
nipkow@8743: 
nipkow@8771: We now examine Isabelle's functional programming constructs systematically,
nipkow@8771: starting with inductive datatypes.
nipkow@8771: 
nipkow@8743: 
nipkow@8743: \section{Datatypes}
nipkow@8743: \label{sec:datatype}
nipkow@8743: 
nipkow@8743: Inductive datatypes are part of almost every non-trivial application of HOL.
nipkow@8743: First we take another look at a very important example, the datatype of
nipkow@8743: lists, before we turn to datatypes in general. The section closes with a
nipkow@8743: case study.
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \subsection{Lists}
nipkow@8743: \indexbold{*list}
nipkow@8743: 
nipkow@8743: Lists are one of the essential datatypes in computing. Readers of this
nipkow@8743: tutorial and users of HOL need to be familiar with their basic operations.
nipkow@8771: Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
nipkow@8771: \isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
nipkow@8743: The latter contains many further operations. For example, the functions
nipkow@8771: \isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
nipkow@8743: element and the remainder of a list. (However, pattern-matching is usually
nipkow@8771: preferable to \isa{hd} and \isa{tl}.)  Theory \isa{List} also contains
nipkow@8743: more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
nipkow@8743: $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
nipkow@8743: always use HOL's predefined lists.
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \subsection{The general format}
nipkow@8743: \label{sec:general-datatype}
nipkow@8743: 
nipkow@8743: The general HOL \isacommand{datatype} definition is of the form
nipkow@8743: \[
nipkow@8743: \isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
nipkow@8743: C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
nipkow@8743: C@m~\tau@{m1}~\dots~\tau@{mk@m}
nipkow@8743: \]
nipkow@8771: where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct
nipkow@8743: constructor names and $\tau@{ij}$ are types; it is customary to capitalize
nipkow@8743: the first letter in constructor names. There are a number of
nipkow@8743: restrictions (such as that the type should not be empty) detailed
nipkow@8743: elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
nipkow@8743: 
nipkow@8743: Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and
nipkow@8743: \isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically
nipkow@8743: during proofs by simplification.  The same is true for the equations in
nipkow@8743: primitive recursive function definitions.
nipkow@8743: 
nipkow@9644: Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
nipkow@9644: the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is
nipkow@9644: just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
nipkow@9644:   1}.  In general, \isa{size} returns \isa{0} for all constructors that do
nipkow@9644: not have an argument of type $t$, and for all other constructors \isa{1 +}
nipkow@9644: the sum of the sizes of all arguments of type $t$. Note that because
nipkow@9644: \isa{size} is defined on every datatype, it is overloaded; on lists
nipkow@9644: \isa{size} is also called \isa{length}, which is not overloaded.
nipkow@9644: 
nipkow@9644: 
nipkow@8743: \subsection{Primitive recursion}
nipkow@8743: 
nipkow@8743: Functions on datatypes are usually defined by recursion. In fact, most of the
nipkow@8743: time they are defined by what is called \bfindex{primitive recursion}.
nipkow@8743: The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of
nipkow@8743: equations
nipkow@8743: \[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
nipkow@8743: such that $C$ is a constructor of the datatype $t$ and all recursive calls of
nipkow@8743: $f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
nipkow@8743: Isabelle immediately sees that $f$ terminates because one (fixed!) argument
nipkow@8743: becomes smaller with every recursive call. There must be exactly one equation
nipkow@8743: for each constructor.  Their order is immaterial.
nipkow@8771: A more general method for defining total recursive functions is introduced in
nipkow@8743: \S\ref{sec:recdef}.
nipkow@8743: 
nipkow@9493: \begin{exercise}\label{ex:Tree}
nipkow@8743: \input{Misc/document/Tree.tex}%
nipkow@8743: \end{exercise}
nipkow@8743: 
nipkow@9721: \input{Misc/document/case_exprs.tex}
nipkow@8743: 
nipkow@8743: \begin{warn}
nipkow@8743:   Induction is only allowed on free (or \isasymAnd-bound) variables that
nipkow@9644:   should not occur among the assumptions of the subgoal; see
nipkow@9644:   \S\ref{sec:ind-var-in-prems} for details. Case distinction
nipkow@8743:   (\isa{case_tac}) works for arbitrary terms, which need to be
nipkow@8743:   quoted if they are non-atomic.
nipkow@8743: \end{warn}
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \input{Ifexpr/document/Ifexpr.tex}
nipkow@8743: 
nipkow@8743: \section{Some basic types}
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \subsection{Natural numbers}
nipkow@9644: \label{sec:nat}
nipkow@8743: \index{arithmetic|(}
nipkow@8743: 
nipkow@8743: \input{Misc/document/fakenat.tex}
nipkow@8743: \input{Misc/document/natsum.tex}
nipkow@8743: 
nipkow@8743: The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
nipkow@8743: \ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},
nipkow@8743: \isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and
nipkow@8743: \isaindexbold{max} are predefined, as are the relations
nipkow@8743: \indexboldpos{\isasymle}{$HOL2arithrel} and
nipkow@8743: \ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation
nipkow@8743: \isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although
nipkow@8743: Isabelle does not prove this completely automatically. Note that \isa{1} and
nipkow@8743: \isa{2} are available as abbreviations for the corresponding
nipkow@8743: \isa{Suc}-expressions. If you need the full set of numerals,
nipkow@8743: see~\S\ref{nat-numerals}.
nipkow@8743: 
nipkow@8743: \begin{warn}
nipkow@9494:   The constant \ttindexbold{0} and the operations
nipkow@9494:   \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
nipkow@9494:   \ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max},
nipkow@8743:   \indexboldpos{\isasymle}{$HOL2arithrel} and
nipkow@8743:   \ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available
nipkow@8743:   not just for natural numbers but at other types as well (see
nipkow@9494:   \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there
nipkow@9494:   is nothing to indicate that you are talking about natural numbers.  Hence
nipkow@9494:   Isabelle can only infer that \isa{x} is of some arbitrary type where
nipkow@9494:   \isa{0} and \isa{+} are declared. As a consequence, you will be unable to
nipkow@9494:   prove the goal (although it may take you some time to realize what has
nipkow@9494:   happened if \texttt{show_types} is not set).  In this particular example,
nipkow@9494:   you need to include an explicit type constraint, for example \isa{x+0 =
nipkow@9494:     (x::nat)}.  If there is enough contextual information this may not be
nipkow@9494:   necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because
nipkow@9494:   \isa{Suc} is not overloaded.
nipkow@8743: \end{warn}
nipkow@8743: 
nipkow@8743: Simple arithmetic goals are proved automatically by both \isa{auto}
nipkow@8743: and the simplification methods introduced in \S\ref{sec:Simplification}.  For
nipkow@8743: example,
nipkow@8743: 
nipkow@8743: \input{Misc/document/arith1.tex}%
nipkow@8743: is proved automatically. The main restriction is that only addition is taken
nipkow@8743: into account; other arithmetic operations and quantified formulae are ignored.
nipkow@8743: 
nipkow@8743: For more complex goals, there is the special method
nipkow@8743: \isaindexbold{arith} (which attacks the first subgoal). It proves
nipkow@8743: arithmetic goals involving the usual logical connectives (\isasymnot,
nipkow@8743: \isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and
nipkow@8743: the operations \isa{+}, \isa{-}, \isa{min} and \isa{max}. For example,
nipkow@8743: 
nipkow@8743: \input{Misc/document/arith2.tex}%
nipkow@8743: succeeds because \isa{k*k} can be treated as atomic.
nipkow@8743: In contrast,
nipkow@8743: 
nipkow@8743: \input{Misc/document/arith3.tex}%
nipkow@8743: is not even proved by \isa{arith} because the proof relies essentially
nipkow@8743: on properties of multiplication.
nipkow@8743: 
nipkow@8743: \begin{warn}
nipkow@8743:   The running time of \isa{arith} is exponential in the number of occurrences
nipkow@8743:   of \ttindexboldpos{-}{$HOL2arithfun}, \isaindexbold{min} and
nipkow@8743:   \isaindexbold{max} because they are first eliminated by case distinctions.
nipkow@8743: 
nipkow@8743:   \isa{arith} is incomplete even for the restricted class of formulae
nipkow@8743:   described above (known as ``linear arithmetic''). If divisibility plays a
nipkow@8743:   role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$.
nipkow@8743:   Fortunately, such examples are rare in practice.
nipkow@8743: \end{warn}
nipkow@8743: 
nipkow@8743: \index{arithmetic|)}
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \subsection{Products}
nipkow@9541: \input{Misc/document/pairs.tex}
nipkow@8743: 
nipkow@8743: %FIXME move stuff below into section on proofs about products?
nipkow@8743: \begin{warn}
nipkow@8743:   Abstraction over pairs and tuples is merely a convenient shorthand for a
nipkow@8743:   more complex internal representation.  Thus the internal and external form
nipkow@8743:   of a term may differ, which can affect proofs. If you want to avoid this
nipkow@8743:   complication, use \isa{fst} and \isa{snd}, i.e.\ write
nipkow@8743:   \isa{\isasymlambda{}p.~fst p + snd p} instead of
nipkow@8743:   \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{proofs-about-products} for
nipkow@8743:   theorem proving with tuple patterns.
nipkow@8743: \end{warn}
nipkow@8743: 
nipkow@9541: Note that products, like natural numbers, are datatypes, which means
nipkow@8743: in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
nipkow@8743: products (see \S\ref{proofs-about-products}).
nipkow@8743: 
nipkow@9541: Instead of tuples with many components (where ``many'' is not much above 2),
nipkow@9541: it is far preferable to use record types (see \S\ref{sec:records}).
nipkow@9541: 
nipkow@8743: \section{Definitions}
nipkow@8743: \label{sec:Definitions}
nipkow@8743: 
nipkow@8743: A definition is simply an abbreviation, i.e.\ a new name for an existing
nipkow@8743: construction. In particular, definitions cannot be recursive. Isabelle offers
nipkow@8743: definitions on the level of types and terms. Those on the type level are
nipkow@8743: called type synonyms, those on the term level are called (constant)
nipkow@8743: definitions.
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \subsection{Type synonyms}
nipkow@8771: \indexbold{type synonym}
nipkow@8743: 
nipkow@8743: Type synonyms are similar to those found in ML. Their syntax is fairly self
nipkow@8743: explanatory:
nipkow@8743: 
nipkow@8743: \input{Misc/document/types.tex}%
nipkow@8743: 
nipkow@8743: Note that pattern-matching is not allowed, i.e.\ each definition must be of
nipkow@8743: the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
nipkow@8743: Section~\S\ref{sec:Simplification} explains how definitions are used
nipkow@8743: in proofs.
nipkow@8743: 
nipkow@9844: \input{Misc/document/prime_def.tex}
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \chapter{More Functional Programming}
nipkow@8743: 
nipkow@8743: The purpose of this chapter is to deepen the reader's understanding of the
nipkow@8771: concepts encountered so far and to introduce advanced forms of datatypes and
nipkow@8771: recursive functions. The first two sections give a structured presentation of
nipkow@8771: theorem proving by simplification (\S\ref{sec:Simplification}) and discuss
nipkow@8771: important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can
nipkow@8771: be skipped by readers less interested in proofs. They are followed by a case
nipkow@8771: study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced
nipkow@8771: datatypes, including those involving function spaces, are covered in
nipkow@8771: \S\ref{sec:advanced-datatypes}, which closes with another case study, search
nipkow@8771: trees (``tries'').  Finally we introduce \isacommand{recdef}, a very general
nipkow@8771: form of recursive function definition which goes well beyond what
nipkow@8771: \isacommand{primrec} allows (\S\ref{sec:recdef}).
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \section{Simplification}
nipkow@8743: \label{sec:Simplification}
nipkow@8743: \index{simplification|(}
nipkow@8743: 
nipkow@9541: So far we have proved our theorems by \isa{auto}, which ``simplifies''
nipkow@9541: \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
nipkow@9541: that it did not need to so far. However, when you go beyond toy examples, you
nipkow@9541: need to understand the ingredients of \isa{auto}.  This section covers the
nipkow@9541: method that \isa{auto} always applies first, namely simplification.
nipkow@8743: 
nipkow@8743: Simplification is one of the central theorem proving tools in Isabelle and
nipkow@8743: many other systems. The tool itself is called the \bfindex{simplifier}. The
nipkow@9754: purpose of this section is introduce the many features of the simplifier.
nipkow@9754: Anybody intending to use HOL should read this section. Later on
nipkow@9754: (\S\ref{sec:simplification-II}) we explain some more advanced features and a
nipkow@9754: little bit of how the simplifier works. The serious student should read that
nipkow@9754: section as well, in particular in order to understand what happened if things
nipkow@9754: do not simplify as expected.
nipkow@8743: 
nipkow@9458: \subsubsection{What is simplification}
nipkow@9458: 
nipkow@8743: In its most basic form, simplification means repeated application of
nipkow@8743: equations from left to right. For example, taking the rules for \isa{\at}
nipkow@8743: and applying them to the term \isa{[0,1] \at\ []} results in a sequence of
nipkow@8743: simplification steps:
nipkow@8743: \begin{ttbox}\makeatother
nipkow@8743: (0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
nipkow@8743: \end{ttbox}
nipkow@9933: This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
nipkow@9933: equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.
nipkow@9933: ``Rewriting'' is more honest than ``simplification'' because the terms do not
nipkow@9933: necessarily become simpler in the process.
nipkow@8743: 
nipkow@9844: \input{Misc/document/simp.tex}
nipkow@8743: 
nipkow@8743: \index{simplification|)}
nipkow@8743: 
nipkow@9844: \input{Misc/document/Itrev.tex}
nipkow@8743: 
nipkow@9493: \begin{exercise}
nipkow@9493: \input{Misc/document/Tree2.tex}%
nipkow@9493: \end{exercise}
nipkow@8743: 
nipkow@9844: \input{CodeGen/document/CodeGen.tex}
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \section{Advanced datatypes}
nipkow@8743: \label{sec:advanced-datatypes}
nipkow@8743: \index{*datatype|(}
nipkow@8743: \index{*primrec|(}
nipkow@8743: %|)
nipkow@8743: 
nipkow@8743: This section presents advanced forms of \isacommand{datatype}s.
nipkow@8743: 
nipkow@8743: \subsection{Mutual recursion}
nipkow@8743: \label{sec:datatype-mut-rec}
nipkow@8743: 
nipkow@8743: \input{Datatype/document/ABexpr.tex}
nipkow@8743: 
nipkow@8743: \subsection{Nested recursion}
nipkow@9644: \label{sec:nested-datatype}
nipkow@8743: 
nipkow@9644: {\makeatother\input{Datatype/document/Nested.tex}}
nipkow@8743: 
nipkow@8743: 
nipkow@8743: \subsection{The limits of nested recursion}
nipkow@8743: 
nipkow@8743: How far can we push nested recursion? By the unfolding argument above, we can
nipkow@8743: reduce nested to mutual recursion provided the nested recursion only involves
nipkow@8743: previously defined datatypes. This does not include functions:
nipkow@9792: \begin{isabelle}
nipkow@9792: \isacommand{datatype} t = C "t \isasymRightarrow\ bool"
nipkow@9792: \end{isabelle}
nipkow@8743: is a real can of worms: in HOL it must be ruled out because it requires a type
nipkow@8743: \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
nipkow@8743: same cardinality---an impossibility. For the same reason it is not possible
nipkow@8743: to allow recursion involving the type \isa{set}, which is isomorphic to
nipkow@8743: \isa{t \isasymFun\ bool}.
nipkow@8743: 
nipkow@8743: Fortunately, a limited form of recursion
nipkow@8743: involving function spaces is permitted: the recursive type may occur on the
nipkow@8743: right of a function arrow, but never on the left. Hence the above can of worms
nipkow@8743: is ruled out but the following example of a potentially infinitely branching tree is
nipkow@8743: accepted:
nipkow@8771: \smallskip
nipkow@8743: 
nipkow@8743: \input{Datatype/document/Fundata.tex}
nipkow@8743: \bigskip
nipkow@8743: 
nipkow@9792: If you need nested recursion on the left of a function arrow, there are
nipkow@9792: alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like
nipkow@9792: \begin{isabelle}
nipkow@9792: \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
nipkow@9792: \end{isabelle}
nipkow@9792: do indeed make sense (but note the intentionally different arrow
nipkow@9792: \isa{\isasymrightarrow}). There is even a version of LCF on top of HOL,
nipkow@9792: called HOLCF~\cite{MuellerNvOS99}.
nipkow@8743: 
nipkow@8743: \index{*primrec|)}
nipkow@8743: \index{*datatype|)}
nipkow@8743: 
nipkow@8743: \subsection{Case study: Tries}
nipkow@8743: 
nipkow@8743: Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
nipkow@8743: indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
nipkow@8743: trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
nipkow@8743: ``cat''.  When searching a string in a trie, the letters of the string are
nipkow@8743: examined sequentially. Each letter determines which subtrie to search next.
nipkow@8743: In this case study we model tries as a datatype, define a lookup and an
nipkow@8743: update function, and prove that they behave as expected.
nipkow@8743: 
nipkow@8743: \begin{figure}[htbp]
nipkow@8743: \begin{center}
nipkow@8743: \unitlength1mm
nipkow@8743: \begin{picture}(60,30)
nipkow@8743: \put( 5, 0){\makebox(0,0)[b]{l}}
nipkow@8743: \put(25, 0){\makebox(0,0)[b]{e}}
nipkow@8743: \put(35, 0){\makebox(0,0)[b]{n}}
nipkow@8743: \put(45, 0){\makebox(0,0)[b]{r}}
nipkow@8743: \put(55, 0){\makebox(0,0)[b]{t}}
nipkow@8743: %
nipkow@8743: \put( 5, 9){\line(0,-1){5}}
nipkow@8743: \put(25, 9){\line(0,-1){5}}
nipkow@8743: \put(44, 9){\line(-3,-2){9}}
nipkow@8743: \put(45, 9){\line(0,-1){5}}
nipkow@8743: \put(46, 9){\line(3,-2){9}}
nipkow@8743: %
nipkow@8743: \put( 5,10){\makebox(0,0)[b]{l}}
nipkow@8743: \put(15,10){\makebox(0,0)[b]{n}}
nipkow@8743: \put(25,10){\makebox(0,0)[b]{p}}
nipkow@8743: \put(45,10){\makebox(0,0)[b]{a}}
nipkow@8743: %
nipkow@8743: \put(14,19){\line(-3,-2){9}}
nipkow@8743: \put(15,19){\line(0,-1){5}}
nipkow@8743: \put(16,19){\line(3,-2){9}}
nipkow@8743: \put(45,19){\line(0,-1){5}}
nipkow@8743: %
nipkow@8743: \put(15,20){\makebox(0,0)[b]{a}}
nipkow@8743: \put(45,20){\makebox(0,0)[b]{c}}
nipkow@8743: %
nipkow@8743: \put(30,30){\line(-3,-2){13}}
nipkow@8743: \put(30,30){\line(3,-2){13}}
nipkow@8743: \end{picture}
nipkow@8743: \end{center}
nipkow@8743: \caption{A sample trie}
nipkow@8743: \label{fig:trie}
nipkow@8743: \end{figure}
nipkow@8743: 
nipkow@8743: Proper tries associate some value with each string. Since the
nipkow@8743: information is stored only in the final node associated with the string, many
nipkow@8743: nodes do not carry any value. This distinction is captured by the
nipkow@8771: following predefined datatype (from theory \isa{Option}, which is a parent
nipkow@8771: of \isa{Main}):
nipkow@8771: \smallskip
nipkow@8743: \input{Trie/document/Option2.tex}
nipkow@8771: \indexbold{*option}\indexbold{*None}\indexbold{*Some}%
nipkow@8743: \input{Trie/document/Trie.tex}
nipkow@8743: 
nipkow@8743: \begin{exercise}
nipkow@8743:   Write an improved version of \isa{update} that does not suffer from the
nipkow@8743:   space leak in the version above. Prove the main theorem for your improved
nipkow@8743:   \isa{update}.
nipkow@8743: \end{exercise}
nipkow@8743: 
nipkow@8743: \begin{exercise}
nipkow@8743:   Write a function to \emph{delete} entries from a trie. An easy solution is
nipkow@8743:   a clever modification of \isa{update} which allows both insertion and
nipkow@8743:   deletion with a single function.  Prove (a modified version of) the main
nipkow@8743:   theorem above. Optimize you function such that it shrinks tries after
nipkow@8743:   deletion, if possible.
nipkow@8743: \end{exercise}
nipkow@8743: 
nipkow@8743: \section{Total recursive functions}
nipkow@8743: \label{sec:recdef}
nipkow@8743: \index{*recdef|(}
nipkow@8743: 
nipkow@8743: Although many total functions have a natural primitive recursive definition,
nipkow@8743: this is not always the case. Arbitrary total recursive functions can be
nipkow@8743: defined by means of \isacommand{recdef}: you can use full pattern-matching,
nipkow@8743: recursion need not involve datatypes, and termination is proved by showing
nipkow@8743: that the arguments of all recursive calls are smaller in a suitable (user
nipkow@8743: supplied) sense.
nipkow@8743: 
nipkow@8743: \subsection{Defining recursive functions}
nipkow@8743: 
nipkow@8743: \input{Recdef/document/examples.tex}
nipkow@8743: 
nipkow@8743: \subsection{Proving termination}
nipkow@8743: 
nipkow@8743: \input{Recdef/document/termination.tex}
nipkow@8743: 
nipkow@8743: \subsection{Simplification with recdef}
paulson@10181: \label{sec:recdef-simplification}
nipkow@8743: 
nipkow@8743: \input{Recdef/document/simplification.tex}
nipkow@8743: 
nipkow@8743: \subsection{Induction}
nipkow@8743: \index{induction!recursion|(}
nipkow@8743: \index{recursion induction|(}
nipkow@8743: 
nipkow@8743: \input{Recdef/document/Induction.tex}
nipkow@9644: \label{sec:recdef-induction}
nipkow@8743: 
nipkow@8743: \index{induction!recursion|)}
nipkow@8743: \index{recursion induction|)}
nipkow@8743: \index{*recdef|)}