8749
|
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
|
8771
|
7 |
measure of the argument goes down in each recursive call. As a result,
|
|
8 |
\isa{$f$.simps} will contain the defining equations (or variants derived from
|
8749
|
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}%
|
9674
|
18 |
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
|
|
19 |
\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
|
|
20 |
\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
|
8749
|
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}%
|
9674
|
28 |
\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
|
8749
|
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}%
|
9674
|
34 |
\isacommand{by}{\isacharparenleft}arith{\isacharparenright}%
|
8749
|
35 |
\begin{isamarkuptext}%
|
|
36 |
\noindent
|
8771
|
37 |
Because \isacommand{recdef}'s termination prover involves simplification,
|
|
38 |
we have turned our lemma into a simplification rule. Therefore our second
|
8749
|
39 |
attempt to define our function will automatically take it into account:%
|
|
40 |
\end{isamarkuptext}%
|
9674
|
41 |
\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
|
|
42 |
\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
|
|
43 |
\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
|
8749
|
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}%
|
9674
|
50 |
\isacommand{theorem}\ wow{\isacharcolon}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
|
|
51 |
\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
|
8749
|
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}%
|
9674
|
60 |
\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ termi{\isacharunderscore}lem%
|
8749
|
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}%
|
9674
|
79 |
\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
|
|
80 |
\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isacharpercent}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
|
|
81 |
\ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
|
|
82 |
\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
|
|
83 |
\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
|
8749
|
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}%
|
9145
|
90 |
%%% Local Variables:
|
|
91 |
%%% mode: latex
|
|
92 |
%%% TeX-master: "root"
|
|
93 |
%%% End:
|