summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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