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