equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Nested1}% |
3 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}% |
4 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}% |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 \noindent |
6 \noindent |
6 Although the definition of \isa{trev} is quite natural, we will have |
7 Although the definition of \isa{trev} is quite natural, we will have |
7 overcome a minor difficulty in convincing Isabelle of is termination. |
8 overcome a minor difficulty in convincing Isabelle of is termination. |
18 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
19 \noindent |
20 \noindent |
20 Remember that function \isa{size} is defined for each \isacommand{datatype}. |
21 Remember that function \isa{size} is defined for each \isacommand{datatype}. |
21 However, the definition does not succeed. Isabelle complains about an |
22 However, the definition does not succeed. Isabelle complains about an |
22 unproved termination condition |
23 unproved termination condition |
23 % |
|
24 \begin{isabelle}% |
24 \begin{isabelle}% |
25 \ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}% |
25 \ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}% |
26 \end{isabelle}% |
26 \end{isabelle} |
27 |
|
28 where \isa{set} returns the set of elements of a list (no special |
27 where \isa{set} returns the set of elements of a list (no special |
29 knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle |
28 knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle |
30 (when \isa{term} was defined). First we have to understand why the |
29 (when \isa{term} was defined). First we have to understand why the |
31 recursive call of \isa{trev} underneath \isa{map} leads to the above |
30 recursive call of \isa{trev} underneath \isa{map} leads to the above |
32 condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map} |
31 condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map} |