--- a/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 01 20:20:19 2007 +0100
@@ -22,7 +22,7 @@
We have already seen an instance of underdefinedness by means of
non-exhaustive pattern matching: the definition of @{term last} in
-\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}
+\S\ref{sec:fun}. The same is allowed for \isacommand{primrec}
*}
consts hd :: "'a list \<Rightarrow> 'a"
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Thu Nov 01 20:20:19 2007 +0100
@@ -38,7 +38,7 @@
We have already seen an instance of underdefinedness by means of
non-exhaustive pattern matching: the definition of \isa{last} in
-\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}%
+\S\ref{sec:fun}. The same is allowed for \isacommand{primrec}%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Thu Nov 01 20:20:19 2007 +0100
@@ -213,9 +213,9 @@
\isa{term} are still awkward because they expect a conjunction. One
could derive a new induction principle as well (see
\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
-and to define functions with \isacommand{recdef} instead.
-Simple uses of \isacommand{recdef} are described in \S\ref{sec:recdef} below,
-and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{recdef} can
+and to define functions with \isacommand{fun} instead.
+Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below,
+and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can
handle nested recursion.
Of course, you may also combine mutual and nested recursion of datatypes. For example,
--- a/doc-src/TutorialI/IsaMakefile Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/IsaMakefile Thu Nov 01 20:20:19 2007 +0100
@@ -4,7 +4,7 @@
## targets
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \
HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \
HOL-Protocol HOL-Documents styles
images:
@@ -95,6 +95,15 @@
@rm -f tutorial.dvi
+## HOL-Fun
+
+HOL-Fun: HOL $(LOG)/HOL-Fun.gz
+
+$(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy
+ $(USEDIR) Fun
+ @rm -f tutorial.dvi
+
+
## HOL-Recdef
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Nov 01 20:20:19 2007 +0100
@@ -155,7 +155,7 @@
txt{*\noindent
To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
the same general induction method as for recursion induction (see
-\S\ref{sec:recdef-induction}):
+\S\ref{sec:fun-induction}):
*};
apply(induct_tac k rule: nat_less_induct);
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Nov 01 20:20:19 2007 +0100
@@ -216,7 +216,7 @@
\noindent
To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use
the same general induction method as for recursion induction (see
-\S\ref{sec:recdef-induction}):%
+\S\ref{sec:fun-induction}):%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
--- a/doc-src/TutorialI/Rules/rules.tex Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Nov 01 20:20:19 2007 +0100
@@ -1841,7 +1841,7 @@
\label{sec:THEN}
Let us reproduce our examples in Isabelle. Recall that in
-{\S}\ref{sec:recdef-simplification} we declared the recursive function
+{\S}\ref{sec:fun-simplification} we declared the recursive function
\isa{gcd}:\index{*gcd (constant)|(}
\begin{isabelle}
\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
@@ -2473,7 +2473,7 @@
%
We use induction: \isa{gcd.induct} is the
induction rule returned by \isa{recdef}. We simplify using
-rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the
+rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the
definition of \isa{gcd} can loop.
\begin{isabelle}
\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\
--- a/doc-src/TutorialI/Sets/sets.tex Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Thu Nov 01 20:20:19 2007 +0100
@@ -875,9 +875,9 @@
\index{relations!well-founded|(}%
A well-founded relation captures the notion of a terminating process.
-Each \commdx{recdef}
-declaration must specify a well-founded relation that
-justifies the termination of the desired recursive function. Most of the
+Complex recursive functions definitions \ref{sec:?????TN}
+must specify a well-founded relation that
+justifies their termination. Most of the
forms of induction found in mathematics are merely special cases of
induction over a well-founded relation.
@@ -898,7 +898,7 @@
You may want to skip the rest of this section until you need to perform a
complex recursive function definition or induction. The induction rule
returned by
-\isacommand{recdef} is good enough for most purposes. We use an explicit
+\isacommand{fun} is good enough for most purposes. We use an explicit
well-founded induction only in {\S}\ref{sec:CTL-revisited}.
\end{warn}
@@ -956,9 +956,9 @@
\rulenamedx{wf_lex_prod}
\end{isabelle}
-These constructions can be used in a
-\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
-the well-founded relation used to prove termination.
+%These constructions can be used in a
+%\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
+%the well-founded relation used to prove termination.
The \bfindex{multiset ordering}, useful for hard termination proofs, is
available in the Library~\cite{HOL-Library}.
--- a/doc-src/TutorialI/fp.tex Thu Nov 01 13:44:44 2007 +0100
+++ b/doc-src/TutorialI/fp.tex Thu Nov 01 20:20:19 2007 +0100
@@ -194,7 +194,7 @@
becomes smaller with every recursive call. There must be at most one equation
for each constructor. Their order is immaterial.
A more general method for defining total recursive functions is introduced in
-{\S}\ref{sec:recdef}.
+{\S}\ref{sec:fun}.
\begin{exercise}\label{ex:Tree}
\input{Misc/document/Tree.tex}%
@@ -265,7 +265,7 @@
(nonrecursive!) definition from which the user-supplied recursion equations are
automatically proved. This process is
hidden from the user, who does not have to understand the details. Other commands described
-later, like \isacommand{recdef} and \isacommand{inductive}, work similarly.
+later, like \isacommand{fun} and \isacommand{inductive}, work similarly.
This strict adherence to the definitional approach reduces the risk of
soundness errors.
@@ -281,9 +281,9 @@
study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
datatypes, including those involving function spaces, are covered in
{\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
-trees (``tries''). Finally we introduce \isacommand{recdef}, a general
+trees (``tries''). Finally we introduce \isacommand{fun}, a general
form of recursive function definition that goes well beyond
-\isacommand{primrec} ({\S}\ref{sec:recdef}).
+\isacommand{primrec} ({\S}\ref{sec:fun}).
\section{Simplification}
@@ -460,35 +460,18 @@
\index{tries|)}
\section{Total Recursive Functions}
-\label{sec:recdef}
-\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
+\label{sec:fun}
+\index{fun@\isacommand {fun} (command)|(}\index{functions!total|(}
Although many total functions have a natural primitive recursive definition,
this is not always the case. Arbitrary total recursive functions can be
-defined by means of \isacommand{recdef}: you can use full pattern-matching,
+defined by means of \isacommand{fun}: you can use full pattern-matching,
recursion need not involve datatypes, and termination is proved by showing
-that the arguments of all recursive calls are smaller in a suitable (user
-supplied) sense. In this section we restrict ourselves to measure functions;
-more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
-
-\subsection{Defining Recursive Functions}
-\label{sec:recdef-examples}
-\input{Recdef/document/examples.tex}
-
-\subsection{Proving Termination}
-\input{Recdef/document/termination.tex}
+that the arguments of all recursive calls are smaller in a suitable sense.
+In this section we restrict ourselves to functions where Isabelle can prove
+termination automatically. User supplied termination proofs are discussed in
+{\S}\ref{sec:beyond-measure}.
-\subsection{Simplification and Recursive Functions}
-\label{sec:recdef-simplification}
-\input{Recdef/document/simplification.tex}
+\input{Fun/document/fun0.tex}
-\subsection{Induction and Recursive Functions}
-\index{induction!recursion|(}
-\index{recursion induction|(}
-
-\input{Recdef/document/Induction.tex}
-\label{sec:recdef-induction}
-
-\index{induction!recursion|)}
-\index{recursion induction|)}
-\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}
+\index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}