63 \isacommand{recdef}. For example, the greater-than relation can be made |
63 \isacommand{recdef}. For example, the greater-than relation can be made |
64 well-founded by cutting it off at a certain point. Here is an example |
64 well-founded by cutting it off at a certain point. Here is an example |
65 of a recursive function that calls itself with increasing values up to ten:% |
65 of a recursive function that calls itself with increasing values up to ten:% |
66 \end{isamarkuptext}% |
66 \end{isamarkuptext}% |
67 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
67 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
68 \isacommand{recdef}\ \end{isabellebody}% |
68 \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 |
|
69 {\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}% |
|
70 \begin{isamarkuptext}% |
|
71 \noindent |
|
72 Since \isacommand{recdef} is not prepared for the relation supplied above, |
|
73 Isabelle rejects the definition. We should first have proved that |
|
74 our relation was well-founded:% |
|
75 \end{isamarkuptext}% |
|
76 \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}% |
|
77 \begin{isamarkuptxt}% |
|
78 \noindent |
|
79 The proof is by showing that our relation is a subset of another well-founded |
|
80 relation: one given by a measure function.\index{*wf_subset (theorem)}% |
|
81 \end{isamarkuptxt}% |
|
82 \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}% |
|
83 \begin{isamarkuptxt}% |
|
84 \begin{isabelle}% |
|
85 \ {\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}% |
|
86 \end{isabelle} |
|
87 |
|
88 \noindent |
|
89 The inclusion remains to be proved. After unfolding some definitions, |
|
90 we are left with simple arithmetic:% |
|
91 \end{isamarkuptxt}% |
|
92 \isacommand{apply}\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}% |
|
93 \begin{isamarkuptxt}% |
|
94 \begin{isabelle}% |
|
95 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b% |
|
96 \end{isabelle} |
|
97 |
|
98 \noindent |
|
99 And that is dispatched automatically:% |
|
100 \end{isamarkuptxt}% |
|
101 \isacommand{by}\ arith% |
|
102 \begin{isamarkuptext}% |
|
103 \noindent |
|
104 |
|
105 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a |
|
106 crucial hint to our definition:% |
|
107 \end{isamarkuptext}% |
|
108 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% |
|
109 \begin{isamarkuptext}% |
|
110 \noindent |
|
111 Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharhash}{\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the |
|
112 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
|
113 goal in the lemma above would have arisen instead in the \isacommand{recdef} |
|
114 termination proof, where we have less control. A tailor-made termination |
|
115 relation makes even more sense when it can be used in several function |
|
116 declarations.% |
|
117 \end{isamarkuptext}% |
|
118 \end{isabellebody}% |
69 %%% Local Variables: |
119 %%% Local Variables: |
70 %%% mode: latex |
120 %%% mode: latex |
71 %%% TeX-master: "root" |
121 %%% TeX-master: "root" |
72 %%% End: |
122 %%% End: |