2 theory simplification = Main:;
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:
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))";
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"}
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
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
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:
51 consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
52 recdef gcd1 "measure (\<lambda>(m,n).n)"
54 "gcd1 (m, n) = gcd1(n, m mod n)";
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.
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:
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))";
71 In fact, this is probably the neatest solution next to pattern matching.
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
78 lemma [simp]: "gcd (m, 0) = m";
81 lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
86 Now we can disable the original simplification rule:
89 declare gcd.simps [simp del]