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