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