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