8745
+ − 1
(*<*)
16417
+ − 2
theory simplification imports Main begin;
8745
+ − 3
(*>*)
+ − 4
+ − 5
text{*
11458
+ − 6
Once we have proved all the termination conditions, the \isacommand{recdef}
+ − 7
recursion equations become simplification rules, just as with
8745
+ − 8
\isacommand{primrec}. In most cases this works fine, but there is a subtle
+ − 9
problem that must be mentioned: simplification may not
19792
+ − 10
terminate because of automatic splitting of @{text "if"}.
11458
+ − 11
\index{*if expressions!splitting of}
8745
+ − 12
Let us look at an example:
+ − 13
*}
+ − 14
10171
+ − 15
consts gcd :: "nat\<times>nat \<Rightarrow> nat";
+ − 16
recdef gcd "measure (\<lambda>(m,n).n)"
8745
+ − 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
12473
+ − 22
@{term[display]"n ~= (0::nat) ==> m mod n < n"}
10885
+ − 23
is proved automatically because it is already present as a lemma in
+ − 24
HOL\@. Thus the recursion equation becomes a simplification
8745
+ − 25
rule. Of course the equation is nonterminating if we are allowed to unfold
10171
+ − 26
the recursive call inside the @{text else} branch, which is why programming
8745
+ − 27
languages and our simplifier don't do that. Unfortunately the simplifier does
11458
+ − 28
something else that leads to the same problem: it splits
19792
+ − 29
each @{text "if"}-expression unless its
11458
+ − 30
condition simplifies to @{term True} or @{term False}. For
8745
+ − 31
example, simplification reduces
9541
+ − 32
@{term[display]"gcd(m,n) = k"}
8745
+ − 33
in one step to
9541
+ − 34
@{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
8745
+ − 35
where the condition cannot be reduced further, and splitting leads to
9541
+ − 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
19792
+ − 38
an @{text "if"}, it is unfolded again, which leads to an infinite chain of
9541
+ − 39
simplification steps. Fortunately, this problem can be avoided in many
+ − 40
different ways.
8745
+ − 41
11458
+ − 42
The most radical solution is to disable the offending theorem
+ − 43
@{thm[source]split_if},
11215
+ − 44
as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
11458
+ − 45
approach: you will often have to invoke the rule explicitly when
19792
+ − 46
@{text "if"} is involved.
8745
+ − 47
+ − 48
If possible, the definition should be given by pattern matching on the left
19792
+ − 49
rather than @{text "if"} on the right. In the case of @{term gcd} the
8745
+ − 50
following alternative definition suggests itself:
+ − 51
*}
+ − 52
10171
+ − 53
consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
+ − 54
recdef gcd1 "measure (\<lambda>(m,n).n)"
8745
+ − 55
"gcd1 (m, 0) = m"
+ − 56
"gcd1 (m, n) = gcd1(n, m mod n)";
+ − 57
+ − 58
+ − 59
text{*\noindent
11458
+ − 60
The order of equations is important: it hides the side condition
12473
+ − 61
@{prop"n ~= (0::nat)"}. Unfortunately, in general the case distinction
8745
+ − 62
may not be expressible by pattern matching.
+ − 63
19792
+ − 64
A simple alternative is to replace @{text "if"} by @{text case},
11458
+ − 65
which is also available for @{typ bool} and is not split automatically:
8745
+ − 66
*}
+ − 67
10171
+ − 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))";
8745
+ − 71
+ − 72
text{*\noindent
11458
+ − 73
This is probably the neatest solution next to pattern matching, and it is
+ − 74
always available.
8745
+ − 75
+ − 76
A final alternative is to replace the offending simplification rules by
10171
+ − 77
derived conditional ones. For @{term gcd} it means we have to prove
10795
+ − 78
these lemmas:
8745
+ − 79
*}
+ − 80
+ − 81
lemma [simp]: "gcd (m, 0) = m";
10171
+ − 82
apply(simp);
+ − 83
done
11458
+ − 84
10171
+ − 85
lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
+ − 86
apply(simp);
+ − 87
done
8745
+ − 88
+ − 89
text{*\noindent
11458
+ − 90
Simplification terminates for these proofs because the condition of the @{text
19792
+ − 91
"if"} simplifies to @{term True} or @{term False}.
10795
+ − 92
Now we can disable the original simplification rule:
8745
+ − 93
*}
+ − 94
9933
+ − 95
declare gcd.simps [simp del]
8745
+ − 96
+ − 97
(*<*)
+ − 98
end
+ − 99
(*>*)