--- a/doc-src/TutorialI/Recdef/document/simplification.tex Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
%
\begin{isabellebody}%
+\def\isabellecontext{simplification}%
%
\begin{isamarkuptext}%
Once we have succeeded in proving all termination conditions, the recursion
@@ -16,11 +17,9 @@
\noindent
According to the measure function, the second argument should decrease with
each recursive call. The resulting termination condition
-%
\begin{isabelle}%
\ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
-\end{isabelle}%
-
+\end{isabelle}
is provded automatically because it is already present as a lemma in the
arithmetic library. Thus the recursion equation becomes a simplification
rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -29,23 +28,17 @@
something else which leads to the same problem: it splits \isa{if}s if the
condition simplifies to neither \isa{True} nor \isa{False}. For
example, simplification reduces
-%
\begin{isabelle}%
\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
-\end{isabelle}%
-
+\end{isabelle}
in one step to
-%
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
-\end{isabelle}%
-
+\end{isabelle}
where the condition cannot be reduced further, and splitting leads to
-%
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
-\end{isabelle}%
-
+\end{isabelle}
Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
an \isa{if}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many