15 |
15 |
16 Isabelle may fail to prove the termination condition for some |
16 Isabelle may fail to prove the termination condition for some |
17 recursive call. Let us try the following artificial function:% |
17 recursive call. Let us try the following artificial function:% |
18 \end{isamarkuptext}% |
18 \end{isamarkuptext}% |
19 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
19 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
20 \isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline |
20 \isacommand{recdef}\ \end{isabellebody}% |
21 \ \ {\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}% |
|
22 \begin{isamarkuptext}% |
|
23 \noindent |
|
24 Isabelle prints a |
|
25 \REMARK{error or warning? change this part? rename g to f?} |
|
26 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 awkward behaviour of subtraction |
|
34 on type \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 in our second attempt a hint: the \attrdx{recdef_simp} attribute |
|
42 says to use \isa{termi{\isacharunderscore}lem} as |
|
43 a simplification rule.% |
|
44 \end{isamarkuptext}% |
|
45 \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
|
46 \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline |
|
47 \ \ {\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 |
|
48 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}% |
|
49 \begin{isamarkuptext}% |
|
50 \noindent |
|
51 This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely |
|
52 the stated recursion equation for \isa{g}, which has been stored as a |
|
53 simplification rule. Thus we can automatically prove results such as this one:% |
|
54 \end{isamarkuptext}% |
|
55 \isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
|
56 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
57 \isacommand{done}% |
|
58 \begin{isamarkuptext}% |
|
59 \noindent |
|
60 More exciting theorems require induction, which is discussed below. |
|
61 |
|
62 If the termination proof requires a new lemma that is of general use, you can |
|
63 turn it permanently into a simplification rule, in which case the above |
|
64 \isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not |
|
65 sufficiently general to warrant this distinction. |
|
66 |
|
67 The attentive reader may wonder why we chose to call our function \isa{g} |
|
68 rather than \isa{f} the second time around. The reason is that, despite |
|
69 the failed termination proof, the definition of \isa{f} did not |
|
70 fail, and thus we could not define it a second time. However, all theorems |
|
71 about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition |
|
72 the unproved termination condition. Moreover, the theorems |
|
73 \isa{f{\isachardot}simps} are not stored as simplification rules. |
|
74 However, this mechanism |
|
75 allows a delayed proof of termination: instead of proving |
|
76 \isa{termi{\isacharunderscore}lem} up front, we could prove |
|
77 it later on and then use it to remove the preconditions from the theorems |
|
78 about \isa{f}. In most cases this is more cumbersome than proving things |
|
79 up front. |
|
80 \REMARK{FIXME, with one exception: nested recursion.}% |
|
81 \end{isamarkuptext}% |
|
82 \end{isabellebody}% |
|
83 %%% Local Variables: |
21 %%% Local Variables: |
84 %%% mode: latex |
22 %%% mode: latex |
85 %%% TeX-master: "root" |
23 %%% TeX-master: "root" |
86 %%% End: |
24 %%% End: |