equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}% |
3 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}% |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 \noindent |
5 \noindent |
5 Although the definition of \isa{trev} is quite natural, we will have |
6 Although the definition of \isa{trev} is quite natural, we will have |
6 overcome a minor difficulty in convincing Isabelle of is termination. |
7 overcome a minor difficulty in convincing Isabelle of is termination. |
36 the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any recursive call of \isa{trev} is strictly |
37 the size of the argument \isa{\mbox{t}\ {\isasymin}\ set\ \mbox{ts}} of any recursive call of \isa{trev} is strictly |
37 less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}. |
38 less than \isa{size\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}. |
38 We will now prove the termination condition and continue with our definition. |
39 We will now prove the termination condition and continue with our definition. |
39 Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.% |
40 Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.% |
40 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
41 \end{isabelle}% |
42 \end{isabellebody}% |
42 %%% Local Variables: |
43 %%% Local Variables: |
43 %%% mode: latex |
44 %%% mode: latex |
44 %%% TeX-master: "root" |
45 %%% TeX-master: "root" |
45 %%% End: |
46 %%% End: |