doc-src/TutorialI/Recdef/document/termination.tex
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10522 ed3964d1f1a4
child 10795 9e888d60d3e5
permissions -rw-r--r--
*** empty log message ***
nipkow@9722
     1
%
nipkow@9722
     2
\begin{isabellebody}%
wenzelm@9924
     3
\def\isabellecontext{termination}%
nipkow@8749
     4
%
nipkow@8749
     5
\begin{isamarkuptext}%
nipkow@8749
     6
When a function is defined via \isacommand{recdef}, Isabelle tries to prove
nipkow@8749
     7
its termination with the help of the user-supplied measure.  All of the above
nipkow@8749
     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@9792
    10
$f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived
nipkow@9792
    11
from them) as theorems. For example, look (via \isacommand{thm}) at
nipkow@10187
    12
\isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define
nipkow@9792
    13
the same function. What is more, those equations are automatically declared as
nipkow@8749
    14
simplification rules.
nipkow@8749
    15
nipkow@10522
    16
In general, Isabelle may not be able to prove all termination conditions
nipkow@8749
    17
(there is one for each recursive call) automatically. For example,
nipkow@8749
    18
termination of the following artificial function%
nipkow@8749
    19
\end{isamarkuptext}%
nipkow@9933
    20
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
wenzelm@9674
    21
\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10187
    22
\ \ {\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}%
nipkow@8749
    23
\begin{isamarkuptext}%
nipkow@8749
    24
\noindent
nipkow@8749
    25
is not proved automatically (although maybe it should be). Isabelle prints a
nipkow@8749
    26
kind of error message showing you what it was unable to prove. You will then
nipkow@8749
    27
have to prove it as a separate lemma before you attempt the definition
nipkow@8749
    28
of your function once more. In our case the required lemma is the obvious one:%
nipkow@8749
    29
\end{isamarkuptext}%
nipkow@9933
    30
\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
nipkow@8749
    31
\begin{isamarkuptxt}%
nipkow@8749
    32
\noindent
nipkow@9792
    33
It was not proved automatically because of the special nature of \isa{{\isacharminus}}
nipkow@8749
    34
on \isa{nat}. This requires more arithmetic than is tried by default:%
nipkow@8749
    35
\end{isamarkuptxt}%
nipkow@10171
    36
\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
nipkow@10171
    37
\isacommand{done}%
nipkow@8749
    38
\begin{isamarkuptext}%
nipkow@8749
    39
\noindent
nipkow@8771
    40
Because \isacommand{recdef}'s termination prover involves simplification,
nipkow@9933
    41
we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as
nipkow@10654
    42
a simplification rule:\indexbold{*recdef_simp}%
nipkow@8749
    43
\end{isamarkuptext}%
nipkow@9933
    44
\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
wenzelm@9674
    45
\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10187
    46
\ \ {\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}\isanewline
nipkow@9992
    47
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}%
nipkow@8749
    48
\begin{isamarkuptext}%
nipkow@8749
    49
\noindent
nipkow@9792
    50
This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
nipkow@9792
    51
the stated recursion equation for \isa{g} and they are simplification
nipkow@8749
    52
rules. Thus we can automatically prove%
nipkow@8749
    53
\end{isamarkuptext}%
nipkow@10187
    54
\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10171
    55
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
nipkow@10171
    56
\isacommand{done}%
nipkow@8749
    57
\begin{isamarkuptext}%
nipkow@8749
    58
\noindent
nipkow@8749
    59
More exciting theorems require induction, which is discussed below.
nipkow@8749
    60
nipkow@9933
    61
If the termination proof requires a new lemma that is of general use, you can
nipkow@9933
    62
turn it permanently into a simplification rule, in which case the above
nipkow@9933
    63
\isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
nipkow@9933
    64
sufficiently general to warrant this distinction.
nipkow@9933
    65
nipkow@8749
    66
The attentive reader may wonder why we chose to call our function \isa{g}
nipkow@8749
    67
rather than \isa{f} the second time around. The reason is that, despite
nipkow@8749
    68
the failed termination proof, the definition of \isa{f} did not
nipkow@9792
    69
fail, and thus we could not define it a second time. However, all theorems
nipkow@9792
    70
about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition
nipkow@9792
    71
the unproved termination condition. Moreover, the theorems
nipkow@9792
    72
\isa{f{\isachardot}simps} are not simplification rules. However, this mechanism
nipkow@9792
    73
allows a delayed proof of termination: instead of proving
nipkow@9792
    74
\isa{termi{\isacharunderscore}lem} up front, we could prove 
nipkow@8749
    75
it later on and then use it to remove the preconditions from the theorems
nipkow@8749
    76
about \isa{f}. In most cases this is more cumbersome than proving things
nipkow@9792
    77
up front.
nipkow@10186
    78
%FIXME, with one exception: nested recursion.%
nipkow@8749
    79
\end{isamarkuptext}%
nipkow@9722
    80
\end{isabellebody}%
wenzelm@9145
    81
%%% Local Variables:
wenzelm@9145
    82
%%% mode: latex
wenzelm@9145
    83
%%% TeX-master: "root"
wenzelm@9145
    84
%%% End: