diff -r 2899182af616 -r 865918597b63 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Oct 11 12:52:56 2000 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Oct 11 13:15:04 2000 +0200
@@ -28,11 +28,14 @@
 recursion|see{recursion, wellfounded}}.  A relation $<$ is
 \bfindex{wellfounded} if it has no infinite descending chain $\cdots <
 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
-of all pairs $(r,l)$, where $l$ is the argument on the left-hand side of an equation
-and $r$ the argument of some recursive call on the corresponding
-right-hand side, induces a wellfounded relation.  For a systematic
-account of termination proofs via wellfounded relations see, for
-example, \cite{Baader-Nipkow}.
+of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
+of an equation and $r$ the argument of some recursive call on the
+corresponding right-hand side, induces a wellfounded relation.  For a
+systematic account of termination proofs via wellfounded relations
+see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
+some of the theory of wellfounded relations. For example
+\isa{wf\ r}\index{*wf|bold} means that relation \isa{r{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is
+wellfounded.
 
 Each \isacommand{recdef} definition should be accompanied (after the
 name of the function) by a wellfounded relation on the argument type
@@ -44,10 +47,63 @@
 
 In addition to \isa{measure}, the library provides
 a number of further constructions for obtaining wellfounded relations.
+Above we have already met \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} of type
+\begin{isabelle}%
+\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}{\isacharparenright}set{\isachardoublequote}%
+\end{isabelle}
+Of course the lexicographic product can also be interated, as in the following
+function definition:%
+\end{isamarkuptext}%
+\isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ contrived\isanewline
+\ \ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}i{\isachardot}\ i{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}j{\isachardot}\ j{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}k{\isachardot}\ k{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}%
+\begin{isamarkuptext}%
+Lexicographic products of measure functions already go a long way. A
+further useful construction is the embedding of some type in an
+existing wellfounded relation via the inverse image of a function:
+\begin{isabelle}%
+\ \ \ \ \ inv{\isacharunderscore}image\ {\isacharparenleft}r{\isasymColon}{\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set{\isacharparenright}\ {\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymequiv}\isanewline
+\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharcomma}\ y{\isasymColon}{\isacharprime}a{\isacharparenright}{\isachardot}\ {\isacharparenleft}f\ x{\isacharcomma}\ f\ y{\isacharparenright}\ {\isasymin}\ r{\isacharbraceright}%
+\end{isabelle}
+\begin{sloppypar}
+\noindent
+For example, \isa{measure} is actually defined as \isa{inv{\isacharunderscore}mage\ less{\isacharunderscore}than}, where
+\isa{less{\isacharunderscore}than} of type \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set} is the less-than relation on type \isa{nat}
+(as opposed to \isa{op\ {\isacharless}}, which is of type \isa{{\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool}).
+\end{sloppypar}
 
-wf proof auto if stndard constructions.%
+%Finally there is also {finite_psubset} the proper subset relation on finite sets
+
+All the above constructions are known to \isacommand{recdef}. Thus you
+will never have to prove wellfoundedness of any relation composed
+solely of these building blocks. But of course the proof of
+termination of your function definition, i.e.\ that the arguments
+decrease with every recursive call, may still require you to provide
+additional lemmas.
+
+It is also possible to use your own wellfounded relations with \isacommand{recdef}.
+Here is a simplistic example:%
 \end{isamarkuptext}%
-\end{isabellebody}%
+\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ f\ {\isachardoublequote}id{\isacharparenleft}less{\isacharunderscore}than{\isacharparenright}{\isachardoublequote}\isanewline
+{\isachardoublequote}f\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
+{\isachardoublequote}f\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ f\ n{\isachardoublequote}%
+\begin{isamarkuptext}%
+Since \isacommand{recdef} is not prepared for \isa{id}, the identity
+function, this leads to the complaint that it could not prove
+\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}, the wellfoundedness of \isa{id\ less{\isacharunderscore}than}. We should first have proved that \isa{id} preserves wellfoundedness%
+\end{isamarkuptext}%
+\isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}\ simp%
+\begin{isamarkuptext}%
+\noindent
+and should have added the following hint to our above definition:%
+\end{isamarkuptext}%
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf\ add{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"