8745

1 
(*<*)

16417

2 
theory ABexpr imports Main begin;

8745

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 

27015

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


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


40 
"evala (IF b a1 a2) env =


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


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


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


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


45 
"evala (Num n) env = n" 


46 


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


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


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

8745

50 


51 
text{*\noindent


52 

27015

53 
Both take an expression and an environment (a mapping from variables


54 
@{typ"'a"} to values @{typ"nat"}) and return its arithmetic/boolean


55 
value. Since the datatypes are mutually recursive, so are functions


56 
that operate on them. Hence they need to be defined in a single


57 
\isacommand{primrec} section. Notice the \isakeyword{and} separating


58 
the declarations of @{const evala} and @{const evalb}. Their defining


59 
equations need not be split into two groups;


60 
the empty line is purely for readability.

8745

61 


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


63 
*}


64 

27015

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


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


67 
"substa s (IF b a1 a2) =


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


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


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


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


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


73 


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


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


76 
"substb s (Neg b) = Neg (substb s b)"

8745

77 


78 
text{*\noindent

27015

79 
Their first argument is a function mapping variables to expressions, the

8745

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

9792

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


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

8745

83 


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


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


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


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


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


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


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


91 
theorems simultaneously:


92 
*}


93 

10971

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


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

8745

96 
apply(induct_tac a and b);


97 


98 
txt{*\noindent


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


100 
*}


101 

10171

102 
apply simp_all;


103 
(*<*)done(*>*)

8745

104 


105 
text{*


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


107 
an inductive proof expects a goal of the form


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


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

9792

110 
\begin{isabelle}

10971

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

9792

112 
\end{isabelle}

8745

113 


114 
\begin{exercise}

9792

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


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

11458

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


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


119 
Prove that @{text"norma"}

9792

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


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

12334

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


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

8745

124 
\end{exercise}


125 
*}

12334

126 
(*<*)

27015

127 
primrec norma :: "'a aexp \<Rightarrow> 'a aexp" and


128 
normb :: "'a bexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp \<Rightarrow> 'a aexp" where


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


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


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


132 
"norma (Var v) = Var v" 


133 
"norma (Num n) = Num n" 

12334

134 

27015

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


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

12334

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


138 


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


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


141 
apply (induct_tac a and b)


142 
apply (simp_all)


143 
done


144 

27015

145 
primrec normala :: "'a aexp \<Rightarrow> bool" and


146 
normalb :: "'a bexp \<Rightarrow> bool" where


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


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


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


150 
"normala (Var v) = True" 


151 
"normala (Num n) = True" 

12334

152 

27015

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


154 
"normalb (And b1 b2) = False" 

12334

155 
"normalb (Neg b) = False"


156 


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


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


159 
apply (induct_tac a and b)


160 
apply (auto)


161 
done


162 

8745

163 
end


164 
(*>*)
