8743

1 
\chapter{Functional Programming in HOL}


2 


3 
Although on the surface this chapter is mainly concerned with how to write


4 
functional programs in HOL and how to verify them, most of the


5 
constructs and proof procedures introduced are general purpose and recur in


6 
any specification or verification task.


7 

9541

8 
The dedicated functional programmer should be warned: HOL offers only


9 
\emph{total functional programming}  all functions in HOL must be total;


10 
lazy data structures are not directly available. On the positive side,


11 
functions in HOL need not be computable: HOL is a specification language that


12 
goes well beyond what can be expressed as a program. However, for the time


13 
being we concentrate on the computable.

8743

14 


15 
\section{An introductory theory}


16 
\label{sec:introtheory}


17 


18 
Functional programming needs datatypes and functions. Both of them can be


19 
defined in a theory with a syntax reminiscent of languages like ML or


20 
Haskell. As an example consider the theory in figure~\ref{fig:ToyList}.


21 
We will now examine it line by line.


22 


23 
\begin{figure}[htbp]


24 
\begin{ttbox}\makeatother


25 
\input{ToyList2/ToyList1}\end{ttbox}


26 
\caption{A theory of lists}


27 
\label{fig:ToyList}


28 
\end{figure}


29 


30 
{\makeatother\input{ToyList/document/ToyList.tex}}


31 


32 
The complete proof script is shown in figure~\ref{fig:ToyListproofs}. The


33 
concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyListproofs}


34 
constitutes the complete theory \texttt{ToyList} and should reside in file


35 
\texttt{ToyList.thy}. It is good practice to present all declarations and


36 
definitions at the beginning of a theory to facilitate browsing.


37 


38 
\begin{figure}[htbp]


39 
\begin{ttbox}\makeatother


40 
\input{ToyList2/ToyList2}\end{ttbox}


41 
\caption{Proofs about lists}


42 
\label{fig:ToyListproofs}


43 
\end{figure}


44 


45 
\subsubsection*{Review}


46 


47 
This is the end of our toy proof. It should have familiarized you with


48 
\begin{itemize}


49 
\item the standard theorem proving procedure:


50 
state a goal (lemma or theorem); proceed with proof until a separate lemma is


51 
required; prove that lemma; come back to the original goal.


52 
\item a specific procedure that works well for functional programs:


53 
induction followed by allout simplification via \isa{auto}.


54 
\item a basic repertoire of proof commands.


55 
\end{itemize}


56 


57 


58 
\section{Some helpful commands}


59 
\label{sec:commandsandhints}


60 


61 
This section discusses a few basic commands for manipulating the proof state


62 
and can be skipped by casual readers.


63 


64 
There are two kinds of commands used during a proof: the actual proof


65 
commands and auxiliary commands for examining the proof state and controlling


66 
the display. Simple proof commands are of the form


67 
\isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a


68 
synonym for ``theorem proving function''. Typical examples are


69 
\isa{induct_tac} and \isa{auto}. Further methods are introduced throughout


70 
the tutorial. Unless stated otherwise you may assume that a method attacks


71 
merely the first subgoal. An exception is \isa{auto} which tries to solve all


72 
subgoals.


73 


74 
The most useful auxiliary commands are:


75 
\begin{description}


76 
\item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the


77 
last command; \isacommand{undo} can be undone by


78 
\isacommand{redo}\indexbold{*redo}. Both are only needed at the shell


79 
level and should not occur in the final theory.


80 
\item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays


81 
the current proof state, for example when it has disappeared off the


82 
screen.


83 
\item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to


84 
print only the first $n$ subgoals from now on and redisplays the current


85 
proof state. This is helpful when there are many subgoals.


86 
\item[Modifying the order of subgoals:]


87 
\isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and


88 
\isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front.


89 
\item[Printing theorems:]


90 
\isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$


91 
prints the named theorems.


92 
\item[Displaying types:] We have already mentioned the flag


93 
\ttindex{show_types} above. It can also be useful for detecting typos in


94 
formulae early on. For example, if \texttt{show_types} is set and the goal


95 
\isa{rev(rev xs) = xs} is started, Isabelle prints the additional output


96 
\par\noindent


97 
\begin{isabelle}%


98 
Variables:\isanewline


99 
~~xs~::~'a~list


100 
\end{isabelle}%


101 
\par\noindent


102 
which tells us that Isabelle has correctly inferred that


103 
\isa{xs} is a variable of list type. On the other hand, had we


104 
made a typo as in \isa{rev(re xs) = xs}, the response


105 
\par\noindent


106 
\begin{isabelle}%


107 
Variables:\isanewline


108 
~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline


109 
~~xs~::~'a~list%


110 
\end{isabelle}%


111 
\par\noindent


112 
would have alerted us because of the unexpected variable \isa{re}.


113 
\item[Reading terms and types:] \isacommand{term}\indexbold{*term}


114 
\textit{string} reads, typechecks and prints the given string as a term in


115 
the current context; the inferred type is output as well.


116 
\isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given


117 
string as a type in the current context.


118 
\item[(Re)loading theories:] When you start your interaction you must open a

8771

119 
named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle


120 
automatically loads all the required parent theories from their respective


121 
files (which may take a moment, unless the theories are already loaded and

9541

122 
the files have not been modified).

8743

123 


124 
If you suddenly discover that you need to modify a parent theory of your

9494

125 
current theory you must first abandon your current theory\indexbold{abandon


126 
theory}\indexbold{theory!abandon} (at the shell

8743

127 
level type \isacommand{kill}\indexbold{*kill}). After the parent theory has


128 
been modified you go back to your original theory. When its first line


129 
\isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the


130 
modified parent is reloaded automatically.

9541

131 


132 
The only time when you need to load a theory by hand is when you simply


133 
want to check if it loads successfully without wanting to make use of the


134 
theory itself. This you can do by typing


135 
\isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.

8743

136 
\end{description}


137 
Further commands are found in the Isabelle/Isar Reference Manual.


138 

8771

139 
We now examine Isabelle's functional programming constructs systematically,


140 
starting with inductive datatypes.


141 

8743

142 


143 
\section{Datatypes}


144 
\label{sec:datatype}


145 


146 
Inductive datatypes are part of almost every nontrivial application of HOL.


147 
First we take another look at a very important example, the datatype of


148 
lists, before we turn to datatypes in general. The section closes with a


149 
case study.


150 


151 


152 
\subsection{Lists}


153 
\indexbold{*list}


154 


155 
Lists are one of the essential datatypes in computing. Readers of this


156 
tutorial and users of HOL need to be familiar with their basic operations.

8771

157 
Theory \isa{ToyList} is only a small fragment of HOL's predefined theory


158 
\isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.

8743

159 
The latter contains many further operations. For example, the functions

8771

160 
\isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first

8743

161 
element and the remainder of a list. (However, patternmatching is usually

8771

162 
preferable to \isa{hd} and \isa{tl}.) Theory \isa{List} also contains

8743

163 
more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates


164 
$x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we


165 
always use HOL's predefined lists.


166 


167 


168 
\subsection{The general format}


169 
\label{sec:generaldatatype}


170 


171 
The general HOL \isacommand{datatype} definition is of the form


172 
\[


173 
\isacommand{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~


174 
C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~


175 
C@m~\tau@{m1}~\dots~\tau@{mk@m}


176 
\]

8771

177 
where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct

8743

178 
constructor names and $\tau@{ij}$ are types; it is customary to capitalize


179 
the first letter in constructor names. There are a number of


180 
restrictions (such as that the type should not be empty) detailed


181 
elsewhere~\cite{isabelleHOL}. Isabelle notifies you if you violate them.


182 


183 
Laws about datatypes, such as \isa{[] \isasymnoteq~x\#xs} and


184 
\isa{(x\#xs = y\#ys) = (x=y \isasymand~xs=ys)}, are used automatically


185 
during proofs by simplification. The same is true for the equations in


186 
primitive recursive function definitions.


187 

9644

188 
Every datatype $t$ comes equipped with a \isa{size} function from $t$ into


189 
the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is


190 
just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +


191 
1}. In general, \isa{size} returns \isa{0} for all constructors that do


192 
not have an argument of type $t$, and for all other constructors \isa{1 +}


193 
the sum of the sizes of all arguments of type $t$. Note that because


194 
\isa{size} is defined on every datatype, it is overloaded; on lists


195 
\isa{size} is also called \isa{length}, which is not overloaded.


196 


197 

8743

198 
\subsection{Primitive recursion}


199 


200 
Functions on datatypes are usually defined by recursion. In fact, most of the


201 
time they are defined by what is called \bfindex{primitive recursion}.


202 
The keyword \isacommand{primrec}\indexbold{*primrec} is followed by a list of


203 
equations


204 
\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]


205 
such that $C$ is a constructor of the datatype $t$ and all recursive calls of


206 
$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus


207 
Isabelle immediately sees that $f$ terminates because one (fixed!) argument


208 
becomes smaller with every recursive call. There must be exactly one equation


209 
for each constructor. Their order is immaterial.

8771

210 
A more general method for defining total recursive functions is introduced in

8743

211 
\S\ref{sec:recdef}.


212 

9493

213 
\begin{exercise}\label{ex:Tree}

8743

214 
\input{Misc/document/Tree.tex}%


215 
\end{exercise}


216 

9721

217 
\input{Misc/document/case_exprs.tex}

8743

218 


219 
\begin{warn}


220 
Induction is only allowed on free (or \isasymAndbound) variables that

9644

221 
should not occur among the assumptions of the subgoal; see


222 
\S\ref{sec:indvarinprems} for details. Case distinction

8743

223 
(\isa{case_tac}) works for arbitrary terms, which need to be


224 
quoted if they are nonatomic.


225 
\end{warn}


226 


227 


228 
\input{Ifexpr/document/Ifexpr.tex}


229 


230 
\section{Some basic types}


231 


232 


233 
\subsection{Natural numbers}

9644

234 
\label{sec:nat}

8743

235 
\index{arithmetic(}


236 


237 
\input{Misc/document/fakenat.tex}


238 
\input{Misc/document/natsum.tex}


239 


240 
The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},


241 
\ttindexboldpos{}{$HOL2arithfun}, \ttindexboldpos{*}{$HOL2arithfun},


242 
\isaindexbold{div}, \isaindexbold{mod}, \isaindexbold{min} and


243 
\isaindexbold{max} are predefined, as are the relations


244 
\indexboldpos{\isasymle}{$HOL2arithrel} and


245 
\ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation


246 
\isaindexbold{LEAST}. For example, \isa{(LEAST n.$\,$1 < n) = 2}, although


247 
Isabelle does not prove this completely automatically. Note that \isa{1} and


248 
\isa{2} are available as abbreviations for the corresponding


249 
\isa{Suc}expressions. If you need the full set of numerals,


250 
see~\S\ref{natnumerals}.


251 


252 
\begin{warn}

9494

253 
The constant \ttindexbold{0} and the operations


254 
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{}{$HOL2arithfun},


255 
\ttindexboldpos{*}{$HOL2arithfun}, \isaindexbold{min}, \isaindexbold{max},

8743

256 
\indexboldpos{\isasymle}{$HOL2arithrel} and


257 
\ttindexboldpos{<}{$HOL2arithrel} are overloaded, i.e.\ they are available


258 
not just for natural numbers but at other types as well (see

9494

259 
\S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there


260 
is nothing to indicate that you are talking about natural numbers. Hence


261 
Isabelle can only infer that \isa{x} is of some arbitrary type where


262 
\isa{0} and \isa{+} are declared. As a consequence, you will be unable to


263 
prove the goal (although it may take you some time to realize what has


264 
happened if \texttt{show_types} is not set). In this particular example,


265 
you need to include an explicit type constraint, for example \isa{x+0 =


266 
(x::nat)}. If there is enough contextual information this may not be


267 
necessary: \isa{Suc x = x} automatically implies \isa{x::nat} because


268 
\isa{Suc} is not overloaded.

8743

269 
\end{warn}


270 


271 
Simple arithmetic goals are proved automatically by both \isa{auto}


272 
and the simplification methods introduced in \S\ref{sec:Simplification}. For


273 
example,


274 


275 
\input{Misc/document/arith1.tex}%


276 
is proved automatically. The main restriction is that only addition is taken


277 
into account; other arithmetic operations and quantified formulae are ignored.


278 


279 
For more complex goals, there is the special method


280 
\isaindexbold{arith} (which attacks the first subgoal). It proves


281 
arithmetic goals involving the usual logical connectives (\isasymnot,


282 
\isasymand, \isasymor, \isasymimp), the relations \isasymle\ and \isa{<}, and


283 
the operations \isa{+}, \isa{}, \isa{min} and \isa{max}. For example,


284 


285 
\input{Misc/document/arith2.tex}%


286 
succeeds because \isa{k*k} can be treated as atomic.


287 
In contrast,


288 


289 
\input{Misc/document/arith3.tex}%


290 
is not even proved by \isa{arith} because the proof relies essentially


291 
on properties of multiplication.


292 


293 
\begin{warn}


294 
The running time of \isa{arith} is exponential in the number of occurrences


295 
of \ttindexboldpos{}{$HOL2arithfun}, \isaindexbold{min} and


296 
\isaindexbold{max} because they are first eliminated by case distinctions.


297 


298 
\isa{arith} is incomplete even for the restricted class of formulae


299 
described above (known as ``linear arithmetic''). If divisibility plays a


300 
role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$.


301 
Fortunately, such examples are rare in practice.


302 
\end{warn}


303 


304 
\index{arithmetic)}


305 


306 


307 
\subsection{Products}

9541

308 
\input{Misc/document/pairs.tex}

8743

309 


310 
%FIXME move stuff below into section on proofs about products?


311 
\begin{warn}


312 
Abstraction over pairs and tuples is merely a convenient shorthand for a


313 
more complex internal representation. Thus the internal and external form


314 
of a term may differ, which can affect proofs. If you want to avoid this


315 
complication, use \isa{fst} and \isa{snd}, i.e.\ write


316 
\isa{\isasymlambda{}p.~fst p + snd p} instead of


317 
\isa{\isasymlambda(x,y).~x + y}. See~\S\ref{proofsaboutproducts} for


318 
theorem proving with tuple patterns.


319 
\end{warn}


320 

9541

321 
Note that products, like natural numbers, are datatypes, which means

8743

322 
in particular that \isa{induct_tac} and \isa{case_tac} are applicable to


323 
products (see \S\ref{proofsaboutproducts}).


324 

9541

325 
Instead of tuples with many components (where ``many'' is not much above 2),


326 
it is far preferable to use record types (see \S\ref{sec:records}).


327 

8743

328 
\section{Definitions}


329 
\label{sec:Definitions}


330 


331 
A definition is simply an abbreviation, i.e.\ a new name for an existing


332 
construction. In particular, definitions cannot be recursive. Isabelle offers


333 
definitions on the level of types and terms. Those on the type level are


334 
called type synonyms, those on the term level are called (constant)


335 
definitions.


336 


337 


338 
\subsection{Type synonyms}

8771

339 
\indexbold{type synonym}

8743

340 


341 
Type synonyms are similar to those found in ML. Their syntax is fairly self


342 
explanatory:


343 


344 
\input{Misc/document/types.tex}%


345 


346 
Note that patternmatching is not allowed, i.e.\ each definition must be of


347 
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.


348 
Section~\S\ref{sec:Simplification} explains how definitions are used


349 
in proofs.


350 

9844

351 
\input{Misc/document/prime_def.tex}

8743

352 


353 


354 
\chapter{More Functional Programming}


355 


356 
The purpose of this chapter is to deepen the reader's understanding of the

8771

357 
concepts encountered so far and to introduce advanced forms of datatypes and


358 
recursive functions. The first two sections give a structured presentation of


359 
theorem proving by simplification (\S\ref{sec:Simplification}) and discuss


360 
important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can


361 
be skipped by readers less interested in proofs. They are followed by a case


362 
study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced


363 
datatypes, including those involving function spaces, are covered in


364 
\S\ref{sec:advanceddatatypes}, which closes with another case study, search


365 
trees (``tries''). Finally we introduce \isacommand{recdef}, a very general


366 
form of recursive function definition which goes well beyond what


367 
\isacommand{primrec} allows (\S\ref{sec:recdef}).

8743

368 


369 


370 
\section{Simplification}


371 
\label{sec:Simplification}


372 
\index{simplification(}


373 

9541

374 
So far we have proved our theorems by \isa{auto}, which ``simplifies''


375 
\emph{all} subgoals. In fact, \isa{auto} can do much more than that, except


376 
that it did not need to so far. However, when you go beyond toy examples, you


377 
need to understand the ingredients of \isa{auto}. This section covers the


378 
method that \isa{auto} always applies first, namely simplification.

8743

379 


380 
Simplification is one of the central theorem proving tools in Isabelle and


381 
many other systems. The tool itself is called the \bfindex{simplifier}. The

9754

382 
purpose of this section is introduce the many features of the simplifier.


383 
Anybody intending to use HOL should read this section. Later on


384 
(\S\ref{sec:simplificationII}) we explain some more advanced features and a


385 
little bit of how the simplifier works. The serious student should read that


386 
section as well, in particular in order to understand what happened if things


387 
do not simplify as expected.

8743

388 

9458

389 
\subsubsection{What is simplification}


390 

8743

391 
In its most basic form, simplification means repeated application of


392 
equations from left to right. For example, taking the rules for \isa{\at}


393 
and applying them to the term \isa{[0,1] \at\ []} results in a sequence of


394 
simplification steps:


395 
\begin{ttbox}\makeatother


396 
(0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[]


397 
\end{ttbox}

9933

398 
This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the


399 
equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.


400 
``Rewriting'' is more honest than ``simplification'' because the terms do not


401 
necessarily become simpler in the process.

8743

402 

9844

403 
\input{Misc/document/simp.tex}

8743

404 


405 
\index{simplification)}


406 

9844

407 
\input{Misc/document/Itrev.tex}

8743

408 

9493

409 
\begin{exercise}


410 
\input{Misc/document/Tree2.tex}%


411 
\end{exercise}

8743

412 

9844

413 
\input{CodeGen/document/CodeGen.tex}

8743

414 


415 


416 
\section{Advanced datatypes}


417 
\label{sec:advanceddatatypes}


418 
\index{*datatype(}


419 
\index{*primrec(}


420 
%)


421 


422 
This section presents advanced forms of \isacommand{datatype}s.


423 


424 
\subsection{Mutual recursion}


425 
\label{sec:datatypemutrec}


426 


427 
\input{Datatype/document/ABexpr.tex}


428 


429 
\subsection{Nested recursion}

9644

430 
\label{sec:nesteddatatype}

8743

431 

9644

432 
{\makeatother\input{Datatype/document/Nested.tex}}

8743

433 


434 


435 
\subsection{The limits of nested recursion}


436 


437 
How far can we push nested recursion? By the unfolding argument above, we can


438 
reduce nested to mutual recursion provided the nested recursion only involves


439 
previously defined datatypes. This does not include functions:

9792

440 
\begin{isabelle}


441 
\isacommand{datatype} t = C "t \isasymRightarrow\ bool"


442 
\end{isabelle}

8743

443 
is a real can of worms: in HOL it must be ruled out because it requires a type


444 
\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the


445 
same cardinalityan impossibility. For the same reason it is not possible


446 
to allow recursion involving the type \isa{set}, which is isomorphic to


447 
\isa{t \isasymFun\ bool}.


448 


449 
Fortunately, a limited form of recursion


450 
involving function spaces is permitted: the recursive type may occur on the


451 
right of a function arrow, but never on the left. Hence the above can of worms


452 
is ruled out but the following example of a potentially infinitely branching tree is


453 
accepted:

8771

454 
\smallskip

8743

455 


456 
\input{Datatype/document/Fundata.tex}


457 
\bigskip


458 

9792

459 
If you need nested recursion on the left of a function arrow, there are


460 
alternatives to pure HOL: LCF~\cite{paulson87} is a logic where types like


461 
\begin{isabelle}


462 
\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"


463 
\end{isabelle}


464 
do indeed make sense (but note the intentionally different arrow


465 
\isa{\isasymrightarrow}). There is even a version of LCF on top of HOL,


466 
called HOLCF~\cite{MuellerNvOS99}.

8743

467 


468 
\index{*primrec)}


469 
\index{*datatype)}


470 


471 
\subsection{Case study: Tries}


472 


473 
Tries are a classic search tree data structure~\cite{Knuth375} for fast


474 
indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a


475 
trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and


476 
``cat''. When searching a string in a trie, the letters of the string are


477 
examined sequentially. Each letter determines which subtrie to search next.


478 
In this case study we model tries as a datatype, define a lookup and an


479 
update function, and prove that they behave as expected.


480 


481 
\begin{figure}[htbp]


482 
\begin{center}


483 
\unitlength1mm


484 
\begin{picture}(60,30)


485 
\put( 5, 0){\makebox(0,0)[b]{l}}


486 
\put(25, 0){\makebox(0,0)[b]{e}}


487 
\put(35, 0){\makebox(0,0)[b]{n}}


488 
\put(45, 0){\makebox(0,0)[b]{r}}


489 
\put(55, 0){\makebox(0,0)[b]{t}}


490 
%


491 
\put( 5, 9){\line(0,1){5}}


492 
\put(25, 9){\line(0,1){5}}


493 
\put(44, 9){\line(3,2){9}}


494 
\put(45, 9){\line(0,1){5}}


495 
\put(46, 9){\line(3,2){9}}


496 
%


497 
\put( 5,10){\makebox(0,0)[b]{l}}


498 
\put(15,10){\makebox(0,0)[b]{n}}


499 
\put(25,10){\makebox(0,0)[b]{p}}


500 
\put(45,10){\makebox(0,0)[b]{a}}


501 
%


502 
\put(14,19){\line(3,2){9}}


503 
\put(15,19){\line(0,1){5}}


504 
\put(16,19){\line(3,2){9}}


505 
\put(45,19){\line(0,1){5}}


506 
%


507 
\put(15,20){\makebox(0,0)[b]{a}}


508 
\put(45,20){\makebox(0,0)[b]{c}}


509 
%


510 
\put(30,30){\line(3,2){13}}


511 
\put(30,30){\line(3,2){13}}


512 
\end{picture}


513 
\end{center}


514 
\caption{A sample trie}


515 
\label{fig:trie}


516 
\end{figure}


517 


518 
Proper tries associate some value with each string. Since the


519 
information is stored only in the final node associated with the string, many


520 
nodes do not carry any value. This distinction is captured by the

8771

521 
following predefined datatype (from theory \isa{Option}, which is a parent


522 
of \isa{Main}):


523 
\smallskip

8743

524 
\input{Trie/document/Option2.tex}

8771

525 
\indexbold{*option}\indexbold{*None}\indexbold{*Some}%

8743

526 
\input{Trie/document/Trie.tex}


527 


528 
\begin{exercise}


529 
Write an improved version of \isa{update} that does not suffer from the


530 
space leak in the version above. Prove the main theorem for your improved


531 
\isa{update}.


532 
\end{exercise}


533 


534 
\begin{exercise}


535 
Write a function to \emph{delete} entries from a trie. An easy solution is


536 
a clever modification of \isa{update} which allows both insertion and


537 
deletion with a single function. Prove (a modified version of) the main


538 
theorem above. Optimize you function such that it shrinks tries after


539 
deletion, if possible.


540 
\end{exercise}


541 


542 
\section{Total recursive functions}


543 
\label{sec:recdef}


544 
\index{*recdef(}


545 


546 
Although many total functions have a natural primitive recursive definition,


547 
this is not always the case. Arbitrary total recursive functions can be


548 
defined by means of \isacommand{recdef}: you can use full patternmatching,


549 
recursion need not involve datatypes, and termination is proved by showing


550 
that the arguments of all recursive calls are smaller in a suitable (user


551 
supplied) sense.


552 


553 
\subsection{Defining recursive functions}


554 


555 
\input{Recdef/document/examples.tex}


556 


557 
\subsection{Proving termination}


558 


559 
\input{Recdef/document/termination.tex}


560 


561 
\subsection{Simplification with recdef}

10181

562 
\label{sec:recdefsimplification}

8743

563 


564 
\input{Recdef/document/simplification.tex}


565 


566 
\subsection{Induction}


567 
\index{induction!recursion(}


568 
\index{recursion induction(}


569 


570 
\input{Recdef/document/Induction.tex}

9644

571 
\label{sec:recdefinduction}

8743

572 


573 
\index{induction!recursion)}


574 
\index{recursion induction)}


575 
\index{*recdef)}
