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.
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.
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
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
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.
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.