doc-src/TutorialI/Recdef/document/simplification.tex

 \isacommand{primrec}. In most cases this works fine, but there is a subtle
 problem that must be mentioned: simplification may not
 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
 the recursive call inside the \isa{else} branch, which is why programming
 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
 \S\ref{sec:SimpFeatures}.
 However, we do not recommend this because it means you will often have to

 
 If possible, the definition should be given by pattern matching on the left
 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
 \isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 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.
 
 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
 %%% TeX-master: "root"
 %%% End: