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 $n-m$ else $m-n$'',
|
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 |
(*>*)
|