diff -r 279da0358aa9 -r 09a6c44a48ea doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Thu Jul 26 18:23:38 2001 +0200 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Aug 03 18:04:55 2001 +0200 @@ -3,11 +3,12 @@ \def\isabellecontext{simplification}% % \begin{isamarkuptext}% -Once we have succeeded in proving all termination conditions, the recursion -equations become simplification rules, just as with +Once we have proved all the termination conditions, the \isacommand{recdef} +recursion equations become simplification rules, just as with \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}. +\index{*if expressions!splitting of} Let us look at an example:% \end{isamarkuptext}% \isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline @@ -25,8 +26,9 @@ 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 +something else that leads to the same problem: it splits +each \isa{if}-expression unless its +condition simplifies to \isa{True} or \isa{False}. For example, simplification reduces \begin{isabelle}% \ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k% @@ -44,9 +46,10 @@ simplification steps. Fortunately, this problem can be avoided in many different ways. -The most radical solution is to disable the offending \isa{split{\isacharunderscore}if} +The most radical solution is to disable the offending theorem +\isa{split{\isacharunderscore}if}, as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this -because it means you will often have to invoke the rule explicitly when +approach: you will often have to invoke the rule explicitly when \isa{if} is involved. If possible, the definition should be given by pattern matching on the left @@ -59,19 +62,20 @@ \ \ {\isachardoublequote}gcd{\isadigit{1}}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isadigit{1}}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent -Note that the order of equations is important and hides the side condition -\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction +The order of equations is important: it hides the side condition +\isa{n\ {\isasymnoteq}\ {\isadigit{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:% +A simple alternative is to replace \isa{if} by \isa{case}, +which is also available for \isa{bool} and is not split automatically:% \end{isamarkuptext}% \isacommand{consts}\ gcd{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isacommand{recdef}\ gcd{\isadigit{2}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline \ \ {\isachardoublequote}gcd{\isadigit{2}}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent -In fact, this is probably the neatest solution next to pattern matching. +This is probably the neatest solution next to pattern matching, and it is +always available. A final alternative is to replace the offending simplification rules by derived conditional ones. For \isa{gcd} it means we have to prove @@ -80,11 +84,13 @@ \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isacommand{done}\isanewline +\isanewline \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% \noindent +Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}. Now we can disable the original simplification rule:% \end{isamarkuptext}% \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline