8745
|
1 |
(*<*)
|
|
2 |
theory Ifexpr = Main:;
|
|
3 |
(*>*)
|
|
4 |
|
|
5 |
text{*
|
|
6 |
\subsubsection{How can we model boolean expressions?}
|
|
7 |
|
|
8 |
We want to represent boolean expressions built up from variables and
|
|
9 |
constants by negation and conjunction. The following datatype serves exactly
|
|
10 |
that purpose:
|
|
11 |
*}
|
|
12 |
|
|
13 |
datatype boolex = Const bool | Var nat | Neg boolex
|
|
14 |
| And boolex boolex;
|
|
15 |
|
|
16 |
text{*\noindent
|
|
17 |
The two constants are represented by \isa{Const~True} and
|
|
18 |
\isa{Const~False}. Variables are represented by terms of the form
|
|
19 |
\isa{Var~$n$}, where $n$ is a natural number (type \isa{nat}).
|
|
20 |
For example, the formula $P@0 \land \neg P@1$ is represented by the term
|
|
21 |
\isa{And~(Var~0)~(Neg(Var~1))}.
|
|
22 |
|
|
23 |
\subsubsection{What is the value of a boolean expression?}
|
|
24 |
|
|
25 |
The value of a boolean expression depends on the value of its variables.
|
|
26 |
Hence the function \isa{value} takes an additional parameter, an {\em
|
|
27 |
environment} of type \isa{nat \isasymFun\ bool}, which maps variables to
|
|
28 |
their values:
|
|
29 |
*}
|
|
30 |
|
|
31 |
consts value :: "boolex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
|
|
32 |
primrec
|
|
33 |
"value (Const b) env = b"
|
|
34 |
"value (Var x) env = env x"
|
|
35 |
"value (Neg b) env = (\\<not> value b env)"
|
|
36 |
"value (And b c) env = (value b env \\<and> value c env)";
|
|
37 |
|
|
38 |
text{*\noindent
|
|
39 |
\subsubsection{If-expressions}
|
|
40 |
|
|
41 |
An alternative and often more efficient (because in a certain sense
|
|
42 |
canonical) representation are so-called \emph{If-expressions} built up
|
|
43 |
from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
|
|
44 |
(\isa{IF}):
|
|
45 |
*}
|
|
46 |
|
|
47 |
datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
|
|
48 |
|
|
49 |
text{*\noindent
|
|
50 |
The evaluation if If-expressions proceeds as for \isa{boolex}:
|
|
51 |
*}
|
|
52 |
|
|
53 |
consts valif :: "ifex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
|
|
54 |
primrec
|
|
55 |
"valif (CIF b) env = b"
|
|
56 |
"valif (VIF x) env = env x"
|
|
57 |
"valif (IF b t e) env = (if valif b env then valif t env
|
|
58 |
else valif e env)";
|
|
59 |
|
|
60 |
text{*
|
|
61 |
\subsubsection{Transformation into and of If-expressions}
|
|
62 |
|
|
63 |
The type \isa{boolex} is close to the customary representation of logical
|
|
64 |
formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
|
|
65 |
translate from \isa{boolex} into \isa{ifex}:
|
|
66 |
*}
|
|
67 |
|
|
68 |
consts bool2if :: "boolex \\<Rightarrow> ifex";
|
|
69 |
primrec
|
|
70 |
"bool2if (Const b) = CIF b"
|
|
71 |
"bool2if (Var x) = VIF x"
|
|
72 |
"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"
|
|
73 |
"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)";
|
|
74 |
|
|
75 |
text{*\noindent
|
|
76 |
At last, we have something we can verify: that \isa{bool2if} preserves the
|
|
77 |
value of its argument:
|
|
78 |
*}
|
|
79 |
|
|
80 |
lemma "valif (bool2if b) env = value b env";
|
|
81 |
|
|
82 |
txt{*\noindent
|
|
83 |
The proof is canonical:
|
|
84 |
*}
|
|
85 |
|
|
86 |
apply(induct_tac b);
|
|
87 |
apply(auto).;
|
|
88 |
|
|
89 |
text{*\noindent
|
|
90 |
In fact, all proofs in this case study look exactly like this. Hence we do
|
|
91 |
not show them below.
|
|
92 |
|
|
93 |
More interesting is the transformation of If-expressions into a normal form
|
|
94 |
where the first argument of \isa{IF} cannot be another \isa{IF} but
|
|
95 |
must be a constant or variable. Such a normal form can be computed by
|
|
96 |
repeatedly replacing a subterm of the form \isa{IF~(IF~b~x~y)~z~u} by
|
|
97 |
\isa{IF b (IF x z u) (IF y z u)}, which has the same value. The following
|
|
98 |
primitive recursive functions perform this task:
|
|
99 |
*}
|
|
100 |
|
|
101 |
consts normif :: "ifex \\<Rightarrow> ifex \\<Rightarrow> ifex \\<Rightarrow> ifex";
|
|
102 |
primrec
|
|
103 |
"normif (CIF b) t e = IF (CIF b) t e"
|
|
104 |
"normif (VIF x) t e = IF (VIF x) t e"
|
|
105 |
"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)";
|
|
106 |
|
|
107 |
consts norm :: "ifex \\<Rightarrow> ifex";
|
|
108 |
primrec
|
|
109 |
"norm (CIF b) = CIF b"
|
|
110 |
"norm (VIF x) = VIF x"
|
|
111 |
"norm (IF b t e) = normif b (norm t) (norm e)";
|
|
112 |
|
|
113 |
text{*\noindent
|
|
114 |
Their interplay is a bit tricky, and we leave it to the reader to develop an
|
|
115 |
intuitive understanding. Fortunately, Isabelle can help us to verify that the
|
|
116 |
transformation preserves the value of the expression:
|
|
117 |
*}
|
|
118 |
|
|
119 |
theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)
|
|
120 |
|
|
121 |
text{*\noindent
|
|
122 |
The proof is canonical, provided we first show the following simplification
|
|
123 |
lemma (which also helps to understand what \isa{normif} does):
|
|
124 |
*}
|
|
125 |
|
|
126 |
lemma [simp]:
|
|
127 |
"\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
|
|
128 |
(*<*)
|
|
129 |
apply(induct_tac b);
|
|
130 |
apply(auto).;
|
|
131 |
|
|
132 |
theorem "valif (norm b) env = valif b env";
|
|
133 |
apply(induct_tac b);
|
|
134 |
apply(auto).;
|
|
135 |
(*>*)
|
|
136 |
text{*\noindent
|
|
137 |
Note that the lemma does not have a name, but is implicitly used in the proof
|
|
138 |
of the theorem shown above because of the \isa{[simp]} attribute.
|
|
139 |
|
|
140 |
But how can we be sure that \isa{norm} really produces a normal form in
|
|
141 |
the above sense? We define a function that tests If-expressions for normality
|
|
142 |
*}
|
|
143 |
|
|
144 |
consts normal :: "ifex \\<Rightarrow> bool";
|
|
145 |
primrec
|
|
146 |
"normal(CIF b) = True"
|
|
147 |
"normal(VIF x) = True"
|
|
148 |
"normal(IF b t e) = (normal t \\<and> normal e \\<and>
|
|
149 |
(case b of CIF b \\<Rightarrow> True | VIF x \\<Rightarrow> True | IF x y z \\<Rightarrow> False))";
|
|
150 |
|
|
151 |
text{*\noindent
|
|
152 |
and prove \isa{normal(norm b)}. Of course, this requires a lemma about
|
|
153 |
normality of \isa{normif}:
|
|
154 |
*}
|
|
155 |
|
|
156 |
lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*)
|
|
157 |
apply(induct_tac b);
|
|
158 |
apply(auto).;
|
|
159 |
|
|
160 |
theorem "normal(norm b)";
|
|
161 |
apply(induct_tac b);
|
|
162 |
apply(auto).;
|
|
163 |
|
|
164 |
end(*>*)
|