doc-src/TutorialI/Recdef/simplification.thy
author paulson
Fri, 05 Jan 2001 18:32:57 +0100
changeset 10795 9e888d60d3e5
parent 10178 aecb5bf6f76f
child 10885 90695f46440b
permissions -rw-r--r--
minor edits to Chapters 1-3
     1 (*<*)
     2 theory simplification = Main:;
     3 (*>*)
     4 
     5 text{*
     6 Once we have succeeded in proving all termination conditions, the recursion
     7 equations become simplification rules, just as with
     8 \isacommand{primrec}. In most cases this works fine, but there is a subtle
     9 problem that must be mentioned: simplification may not
    10 terminate because of automatic splitting of @{text if}.
    11 Let us look at an example:
    12 *}
    13 
    14 consts gcd :: "nat\<times>nat \<Rightarrow> nat";
    15 recdef gcd "measure (\<lambda>(m,n).n)"
    16   "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
    17 
    18 text{*\noindent
    19 According to the measure function, the second argument should decrease with
    20 each recursive call. The resulting termination condition
    21 @{term[display]"n ~= 0 ==> m mod n < n"}
    22 is provded automatically because it is already present as a lemma in the
    23 arithmetic library. Thus the recursion equation becomes a simplification
    24 rule. Of course the equation is nonterminating if we are allowed to unfold
    25 the recursive call inside the @{text else} branch, which is why programming
    26 languages and our simplifier don't do that. Unfortunately the simplifier does
    27 something else which leads to the same problem: it splits @{text if}s if the
    28 condition simplifies to neither @{term True} nor @{term False}. For
    29 example, simplification reduces
    30 @{term[display]"gcd(m,n) = k"}
    31 in one step to
    32 @{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
    33 where the condition cannot be reduced further, and splitting leads to
    34 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
    35 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
    36 an @{text if}, it is unfolded again, which leads to an infinite chain of
    37 simplification steps. Fortunately, this problem can be avoided in many
    38 different ways.
    39 
    40 The most radical solution is to disable the offending
    41 @{thm[source]split_if} as shown in the section on case splits in
    42 \S\ref{sec:Simplification}.  However, we do not recommend this because it
    43 means you will often have to invoke the rule explicitly when @{text if} is
    44 involved.
    45 
    46 If possible, the definition should be given by pattern matching on the left
    47 rather than @{text if} on the right. In the case of @{term gcd} the
    48 following alternative definition suggests itself:
    49 *}
    50 
    51 consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
    52 recdef gcd1 "measure (\<lambda>(m,n).n)"
    53   "gcd1 (m, 0) = m"
    54   "gcd1 (m, n) = gcd1(n, m mod n)";
    55 
    56 
    57 text{*\noindent
    58 Note that the order of equations is important and hides the side condition
    59 @{prop"n ~= 0"}. Unfortunately, in general the case distinction
    60 may not be expressible by pattern matching.
    61 
    62 A very simple alternative is to replace @{text if} by @{text case}, which
    63 is also available for @{typ bool} but is not split automatically:
    64 *}
    65 
    66 consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
    67 recdef gcd2 "measure (\<lambda>(m,n).n)"
    68   "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
    69 
    70 text{*\noindent
    71 In fact, this is probably the neatest solution next to pattern matching.
    72 
    73 A final alternative is to replace the offending simplification rules by
    74 derived conditional ones. For @{term gcd} it means we have to prove
    75 these lemmas:
    76 *}
    77 
    78 lemma [simp]: "gcd (m, 0) = m";
    79 apply(simp);
    80 done
    81 lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
    82 apply(simp);
    83 done
    84 
    85 text{*\noindent
    86 Now we can disable the original simplification rule:
    87 *}
    88 
    89 declare gcd.simps [simp del]
    90 
    91 (*<*)
    92 end
    93 (*>*)