23004
|
1 |
\section{Introduction}
|
|
2 |
|
27026
|
3 |
Starting from Isabelle 2007, new facilities for recursive
|
26851
|
4 |
function definitions~\cite{krauss2006} are available. They provide
|
23805
|
5 |
better support for general recursive definitions than previous
|
26851
|
6 |
packages. But despite all tool support, function definitions can
|
23805
|
7 |
sometimes be a difficult thing.
|
23004
|
8 |
|
23188
|
9 |
This tutorial is an example-guided introduction to the practical use
|
23805
|
10 |
of the package and related tools. It should help you get started with
|
|
11 |
defining functions quickly. For the more difficult definitions we will
|
|
12 |
discuss what problems can arise, and how they can be solved.
|
|
13 |
|
27026
|
14 |
We assume that you have mastered the fundamentals of Isabelle/HOL
|
23805
|
15 |
and are able to write basic specifications and proofs. To start out
|
|
16 |
with Isabelle in general, consult the Isabelle/HOL tutorial
|
|
17 |
\cite{isa-tutorial}.
|
|
18 |
|
|
19 |
|
23004
|
20 |
|
23805
|
21 |
\paragraph{Structure of this tutorial.}
|
|
22 |
Section 2 introduces the syntax and basic operation of the \cmd{fun}
|
|
23 |
command, which provides full automation with reasonable default
|
27026
|
24 |
behavior. The impatient reader can stop after that
|
23805
|
25 |
section, and consult the remaining sections only when needed.
|
|
26 |
Section 3 introduces the more verbose \cmd{function} command which
|
27026
|
27 |
gives fine-grained control. This form should be used
|
23805
|
28 |
whenever the short form fails.
|
27026
|
29 |
After that we discuss more specialized issues:
|
|
30 |
termination, mutual, nested and higher-order recursion, partiality, pattern matching
|
23805
|
31 |
and others.
|
23004
|
32 |
|
23805
|
33 |
|
|
34 |
\paragraph{Some background.}
|
23004
|
35 |
Following the LCF tradition, the package is realized as a definitional
|
|
36 |
extension: Recursive definitions are internally transformed into a
|
|
37 |
non-recursive form, such that the function can be defined using
|
|
38 |
standard definition facilities. Then the recursive specification is
|
|
39 |
derived from the primitive definition. This is a complex task, but it
|
|
40 |
is fully automated and mostly transparent to the user. Definitional
|
|
41 |
extensions are valuable because they are conservative by construction:
|
23805
|
42 |
The \qt{new} concept of general wellfounded recursion is completely reduced
|
23004
|
43 |
to existing principles.
|
|
44 |
|
|
45 |
|
|
46 |
|
|
47 |
|
27026
|
48 |
The new \cmd{function} command, and its short form \cmd{fun} have mostly
|
|
49 |
replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
|
|
50 |
a few of technical issues around \cmd{recdef}, and allow definitions
|
23004
|
51 |
which were not previously possible.
|
|
52 |
|
|
53 |
|
|
54 |
|
23188
|
55 |
|