paulson@11419

1 
\chapter{Functional Programming in HOL}

paulson@11419

2 

paulson@11419

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

paulson@11419

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

paulson@11419

5 
proof procedures introduced are general purpose and recur in any specification

paulson@11419

6 
or verification task. In fact, we really should speak of functional

paulson@11419

7 
\emph{modelling} rather than \emph{programming}: our primary aim is not

paulson@11419

8 
to write programs but to design abstract models of systems. HOL is

paulson@11419

9 
a specification language that goes well beyond what can be expressed as a

paulson@11419

10 
program. However, for the time being we concentrate on the computable.

paulson@11419

11 

paulson@11419

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

paulson@11419

13 
\emph{total functional programming}  all functions in HOL must be total,

paulson@11419

14 
i.e.\ they must terminate for all inputs; lazy data structures are not

paulson@11419

15 
directly available.

paulson@11419

16 

paulson@11419

17 
\section{An Introductory Theory}

paulson@11419

18 
\label{sec:introtheory}

paulson@11419

19 

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

23 
We will now examine it line by line.

paulson@11419

24 

paulson@11419

25 
\begin{figure}[htbp]

paulson@11419

26 
\begin{ttbox}\makeatother

paulson@11419

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

paulson@11419

28 
\caption{A theory of lists}

paulson@11419

29 
\label{fig:ToyList}

paulson@11419

30 
\end{figure}

paulson@11419

31 

paulson@11419

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

paulson@11419

33 

paulson@11419

34 
The complete proof script is shown in Fig.\ts\ref{fig:ToyListproofs}. The

paulson@11419

35 
concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyListproofs}

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

39 

paulson@11419

40 
\begin{figure}[htbp]

paulson@11419

41 
\begin{ttbox}\makeatother

paulson@11419

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

paulson@11419

43 
\caption{Proofs about lists}

paulson@11419

44 
\label{fig:ToyListproofs}

paulson@11419

45 
\end{figure}

paulson@11419

46 

paulson@11419

47 
\subsubsection*{Review}

paulson@11419

48 

paulson@11419

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

paulson@11419

50 
\begin{itemize}

paulson@11419

51 
\item the standard theorem proving procedure:

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

56 
\item a basic repertoire of proof commands.

nipkow@8743

57 
\end{itemize}

nipkow@8743

58 

nipkow@8743

59 

paulson@10885

60 
\section{Some Helpful Commands}

nipkow@8743

61 
\label{sec:commandsandhints}

nipkow@8743

62 

nipkow@8743

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

nipkow@8743

64 
and can be skipped by casual readers.

nipkow@8743

65 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

68 
the display. Simple proof commands are of the form

paulson@11419

69 
\commdx{apply}\isa{(method)}, where \isa{method} is typically

paulson@11419

70 
\isa{induct_tac} or \isa{auto}. All such theorem proving operations

paulson@11419

71 
are referred to as \bfindex{methods}, and further ones are

paulson@11419

72 
introduced throughout the tutorial. Unless stated otherwise, you may

paulson@11419

73 
assume that a method attacks merely the first subgoal. An exception is

paulson@11419

74 
\isa{auto}, which tries to solve all subgoals.

nipkow@8743

75 

paulson@11419

76 
The most useful auxiliary commands are as follows:

nipkow@8743

77 
\begin{description}

paulson@11419

78 
\item[Undoing:] \commdx{undo} undoes the effect of

paulson@11419

79 
the

nipkow@8743

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

paulson@11419

81 
\commdx{redo}. Both are only needed at the shell

nipkow@8743

82 
level and should not occur in the final theory.

paulson@11419

83 
\item[Printing the current state:] \commdx{pr}

paulson@11419

84 
redisplays

paulson@11302

85 
the current proof state, for example when it has scrolled past the top of

paulson@11302

86 
the screen.

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

90 
\item[Modifying the order of subgoals:]

paulson@11419

91 
\commdx{defer} moves the first subgoal to the end and

paulson@11419

92 
\commdx{prefer}~$n$ moves subgoal $n$ to the front.

nipkow@8743

93 
\item[Printing theorems:]

paulson@11419

94 
\commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$

nipkow@8743

95 
prints the named theorems.

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

100 
\par\noindent

nipkow@8743

101 
\begin{isabelle}%

nipkow@8743

102 
Variables:\isanewline

nipkow@8743

103 
~~xs~::~'a~list

nipkow@8743

104 
\end{isabelle}%

nipkow@8743

105 
\par\noindent

nipkow@8743

106 
which tells us that Isabelle has correctly inferred that

nipkow@8743

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

nipkow@8743

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

nipkow@8743

109 
\par\noindent

nipkow@8743

110 
\begin{isabelle}%

nipkow@8743

111 
Variables:\isanewline

nipkow@8743

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

nipkow@8743

113 
~~xs~::~'a~list%

nipkow@8743

114 
\end{isabelle}%

nipkow@8743

115 
\par\noindent

nipkow@8743

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

paulson@11419

117 
\item[Reading terms and types:] \commdx{term}

nipkow@8743

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

nipkow@8743

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

paulson@11419

120 
\commdx{typ} \textit{string} reads and prints the given

nipkow@8743

121 
string as a type in the current context.

nipkow@8743

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

nipkow@8771

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

nipkow@8771

124 
automatically loads all the required parent theories from their respective

nipkow@8771

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

nipkow@9541

126 
the files have not been modified).

nipkow@8743

127 

nipkow@8743

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

paulson@11428

129 
current theory, you must first abandon your current theory%

paulson@11428

130 
\indexbold{abandoning a theory}\indexbold{theories!abandoning}

paulson@11428

131 
(at the shell

paulson@11419

132 
level type \commdx{kill}). After the parent theory has

nipkow@10971

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

nipkow@10971

134 
\isa{\isacommand{theory}~T~=~\dots~:} is processed, the

nipkow@8743

135 
modified parent is reloaded automatically.

nipkow@9541

136 

nipkow@10978

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

nipkow@10978

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

nipkow@10978

139 
% theory itself. This you can do by typing

paulson@11419

140 
% \isa{\commdx{use\_thy}~"T"}.

nipkow@8743

141 
\end{description}

nipkow@8743

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

nipkow@8743

143 

nipkow@8771

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

nipkow@8771

145 
starting with inductive datatypes.

nipkow@8771

146 

nipkow@8743

147 

nipkow@8743

148 
\section{Datatypes}

nipkow@8743

149 
\label{sec:datatype}

nipkow@8743

150 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

154 
case study.

nipkow@8743

155 

nipkow@8743

156 

nipkow@8743

157 
\subsection{Lists}

nipkow@8743

158 

paulson@11428

159 
\index{*list (type)}%

nipkow@8743

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

nipkow@8743

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

nipkow@8771

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

paulson@11428

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

nipkow@8743

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

paulson@11419

165 
\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first

nipkow@8743

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

paulson@10795

167 
preferable to \isa{hd} and \isa{tl}.)

nipkow@10800

168 
Also available are higherorder functions like \isa{map} and \isa{filter}.

paulson@10795

169 
Theory \isa{List} also contains

nipkow@8743

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

nipkow@8743

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

nipkow@8743

172 
always use HOL's predefined lists.

nipkow@8743

173 

nipkow@8743

174 

paulson@10885

175 
\subsection{The General Format}

nipkow@8743

176 
\label{sec:generaldatatype}

nipkow@8743

177 

nipkow@8743

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

nipkow@8743

179 
\[

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

183 
\]

nipkow@8771

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

189 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

193 
primitive recursive function definitions.

nipkow@8743

194 

nipkow@9644

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

nipkow@10538

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

nipkow@9644

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

paulson@11419

198 
1}. In general, \cdx{size} returns \isa{0} for all constructors

nipkow@10237

199 
that do not have an argument of type $t$, and for all other constructors

nipkow@10237

200 
\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because

nipkow@9644

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

paulson@11419

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

paulson@10795

203 
Isabelle will always show \isa{size} on lists as \isa{length}.

nipkow@9644

204 

nipkow@9644

205 

paulson@10885

206 
\subsection{Primitive Recursion}

nipkow@8743

207 

nipkow@8743

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

paulson@11428

209 
time they are defined by what is called \textbf{primitive recursion}.

paulson@11428

210 
The keyword \commdx{primrec} is followed by a list of

nipkow@8743

211 
equations

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@10654

216 
becomes smaller with every recursive call. There must be at most one equation

nipkow@8743

217 
for each constructor. Their order is immaterial.

nipkow@8771

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

nipkow@10538

219 
{\S}\ref{sec:recdef}.

nipkow@8743

220 

nipkow@9493

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

nipkow@8743

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

nipkow@8743

223 
\end{exercise}

nipkow@8743

224 

nipkow@9721

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

nipkow@8743

226 

nipkow@8743

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

nipkow@8743

228 

paulson@10885

229 
\section{Some Basic Types}

nipkow@8743

230 

nipkow@8743

231 

paulson@10885

232 
\subsection{Natural Numbers}

nipkow@9644

233 
\label{sec:nat}

paulson@11428

234 
\index{linear arithmetic(}

nipkow@8743

235 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

238 

paulson@11428

239 
\index{linear arithmetic)}

nipkow@8743

240 

nipkow@8743

241 

nipkow@10396

242 
\subsection{Pairs}

nipkow@9541

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

nipkow@8743

244 

nipkow@10608

245 
\subsection{Datatype {\tt\slshape option}}

nipkow@10543

246 
\label{sec:option}

nipkow@10543

247 
\input{Misc/document/Option2.tex}

nipkow@10543

248 

nipkow@8743

249 
\section{Definitions}

nipkow@8743

250 
\label{sec:Definitions}

nipkow@8743

251 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

256 
definitions.

nipkow@8743

257 

nipkow@8743

258 

paulson@10885

259 
\subsection{Type Synonyms}

nipkow@8743

260 

paulson@11428

261 
\indexbold{type synonyms(}%

paulson@11428

262 
Type synonyms are similar to those found in ML\@. They are issued by a

paulson@11428

263 
\commdx{types} command:

nipkow@8743

264 

nipkow@8743

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

nipkow@8743

266 

nipkow@8743

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

nipkow@8743

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

nipkow@11215

269 
Section~{\S}\ref{sec:SimpwithDefs} explains how definitions are used

paulson@11428

270 
in proofs.%

paulson@11428

271 
\indexbold{type synonyms)}

nipkow@8743

272 

nipkow@9844

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

nipkow@8743

274 

nipkow@11203

275 
\input{Misc/document/Translations.tex}

nipkow@11203

276 

nipkow@8743

277 

nipkow@11201

278 
\section{The Definitional Approach}

nipkow@11201

279 
\label{sec:definitional}

nipkow@11201

280 

nipkow@11201

281 
As we pointed out at the beginning of the chapter, asserting arbitrary

nipkow@11201

282 
axioms, e.g. $f(n) = f(n) + 1$, may easily lead to contradictions. In order

nipkow@11201

283 
to avoid this danger, this tutorial advocates the definitional rather than

nipkow@11201

284 
the axiomatic approach: introduce new concepts by definitions, thus

nipkow@11201

285 
preserving consistency. However, on the face of it, Isabelle/HOL seems to

nipkow@11201

286 
support many more constructs than just definitions, for example

nipkow@11201

287 
\isacommand{primrec}. The crucial point is that internally, everything

nipkow@11201

288 
(except real axioms) is reduced to a definition. For example, given some

nipkow@11201

289 
\isacommand{primrec} function definition, this is turned into a proper

nipkow@11201

290 
(nonrecursive!) definition, and the usersupplied recursion equations are

nipkow@11213

291 
derived as theorems from that definition. This tricky process is completely

nipkow@11201

292 
hidden from the user and it is not necessary to understand the details. The

nipkow@11201

293 
result of the definitional approach is that \isacommand{primrec} is as safe

nipkow@11201

294 
as pure \isacommand{defs} are, but more convenient. And this is not just the

nipkow@11201

295 
case for \isacommand{primrec} but also for the other commands described

nipkow@11201

296 
later, like \isacommand{recdef} and \isacommand{inductive}.

nipkow@11203

297 
This strict adherence to the definitional approach reduces the risk of

nipkow@11203

298 
soundness errors inside Isabelle/HOL.

nipkow@11201

299 

nipkow@8743

300 
\chapter{More Functional Programming}

nipkow@8743

301 

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@10538

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

nipkow@10538

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

nipkow@8771

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

nipkow@10538

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

nipkow@8771

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

nipkow@10538

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

nipkow@8771

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

nipkow@8771

312 
form of recursive function definition which goes well beyond what

nipkow@10538

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

nipkow@8743

314 

nipkow@8743

315 

nipkow@8743

316 
\section{Simplification}

nipkow@8743

317 
\label{sec:Simplification}

nipkow@8743

318 
\index{simplification(}

nipkow@8743

319 

paulson@10795

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

nipkow@9541

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

nipkow@9541

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

nipkow@9541

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

nipkow@10971

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

nipkow@8743

325 

nipkow@8743

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

nipkow@8743

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

nipkow@11159

328 
purpose of this section is to introduce the many features of the simplifier.

nipkow@10971

329 
Anybody intending to perform proofs in HOL should read this section. Later on

nipkow@10538

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

nipkow@9754

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

nipkow@9754

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

nipkow@9754

333 
do not simplify as expected.

nipkow@8743

334 

nipkow@11214

335 
\subsection{What is Simplification}

nipkow@9458

336 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

340 
simplification steps:

nipkow@8743

341 
\begin{ttbox}\makeatother

nipkow@8743

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

nipkow@8743

343 
\end{ttbox}

nipkow@9933

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

nipkow@9933

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

nipkow@9933

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

nipkow@9933

347 
necessarily become simpler in the process.

nipkow@8743

348 

nipkow@9844

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

nipkow@8743

350 

nipkow@8743

351 
\index{simplification)}

nipkow@8743

352 

nipkow@9844

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

nipkow@8743

354 

nipkow@9493

355 
\begin{exercise}

nipkow@9493

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

nipkow@9493

357 
\end{exercise}

nipkow@8743

358 

nipkow@9844

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

nipkow@8743

360 

nipkow@8743

361 

paulson@10885

362 
\section{Advanced Datatypes}

nipkow@8743

363 
\label{sec:advanceddatatypes}

paulson@11428

364 
\index{datatype@\isacommand {datatype} (command)(}

paulson@11428

365 
\index{primrec@\isacommand {primrec} (command)(}

nipkow@8743

366 
%)

nipkow@8743

367 

paulson@11428

368 
This section presents advanced forms of datatypes: mutual and nested

paulson@11428

369 
recursion. A series of examples will culminate in a treatment of the trie

paulson@11428

370 
data structure.

paulson@11428

371 

nipkow@8743

372 

paulson@10885

373 
\subsection{Mutual Recursion}

nipkow@8743

374 
\label{sec:datatypemutrec}

nipkow@8743

375 

nipkow@8743

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

nipkow@8743

377 

paulson@10885

378 
\subsection{Nested Recursion}

nipkow@9644

379 
\label{sec:nesteddatatype}

nipkow@8743

380 

nipkow@9644

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

nipkow@8743

382 

nipkow@8743

383 

paulson@11419

384 
\subsection{The Limits of Nested Recursion}

paulson@11419

385 

paulson@11419

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

paulson@11419

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

paulson@11419

388 
previously defined datatypes. This does not include functions:

paulson@11419

389 
\begin{isabelle}

paulson@11419

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

paulson@11419

391 
\end{isabelle}

paulson@11419

392 
This declaration is a real can of worms.

paulson@11419

393 
In HOL it must be ruled out because it requires a type

paulson@11419

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

paulson@11419

395 
same cardinality  an impossibility. For the same reason it is not possible

paulson@11419

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

paulson@11419

397 
\isa{t \isasymFun\ bool}.

paulson@11419

398 

paulson@11419

399 
Fortunately, a limited form of recursion

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

403 
accepted:

paulson@11419

404 
\smallskip

paulson@11419

405 

paulson@11419

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

paulson@11419

407 
\bigskip

paulson@11419

408 

paulson@11419

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

paulson@11419

410 
alternatives to pure HOL\@. In the Logic for Computable Functions

paulson@11419

411 
(LCF), types like

paulson@11419

412 
\begin{isabelle}

paulson@11419

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

paulson@11419

414 
\end{isabelle}

paulson@11419

415 
do indeed make sense~\cite{paulson87}. Note the different arrow,

paulson@11419

416 
\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},

paulson@11419

417 
expressing the type of \emph{continuous} functions.

paulson@11419

418 
There is even a version of LCF on top of HOL,

paulson@11419

419 
called HOLCF~\cite{MuellerNvOS99}.

paulson@11428

420 
\index{datatype@\isacommand {datatype} (command))}

paulson@11428

421 
\index{primrec@\isacommand {primrec} (command))}

paulson@11419

422 

paulson@11419

423 

paulson@11419

424 
\subsection{Case Study: Tries}

paulson@11419

425 
\label{sec:Trie}

paulson@11419

426 

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

434 

paulson@11419

435 
\begin{figure}[htbp]

paulson@11419

436 
\begin{center}

nipkow@8743

437 
\unitlength1mm

nipkow@8743

438 
\begin{picture}(60,30)

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

444 
%

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

450 
%

nipkow@8743

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

nipkow@8743

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

paulson@11419

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

paulson@11419

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

paulson@11419

455 
%

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

460 
%

paulson@11419

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

paulson@11419

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

paulson@11419

463 
%

paulson@11419

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

paulson@11419

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

paulson@11419

466 
\end{picture}

paulson@11419

467 
\end{center}

paulson@11419

468 
\caption{A sample trie}

paulson@11419

469 
\label{fig:trie}

paulson@11419

470 
\end{figure}

paulson@11419

471 

paulson@11419

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

paulson@11419

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

paulson@11419

474 
nodes do not carry any value. This distinction is modeled with the help

paulson@11419

475 
of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).

paulson@11419

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

paulson@11419

477 

paulson@11419

478 
\section{Total Recursive Functions}

paulson@11419

479 
\label{sec:recdef}

paulson@11428

480 
\index{recdef@\isacommand {recdef} (command)(}\index{functions!total(}

paulson@11419

481 

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

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

paulson@11419

487 
supplied) sense. In this section we restrict ourselves to measure functions;

paulson@11419

488 
more advanced termination proofs are discussed in {\S}\ref{sec:beyondmeasure}.

paulson@11419

489 

paulson@11419

490 
\subsection{Defining Recursive Functions}

paulson@11419

491 
\label{sec:recdefexamples}

paulson@11419

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

paulson@11419

493 

paulson@11419

494 
\subsection{Proving Termination}

paulson@11419

495 

paulson@11419

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

paulson@11419

497 

paulson@11419

498 
\subsection{Simplification with Recdef}

paulson@11419

499 
\label{sec:recdefsimplification}

paulson@11419

500 

paulson@11419

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

paulson@11419

502 

paulson@11419

503 
\subsection{Induction}

paulson@11419

504 
\index{induction!recursion(}

nipkow@8743

505 
\index{recursion induction(}

nipkow@8743

506 

nipkow@8743

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

nipkow@9644

508 
\label{sec:recdefinduction}

nipkow@8743

509 

nipkow@8743

510 
\index{induction!recursion)}

nipkow@8743

511 
\index{recursion induction)}

paulson@11428

512 
\index{recdef@\isacommand {recdef} (command))}\index{functions!total)}
