doc-src/IsarAdvanced/Functions/intro.tex

regression tests: send failure reports to [e-mail], too

\section{Introduction}

In Isabelle 2007, new facilities for recursive function definitions
are available.

This document is intended as a tutorial for both inexperienced and
advanced users, and demonstrates the use of the package with a lot of
examples.

% 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 in the future. It solves
a few of technical issues around \cmd{recdef}, and allows definitions
which were not previously possible.