1.1 --- a/doc-src/IsarRef/logics.tex	Mon Sep 03 10:00:24 2007 +0200
     1.2 +++ b/doc-src/IsarRef/logics.tex	Mon Sep 03 16:50:53 2007 +0200
     1.3 @@ -435,9 +435,153 @@
     1.4  
     1.5  \subsection{Recursive functions}\label{sec:recursion}
     1.6  
     1.7 -\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
     1.8 +\indexisarcmdof{HOL}{primrec}
     1.9 +
    1.10  \begin{matharray}{rcl}
    1.11    \isarcmd{primrec} & : & \isartrans{theory}{theory} \\
    1.12 +  \isarcmd{fun} & : & \isartrans{theory}{theory} \\
    1.13 +  \isarcmd{function} & : & \isartrans{theory}{proof(prove)} \\
    1.14 +  \isarcmd{termination} & : & \isartrans{theory}{proof(prove)} \\
    1.15 +\end{matharray}
    1.16 +
    1.17 +\railalias{funopts}{function\_opts}
    1.18 +
    1.19 +\begin{rail}
    1.20 +  'primrec' parname? (equation +)
    1.21 +  ;
    1.22 +  equation: thmdecl? prop
    1.23 +  ;
    1.24 +  ('fun' | 'function') (funopts)? fixes 'where' clauses
    1.25 +  ;
    1.26 +  clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
    1.27 +  ;
    1.28 +  funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
    1.29 +  'default' term) + ',') ')'
    1.30 +  ;
    1.31 +  'termination' ( term )?
    1.32 +\end{rail}
    1.33 +
    1.34 +\begin{descr}
    1.35 +  
    1.36 +\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
    1.37 +  datatypes, see also \cite{isabelle-HOL}.
    1.38 +  
    1.39 +\item [$\isarkeyword{function}$] defines functions by general
    1.40 +  wellfounded recursion. A detailed description with examples can be
    1.41 +  found in \cite{isabelle-function}. The function is specified by a
    1.42 +  set of (possibly conditional) recursive equations with arbitrary
    1.43 +  pattern matching. The command generates proof obligations for the
    1.44 +  completeness and the compatibility of patterns.
    1.45 +
    1.46 +  The defined function is considered partial, and the resulting
    1.47 +  simplification rules (named $f.psimps$) and induction rule (named
    1.48 +  $f.pinduct$) are guarded by a generated domain predicate $f_dom$. 
    1.49 +  The $\isarkeyword{termination}$ command can then be used to establish
    1.50 +  that the function is total.
    1.51 +
    1.52 +\item [$\isarkeyword{fun}$] is a shorthand notation for
    1.53 +  $\isarkeyword{function}~(\textit{sequential})$, followed by automated
    1.54 +  proof attemts regarding pattern matching and termination. For
    1.55 +  details, see \cite{isabelle-function}.
    1.56 +
    1.57 +\item [$\isarkeyword{termination}$~f] commences a termination proof
    1.58 +  for the previously defined function $f$. If no name is given, it
    1.59 +  refers to the most recent function definition. After the proof is
    1.60 +  closed, the recursive equations and the induction principle is established.
    1.61 +\end{descr}
    1.62 +
    1.63 +Recursive definitions introduced by both the $\isarkeyword{primrec}$
    1.64 +and the $\isarkeyword{function}$ command accommodate reasoning by
    1.65 +induction (cf.\ \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$
    1.66 +(where $c$ is the name of the function definition) refers to a
    1.67 +specific induction rule, with parameters named according to the
    1.68 +user-specified equations.  Case names of $\isarkeyword{primrec}$ are
    1.69 +that of the datatypes involved, while those of
    1.70 +$\isarkeyword{function}$ are numbered (starting from $1$).
    1.71 +
    1.72 +The equations provided by these packages may be referred later as theorem list
    1.73 +$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
    1.74 +Individual equations may be named explicitly as well.
    1.75 +
    1.76 +The $\isarkeyword{function}$ command accepts the following options:
    1.77 +
    1.78 +\begin{descr}
    1.79 +\item [\emph{sequential}] enables a preprocessor which disambiguates
    1.80 +  overlapping patterns by making them mutually disjoint. Earlier
    1.81 +  equations take precedence over later ones. This allows to give the
    1.82 +  specification in a format very similar to functional programming.
    1.83 +  Note that the resulting simplification and induction rules
    1.84 +  correspond to the transformed specification, not the one given
    1.85 +  originally. This usually means that each equation given by the user
    1.86 +  may result in several theroems.
    1.87 +  Also note that this automatic transformation only works
    1.88 +  for ML-style datatype patterns.
    1.89 +
    1.90 +
    1.91 +\item [\emph{in name}] gives the target for the definition.
    1.92 +
    1.93 +\item [\emph{domintros}] enables the automated generation of
    1.94 +  introduction rules for the domain predicate. While mostly not
    1.95 +  needed, they can be helpful in some proofs about partial functions.
    1.96 +
    1.97 +\item [\emph{tailrec}] generates the unconstrained recursive equations
    1.98 +  even without a termination proof, provided that the function is
    1.99 +  tail-recursive. This currently only works 
   1.100 +
   1.101 +\item [\emph{default d}] allows to specify a default value for a
   1.102 +  (partial) function, which will ensure that $f(x)=d(x)$ whenever $x
   1.103 +  \notin \textit{f\_dom}$. This feature is experimental.
   1.104 +\end{descr}
   1.105 +
   1.106 +\subsubsection{Proof methods related to recursive definitions}
   1.107 +
   1.108 +\indexisarmethof{HOL}{pat\_completeness}
   1.109 +\indexisarmethof{HOL}{relation}
   1.110 +\indexisarmethof{HOL}{lexicographic\_order}
   1.111 +
   1.112 +\begin{matharray}{rcl}
   1.113 +  pat\_completeness & : & \isarmeth \\
   1.114 +  relation & : & \isarmeth \\
   1.115 +  lexicographic\_order & : & \isarmeth \\
   1.116 +\end{matharray}
   1.117 +
   1.118 +\begin{rail}
   1.119 +  'pat\_completeness'
   1.120 +  ;
   1.121 +  'relation' term
   1.122 +  ;
   1.123 +  'lexicographic\_order' clasimpmod
   1.124 +\end{rail}
   1.125 +
   1.126 +\begin{descr}
   1.127 +\item [\emph{pat\_completeness}] Specialized method to solve goals
   1.128 +  regarding the completeness of pattern matching, as required by the
   1.129 +  $\isarkeyword{function}$ package (cf.~\cite{isabelle-function}).
   1.130 +
   1.131 +\item [\emph{relation R}] Introduces a termination proof using the
   1.132 +  relation $R$. The resulting proof state will contain goals
   1.133 +  expressing that $R$ is wellfounded, and that the arguments
   1.134 +  of recursive calls decrease with respect to $R$. Usually, this
   1.135 +  method is used as the initial proof step of manual termination
   1.136 +  proofs.
   1.137 +
   1.138 +\item [\emph{lexicographic\_order}] Attempts a fully automated
   1.139 +  termination proof by searching for a lexicographic combination of
   1.140 +  size measures on the arguments of the function. The method
   1.141 +  accepts the same arguments as the \emph{auto} method, which it uses
   1.142 +  internally to prove local descents. Hence, modifiers like
   1.143 +  \emph{simp}, \emph{intro} etc.\ can be used to add ``hints'' for the
   1.144 +  automated proofs. In case of failure, extensive information is
   1.145 +  printed, which can help to analyse the failure (cf.~\cite{isabelle-function}).
   1.146 +\end{descr}
   1.147 +
   1.148 +\subsubsection{Legacy recursion package}
   1.149 +\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc}
   1.150 +
   1.151 +The use of the legacy $\isarkeyword{recdef}$ command is now deprecated
   1.152 +in favour of $\isarkeyword{function}$ and $\isarkeyword{fun}$.
   1.153 +
   1.154 +\begin{matharray}{rcl}
   1.155    \isarcmd{recdef} & : & \isartrans{theory}{theory} \\
   1.156    \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\
   1.157  \end{matharray}
   1.158 @@ -455,15 +599,10 @@
   1.159  \railterm{recdeftc}
   1.160  
   1.161  \begin{rail}
   1.162 -  'primrec' parname? (equation +)
   1.163 -  ;
   1.164    'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
   1.165    ;
   1.166    recdeftc thmdecl? tc
   1.167    ;
   1.168 -
   1.169 -  equation: thmdecl? prop
   1.170 -  ;
   1.171    hints: '(' 'hints' (recdefmod *) ')'
   1.172    ;
   1.173    recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   1.174 @@ -474,9 +613,6 @@
   1.175  
   1.176  \begin{descr}
   1.177    
   1.178 -\item [$\isarkeyword{primrec}$] defines primitive recursive functions over
   1.179 -  datatypes, see also \cite{isabelle-HOL}.
   1.180 -  
   1.181  \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   1.182    functions (using the TFL package), see also \cite{isabelle-HOL}.  The
   1.183    ``$(permissive)$'' option tells TFL to recover from failed proof attempts,
   1.184 @@ -496,19 +632,6 @@
   1.185  
   1.186  \end{descr}
   1.187  
   1.188 -Both kinds of recursive definitions accommodate reasoning by induction (cf.\
   1.189 -\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of
   1.190 -the function definition) refers to a specific induction rule, with parameters
   1.191 -named according to the user-specified equations.  Case names of
   1.192 -$\isarkeyword{primrec}$ are that of the datatypes involved, while those of
   1.193 -$\isarkeyword{recdef}$ are numbered (starting from $1$).
   1.194 -
   1.195 -The equations provided by these packages may be referred later as theorem list
   1.196 -$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
   1.197 -Individual equations may be named explicitly as well; note that for
   1.198 -$\isarkeyword{recdef}$ each specification given by the user may result in
   1.199 -several theorems.
   1.200 -
   1.201  \medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using
   1.202  the following attributes.
   1.203  

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