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 @{name"if"}.
11 Let us look at an example:
14 consts gcd :: "nat*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
22 @{term[display]"n ~= 0 ==> m mod n < n"}
24 is provded automatically because it is already present as a lemma in the
25 arithmetic library. Thus the recursion equation becomes a simplification
26 rule. Of course the equation is nonterminating if we are allowed to unfold
27 the recursive call inside the @{name"if"} branch, which is why programming
28 languages and our simplifier don't do that. Unfortunately the simplifier does
29 something else which leads to the same problem: it splits @{name"if"}s if the
30 condition simplifies to neither @{term"True"} nor @{term"False"}. For
31 example, simplification reduces
33 @{term[display]"gcd(m,n) = k"}
37 @{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
39 where the condition cannot be reduced further, and splitting leads to
41 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
43 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
44 an @{name"if"}, it is unfolded again, which leads to an infinite chain of
45 simplification steps. Fortunately, this problem can be avoided in many
48 The most radical solution is to disable the offending \@{name"split_if"} as
49 shown in the section on case splits in \S\ref{sec:Simplification}. However,
50 we do not recommend this because it means you will often have to invoke the
51 rule explicitly when @{name"if"} is involved.
53 If possible, the definition should be given by pattern matching on the left
54 rather than @{name"if"} on the right. In the case of @{term"gcd"} the
55 following alternative definition suggests itself:
58 consts gcd1 :: "nat*nat \\<Rightarrow> nat";
59 recdef gcd1 "measure (\\<lambda>(m,n).n)"
61 "gcd1 (m, n) = gcd1(n, m mod n)";
65 Note that the order of equations is important and hides the side condition
66 @{prop"n ~= 0"}. Unfortunately, in general the case distinction
67 may not be expressible by pattern matching.
69 A very simple alternative is to replace @{name"if"} by @{name"case"}, which
70 is also available for @{typ"bool"} but is not split automatically:
73 consts gcd2 :: "nat*nat \\<Rightarrow> nat";
74 recdef gcd2 "measure (\\<lambda>(m,n).n)"
75 "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
78 In fact, this is probably the neatest solution next to pattern matching.
80 A final alternative is to replace the offending simplification rules by
81 derived conditional ones. For @{term"gcd"} it means we have to prove
84 lemma [simp]: "gcd (m, 0) = m";
86 lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
90 after which we can disable the original simplification rule:
93 lemmas [simp del] = gcd.simps;