35 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by |
35 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by |
36 an @{text if}, it is unfolded again, which leads to an infinite chain of |
36 an @{text if}, it is unfolded again, which leads to an infinite chain of |
37 simplification steps. Fortunately, this problem can be avoided in many |
37 simplification steps. Fortunately, this problem can be avoided in many |
38 different ways. |
38 different ways. |
39 |
39 |
40 The most radical solution is to disable the offending |
40 The most radical solution is to disable the offending @{thm[source]split_if} |
41 @{thm[source]split_if} as shown in the section on case splits in |
41 as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this |
42 \S\ref{sec:Simplification}. However, we do not recommend this because it |
42 because it means you will often have to invoke the rule explicitly when |
43 means you will often have to invoke the rule explicitly when @{text if} is |
43 @{text if} is involved. |
44 involved. |
|
45 |
44 |
46 If possible, the definition should be given by pattern matching on the left |
45 If possible, the definition should be given by pattern matching on the left |
47 rather than @{text if} on the right. In the case of @{term gcd} the |
46 rather than @{text if} on the right. In the case of @{term gcd} the |
48 following alternative definition suggests itself: |
47 following alternative definition suggests itself: |
49 *} |
48 *} |