author paulson Thu, 09 Apr 1998 12:31:35 +0200 changeset 4803 8428d4699d58 parent 4802 c15f46833f7a child 4804 02b7c759159b
Clearer description of recdef, including use of {}
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions doc-src/Logics/logics.ind file | annotate | diff | comparison | revisions
--- a/doc-src/Logics/HOL.tex	Thu Apr 09 12:29:39 1998 +0200
+++ b/doc-src/Logics/HOL.tex	Thu Apr 09 12:31:35 1998 +0200
@@ -1963,15 +1963,16 @@
\index{*primrec|)}

-\subsection{Well-founded recursive functions}
+\subsection{General recursive functions}
\label{sec:HOL:recdef}
\index{recursion!general|(}
\index{*recdef|(}

-Well-founded recursion can express any function whose termination can be
-proved by showing that each recursive call makes the argument smaller in a
-suitable sense.  The recursion need not involve datatypes and there are few
-syntactic restrictions.  Nested recursion and pattern-matching are allowed.
+Using \texttt{recdef}, you can declare functions involving nested recursion
+and pattern-matching.  Recursion need not involve datatypes and there are few
+syntactic restrictions.  Termination is proved by showing that each recursive
+call makes the argument smaller in a suitable sense, which you specify by
+supplying a well-founded relation.

Here is a simple example, the Fibonacci function.  The first line declares
\texttt{fib} to be a constant.  The well-founded relation is simply~$<$ (on
@@ -1989,6 +1990,14 @@
overlap, as in functional programming.  The \texttt{recdef} package
disambiguates overlapping patterns by taking the order of rules into account.
For missing patterns, the function is defined to return an arbitrary value.
+For example, here is a declaration of the list function \cdx{hd}:
+\begin{ttbox}
+consts hd :: 'a list => 'a
+recdef hd "\{\}"
+    "hd (x#l) = x"
+\end{ttbox}
+Because this function is not recursive, we may supply the empty well-founded
+relation, $\{\}$.

The well-founded relation defines a notion of smaller'' for the function's
argument type.  The relation $\prec$ is \textbf{well-founded} provided it
--- a/doc-src/Logics/logics.ind	Thu Apr 09 12:29:39 1998 +0200
+++ b/doc-src/Logics/logics.ind	Thu Apr 09 12:31:35 1998 +0200
@@ -357,7 +357,7 @@

\indexspace

-  \item {\tt hd} constant, 82
+  \item {\tt hd} constant, 82, 94
\item higher-order logic, 59--103
\item {\tt HOL} theory, 1, 59
\item {\sc hol} system, 59, 62