--- a/doc-src/Functions/Thy/document/Functions.tex Fri Feb 25 17:11:05 2011 +0100
+++ b/doc-src/Functions/Thy/document/Functions.tex Fri Feb 25 17:11:24 2011 +0100
@@ -1464,78 +1464,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{A Useful Special Case: Tail recursion%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The domain predicate is our trick that allows us to model partiality
- in a world of total functions. The downside of this is that we have
- to carry it around all the time. The termination proof above allowed
- us to replace the abstract \isa{findzero{\isaliteral{5F}{\isacharunderscore}}dom\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}} by the more
- concrete \isa{n\ {\isaliteral{5C3C6C653E}{\isasymle}}\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}}, but the condition is still
- there and can only be discharged for special cases.
- In particular, the domain predicate guards the unfolding of our
- function, since it is there as a condition in the \isa{psimp}
- rules.
-
- Now there is an important special case: We can actually get rid
- of the condition in the simplification rules, \emph{if the function
- is tail-recursive}. The reason is that for all tail-recursive
- equations there is a total function satisfying them, even if they
- are non-terminating.
-
-% A function is tail recursive, if each call to the function is either
-% equal
-%
-% So the outer form of the
-%
-%if it can be written in the following
-% form:
-% {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
-
-
- The function package internally does the right construction and can
- derive the unconditional simp rules, if we ask it to do so. Luckily,
- our \isa{findzero} function is tail-recursive, so we can just go
- back and add another option to the \cmd{function} command:
-
-\vspace{1ex}
-\noindent\cmd{function} \isa{{\isaliteral{28}{\isacharparenleft}}domintros{\isaliteral{2C}{\isacharcomma}}\ tailrec{\isaliteral{29}{\isacharparenright}}\ findzero\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequote}}}\\%
-\cmd{where}\isanewline%
-\ \ \ldots\\%
-
-
- \noindent Now, we actually get unconditional simplification rules, even
- though the function is partial:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{thm}\isamarkupfalse%
-\ findzero{\isaliteral{2E}{\isachardot}}simps%
-\begin{isamarkuptext}%
-\begin{isabelle}%
-findzero\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{3F}{\isacharquery}}n\ else\ findzero\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{3F}{\isacharquery}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-
- \noindent Of course these would make the simplifier loop, so we better remove
- them from the simpset:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{declare}\isamarkupfalse%
-\ findzero{\isaliteral{2E}{\isachardot}}simps{\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}%
-\begin{isamarkuptext}%
-Getting rid of the domain conditions in the simplification rules is
- not only useful because it simplifies proofs. It is also required in
- order to use Isabelle's code generator to generate ML code
- from a function definition.
- Since the code generator only works with equations, it cannot be
- used with \isa{psimp} rules. Thus, in order to generate code for
- partial functions, they must be defined as a tail recursion.
- Luckily, many functions have a relatively natural tail recursive
- definition.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Nested recursion%
}
\isamarkuptrue%