1 (*<*) |
|
2 theory Ifexpr imports Main begin; |
|
3 (*>*) |
|
4 |
|
5 subsection{*Case Study: Boolean Expressions*} |
|
6 |
|
7 text{*\label{sec:boolex}\index{boolean expressions example|(} |
|
8 The aim of this case study is twofold: it shows how to model boolean |
|
9 expressions and some algorithms for manipulating them, and it demonstrates |
|
10 the constructs introduced above. |
|
11 *} |
|
12 |
|
13 subsubsection{*Modelling Boolean Expressions*} |
|
14 |
|
15 text{* |
|
16 We want to represent boolean expressions built up from variables and |
|
17 constants by negation and conjunction. The following datatype serves exactly |
|
18 that purpose: |
|
19 *} |
|
20 |
|
21 datatype boolex = Const bool | Var nat | Neg boolex |
|
22 | And boolex boolex; |
|
23 |
|
24 text{*\noindent |
|
25 The two constants are represented by @{term"Const True"} and |
|
26 @{term"Const False"}. Variables are represented by terms of the form |
|
27 @{term"Var n"}, where @{term"n"} is a natural number (type @{typ"nat"}). |
|
28 For example, the formula $P@0 \land \neg P@1$ is represented by the term |
|
29 @{term"And (Var 0) (Neg(Var 1))"}. |
|
30 |
|
31 \subsubsection{The Value of a Boolean Expression} |
|
32 |
|
33 The value of a boolean expression depends on the value of its variables. |
|
34 Hence the function @{text"value"} takes an additional parameter, an |
|
35 \emph{environment} of type @{typ"nat => bool"}, which maps variables to their |
|
36 values: |
|
37 *} |
|
38 |
|
39 primrec "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where |
|
40 "value (Const b) env = b" | |
|
41 "value (Var x) env = env x" | |
|
42 "value (Neg b) env = (\<not> value b env)" | |
|
43 "value (And b c) env = (value b env \<and> value c env)" |
|
44 |
|
45 text{*\noindent |
|
46 \subsubsection{If-Expressions} |
|
47 |
|
48 An alternative and often more efficient (because in a certain sense |
|
49 canonical) representation are so-called \emph{If-expressions} built up |
|
50 from constants (@{term"CIF"}), variables (@{term"VIF"}) and conditionals |
|
51 (@{term"IF"}): |
|
52 *} |
|
53 |
|
54 datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex; |
|
55 |
|
56 text{*\noindent |
|
57 The evaluation of If-expressions proceeds as for @{typ"boolex"}: |
|
58 *} |
|
59 |
|
60 primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where |
|
61 "valif (CIF b) env = b" | |
|
62 "valif (VIF x) env = env x" | |
|
63 "valif (IF b t e) env = (if valif b env then valif t env |
|
64 else valif e env)" |
|
65 |
|
66 text{* |
|
67 \subsubsection{Converting Boolean and If-Expressions} |
|
68 |
|
69 The type @{typ"boolex"} is close to the customary representation of logical |
|
70 formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to |
|
71 translate from @{typ"boolex"} into @{typ"ifex"}: |
|
72 *} |
|
73 |
|
74 primrec bool2if :: "boolex \<Rightarrow> ifex" where |
|
75 "bool2if (Const b) = CIF b" | |
|
76 "bool2if (Var x) = VIF x" | |
|
77 "bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)" | |
|
78 "bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)" |
|
79 |
|
80 text{*\noindent |
|
81 At last, we have something we can verify: that @{term"bool2if"} preserves the |
|
82 value of its argument: |
|
83 *} |
|
84 |
|
85 lemma "valif (bool2if b) env = value b env"; |
|
86 |
|
87 txt{*\noindent |
|
88 The proof is canonical: |
|
89 *} |
|
90 |
|
91 apply(induct_tac b); |
|
92 apply(auto); |
|
93 done |
|
94 |
|
95 text{*\noindent |
|
96 In fact, all proofs in this case study look exactly like this. Hence we do |
|
97 not show them below. |
|
98 |
|
99 More interesting is the transformation of If-expressions into a normal form |
|
100 where the first argument of @{term"IF"} cannot be another @{term"IF"} but |
|
101 must be a constant or variable. Such a normal form can be computed by |
|
102 repeatedly replacing a subterm of the form @{term"IF (IF b x y) z u"} by |
|
103 @{term"IF b (IF x z u) (IF y z u)"}, which has the same value. The following |
|
104 primitive recursive functions perform this task: |
|
105 *} |
|
106 |
|
107 primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where |
|
108 "normif (CIF b) t e = IF (CIF b) t e" | |
|
109 "normif (VIF x) t e = IF (VIF x) t e" | |
|
110 "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)" |
|
111 |
|
112 primrec norm :: "ifex \<Rightarrow> ifex" where |
|
113 "norm (CIF b) = CIF b" | |
|
114 "norm (VIF x) = VIF x" | |
|
115 "norm (IF b t e) = normif b (norm t) (norm e)" |
|
116 |
|
117 text{*\noindent |
|
118 Their interplay is tricky; we leave it to you to develop an |
|
119 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
|
120 transformation preserves the value of the expression: |
|
121 *} |
|
122 |
|
123 theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*) |
|
124 |
|
125 text{*\noindent |
|
126 The proof is canonical, provided we first show the following simplification |
|
127 lemma, which also helps to understand what @{term"normif"} does: |
|
128 *} |
|
129 |
|
130 lemma [simp]: |
|
131 "\<forall>t e. valif (normif b t e) env = valif (IF b t e) env"; |
|
132 (*<*) |
|
133 apply(induct_tac b); |
|
134 by(auto); |
|
135 |
|
136 theorem "valif (norm b) env = valif b env"; |
|
137 apply(induct_tac b); |
|
138 by(auto); |
|
139 (*>*) |
|
140 text{*\noindent |
|
141 Note that the lemma does not have a name, but is implicitly used in the proof |
|
142 of the theorem shown above because of the @{text"[simp]"} attribute. |
|
143 |
|
144 But how can we be sure that @{term"norm"} really produces a normal form in |
|
145 the above sense? We define a function that tests If-expressions for normality: |
|
146 *} |
|
147 |
|
148 primrec normal :: "ifex \<Rightarrow> bool" where |
|
149 "normal(CIF b) = True" | |
|
150 "normal(VIF x) = True" | |
|
151 "normal(IF b t e) = (normal t \<and> normal e \<and> |
|
152 (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))" |
|
153 |
|
154 text{*\noindent |
|
155 Now we prove @{term"normal(norm b)"}. Of course, this requires a lemma about |
|
156 normality of @{term"normif"}: |
|
157 *} |
|
158 |
|
159 lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)"; |
|
160 (*<*) |
|
161 apply(induct_tac b); |
|
162 by(auto); |
|
163 |
|
164 theorem "normal(norm b)"; |
|
165 apply(induct_tac b); |
|
166 by(auto); |
|
167 (*>*) |
|
168 |
|
169 text{*\medskip |
|
170 How do we come up with the required lemmas? Try to prove the main theorems |
|
171 without them and study carefully what @{text auto} leaves unproved. This |
|
172 can provide the clue. The necessity of universal quantification |
|
173 (@{text"\<forall>t e"}) in the two lemmas is explained in |
|
174 \S\ref{sec:InductionHeuristics} |
|
175 |
|
176 \begin{exercise} |
|
177 We strengthen the definition of a @{const normal} If-expression as follows: |
|
178 the first argument of all @{term IF}s must be a variable. Adapt the above |
|
179 development to this changed requirement. (Hint: you may need to formulate |
|
180 some of the goals as implications (@{text"\<longrightarrow>"}) rather than |
|
181 equalities (@{text"="}).) |
|
182 \end{exercise} |
|
183 \index{boolean expressions example|)} |
|
184 *} |
|
185 (*<*) |
|
186 |
|
187 primrec normif2 :: "ifex => ifex => ifex => ifex" where |
|
188 "normif2 (CIF b) t e = (if b then t else e)" | |
|
189 "normif2 (VIF x) t e = IF (VIF x) t e" | |
|
190 "normif2 (IF b t e) u f = normif2 b (normif2 t u f) (normif2 e u f)" |
|
191 |
|
192 primrec norm2 :: "ifex => ifex" where |
|
193 "norm2 (CIF b) = CIF b" | |
|
194 "norm2 (VIF x) = VIF x" | |
|
195 "norm2 (IF b t e) = normif2 b (norm2 t) (norm2 e)" |
|
196 |
|
197 primrec normal2 :: "ifex => bool" where |
|
198 "normal2(CIF b) = True" | |
|
199 "normal2(VIF x) = True" | |
|
200 "normal2(IF b t e) = (normal2 t & normal2 e & |
|
201 (case b of CIF b => False | VIF x => True | IF x y z => False))" |
|
202 |
|
203 lemma [simp]: |
|
204 "ALL t e. valif (normif2 b t e) env = valif (IF b t e) env" |
|
205 apply(induct b) |
|
206 by(auto) |
|
207 |
|
208 theorem "valif (norm2 b) env = valif b env" |
|
209 apply(induct b) |
|
210 by(auto) |
|
211 |
|
212 lemma [simp]: "ALL t e. normal2 t & normal2 e --> normal2(normif2 b t e)" |
|
213 apply(induct b) |
|
214 by(auto) |
|
215 |
|
216 theorem "normal2(norm2 b)" |
|
217 apply(induct b) |
|
218 by(auto) |
|
219 |
|
220 end |
|
221 (*>*) |
|