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}\ 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 |
68 \isacommand{recdef}\ f\ {\isachardoublequote}{\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}{\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}% |
69 {\isachardoublequote}f\ i\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{1}}{\isadigit{0}}\ {\isasymle}\ i\ then\ {\isadigit{0}}\ else\ i\ {\isacharasterisk}\ f{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
70 \begin{isamarkuptext}% |
70 \begin{isamarkuptext}% |
71 \noindent |
71 \noindent |
72 Since \isacommand{recdef} is not prepared for the relation supplied above, |
72 Since \isacommand{recdef} is not prepared for the relation supplied above, |
73 Isabelle rejects the definition. We should first have proved that |
73 Isabelle rejects the definition. We should first have proved that |
74 our relation was well-founded:% |
74 our relation was well-founded:% |
106 crucial hint to our definition:% |
106 crucial hint to our definition:% |
107 \end{isamarkuptext}% |
107 \end{isamarkuptext}% |
108 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% |
108 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% |
109 \begin{isamarkuptext}% |
109 \begin{isamarkuptext}% |
110 \noindent |
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 |
111 Alternatively, we could have given \isa{measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isadigit{1}}{\isadigit{0}}{\isacharminus}k{\isacharparenright}} for the |
112 well-founded relation in our \isacommand{recdef}. However, the arithmetic |
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} |
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 |
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 |
115 relation makes even more sense when it can be used in several function |
116 declarations.% |
116 declarations.% |