56 solely of these building blocks. But of course the proof of |
56 solely of these building blocks. But of course the proof of |
57 termination of your function definition, i.e.\ that the arguments |
57 termination of your function definition, i.e.\ that the arguments |
58 decrease with every recursive call, may still require you to provide |
58 decrease with every recursive call, may still require you to provide |
59 additional lemmas. |
59 additional lemmas. |
60 |
60 |
61 It is also possible to use your own well-founded relations with \isacommand{recdef}. |
61 It is also possible to use your own well-founded relations with |
62 Here is a simplistic example:% |
62 \isacommand{recdef}. For example, the greater-than relation can be made |
|
63 well-founded by cutting it off at a certain point. Here is an example |
|
64 of a recursive function that calls itself with increasing values up to ten:% |
63 \end{isamarkuptext}% |
65 \end{isamarkuptext}% |
64 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
66 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
65 \isacommand{recdef}\ f\ {\isachardoublequote}id{\isacharparenleft}less{\isacharunderscore}than{\isacharparenright}{\isachardoublequote}\isanewline |
67 \isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}\isanewline |
66 {\isachardoublequote}f\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
68 {\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isacharhash}{\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
67 {\isachardoublequote}f\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ f\ n{\isachardoublequote}% |
|
68 \begin{isamarkuptext}% |
69 \begin{isamarkuptext}% |
69 \noindent |
70 \noindent |
70 Since \isacommand{recdef} is not prepared for \isa{id}, the identity |
71 Since \isacommand{recdef} is not prepared for the relation supplied above, |
71 function, this leads to the complaint that it could not prove |
72 Isabelle rejects the definition. We should first have proved that |
72 \isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}. |
73 our relation was well-founded:% |
73 We should first have proved that \isa{id} preserves well-foundedness% |
|
74 \end{isamarkuptext}% |
74 \end{isamarkuptext}% |
75 \isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline |
75 \isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}% |
76 \isacommand{by}\ simp% |
76 \begin{isamarkuptxt}% |
|
77 The proof is by showing that our relation is a subset of another well-founded |
|
78 relation: one given by a measure function.% |
|
79 \end{isamarkuptxt}% |
|
80 \isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}% |
|
81 \begin{isamarkuptxt}% |
|
82 \begin{isabelle}% |
|
83 \ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}% |
|
84 \end{isabelle} |
|
85 |
|
86 \noindent |
|
87 The inclusion remains to be proved. After unfolding some definitions, |
|
88 we are left with simple arithmetic:% |
|
89 \end{isamarkuptxt}% |
|
90 \isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}% |
|
91 \begin{isamarkuptxt}% |
|
92 \begin{isabelle}% |
|
93 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}y\ {\isacharless}\ x{\isacharsemicolon}\ x\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ x\ {\isacharless}\ N\ {\isacharminus}\ y% |
|
94 \end{isabelle} |
|
95 |
|
96 \noindent |
|
97 And that is dispatched automatically:% |
|
98 \end{isamarkuptxt}% |
|
99 \isacommand{by}\ arith% |
77 \begin{isamarkuptext}% |
100 \begin{isamarkuptext}% |
78 \noindent |
101 \noindent |
79 and should have appended the following hint to our definition above: |
102 |
|
103 Armed with this lemma, we can append a crucial hint to our definition: |
80 \indexbold{*recdef_wf}% |
104 \indexbold{*recdef_wf}% |
81 \end{isamarkuptext}% |
105 \end{isamarkuptext}% |
82 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}% |
106 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% |
|
107 \begin{isamarkuptext}% |
|
108 \noindent |
|
109 Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the |
|
110 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
|
111 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
|
112 termination proof, where we have less control. A tailor-made termination |
|
113 relation makes even more sense when it can be used in several function |
|
114 declarations.% |
|
115 \end{isamarkuptext}% |
|
116 \end{isabellebody}% |
83 %%% Local Variables: |
117 %%% Local Variables: |
84 %%% mode: latex |
118 %%% mode: latex |
85 %%% TeX-master: "root" |
119 %%% TeX-master: "root" |
86 %%% End: |
120 %%% End: |