8745

1 
(*<*)


2 
theory ABexpr = Main:;


3 
(*>*)


4 


5 
text{*


6 
Sometimes it is necessary to define two datatypes that depend on each


7 
other. This is called \textbf{mutual recursion}. As an example consider a


8 
language of arithmetic and boolean expressions where


9 
\begin{itemize}


10 
\item arithmetic expressions contain boolean expressions because there are


11 
conditional arithmetic expressions like ``if $m<n$ then $nm$ else $mn$'',


12 
and


13 
\item boolean expressions contain arithmetic expressions because of


14 
comparisons like ``$m<n$''.


15 
\end{itemize}


16 
In Isabelle this becomes


17 
*}


18 


19 
datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp"


20 
 Sum "'a aexp" "'a aexp"


21 
 Diff "'a aexp" "'a aexp"


22 
 Var 'a


23 
 Num nat


24 
and 'a bexp = Less "'a aexp" "'a aexp"


25 
 And "'a bexp" "'a bexp"


26 
 Neg "'a bexp";


27 


28 
text{*\noindent


29 
Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},


30 
except that we have fixed the values to be of type \isa{nat} and that we


31 
have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean


32 
expressions can be arithmetic comparisons, conjunctions and negations.


33 
The semantics is fixed via two evaluation functions


34 
*}


35 


36 
consts evala :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a aexp \\<Rightarrow> nat"


37 
evalb :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a bexp \\<Rightarrow> bool";


38 


39 
text{*\noindent


40 
that take an environment (a mapping from variables \isa{'a} to values


41 
\isa{nat}) and an expression and return its arithmetic/boolean


42 
value. Since the datatypes are mutually recursive, so are functions that


43 
operate on them. Hence they need to be defined in a single \isacommand{primrec}


44 
section:


45 
*}


46 


47 
primrec


48 
"evala env (IF b a1 a2) =


49 
(if evalb env b then evala env a1 else evala env a2)"


50 
"evala env (Sum a1 a2) = evala env a1 + evala env a2"


51 
"evala env (Diff a1 a2) = evala env a1  evala env a2"


52 
"evala env (Var v) = env v"


53 
"evala env (Num n) = n"


54 


55 
"evalb env (Less a1 a2) = (evala env a1 < evala env a2)"


56 
"evalb env (And b1 b2) = (evalb env b1 \\<and> evalb env b2)"


57 
"evalb env (Neg b) = (\\<not> evalb env b)"


58 


59 
text{*\noindent


60 
In the same fashion we also define two functions that perform substitution:


61 
*}


62 


63 
consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp"


64 
substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp";


65 


66 
text{*\noindent


67 
The first argument is a function mapping variables to expressions, the


68 
substitution. It is applied to all variables in the second argument. As a


69 
result, the type of variables in the expression may change from \isa{'a}


70 
to \isa{'b}. Note that there are only arithmetic and no boolean variables.


71 
*}


72 


73 
primrec


74 
"substa s (IF b a1 a2) =


75 
IF (substb s b) (substa s a1) (substa s a2)"


76 
"substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"


77 
"substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)"


78 
"substa s (Var v) = s v"


79 
"substa s (Num n) = Num n"


80 


81 
"substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"


82 
"substb s (And b1 b2) = And (substb s b1) (substb s b2)"


83 
"substb s (Neg b) = Neg (substb s b)";


84 


85 
text{*


86 
Now we can prove a fundamental theorem about the interaction between


87 
evaluation and substitution: applying a substitution $s$ to an expression $a$


88 
and evaluating the result in an environment $env$ yields the same result as


89 
evaluation $a$ in the environment that maps every variable $x$ to the value


90 
of $s(x)$ under $env$. If you try to prove this separately for arithmetic or


91 
boolean expressions (by induction), you find that you always need the other


92 
theorem in the induction step. Therefore you need to state and prove both


93 
theorems simultaneously:


94 
*}


95 


96 
lemma "evala env (substa s a) = evala (\\<lambda>x. evala env (s x)) a \\<and>


97 
evalb env (substb s b) = evalb (\\<lambda>x. evala env (s x)) b";


98 
apply(induct_tac a and b);


99 


100 
txt{*\noindent


101 
The resulting 8 goals (one for each constructor) are proved in one fell swoop:


102 
*}


103 


104 
apply auto.;


105 


106 
text{*


107 
In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,


108 
an inductive proof expects a goal of the form


109 
\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]


110 
where each variable $x@i$ is of type $\tau@i$. Induction is started by


111 
\begin{ttbox}


112 
apply(induct_tac \(x@1\) \texttt{and} \(\dots\) \texttt{and} \(x@n\));


113 
\end{ttbox}


114 


115 
\begin{exercise}


116 
Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that


117 
replaces \isa{IF}s with complex boolean conditions by nested


118 
\isa{IF}s where each condition is a \isa{Less}  \isa{And} and


119 
\isa{Neg} should be eliminated completely. Prove that \isa{norma}


120 
preserves the value of an expression and that the result of \isa{norma}


121 
is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in


122 
it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).


123 
\end{exercise}


124 
*}


125 
(*<*)


126 
end


127 
(*>*)
