1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Apr 19 11:56:31 2000 +0200
     1.3 @@ -0,0 +1,105 @@
     1.4 +(*<*)
     1.5 +theory simplification = Main:;
     1.6 +(*>*)
     1.7 +
     1.8 +text{*
     1.9 +Once we have succeeded in proving all termination conditions, the recursion
    1.10 +equations become simplification rules, just as with
    1.11 +\isacommand{primrec}. In most cases this works fine, but there is a subtle
    1.12 +problem that must be mentioned: simplification may not
    1.13 +terminate because of automatic splitting of \isa{if}.
    1.14 +Let us look at an example:
    1.15 +*}
    1.16 +
    1.17 +consts gcd :: "nat*nat \\<Rightarrow> nat";
    1.18 +recdef gcd "measure (\\<lambda>(m,n).n)"
    1.19 +  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
    1.20 +
    1.21 +text{*\noindent
    1.22 +According to the measure function, the second argument should decrease with
    1.23 +each recursive call. The resulting termination condition
    1.24 +*}
    1.25 +
    1.26 +(*<*)term(*>*) "n \\<noteq> 0 \\<Longrightarrow> m mod n < n";
    1.27 +
    1.28 +text{*\noindent
    1.29 +is provded automatically because it is already present as a lemma in the
    1.30 +arithmetic library. Thus the recursion equation becomes a simplification
    1.31 +rule. Of course the equation is nonterminating if we are allowed to unfold
    1.32 +the recursive call inside the \isa{else} branch, which is why programming
    1.33 +languages and our simplifier don't do that. Unfortunately the simplifier does
    1.34 +something else which leads to the same problem: it splits \isa{if}s if the
    1.35 +condition simplifies to neither \isa{True} nor \isa{False}. For
    1.36 +example, simplification reduces
    1.37 +*}
    1.38 +
    1.39 +(*<*)term(*>*) "gcd(m,n) = k";
    1.40 +
    1.41 +text{*\noindent
    1.42 +in one step to
    1.43 +*}
    1.44 +
    1.45 +(*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k";
    1.46 +
    1.47 +text{*\noindent
    1.48 +where the condition cannot be reduced further, and splitting leads to
    1.49 +*}
    1.50 +
    1.51 +(*<*)term(*>*) "(n=0 \\<longrightarrow> m=k) \\<and> (n\\<noteq>0 \\<longrightarrow> gcd(n, m mod n)=k)";
    1.52 +
    1.53 +text{*\noindent
    1.54 +Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
    1.55 +an \isa{if}, this leads to an infinite chain of simplification steps.
    1.56 +Fortunately, this problem can be avoided in many different ways.
    1.57 +
    1.58 +Of course the most radical solution is to disable the offending
    1.59 +\isa{split_if} as shown in the section on case splits in
    1.60 +\S\ref{sec:SimpFeatures}.
    1.61 +However, we do not recommend this because it means you will often have to
    1.62 +invoke the rule explicitly when \isa{if} is involved.
    1.63 +
    1.64 +If possible, the definition should be given by pattern matching on the left
    1.65 +rather than \isa{if} on the right. In the case of \isa{gcd} the
    1.66 +following alternative definition suggests itself:
    1.67 +*}
    1.68 +
    1.69 +consts gcd1 :: "nat*nat \\<Rightarrow> nat";
    1.70 +recdef gcd1 "measure (\\<lambda>(m,n).n)"
    1.71 +  "gcd1 (m, 0) = m"
    1.72 +  "gcd1 (m, n) = gcd1(n, m mod n)";
    1.73 +
    1.74 +
    1.75 +text{*\noindent
    1.76 +Note that the order of equations is important and hides the side condition
    1.77 +\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
    1.78 +may not be expressible by pattern matching.
    1.79 +
    1.80 +A very simple alternative is to replace \isa{if} by \isa{case}, which
    1.81 +is also available for \isa{bool} but is not split automatically:
    1.82 +*}
    1.83 +
    1.84 +consts gcd2 :: "nat*nat \\<Rightarrow> nat";
    1.85 +recdef gcd2 "measure (\\<lambda>(m,n).n)"
    1.86 +  "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
    1.87 +
    1.88 +text{*\noindent
    1.89 +In fact, this is probably the neatest solution next to pattern matching.
    1.90 +
    1.91 +A final alternative is to replace the offending simplification rules by
    1.92 +derived conditional ones. For \isa{gcd} it means we have to prove
    1.93 +*}
    1.94 +
    1.95 +lemma [simp]: "gcd (m, 0) = m";
    1.96 +apply(simp).;
    1.97 +lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
    1.98 +apply(simp).;
    1.99 +
   1.100 +text{*\noindent
   1.101 +after which we can disable the original simplification rule:
   1.102 +*}
   1.103 +
   1.104 +lemmas [simp del] = gcd.simps;
   1.105 +
   1.106 +(*<*)
   1.107 +end
   1.108 +(*>*)