--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,114 @@
+\begin{isabelle}%
+%
+\begin{isamarkuptext}%
+Sometimes it is necessary to define two datatypes that depend on each
+other. This is called \textbf{mutual recursion}. As an example consider a
+language of arithmetic and boolean expressions where
+\begin{itemize}
+\item arithmetic expressions contain boolean expressions because there are
+ conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
+ and
+\item boolean expressions contain arithmetic expressions because of
+ comparisons like ``$m<n$''.
+\end{itemize}
+In Isabelle this becomes%
+\end{isamarkuptext}%
+\isacommand{datatype}~'a~aexp~=~IF~~~{"}'a~bexp{"}~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
+~~~~~~~~~~~~~~~~~|~Sum~~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
+~~~~~~~~~~~~~~~~~|~Diff~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
+~~~~~~~~~~~~~~~~~|~Var~'a\isanewline
+~~~~~~~~~~~~~~~~~|~Num~nat\isanewline
+\isakeyword{and}~~~~~~'a~bexp~=~Less~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline
+~~~~~~~~~~~~~~~~~|~And~~{"}'a~bexp{"}~{"}'a~bexp{"}\isanewline
+~~~~~~~~~~~~~~~~~|~Neg~~{"}'a~bexp{"}%
+\begin{isamarkuptext}%
+\noindent
+Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
+except that we have fixed the values to be of type \isa{nat} and that we
+have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
+expressions can be arithmetic comparisons, conjunctions and negations.
+The semantics is fixed via two evaluation functions%
+\end{isamarkuptext}%
+\isacommand{consts}~~evala~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~nat{"}\isanewline
+~~~~~~~~evalb~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~bexp~{\isasymRightarrow}~bool{"}%
+\begin{isamarkuptext}%
+\noindent
+that take an environment (a mapping from variables \isa{'a} to values
+\isa{nat}) and an expression and return its arithmetic/boolean
+value. Since the datatypes are mutually recursive, so are functions that
+operate on them. Hence they need to be defined in a single \isacommand{primrec}
+section:%
+\end{isamarkuptext}%
+\isacommand{primrec}\isanewline
+~~{"}evala~env~(IF~b~a1~a2)~=\isanewline
+~~~~~(if~evalb~env~b~then~evala~env~a1~else~evala~env~a2){"}\isanewline
+~~{"}evala~env~(Sum~a1~a2)~=~evala~env~a1~+~evala~env~a2{"}\isanewline
+~~{"}evala~env~(Diff~a1~a2)~=~evala~env~a1~-~evala~env~a2{"}\isanewline
+~~{"}evala~env~(Var~v)~=~env~v{"}\isanewline
+~~{"}evala~env~(Num~n)~=~n{"}\isanewline
+\isanewline
+~~{"}evalb~env~(Less~a1~a2)~=~(evala~env~a1~<~evala~env~a2){"}\isanewline
+~~{"}evalb~env~(And~b1~b2)~=~(evalb~env~b1~{\isasymand}~evalb~env~b2){"}\isanewline
+~~{"}evalb~env~(Neg~b)~=~({\isasymnot}~evalb~env~b){"}%
+\begin{isamarkuptext}%
+\noindent
+In the same fashion we also define two functions that perform substitution:%
+\end{isamarkuptext}%
+\isacommand{consts}~substa~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~'b~aexp{"}\isanewline
+~~~~~~~substb~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~bexp~{\isasymRightarrow}~'b~bexp{"}%
+\begin{isamarkuptext}%
+\noindent
+The first argument is a function mapping variables to expressions, the
+substitution. It is applied to all variables in the second argument. As a
+result, the type of variables in the expression may change from \isa{'a}
+to \isa{'b}. Note that there are only arithmetic and no boolean variables.%
+\end{isamarkuptext}%
+\isacommand{primrec}\isanewline
+~~{"}substa~s~(IF~b~a1~a2)~=\isanewline
+~~~~~IF~(substb~s~b)~(substa~s~a1)~(substa~s~a2){"}\isanewline
+~~{"}substa~s~(Sum~a1~a2)~=~Sum~(substa~s~a1)~(substa~s~a2){"}\isanewline
+~~{"}substa~s~(Diff~a1~a2)~=~Diff~(substa~s~a1)~(substa~s~a2){"}\isanewline
+~~{"}substa~s~(Var~v)~=~s~v{"}\isanewline
+~~{"}substa~s~(Num~n)~=~Num~n{"}\isanewline
+\isanewline
+~~{"}substb~s~(Less~a1~a2)~=~Less~(substa~s~a1)~(substa~s~a2){"}\isanewline
+~~{"}substb~s~(And~b1~b2)~=~And~(substb~s~b1)~(substb~s~b2){"}\isanewline
+~~{"}substb~s~(Neg~b)~=~Neg~(substb~s~b){"}%
+\begin{isamarkuptext}%
+Now we can prove a fundamental theorem about the interaction between
+evaluation and substitution: applying a substitution $s$ to an expression $a$
+and evaluating the result in an environment $env$ yields the same result as
+evaluation $a$ in the environment that maps every variable $x$ to the value
+of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
+boolean expressions (by induction), you find that you always need the other
+theorem in the induction step. Therefore you need to state and prove both
+theorems simultaneously:%
+\end{isamarkuptext}%
+\isacommand{lemma}~{"}evala~env~(substa~s~a)~=~evala~({\isasymlambda}x.~evala~env~(s~x))~a~{\isasymand}\isanewline
+~~~~~~~~evalb~env~(substb~s~b)~=~evalb~({\isasymlambda}x.~evala~env~(s~x))~b{"}\isanewline
+\isacommand{apply}(induct\_tac~a~\isakeyword{and}~b)%
+\begin{isamarkuptxt}%
+\noindent
+The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
+\end{isamarkuptxt}%
+\isacommand{apply}~auto\isacommand{.}%
+\begin{isamarkuptext}%
+In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
+an inductive proof expects a goal of the form
+\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
+where each variable $x@i$ is of type $\tau@i$. Induction is started by
+\begin{ttbox}
+apply(induct_tac \(x@1\) \texttt{and} \(\dots\) \texttt{and} \(x@n\));
+\end{ttbox}
+
+\begin{exercise}
+ Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that
+ replaces \isa{IF}s with complex boolean conditions by nested
+ \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
+ \isa{Neg} should be eliminated completely. Prove that \isa{norma}
+ preserves the value of an expression and that the result of \isa{norma}
+ is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
+ it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
+\end{exercise}%
+\end{isamarkuptext}%
+\end{isabelle}%