5 text{* |
5 text{* |
6 Once we have succeeded in proving all termination conditions, the recursion |
6 Once we have succeeded in proving all termination conditions, the recursion |
7 equations become simplification rules, just as with |
7 equations become simplification rules, just as with |
8 \isacommand{primrec}. In most cases this works fine, but there is a subtle |
8 \isacommand{primrec}. In most cases this works fine, but there is a subtle |
9 problem that must be mentioned: simplification may not |
9 problem that must be mentioned: simplification may not |
10 terminate because of automatic splitting of @{name"if"}. |
10 terminate because of automatic splitting of @{text"if"}. |
11 Let us look at an example: |
11 Let us look at an example: |
12 *} |
12 *} |
13 |
13 |
14 consts gcd :: "nat*nat \\<Rightarrow> nat"; |
14 consts gcd :: "nat*nat \\<Rightarrow> nat"; |
15 recdef gcd "measure (\\<lambda>(m,n).n)" |
15 recdef gcd "measure (\\<lambda>(m,n).n)" |
22 @{term[display]"n ~= 0 ==> m mod n < n"} |
22 @{term[display]"n ~= 0 ==> m mod n < n"} |
23 \end{quote} |
23 \end{quote} |
24 is provded automatically because it is already present as a lemma in the |
24 is provded automatically because it is already present as a lemma in the |
25 arithmetic library. Thus the recursion equation becomes a simplification |
25 arithmetic library. Thus the recursion equation becomes a simplification |
26 rule. Of course the equation is nonterminating if we are allowed to unfold |
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 |
27 the recursive call inside the @{text"if"} branch, which is why programming |
28 languages and our simplifier don't do that. Unfortunately the simplifier does |
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 |
29 something else which leads to the same problem: it splits @{text"if"}s if the |
30 condition simplifies to neither @{term"True"} nor @{term"False"}. For |
30 condition simplifies to neither @{term"True"} nor @{term"False"}. For |
31 example, simplification reduces |
31 example, simplification reduces |
32 \begin{quote} |
32 \begin{quote} |
33 @{term[display]"gcd(m,n) = k"} |
33 @{term[display]"gcd(m,n) = k"} |
34 \end{quote} |
34 \end{quote} |
39 where the condition cannot be reduced further, and splitting leads to |
39 where the condition cannot be reduced further, and splitting leads to |
40 \begin{quote} |
40 \begin{quote} |
41 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"} |
41 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"} |
42 \end{quote} |
42 \end{quote} |
43 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by |
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 |
44 an @{text"if"}, it is unfolded again, which leads to an infinite chain of |
45 simplification steps. Fortunately, this problem can be avoided in many |
45 simplification steps. Fortunately, this problem can be avoided in many |
46 different ways. |
46 different ways. |
47 |
47 |
48 The most radical solution is to disable the offending \@{name"split_if"} as |
48 The most radical solution is to disable the offending |
49 shown in the section on case splits in \S\ref{sec:Simplification}. However, |
49 @{thm[source]split_if} as shown in the section on case splits in |
50 we do not recommend this because it means you will often have to invoke the |
50 \S\ref{sec:Simplification}. However, we do not recommend this because it |
51 rule explicitly when @{name"if"} is involved. |
51 means you will often have to invoke the rule explicitly when @{text"if"} is |
|
52 involved. |
52 |
53 |
53 If possible, the definition should be given by pattern matching on the left |
54 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 rather than @{text"if"} on the right. In the case of @{term"gcd"} the |
55 following alternative definition suggests itself: |
56 following alternative definition suggests itself: |
56 *} |
57 *} |
57 |
58 |
58 consts gcd1 :: "nat*nat \\<Rightarrow> nat"; |
59 consts gcd1 :: "nat*nat \\<Rightarrow> nat"; |
59 recdef gcd1 "measure (\\<lambda>(m,n).n)" |
60 recdef gcd1 "measure (\\<lambda>(m,n).n)" |
64 text{*\noindent |
65 text{*\noindent |
65 Note that the order of equations is important and hides the side condition |
66 Note that the order of equations is important and hides the side condition |
66 @{prop"n ~= 0"}. Unfortunately, in general the case distinction |
67 @{prop"n ~= 0"}. Unfortunately, in general the case distinction |
67 may not be expressible by pattern matching. |
68 may not be expressible by pattern matching. |
68 |
69 |
69 A very simple alternative is to replace @{name"if"} by @{name"case"}, which |
70 A very simple alternative is to replace @{text"if"} by @{text"case"}, which |
70 is also available for @{typ"bool"} but is not split automatically: |
71 is also available for @{typ"bool"} but is not split automatically: |
71 *} |
72 *} |
72 |
73 |
73 consts gcd2 :: "nat*nat \\<Rightarrow> nat"; |
74 consts gcd2 :: "nat*nat \\<Rightarrow> nat"; |
74 recdef gcd2 "measure (\\<lambda>(m,n).n)" |
75 recdef gcd2 "measure (\\<lambda>(m,n).n)" |