1 (*<*) |
|
2 theory simplification imports Main begin; |
|
3 (*>*) |
|
4 |
|
5 text{* |
|
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: |
|
13 *} |
|
14 |
|
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))"; |
|
18 |
|
19 text{*\noindent |
|
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::nat) ==> 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"} |
|
33 in one step to |
|
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 |
|
40 different ways. |
|
41 |
|
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. |
|
47 |
|
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: |
|
51 *} |
|
52 |
|
53 consts gcd1 :: "nat\<times>nat \<Rightarrow> nat"; |
|
54 recdef gcd1 "measure (\<lambda>(m,n).n)" |
|
55 "gcd1 (m, 0) = m" |
|
56 "gcd1 (m, n) = gcd1(n, m mod n)"; |
|
57 |
|
58 |
|
59 text{*\noindent |
|
60 The order of equations is important: it hides the side condition |
|
61 @{prop"n ~= (0::nat)"}. Unfortunately, in general the case distinction |
|
62 may not be expressible by pattern matching. |
|
63 |
|
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: |
|
66 *} |
|
67 |
|
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))"; |
|
71 |
|
72 text{*\noindent |
|
73 This is probably the neatest solution next to pattern matching, and it is |
|
74 always available. |
|
75 |
|
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 |
|
78 these lemmas: |
|
79 *} |
|
80 |
|
81 lemma [simp]: "gcd (m, 0) = m"; |
|
82 apply(simp); |
|
83 done |
|
84 |
|
85 lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"; |
|
86 apply(simp); |
|
87 done |
|
88 |
|
89 text{*\noindent |
|
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: |
|
93 *} |
|
94 |
|
95 declare gcd.simps [simp del] |
|
96 |
|
97 (*<*) |
|
98 end |
|
99 (*>*) |
|