author | paulson |

Thu Apr 09 12:31:35 1998 +0200 (1998-04-09 ago) | |

changeset 4803 | 8428d4699d58 |

parent 4802 | c15f46833f7a |

child 4804 | 02b7c759159b |

Clearer description of recdef, including use of {}

doc-src/Logics/HOL.tex | file | annotate | diff | revisions | |

doc-src/Logics/logics.ind | file | annotate | diff | revisions |

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