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