2 theory simplification = Main:;
6 Once we have proved all the termination conditions, the \isacommand{recdef}
7 recursion 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 \index{*if expressions!splitting of}
12 Let us look at an example:
15 consts gcd :: "nat\<times>nat \<Rightarrow> nat";
16 recdef gcd "measure (\<lambda>(m,n).n)"
17 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
20 According to the measure function, the second argument should decrease with
21 each recursive call. The resulting termination condition
22 @{term[display]"n ~= 0 ==> m mod n < n"}
23 is proved automatically because it is already present as a lemma in
24 HOL\@. Thus the recursion equation becomes a simplification
25 rule. Of course the equation is nonterminating if we are allowed to unfold
26 the recursive call inside the @{text else} branch, which is why programming
27 languages and our simplifier don't do that. Unfortunately the simplifier does
28 something else that leads to the same problem: it splits
29 each @{text if}-expression unless its
30 condition simplifies to @{term True} or @{term False}. For
31 example, simplification reduces
32 @{term[display]"gcd(m,n) = k"}
34 @{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
35 where the condition cannot be reduced further, and splitting leads to
36 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
37 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
38 an @{text if}, it is unfolded again, which leads to an infinite chain of
39 simplification steps. Fortunately, this problem can be avoided in many
42 The most radical solution is to disable the offending theorem
43 @{thm[source]split_if},
44 as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
45 approach: you will often have to invoke the rule explicitly when
46 @{text if} is involved.
48 If possible, the definition should be given by pattern matching on the left
49 rather than @{text if} on the right. In the case of @{term gcd} the
50 following alternative definition suggests itself:
53 consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
54 recdef gcd1 "measure (\<lambda>(m,n).n)"
56 "gcd1 (m, n) = gcd1(n, m mod n)";
60 The order of equations is important: it hides the side condition
61 @{prop"n ~= 0"}. Unfortunately, in general the case distinction
62 may not be expressible by pattern matching.
64 A simple alternative is to replace @{text if} by @{text case},
65 which is also available for @{typ bool} and is not split automatically:
68 consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
69 recdef gcd2 "measure (\<lambda>(m,n).n)"
70 "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
73 This is probably the neatest solution next to pattern matching, and it is
76 A final alternative is to replace the offending simplification rules by
77 derived conditional ones. For @{term gcd} it means we have to prove
81 lemma [simp]: "gcd (m, 0) = m";
85 lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
90 Simplification terminates for these proofs because the condition of the @{text
91 if} simplifies to @{term True} or @{term False}.
92 Now we can disable the original simplification rule:
95 declare gcd.simps [simp del]