--- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 01 19:09:44 2000 +0200
@@ -6,10 +6,10 @@
its termination with the help of the user-supplied measure. All of the above
examples are simple enough that Isabelle can prove automatically that the
measure of the argument goes down in each recursive call. As a result,
-\isa{$f$.simps} will contain the defining equations (or variants derived from
-them) as theorems. For example, look (via \isacommand{thm}) at
-\isa{sep.simps} and \isa{sep1.simps} to see that they define the same
-function. What is more, those equations are automatically declared as
+$f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived
+from them) as theorems. For example, look (via \isacommand{thm}) at
+\isa{sep{\isachardot}simps} and \isa{sep\isadigit{1}{\isachardot}simps} to see that they define
+the same function. What is more, those equations are automatically declared as
simplification rules.
In general, Isabelle may not be able to prove all termination condition
@@ -29,7 +29,7 @@
\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-It was not proved automatically because of the special nature of \isa{-}
+It was not proved automatically because of the special nature of \isa{{\isacharminus}}
on \isa{nat}. This requires more arithmetic than is tried by default:%
\end{isamarkuptxt}%
\isacommand{by}{\isacharparenleft}arith{\isacharparenright}%
@@ -44,8 +44,8 @@
\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-This time everything works fine. Now \isa{g.simps} contains precisely the
-stated recursion equation for \isa{g} and they are simplification
+This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
+the stated recursion equation for \isa{g} and they are simplification
rules. Thus we can automatically prove%
\end{isamarkuptext}%
\isacommand{theorem}\ wow{\isacharcolon}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
@@ -54,7 +54,7 @@
\noindent
More exciting theorems require induction, which is discussed below.
-Because lemma \isa{termi_lem} above was only turned into a
+Because lemma \isa{termi{\isacharunderscore}lem} above was only turned into a
simplification rule for the sake of the termination proof, we may want to
disable it again:%
\end{isamarkuptext}%
@@ -63,22 +63,23 @@
The attentive reader may wonder why we chose to call our function \isa{g}
rather than \isa{f} the second time around. The reason is that, despite
the failed termination proof, the definition of \isa{f} did not
-fail (and thus we could not define it a second time). However, all theorems
-about \isa{f}, for example \isa{f.simps}, carry as a precondition the
-unproved termination condition. Moreover, the theorems \isa{f.simps} are
-not simplification rules. However, this mechanism allows a delayed proof of
-termination: instead of proving \isa{termi_lem} up front, we could prove
+fail, and thus we could not define it a second time. However, all theorems
+about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition
+the unproved termination condition. Moreover, the theorems
+\isa{f{\isachardot}simps} are not simplification rules. However, this mechanism
+allows a delayed proof of termination: instead of proving
+\isa{termi{\isacharunderscore}lem} up front, we could prove
it later on and then use it to remove the preconditions from the theorems
about \isa{f}. In most cases this is more cumbersome than proving things
-up front
+up front.
%FIXME, with one exception: nested recursion.
Although all the above examples employ measure functions, \isacommand{recdef}
allows arbitrary wellfounded relations. For example, termination of
-Ackermann's function requires the lexicographic product \isa{<*lex*>}:%
+Ackermann's function requires the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
\end{isamarkuptext}%
\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
-\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isacharpercent}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%