equal
deleted
inserted
replaced
18 \begin{isamarkuptext}% |
18 \begin{isamarkuptext}% |
19 \noindent |
19 \noindent |
20 Remember that function \isa{size} is defined for each \isacommand{datatype}. |
20 Remember that function \isa{size} is defined for each \isacommand{datatype}. |
21 However, the definition does not succeed. Isabelle complains about an |
21 However, the definition does not succeed. Isabelle complains about an |
22 unproved termination condition |
22 unproved termination condition |
23 \begin{quote} |
23 % |
24 |
|
25 \begin{isabelle}% |
24 \begin{isabelle}% |
26 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}% |
27 \end{isabelle}% |
26 \end{isabelle}% |
28 |
27 |
29 \end{quote} |
|
30 where \isa{set} returns the set of elements of a list (no special |
28 where \isa{set} returns the set of elements of a list (no special |
31 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 |
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 |
32 (when \isa{term} was defined). First we have to understand why the |
30 (when \isa{term} was defined). First we have to understand why the |
33 recursive call of \isa{trev} underneath \isa{map} leads to the above |
31 recursive call of \isa{trev} underneath \isa{map} leads to the above |
34 condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map} |
32 condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map} |