I wonder which files i forgot.
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 \isa{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
23 (*<*)term(*>*) "n \\<noteq> 0 \\<Longrightarrow> m mod n < n";
26 is provded automatically because it is already present as a lemma in the
27 arithmetic library. Thus the recursion equation becomes a simplification
28 rule. Of course the equation is nonterminating if we are allowed to unfold
29 the recursive call inside the \isa{else} branch, which is why programming
30 languages and our simplifier don't do that. Unfortunately the simplifier does
31 something else which leads to the same problem: it splits \isa{if}s if the
32 condition simplifies to neither \isa{True} nor \isa{False}. For
33 example, simplification reduces
36 (*<*)term(*>*) "gcd(m,n) = k";
42 (*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k";
45 where the condition cannot be reduced further, and splitting leads to
48 (*<*)term(*>*) "(n=0 \\<longrightarrow> m=k) \\<and> (n\\<noteq>0 \\<longrightarrow> gcd(n, m mod n)=k)";
51 Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
52 an \isa{if}, this leads to an infinite chain of simplification steps.
53 Fortunately, this problem can be avoided in many different ways.
55 Of course the most radical solution is to disable the offending
56 \isa{split_if} as shown in the section on case splits in
57 \S\ref{sec:SimpFeatures}.
58 However, we do not recommend this because it means you will often have to
59 invoke the rule explicitly when \isa{if} is involved.
61 If possible, the definition should be given by pattern matching on the left
62 rather than \isa{if} on the right. In the case of \isa{gcd} the
63 following alternative definition suggests itself:
66 consts gcd1 :: "nat*nat \\<Rightarrow> nat";
67 recdef gcd1 "measure (\\<lambda>(m,n).n)"
69 "gcd1 (m, n) = gcd1(n, m mod n)";
73 Note that the order of equations is important and hides the side condition
74 \isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
75 may not be expressible by pattern matching.
77 A very simple alternative is to replace \isa{if} by \isa{case}, which
78 is also available for \isa{bool} but is not split automatically:
81 consts gcd2 :: "nat*nat \\<Rightarrow> nat";
82 recdef gcd2 "measure (\\<lambda>(m,n).n)"
83 "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
86 In fact, this is probably the neatest solution next to pattern matching.
88 A final alternative is to replace the offending simplification rules by
89 derived conditional ones. For \isa{gcd} it means we have to prove
92 lemma [simp]: "gcd (m, 0) = m";
94 lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
98 after which we can disable the original simplification rule:
101 lemmas [simp del] = gcd.simps;