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

author | paulson |

Fri, 30 Jan 1998 12:31:59 +0100 | |

changeset 4591 | f88e466c43fa |

parent 4590 | 9f8f931e0089 |

child 4592 | ff0c5c57fdfb |

Fixed the description of recdef

--- a/doc-src/Logics/HOL.tex Fri Jan 30 11:34:06 1998 +0100 +++ b/doc-src/Logics/HOL.tex Fri Jan 30 12:31:59 1998 +0100 @@ -1985,6 +1985,11 @@ "fib (Suc(Suc x)) = (fib x + fib (Suc x))" \end{ttbox} +With \texttt{recdef}, function definitions may be incomplete, and patterns may +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. + The well-founded relation defines a notion of ``smaller'' for the function's argument type. The relation $\prec$ is \textbf{well-founded} provided it admits no infinitely decreasing chains @@ -2028,7 +2033,7 @@ "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" \end{ttbox} -The general form of a primitive recursive definition is +The general form of a well-founded recursive definition is \begin{ttbox} recdef {\it function} {\it rel} congs {\it congruence rules} {\bf(optional)} @@ -2057,9 +2062,8 @@ left-hand side must have the form $f\,t$, where $f$ is the function and $t$ is a tuple of distinct variables. If more than one equation is present then $f$ is defined by pattern-matching on components of its argument whose type - is a \texttt{datatype}. The patterns must be exhaustive and - non-overlapping. - + is a \texttt{datatype}. + Unlike with \texttt{primrec}, the reduction rules are not added to the default simpset, and individual rules may not be labelled with identifiers. However, the identifier $f$\texttt{.rules} is visible at the \ML\ level