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