nipkow@8745
|
1 |
(*<*)
|
nipkow@8745
|
2 |
theory termination = Main:;
|
nipkow@8745
|
3 |
(*>*)
|
nipkow@8745
|
4 |
|
nipkow@8745
|
5 |
text{*
|
nipkow@8745
|
6 |
When a function is defined via \isacommand{recdef}, Isabelle tries to prove
|
nipkow@8745
|
7 |
its termination with the help of the user-supplied measure. All of the above
|
nipkow@8745
|
8 |
examples are simple enough that Isabelle can prove automatically that the
|
nipkow@8771
|
9 |
measure of the argument goes down in each recursive call. As a result,
|
nipkow@8771
|
10 |
\isa{$f$.simps} will contain the defining equations (or variants derived from
|
nipkow@8745
|
11 |
them) as theorems. For example, look (via \isacommand{thm}) at
|
nipkow@8745
|
12 |
\isa{sep.simps} and \isa{sep1.simps} to see that they define the same
|
nipkow@8745
|
13 |
function. What is more, those equations are automatically declared as
|
nipkow@8745
|
14 |
simplification rules.
|
nipkow@8745
|
15 |
|
nipkow@8745
|
16 |
In general, Isabelle may not be able to prove all termination condition
|
nipkow@8745
|
17 |
(there is one for each recursive call) automatically. For example,
|
nipkow@8745
|
18 |
termination of the following artificial function
|
nipkow@8745
|
19 |
*}
|
nipkow@8745
|
20 |
|
nipkow@8745
|
21 |
consts f :: "nat*nat \\<Rightarrow> nat";
|
nipkow@8745
|
22 |
recdef f "measure(\\<lambda>(x,y). x-y)"
|
nipkow@8745
|
23 |
"f(x,y) = (if x \\<le> y then x else f(x,y+1))";
|
nipkow@8745
|
24 |
|
nipkow@8745
|
25 |
text{*\noindent
|
nipkow@8745
|
26 |
is not proved automatically (although maybe it should be). Isabelle prints a
|
nipkow@8745
|
27 |
kind of error message showing you what it was unable to prove. You will then
|
nipkow@8745
|
28 |
have to prove it as a separate lemma before you attempt the definition
|
nipkow@8745
|
29 |
of your function once more. In our case the required lemma is the obvious one:
|
nipkow@8745
|
30 |
*}
|
nipkow@8745
|
31 |
|
nipkow@8745
|
32 |
lemma termi_lem[simp]: "\\<not> x \\<le> y \\<Longrightarrow> x - Suc y < x - y";
|
nipkow@8745
|
33 |
|
nipkow@8745
|
34 |
txt{*\noindent
|
nipkow@8745
|
35 |
It was not proved automatically because of the special nature of \isa{-}
|
nipkow@8745
|
36 |
on \isa{nat}. This requires more arithmetic than is tried by default:
|
nipkow@8745
|
37 |
*}
|
nipkow@8745
|
38 |
|
nipkow@9458
|
39 |
by(arith);
|
nipkow@8745
|
40 |
|
nipkow@8745
|
41 |
text{*\noindent
|
nipkow@8771
|
42 |
Because \isacommand{recdef}'s termination prover involves simplification,
|
nipkow@8771
|
43 |
we have turned our lemma into a simplification rule. Therefore our second
|
nipkow@8745
|
44 |
attempt to define our function will automatically take it into account:
|
nipkow@8745
|
45 |
*}
|
nipkow@8745
|
46 |
|
nipkow@8745
|
47 |
consts g :: "nat*nat \\<Rightarrow> nat";
|
nipkow@8745
|
48 |
recdef g "measure(\\<lambda>(x,y). x-y)"
|
nipkow@8745
|
49 |
"g(x,y) = (if x \\<le> y then x else g(x,y+1))";
|
nipkow@8745
|
50 |
|
nipkow@8745
|
51 |
text{*\noindent
|
nipkow@8745
|
52 |
This time everything works fine. Now \isa{g.simps} contains precisely the
|
nipkow@8745
|
53 |
stated recursion equation for \isa{g} and they are simplification
|
nipkow@8745
|
54 |
rules. Thus we can automatically prove
|
nipkow@8745
|
55 |
*}
|
nipkow@8745
|
56 |
|
nipkow@8745
|
57 |
theorem wow: "g(1,0) = g(1,1)";
|
nipkow@9458
|
58 |
by(simp);
|
nipkow@8745
|
59 |
|
nipkow@8745
|
60 |
text{*\noindent
|
nipkow@8745
|
61 |
More exciting theorems require induction, which is discussed below.
|
nipkow@8745
|
62 |
|
nipkow@8745
|
63 |
Because lemma \isa{termi_lem} above was only turned into a
|
nipkow@8745
|
64 |
simplification rule for the sake of the termination proof, we may want to
|
nipkow@8745
|
65 |
disable it again:
|
nipkow@8745
|
66 |
*}
|
nipkow@8745
|
67 |
|
nipkow@8745
|
68 |
lemmas [simp del] = termi_lem;
|
nipkow@8745
|
69 |
|
nipkow@8745
|
70 |
text{*
|
nipkow@8745
|
71 |
The attentive reader may wonder why we chose to call our function \isa{g}
|
nipkow@8745
|
72 |
rather than \isa{f} the second time around. The reason is that, despite
|
nipkow@8745
|
73 |
the failed termination proof, the definition of \isa{f} did not
|
nipkow@8745
|
74 |
fail (and thus we could not define it a second time). However, all theorems
|
nipkow@8745
|
75 |
about \isa{f}, for example \isa{f.simps}, carry as a precondition the
|
nipkow@8745
|
76 |
unproved termination condition. Moreover, the theorems \isa{f.simps} are
|
nipkow@8745
|
77 |
not simplification rules. However, this mechanism allows a delayed proof of
|
nipkow@8745
|
78 |
termination: instead of proving \isa{termi_lem} up front, we could prove
|
nipkow@8745
|
79 |
it later on and then use it to remove the preconditions from the theorems
|
nipkow@8745
|
80 |
about \isa{f}. In most cases this is more cumbersome than proving things
|
nipkow@8745
|
81 |
up front
|
nipkow@8745
|
82 |
%FIXME, with one exception: nested recursion.
|
nipkow@8745
|
83 |
|
nipkow@8745
|
84 |
Although all the above examples employ measure functions, \isacommand{recdef}
|
nipkow@8745
|
85 |
allows arbitrary wellfounded relations. For example, termination of
|
nipkow@8745
|
86 |
Ackermann's function requires the lexicographic product \isa{<*lex*>}:
|
nipkow@8745
|
87 |
*}
|
nipkow@8745
|
88 |
|
nipkow@8745
|
89 |
consts ack :: "nat*nat \\<Rightarrow> nat";
|
nipkow@8745
|
90 |
recdef ack "measure(%m. m) <*lex*> measure(%n. n)"
|
nipkow@8745
|
91 |
"ack(0,n) = Suc n"
|
nipkow@8745
|
92 |
"ack(Suc m,0) = ack(m, 1)"
|
nipkow@8745
|
93 |
"ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
|
nipkow@8745
|
94 |
|
nipkow@8745
|
95 |
text{*\noindent
|
nipkow@8745
|
96 |
For details see the manual~\cite{isabelle-HOL} and the examples in the
|
nipkow@8745
|
97 |
library.
|
nipkow@8745
|
98 |
*}
|
nipkow@8745
|
99 |
|
nipkow@8745
|
100 |
(*<*)
|
nipkow@8745
|
101 |
end
|
nipkow@8745
|
102 |
(*>*)
|