diff -r cd723b2209ea -r 6892fdc7e9f8 doc-src/IsarRef/logics.tex --- 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.