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

27318

96 
apply(induct_tac a and b);

8745

97 

27318

98 
txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:

8745

99 
*}


100 

10171

101 
apply simp_all;


102 
(*<*)done(*>*)

8745

103 


104 
text{*


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


106 
an inductive proof expects a goal of the form


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


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

9792

109 
\begin{isabelle}

27318

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

9792

111 
\end{isabelle}

8745

112 


113 
\begin{exercise}

9792

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


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

11458

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


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


118 
Prove that @{text"norma"}

9792

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


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

12334

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


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

8745

123 
\end{exercise}


124 
*}

12334

125 
(*<*)

27015

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


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


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


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


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


131 
"norma (Var v) = Var v" 


132 
"norma (Num n) = Num n" 

12334

133 

27015

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


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

12334

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


137 


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


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

27318

140 
apply (induct_tac a and b)

12334

141 
apply (simp_all)


142 
done


143 

27015

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


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


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


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


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


149 
"normala (Var v) = True" 


150 
"normala (Num n) = True" 

12334

151 

27015

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


153 
"normalb (And b1 b2) = False" 

12334

154 
"normalb (Neg b) = False"


155 


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


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

27318

158 
apply (induct_tac a and b)

12334

159 
apply (auto)


160 
done


161 

8745

162 
end


163 
(*>*)
