doc-src/IsarAdvanced/Functions/intro.tex

updated

\section{Introduction}

In the upcomung release of Isabelle 2007, new facilities for recursive
function definitions \cite{krauss2006} will be available.

This tutorial is an example-guided introduction to the practical use
of the package. We assume that you have mastered the basic concepts of
Isabelle/HOL and are able to write basic specifications and
proofs. To start out with Isabelle in general, you should read the
tutorial \cite{isa-tutorial}.

% Definitional extension

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 new concept of general wellfounded recursion is completely reduced
to existing principles.




The new \cmd{function} command, and its short form \cmd{fun} will
replace the traditional \cmd{recdef} command \cite{slind-tfl} in the future. It solves
a few of technical issues around \cmd{recdef}, and allows definitions
which were not previously possible.