|
9722
|
1 |
%
|
|
|
2 |
\begin{isabellebody}%
|
|
9924
|
3 |
\def\isabellecontext{termination}%
|
|
8749
|
4 |
%
|
|
|
5 |
\begin{isamarkuptext}%
|
|
11309
|
6 |
When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove
|
|
|
7 |
its termination with the help of the user-supplied measure. Each of the examples
|
|
|
8 |
above is simple enough that Isabelle can automatically prove that the
|
|
|
9 |
argument's measure decreases in each recursive call. As a result,
|
|
9792
|
10 |
$f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived
|
|
|
11 |
from them) as theorems. For example, look (via \isacommand{thm}) at
|
|
10187
|
12 |
\isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define
|
|
9792
|
13 |
the same function. What is more, those equations are automatically declared as
|
|
8749
|
14 |
simplification rules.
|
|
|
15 |
|
|
11458
|
16 |
Isabelle may fail to prove the termination condition for some
|
|
|
17 |
recursive call. Let us try the following artificial function:%
|
|
8749
|
18 |
\end{isamarkuptext}%
|
|
9933
|
19 |
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
|
|
11627
|
20 |
\isacommand{recdef}\ \end{isabellebody}%
|
|
9145
|
21 |
%%% Local Variables:
|
|
|
22 |
%%% mode: latex
|
|
|
23 |
%%% TeX-master: "root"
|
|
|
24 |
%%% End:
|