\section{Introduction}

Starting from Isabelle 2007, new facilities for recursive

function definitions~\cite{krauss2006} are available. They provide

better support for general recursive definitions than previous

packages.  But despite all tool support, function definitions can

sometimes be a difficult thing. 

This tutorial is an example-guided introduction to the practical use

of the package and related tools. It should help you get started with

defining functions quickly. For the more difficult definitions we will

discuss what problems can arise, and how they can be solved.

We assume that you have mastered the fundamentals of Isabelle/HOL

and are able to write basic specifications and proofs. To start out

with Isabelle in general, consult the Isabelle/HOL tutorial

\cite{isa-tutorial}.

\paragraph{Structure of this tutorial.}

Section 2 introduces the syntax and basic operation of the \cmd{fun}

command, which provides full automation with reasonable default

behavior.  The impatient reader can stop after that

section, and consult the remaining sections only when needed.

Section 3 introduces the more verbose \cmd{function} command which

gives fine-grained control. This form should be used

whenever the short form fails.

After that we discuss more specialized issues:

termination, mutual, nested and higher-order recursion, partiality, pattern matching

and others.

\paragraph{Some background.}

Following the LCF tradition, the package is realized as a definitional

extension: Recursive definitions are internally transformed into a

non-recursive form, such that the function can be defined using

standard definition facilities. Then the recursive specification is

derived from the primitive definition.  This is a complex task, but it

is fully automated and mostly transparent to the user. Definitional

extensions are valuable because they are conservative by construction:

The \qt{new} concept of general wellfounded recursion is completely reduced

to existing principles.

The new \cmd{function} command, and its short form \cmd{fun} have mostly

replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve

a few of technical issues around \cmd{recdef}, and allow definitions

which were not previously possible.