lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
%
\begin{isabellebody}%
\def\isabellecontext{Nested{\isadigit{1}}}%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
Although the definition of \isa{trev} below is quite natural, we will have
to overcome a minor difficulty in convincing Isabelle of its termination.
It is precisely this difficulty that is the \textit{raison d'\^etre} of
this subsection.
Defining \isa{trev} by \isacommand{recdef} rather than \isacommand{primrec}
simplifies matters because we are now free to use the recursion equation
suggested at the end of \S\ref{sec:nested-datatype}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{recdef}\ trev\ {\isachardoublequote}measure\ size{\isachardoublequote}\isanewline
\ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
\ {\isachardoublequote}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
Remember that function \isa{size} is defined for each \isacommand{datatype}.
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
\begin{isabelle}%
\ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
\end{isabelle}
where \isa{set} returns the set of elements of a list
and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary
function automatically defined by Isabelle
(while processing the declaration of \isa{term}). Why does the
recursive call of \isa{trev} lead to this
condition? Because \isacommand{recdef} knows that \isa{map}
will apply \isa{trev} only to elements of \isa{ts}. Thus the
condition expresses that the size of the argument \isa{t\ {\isasymin}\ set\ ts} of any
recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ f\ ts{\isacharparenright}},
which equals \isa{Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
\isacommand{recdef} knows about \isa{map}.
The termination condition is easily proved by induction:%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: