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

9792

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


30 
except that we have fixed the values to be of type @{typ"nat"} and that we

10971

31 
have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean

8745

32 
expressions can be arithmetic comparisons, conjunctions and negations.


33 
The semantics is fixed via two evaluation functions


34 
*}


35 

10971

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


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

8745

38 


39 
text{*\noindent

9792

40 
that take an expression and an environment (a mapping from variables @{typ"'a"} to values


41 
@{typ"nat"}) and return its arithmetic/boolean

8745

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

8771

48 
"evala (IF b a1 a2) env =


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


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


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


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


53 
"evala (Num n) env = n"

8745

54 

8771

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

10971

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


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

8745

58 


59 
text{*\noindent


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


61 
*}


62 

10971

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";

8745

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

9792

69 
result, the type of variables in the expression may change from @{typ"'a"}


70 
to @{typ"'b"}. Note that there are only arithmetic and no boolean variables.

8745

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 

10971

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


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

8745

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 

10171

104 
apply simp_all;


105 
(*<*)done(*>*)

8745

106 


107 
text{*


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


109 
an inductive proof expects a goal of the form


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


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

9792

112 
\begin{isabelle}

10971

113 
\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}

9792

114 
\end{isabelle}

8745

115 


116 
\begin{exercise}

9792

117 
Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that


118 
replaces @{term"IF"}s with complex boolean conditions by nested


119 
@{term"IF"}s where each condition is a @{term"Less"}  @{term"And"} and


120 
@{term"Neg"} should be eliminated completely. Prove that @{text"norma"}


121 
preserves the value of an expression and that the result of @{text"norma"}


122 
is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in

8745

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


124 
\end{exercise}


125 
*}


126 
(*<*)


127 
end


128 
(*>*)
