|
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 \isa{if}. |
|
11 Let us look at an example: |
|
12 *} |
|
13 |
|
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))"; |
|
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 *} |
|
22 |
|
23 (*<*)term(*>*) "n \\<noteq> 0 \\<Longrightarrow> m mod n < n"; |
|
24 |
|
25 text{*\noindent |
|
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 |
|
34 *} |
|
35 |
|
36 (*<*)term(*>*) "gcd(m,n) = k"; |
|
37 |
|
38 text{*\noindent |
|
39 in one step to |
|
40 *} |
|
41 |
|
42 (*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k"; |
|
43 |
|
44 text{*\noindent |
|
45 where the condition cannot be reduced further, and splitting leads to |
|
46 *} |
|
47 |
|
48 (*<*)term(*>*) "(n=0 \\<longrightarrow> m=k) \\<and> (n\\<noteq>0 \\<longrightarrow> gcd(n, m mod n)=k)"; |
|
49 |
|
50 text{*\noindent |
|
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. |
|
54 |
|
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. |
|
60 |
|
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: |
|
64 *} |
|
65 |
|
66 consts gcd1 :: "nat*nat \\<Rightarrow> nat"; |
|
67 recdef gcd1 "measure (\\<lambda>(m,n).n)" |
|
68 "gcd1 (m, 0) = m" |
|
69 "gcd1 (m, n) = gcd1(n, m mod n)"; |
|
70 |
|
71 |
|
72 text{*\noindent |
|
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. |
|
76 |
|
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: |
|
79 *} |
|
80 |
|
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))"; |
|
84 |
|
85 text{*\noindent |
|
86 In fact, this is probably the neatest solution next to pattern matching. |
|
87 |
|
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 |
|
90 *} |
|
91 |
|
92 lemma [simp]: "gcd (m, 0) = m"; |
|
93 apply(simp).; |
|
94 lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"; |
|
95 apply(simp).; |
|
96 |
|
97 text{*\noindent |
|
98 after which we can disable the original simplification rule: |
|
99 *} |
|
100 |
|
101 lemmas [simp del] = gcd.simps; |
|
102 |
|
103 (*<*) |
|
104 end |
|
105 (*>*) |