--- a/doc-src/TutorialI/Recdef/document/simplification.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Sun Aug 06 15:26:53 2000 +0200
@@ -8,17 +8,20 @@
terminate because of automatic splitting of \isa{if}.
Let us look at an example:%
\end{isamarkuptext}%
-\isacommand{consts}~gcd~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~gcd~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline
-~~{"}gcd~(m,~n)~=~(if~n=0~then~m~else~gcd(n,~m~mod~n)){"}%
+\isacommand{consts}\ gcd\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ gcd\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
+\ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n)){"}%
\begin{isamarkuptext}%
\noindent
According to the measure function, the second argument should decrease with
-each recursive call. The resulting termination condition%
-\end{isamarkuptext}%
-~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~m~mod~n~<~n{"}%
-\begin{isamarkuptext}%
-\noindent
+each recursive call. The resulting termination condition
+\begin{quote}
+
+\begin{isabelle}%
+n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ m\ mod\ n\ <\ n
+\end{isabelle}%
+
+\end{quote}
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
@@ -26,24 +29,34 @@
languages and our simplifier don't do that. Unfortunately the simplifier does
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%
-\end{isamarkuptext}%
-~{"}gcd(m,n)~=~k{"}%
-\begin{isamarkuptext}%
-\noindent
-in one step to%
-\end{isamarkuptext}%
-~{"}(if~n=0~then~m~else~gcd(n,~m~mod~n))~=~k{"}%
-\begin{isamarkuptext}%
-\noindent
-where the condition cannot be reduced further, and splitting leads to%
-\end{isamarkuptext}%
-~{"}(n=0~{\isasymlongrightarrow}~m=k)~{\isasymand}~(n{\isasymnoteq}0~{\isasymlongrightarrow}~gcd(n,~m~mod~n)=k){"}%
-\begin{isamarkuptext}%
-\noindent
-Since the recursive call \isa{gcd(n, m mod n)} 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 different ways.
+example, simplification reduces
+\begin{quote}
+
+\begin{isabelle}%
+gcd\ (m,\ n)\ =\ k
+\end{isabelle}%
+
+\end{quote}
+in one step to
+\begin{quote}
+
+\begin{isabelle}%
+(if\ n\ =\ 0\ then\ m\ else\ gcd\ (n,\ m\ mod\ n))\ =\ k
+\end{isabelle}%
+
+\end{quote}
+where the condition cannot be reduced further, and splitting leads to
+\begin{quote}
+
+\begin{isabelle}%
+(n\ =\ 0\ {\isasymlongrightarrow}\ m\ =\ k)\ {\isasymand}\ (n\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (n,\ m\ mod\ n)\ =\ k)
+\end{isabelle}%
+
+\end{quote}
+Since the recursive call \isa{gcd\ (n,\ m\ mod\ n)} 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
+different ways.
The most radical solution is to disable the offending
\isa{split_if} as shown in the section on case splits in
@@ -55,10 +68,10 @@
rather than \isa{if} on the right. In the case of \isa{gcd} the
following alternative definition suggests itself:%
\end{isamarkuptext}%
-\isacommand{consts}~gcd1~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~gcd1~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline
-~~{"}gcd1~(m,~0)~=~m{"}\isanewline
-~~{"}gcd1~(m,~n)~=~gcd1(n,~m~mod~n){"}%
+\isacommand{consts}\ gcd1\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ gcd1\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
+\ \ {"}gcd1\ (m,\ 0)\ =\ m{"}\isanewline
+\ \ {"}gcd1\ (m,\ n)\ =\ gcd1(n,\ m\ mod\ n){"}%
\begin{isamarkuptext}%
\noindent
Note that the order of equations is important and hides the side condition
@@ -68,9 +81,9 @@
A very simple alternative is to replace \isa{if} by \isa{case}, which
is also available for \isa{bool} but is not split automatically:%
\end{isamarkuptext}%
-\isacommand{consts}~gcd2~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
-\isacommand{recdef}~gcd2~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline
-~~{"}gcd2(m,n)~=~(case~n=0~of~True~{\isasymRightarrow}~m~|~False~{\isasymRightarrow}~gcd2(n,m~mod~n)){"}%
+\isacommand{consts}\ gcd2\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
+\isacommand{recdef}\ gcd2\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
+\ \ {"}gcd2(m,n)\ =\ (case\ n=0\ of\ True\ {\isasymRightarrow}\ m\ |\ False\ {\isasymRightarrow}\ gcd2(n,m\ mod\ n)){"}%
\begin{isamarkuptext}%
\noindent
In fact, this is probably the neatest solution next to pattern matching.
@@ -78,15 +91,15 @@
A final alternative is to replace the offending simplification rules by
derived conditional ones. For \isa{gcd} it means we have to prove%
\end{isamarkuptext}%
-\isacommand{lemma}~[simp]:~{"}gcd~(m,~0)~=~m{"}\isanewline
+\isacommand{lemma}\ [simp]:\ {"}gcd\ (m,\ 0)\ =\ m{"}\isanewline
\isacommand{by}(simp)\isanewline
-\isacommand{lemma}~[simp]:~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~gcd(m,~n)~=~gcd(n,~m~mod~n){"}\isanewline
+\isacommand{lemma}\ [simp]:\ {"}n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ gcd(m,\ n)\ =\ gcd(n,\ m\ mod\ n){"}\isanewline
\isacommand{by}(simp)%
\begin{isamarkuptext}%
\noindent
after which we can disable the original simplification rule:%
\end{isamarkuptext}%
-\isacommand{lemmas}~[simp~del]~=~gcd.simps\isanewline
+\isacommand{lemmas}\ [simp\ del]\ =\ gcd.simps\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex