8745

1 
(*<*)


2 
theory ABexpr = Main:;


3 
(*>*)


4 


5 
text{*

11458

6 
\index{datatypes!mutually recursive}%

8745

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


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


9 
language of arithmetic and boolean expressions where


10 
\begin{itemize}


11 
\item arithmetic expressions contain boolean expressions because there are

11458

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

8745

13 
and


14 
\item boolean expressions contain arithmetic expressions because of


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


16 
\end{itemize}


17 
In Isabelle this becomes


18 
*}


19 


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


21 
 Sum "'a aexp" "'a aexp"


22 
 Diff "'a aexp" "'a aexp"


23 
 Var 'a


24 
 Num nat


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


26 
 And "'a bexp" "'a bexp"


27 
 Neg "'a bexp";


28 


29 
text{*\noindent

9792

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

11309

31 
except that we have added an @{text IF} constructor,


32 
fixed the values to be of type @{typ"nat"} and declared the two binary


33 
operations @{text Sum} and @{term"Diff"}. Boolean

8745

34 
expressions can be arithmetic comparisons, conjunctions and negations.

11458

35 
The semantics is given by two evaluation functions:

8745

36 
*}


37 

10971

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


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

8745

40 


41 
text{*\noindent

11458

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

9792

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

8745

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


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


46 
section:


47 
*}


48 


49 
primrec

8771

50 
"evala (IF b a1 a2) env =


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


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


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


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


55 
"evala (Num n) env = n"

8745

56 

8771

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

10971

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


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

8745

60 


61 
text{*\noindent


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


63 
*}


64 

10971

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


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

8745

67 


68 
text{*\noindent


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


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

9792

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


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

8745

73 
*}


74 


75 
primrec


76 
"substa s (IF b a1 a2) =


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


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


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


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


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


82 


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


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


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


86 


87 
text{*


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


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


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


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


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


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


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


95 
theorems simultaneously:


96 
*}


97 

10971

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


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

8745

100 
apply(induct_tac a and b);


101 


102 
txt{*\noindent


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


104 
*}


105 

10171

106 
apply simp_all;


107 
(*<*)done(*>*)

8745

108 


109 
text{*


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


111 
an inductive proof expects a goal of the form


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


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

9792

114 
\begin{isabelle}

10971

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

9792

116 
\end{isabelle}

8745

117 


118 
\begin{exercise}

9792

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


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

11458

121 
@{term"IF"}s; it should eliminate the constructors


122 
@{term"And"} and @{term"Neg"}, leaving only @{term"Less"}.


123 
Prove that @{text"norma"}

9792

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


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

12334

126 
it. ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion


127 
of type annotations following lemma @{text subst_id} below).

8745

128 
\end{exercise}


129 
*}

12334

130 
(*<*)


131 
consts norma :: "'a aexp \<Rightarrow> 'a aexp"


132 
normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp"


133 


134 
primrec


135 
"norma (IF b t e) = (normb b (norma t) (norma e))"


136 
"norma (Sum a1 a2) = Sum (norma a1) (norma a2)"


137 
"norma (Diff a1 a2) = Diff (norma a1) (norma a2)"


138 
"norma (Var v) = Var v"


139 
"norma (Num n) = Num n"


140 


141 
"normb (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e"


142 
"normb (And b1 b2) t e = normb b1 (normb b2 t e) e"


143 
"normb (Neg b) t e = normb b e t"


144 


145 
lemma " evala (norma a) env = evala a env


146 
\<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)"


147 
apply (induct_tac a and b)


148 
apply (simp_all)


149 
done


150 


151 
consts normala :: "'a aexp \<Rightarrow> bool"


152 
normalb :: "'b bexp \<Rightarrow> bool"


153 


154 
primrec


155 
"normala (IF b t e) = (normalb b \<and> normala t \<and> normala e)"


156 
"normala (Sum a1 a2) = (normala a1 \<and> normala a2)"


157 
"normala (Diff a1 a2) = (normala a1 \<and> normala a2)"


158 
"normala (Var v) = True"


159 
"normala (Num n) = True"


160 


161 
"normalb (Less a1 a2) = (normala a1 \<and> normala a2)"


162 
"normalb (And b1 b2) = False"


163 
"normalb (Neg b) = False"


164 


165 
lemma "normala (norma (a::'a aexp)) \<and>


166 
(\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))"


167 
apply (induct_tac a and b)


168 
apply (auto)


169 
done


170 

8745

171 
end


172 
(*>*)
