|
1 (*<*) |
|
2 theory ABexpr imports Main begin; |
|
3 (*>*) |
|
4 |
|
5 text{* |
|
6 \index{datatypes!mutually recursive}% |
|
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 |
|
12 conditional expressions like ``if $m<n$ then $n-m$ else $m-n$'', |
|
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 |
|
30 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler}, |
|
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 |
|
34 expressions can be arithmetic comparisons, conjunctions and negations. |
|
35 The semantics is given by two evaluation functions: |
|
36 *} |
|
37 |
|
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)" |
|
50 |
|
51 text{*\noindent |
|
52 |
|
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. |
|
61 |
|
62 In the same fashion we also define two functions that perform substitution: |
|
63 *} |
|
64 |
|
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)" |
|
77 |
|
78 text{*\noindent |
|
79 Their first argument is a function mapping variables to expressions, the |
|
80 substitution. It is applied to all variables in the second argument. As a |
|
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. |
|
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 |
|
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)"; |
|
96 apply(induct_tac a and b); |
|
97 |
|
98 txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
|
99 *} |
|
100 |
|
101 apply simp_all; |
|
102 (*<*)done(*>*) |
|
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 |
|
109 \begin{isabelle} |
|
110 \isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text ")"} |
|
111 \end{isabelle} |
|
112 |
|
113 \begin{exercise} |
|
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 |
|
116 @{term"IF"}s; it should eliminate the constructors |
|
117 @{term"And"} and @{term"Neg"}, leaving only @{term"Less"}. |
|
118 Prove that @{text"norma"} |
|
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 |
|
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). |
|
123 \end{exercise} |
|
124 *} |
|
125 (*<*) |
|
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" | |
|
133 |
|
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" | |
|
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)" |
|
140 apply (induct_tac a and b) |
|
141 apply (simp_all) |
|
142 done |
|
143 |
|
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" | |
|
151 |
|
152 "normalb (Less a1 a2) = (normala a1 \<and> normala a2)" | |
|
153 "normalb (And b1 b2) = False" | |
|
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))" |
|
158 apply (induct_tac a and b) |
|
159 apply (auto) |
|
160 done |
|
161 |
|
162 end |
|
163 (*>*) |