# HG changeset patch
# User krauss
# Date 1298650284 -3600
# Node ID f53e0e0baa4f331c9bf4907a44ca14acd0596f05
# Parent  b0d6acf73588c10133af9026a8c78c100e157a34
updated generated files

diff -r b0d6acf73588 -r f53e0e0baa4f doc-src/Functions/Thy/document/Functions.tex
--- 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%
diff -r b0d6acf73588 -r f53e0e0baa4f doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 25 17:11:05 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 25 17:11:24 2011 +0100
@@ -454,7 +454,7 @@
     ;
     equations: (thmdecl? prop + '|')
     ;
-    functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
+    functionopts: '(' (('sequential' | 'domintros') + ',') ')'
     ;
     'termination' ( term )?
   \end{rail}
@@ -523,14 +523,6 @@
   introduction rules for the domain predicate. While mostly not
   needed, they can be helpful in some proofs about partial functions.
 
-  \item \isa{tailrec} generates the unconstrained recursive
-  equations even without a termination proof, provided that the
-  function is tail-recursive. This currently only works
-
-  \item \isa{{\isaliteral{22}{\isachardoublequote}}default\ d{\isaliteral{22}{\isachardoublequote}}} allows to specify a default value for a
-  (partial) function, which will ensure that \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{3D}{\isacharequal}}\ d\ x{\isaliteral{22}{\isachardoublequote}}}
-  whenever \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}.
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%