--- a/doc-src/TutorialI/document/WFrec.tex Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,169 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{WFrec}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\noindent
-So far, all recursive definitions were shown to terminate via measure
-functions. Sometimes this can be inconvenient or
-impossible. Fortunately, \isacommand{recdef} supports much more
-general definitions. For example, termination of Ackermann's function
-can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
-\isacommand{recdef}\isamarkupfalse%
-\ ack\ {\isachardoublequoteopen}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}ack{\isacharparenleft}{\isadigit{0}}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}ack{\isacharparenleft}Suc\ m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-The lexicographic product decreases if either its first component
-decreases (as in the second equation and in the outer call in the
-third equation) or its first component stays the same and the second
-component decreases (as in the inner call in the third equation).
-
-In general, \isacommand{recdef} supports termination proofs based on
-arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
-This is called \textbf{well-founded
-recursion}\indexbold{recursion!well-founded}. A function definition
-is total if and only if 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 well-founded relation. For a
-systematic account of termination proofs via well-founded relations see, for
-example, Baader and Nipkow~\cite{Baader-Nipkow}.
-
-Each \isacommand{recdef} definition should be accompanied (after the function's
-name) by a well-founded relation on the function's argument type.
-Isabelle/HOL formalizes some of the most important
-constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
-example, \isa{measure\ f} is always well-founded. The lexicographic
-product of two well-founded relations is again well-founded, which we relied
-on when defining Ackermann's function above.
-Of course the lexicographic product can also be iterated:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
-\isacommand{recdef}\isamarkupfalse%
-\ contrived\isanewline
-\ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-Lexicographic products of measure functions already go a long
-way. Furthermore, you may embed a type in an
-existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you
-will never have to prove well-foundedness of any relation composed
-solely of these building blocks. But of course the proof of
-termination of your function definition --- that the arguments
-decrease with every recursive call --- may still require you to provide
-additional lemmas.
-
-It is also possible to use your own well-founded relations with
-\isacommand{recdef}. For example, the greater-than relation can be made
-well-founded by cutting it off at a certain point. Here is an example
-of a recursive function that calls itself with increasing values up to ten:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
-\isacommand{recdef}\isamarkupfalse%
-\ f\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-Since \isacommand{recdef} is not prepared for the relation supplied above,
-Isabelle rejects the definition. We should first have proved that
-our relation was well-founded:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequoteopen}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequoteclose}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-The proof is by showing that our relation is a subset of another well-founded
-relation: one given by a measure function.\index{*wf_subset (theorem)}%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequoteclose}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}%
-\end{isabelle}
-
-\noindent
-The inclusion remains to be proved. After unfolding some definitions,
-we are left with simple arithmetic that is dispatched automatically.%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-
-Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
-crucial hint\cmmdx{hints} to our definition:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the
-well-founded relation in our \isacommand{recdef}. However, the arithmetic
-goal in the lemma above would have arisen instead in the \isacommand{recdef}
-termination proof, where we have less control. A tailor-made termination
-relation makes even more sense when it can be used in several function
-declarations.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: