Documented function package in IsarRef-manual.

--- a/doc-src/IsarRef/logics.tex	Mon Sep 03 10:00:24 2007 +0200
+++ b/doc-src/IsarRef/logics.tex	Mon Sep 03 16:50:53 2007 +0200
@@ -435,9 +435,153 @@
 
 \subsection{Recursive functions}\label{sec:recursion}
 
-\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
+\indexisarcmdof{HOL}{primrec}
+
 \begin{matharray}{rcl}
   \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
+  \isarcmd{fun} & : & \isartrans{theory}{theory} \\
+  \isarcmd{function} & : & \isartrans{theory}{proof(prove)} \\
+  \isarcmd{termination} & : & \isartrans{theory}{proof(prove)} \\
+\end{matharray}
+
+\railalias{funopts}{function\_opts}
+
+\begin{rail}
+  'primrec' parname? (equation +)
+  ;
+  equation: thmdecl? prop
+  ;
+  ('fun' | 'function') (funopts)? fixes 'where' clauses
+  ;
+  clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
+  ;
+  funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
+  'default' term) + ',') ')'
+  ;
+  'termination' ( term )?
+\end{rail}
+
+\begin{descr}
+  
+\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
+  datatypes, see also \cite{isabelle-HOL}.
+  
+\item [$\isarkeyword{function}$] defines functions by general
+  wellfounded recursion. A detailed description with examples can be
+  found in \cite{isabelle-function}. The function is specified by a
+  set of (possibly conditional) recursive equations with arbitrary
+  pattern matching. The command generates proof obligations for the
+  completeness and the compatibility of patterns.
+
+  The defined function is considered partial, and the resulting
+  simplification rules (named $f.psimps$) and induction rule (named
+  $f.pinduct$) are guarded by a generated domain predicate $f_dom$. 
+  The $\isarkeyword{termination}$ command can then be used to establish
+  that the function is total.
+
+\item [$\isarkeyword{fun}$] is a shorthand notation for
+  $\isarkeyword{function}~(\textit{sequential})$, followed by automated
+  proof attemts regarding pattern matching and termination. For
+  details, see \cite{isabelle-function}.
+
+\item [$\isarkeyword{termination}$~f] commences a termination proof
+  for the previously defined function $f$. If no name is given, it
+  refers to the most recent function definition. After the proof is
+  closed, the recursive equations and the induction principle is established.
+\end{descr}
+
+Recursive definitions introduced by both the $\isarkeyword{primrec}$
+and the $\isarkeyword{function}$ command accommodate reasoning by
+induction (cf.\ \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$
+(where $c$ is the name of the function definition) refers to a
+specific induction rule, with parameters named according to the
+user-specified equations.  Case names of $\isarkeyword{primrec}$ are
+that of the datatypes involved, while those of
+$\isarkeyword{function}$ are numbered (starting from $1$).
+
+The equations provided by these packages may be referred later as theorem list
+$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
+Individual equations may be named explicitly as well.
+
+The $\isarkeyword{function}$ command accepts the following options:
+
+\begin{descr}
+\item [\emph{sequential}] enables a preprocessor which disambiguates
+  overlapping patterns by making them mutually disjoint. Earlier
+  equations take precedence over later ones. This allows to give the
+  specification in a format very similar to functional programming.
+  Note that the resulting simplification and induction rules
+  correspond to the transformed specification, not the one given
+  originally. This usually means that each equation given by the user
+  may result in several theroems.
+  Also note that this automatic transformation only works
+  for ML-style datatype patterns.
+
+
+\item [\emph{in name}] gives the target for the definition.
+
+\item [\emph{domintros}] enables the automated generation of
+  introduction rules for the domain predicate. While mostly not
+  needed, they can be helpful in some proofs about partial functions.
+
+\item [\emph{tailrec}] generates the unconstrained recursive equations
+  even without a termination proof, provided that the function is
+  tail-recursive. This currently only works 
+
+\item [\emph{default d}] allows to specify a default value for a
+  (partial) function, which will ensure that $f(x)=d(x)$ whenever $x
+  \notin \textit{f\_dom}$. This feature is experimental.
+\end{descr}
+
+\subsubsection{Proof methods related to recursive definitions}
+
+\indexisarmethof{HOL}{pat\_completeness}
+\indexisarmethof{HOL}{relation}
+\indexisarmethof{HOL}{lexicographic\_order}
+
+\begin{matharray}{rcl}
+  pat\_completeness & : & \isarmeth \\
+  relation & : & \isarmeth \\
+  lexicographic\_order & : & \isarmeth \\
+\end{matharray}
+
+\begin{rail}
+  'pat\_completeness'
+  ;
+  'relation' term
+  ;
+  'lexicographic\_order' clasimpmod
+\end{rail}
+
+\begin{descr}
+\item [\emph{pat\_completeness}] Specialized method to solve goals
+  regarding the completeness of pattern matching, as required by the
+  $\isarkeyword{function}$ package (cf.~\cite{isabelle-function}).
+
+\item [\emph{relation R}] Introduces a termination proof using the
+  relation $R$. The resulting proof state will contain goals
+  expressing that $R$ is wellfounded, and that the arguments
+  of recursive calls decrease with respect to $R$. Usually, this
+  method is used as the initial proof step of manual termination
+  proofs.
+
+\item [\emph{lexicographic\_order}] Attempts a fully automated
+  termination proof by searching for a lexicographic combination of
+  size measures on the arguments of the function. The method
+  accepts the same arguments as the \emph{auto} method, which it uses
+  internally to prove local descents. Hence, modifiers like
+  \emph{simp}, \emph{intro} etc.\ can be used to add ``hints'' for the
+  automated proofs. In case of failure, extensive information is
+  printed, which can help to analyse the failure (cf.~\cite{isabelle-function}).
+\end{descr}
+
+\subsubsection{Legacy recursion package}
+\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
+
+The use of the legacy $\isarkeyword{recdef}$ command is now deprecated
+in favour of $\isarkeyword{function}$ and $\isarkeyword{fun}$.
+
+\begin{matharray}{rcl}
   \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
   \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
 \end{matharray}
@@ -455,15 +599,10 @@
 \railterm{recdeftc}
 
 \begin{rail}
-  'primrec' parname? (equation +)
-  ;
   'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
   ;
   recdeftc thmdecl? tc
   ;
-
-  equation: thmdecl? prop
-  ;
   hints: '(' 'hints' (recdefmod *) ')'
   ;
   recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
@@ -474,9 +613,6 @@
 
 \begin{descr}
   
-\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
-  datatypes, see also \cite{isabelle-HOL}.
-  
 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   functions (using the TFL package), see also \cite{isabelle-HOL}.  The
   ``$(permissive)$'' option tells TFL to recover from failed proof attempts,
@@ -496,19 +632,6 @@
 
 \end{descr}
 
-Both kinds of recursive definitions accommodate reasoning by induction (cf.\
-\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
-the function definition) refers to a specific induction rule, with parameters
-named according to the user-specified equations.  Case names of
-$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
-$\isarkeyword{recdef}$ are numbered (starting from $1$).
-
-The equations provided by these packages may be referred later as theorem list
-$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
-Individual equations may be named explicitly as well; note that for
-$\isarkeyword{recdef}$ each specification given by the user may result in
-several theorems.
-
 \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
 the following attributes.
 

--- a/doc-src/manual.bib	Mon Sep 03 10:00:24 2007 +0200
+++ b/doc-src/manual.bib	Mon Sep 03 16:50:53 2007 +0200
@@ -593,6 +593,13 @@
   crossref =  {ijcar2006},
   pages =     {589--603}}
 
+@manual{isabelle-function,
+  author        = {Alexander Krauss},
+  title         = {Defining Recursive Functions in {Isabelle/HOL}},
+  institution   = TUM,
+  note          = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
+}
+
 @Book{kunen80,
   author	= {Kenneth Kunen},
   title		= {Set Theory: An Introduction to Independence Proofs},