Clearer description of recdef, including use of {}
authorpaulson
Thu Apr 09 12:31:35 1998 +0200 (1998-04-09 ago)
changeset 48038428d4699d58
parent 4802 c15f46833f7a
child 4804 02b7c759159b
Clearer description of recdef, including use of {}
doc-src/Logics/HOL.tex
doc-src/Logics/logics.ind
     1.1 --- a/doc-src/Logics/HOL.tex	Thu Apr 09 12:29:39 1998 +0200
     1.2 +++ b/doc-src/Logics/HOL.tex	Thu Apr 09 12:31:35 1998 +0200
     1.3 @@ -1963,15 +1963,16 @@
     1.4  \index{*primrec|)}
     1.5  
     1.6  
     1.7 -\subsection{Well-founded recursive functions}
     1.8 +\subsection{General recursive functions}
     1.9  \label{sec:HOL:recdef}
    1.10  \index{recursion!general|(}
    1.11  \index{*recdef|(}
    1.12  
    1.13 -Well-founded recursion can express any function whose termination can be
    1.14 -proved by showing that each recursive call makes the argument smaller in a
    1.15 -suitable sense.  The recursion need not involve datatypes and there are few
    1.16 -syntactic restrictions.  Nested recursion and pattern-matching are allowed.
    1.17 +Using \texttt{recdef}, you can declare functions involving nested recursion
    1.18 +and pattern-matching.  Recursion need not involve datatypes and there are few
    1.19 +syntactic restrictions.  Termination is proved by showing that each recursive
    1.20 +call makes the argument smaller in a suitable sense, which you specify by
    1.21 +supplying a well-founded relation.
    1.22  
    1.23  Here is a simple example, the Fibonacci function.  The first line declares
    1.24  \texttt{fib} to be a constant.  The well-founded relation is simply~$<$ (on
    1.25 @@ -1989,6 +1990,14 @@
    1.26  overlap, as in functional programming.  The \texttt{recdef} package
    1.27  disambiguates overlapping patterns by taking the order of rules into account.
    1.28  For missing patterns, the function is defined to return an arbitrary value.
    1.29 +For example, here is a declaration of the list function \cdx{hd}:
    1.30 +\begin{ttbox}
    1.31 +consts hd :: 'a list => 'a
    1.32 +recdef hd "\{\}"
    1.33 +    "hd (x#l) = x"
    1.34 +\end{ttbox}
    1.35 +Because this function is not recursive, we may supply the empty well-founded
    1.36 +relation, $\{\}$.
    1.37  
    1.38  The well-founded relation defines a notion of ``smaller'' for the function's
    1.39  argument type.  The relation $\prec$ is \textbf{well-founded} provided it
     2.1 --- a/doc-src/Logics/logics.ind	Thu Apr 09 12:29:39 1998 +0200
     2.2 +++ b/doc-src/Logics/logics.ind	Thu Apr 09 12:31:35 1998 +0200
     2.3 @@ -357,7 +357,7 @@
     2.4  
     2.5    \indexspace
     2.6  
     2.7 -  \item {\tt hd} constant, 82
     2.8 +  \item {\tt hd} constant, 82, 94
     2.9    \item higher-order logic, 59--103
    2.10    \item {\tt HOL} theory, 1, 59
    2.11    \item {\sc hol} system, 59, 62