1 \section{Introduction} |
|
2 |
|
3 Starting from Isabelle 2007, new facilities for recursive |
|
4 function definitions~\cite{krauss2006} are available. They provide |
|
5 better support for general recursive definitions than previous |
|
6 packages. But despite all tool support, function definitions can |
|
7 sometimes be a difficult thing. |
|
8 |
|
9 This tutorial is an example-guided introduction to the practical use |
|
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 |
|
14 We assume that you have mastered the fundamentals of Isabelle/HOL |
|
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 |
|
20 |
|
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 |
|
24 behavior. The impatient reader can stop after that |
|
25 section, and consult the remaining sections only when needed. |
|
26 Section 3 introduces the more verbose \cmd{function} command which |
|
27 gives fine-grained control. This form should be used |
|
28 whenever the short form fails. |
|
29 After that we discuss more specialized issues: |
|
30 termination, mutual, nested and higher-order recursion, partiality, pattern matching |
|
31 and others. |
|
32 |
|
33 |
|
34 \paragraph{Some background.} |
|
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: |
|
42 The \qt{new} concept of general wellfounded recursion is completely reduced |
|
43 to existing principles. |
|
44 |
|
45 |
|
46 |
|
47 |
|
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 |
|
51 which were not previously possible. |
|
52 |
|
53 |
|
54 |
|
55 |
|