krauss@23004: \section{Introduction}
krauss@23004: 
krauss@27026: Starting from Isabelle 2007, new facilities for recursive
urbanc@26851: function definitions~\cite{krauss2006} are available. They provide
krauss@23805: better support for general recursive definitions than previous
urbanc@26851: packages.  But despite all tool support, function definitions can
krauss@23805: sometimes be a difficult thing. 
krauss@23004: 
krauss@23188: This tutorial is an example-guided introduction to the practical use
krauss@23805: of the package and related tools. It should help you get started with
krauss@23805: defining functions quickly. For the more difficult definitions we will
krauss@23805: discuss what problems can arise, and how they can be solved.
krauss@23004: 
krauss@27026: We assume that you have mastered the fundamentals of Isabelle/HOL
krauss@23805: and are able to write basic specifications and proofs. To start out
krauss@23805: with Isabelle in general, consult the Isabelle/HOL tutorial
krauss@23805: \cite{isa-tutorial}.
krauss@23004: 
krauss@23805: 
krauss@23805: 
krauss@23805: \paragraph{Structure of this tutorial.}
krauss@23805: Section 2 introduces the syntax and basic operation of the \cmd{fun}
krauss@23805: command, which provides full automation with reasonable default
krauss@27026: behavior.  The impatient reader can stop after that
krauss@23805: section, and consult the remaining sections only when needed.
krauss@23805: Section 3 introduces the more verbose \cmd{function} command which
krauss@27026: gives fine-grained control. This form should be used
krauss@23805: whenever the short form fails.
krauss@27026: After that we discuss more specialized issues:
krauss@27026: termination, mutual, nested and higher-order recursion, partiality, pattern matching
krauss@23805: and others.
krauss@23805: 
krauss@23805: 
krauss@23805: \paragraph{Some background.}
krauss@23004: Following the LCF tradition, the package is realized as a definitional
krauss@23004: extension: Recursive definitions are internally transformed into a
krauss@23004: non-recursive form, such that the function can be defined using
krauss@23004: standard definition facilities. Then the recursive specification is
krauss@23004: derived from the primitive definition.  This is a complex task, but it
krauss@23004: is fully automated and mostly transparent to the user. Definitional
krauss@23004: extensions are valuable because they are conservative by construction:
krauss@23805: The \qt{new} concept of general wellfounded recursion is completely reduced
krauss@23004: to existing principles.
krauss@23004: 
krauss@23004: 
krauss@23004: 
krauss@23004: 
krauss@27026: The new \cmd{function} command, and its short form \cmd{fun} have mostly
krauss@27026: replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
krauss@27026: a few of technical issues around \cmd{recdef}, and allow definitions
krauss@23004: which were not previously possible.
krauss@23004: 
krauss@23004: 
krauss@23004: 
krauss@23188: