8745

1 
(*<*)


2 
theory Ifexpr = Main:;


3 
(*>*)


4 

9933

5 
subsection{*Case study: boolean expressions*}


6 


7 
text{*\label{sec:boolex}


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{*How can we model boolean expressions?*}


14 

8745

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

9541

25 
The two constants are represented by @{term"Const True"} and


26 
@{term"Const False"}. Variables are represented by terms of the form

9792

27 
@{term"Var n"}, where @{term"n"} is a natural number (type @{typ"nat"}).

8745

28 
For example, the formula $P@0 \land \neg P@1$ is represented by the term

9541

29 
@{term"And (Var 0) (Neg(Var 1))"}.

8745

30 


31 
\subsubsection{What is the value of a boolean expression?}


32 


33 
The value of a boolean expression depends on the value of its variables.

9792

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:

8745

37 
*}


38 


39 
consts value :: "boolex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";


40 
primrec


41 
"value (Const b) env = b"


42 
"value (Var x) env = env x"


43 
"value (Neg b) env = (\\<not> value b env)"


44 
"value (And b c) env = (value b env \\<and> value c env)";


45 


46 
text{*\noindent


47 
\subsubsection{Ifexpressions}


48 


49 
An alternative and often more efficient (because in a certain sense


50 
canonical) representation are socalled \emph{Ifexpressions} built up

9792

51 
from constants (@{term"CIF"}), variables (@{term"VIF"}) and conditionals


52 
(@{term"IF"}):

8745

53 
*}


54 


55 
datatype ifex = CIF bool  VIF nat  IF ifex ifex ifex;


56 


57 
text{*\noindent

9792

58 
The evaluation if Ifexpressions proceeds as for @{typ"boolex"}:

8745

59 
*}


60 


61 
consts valif :: "ifex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";


62 
primrec


63 
"valif (CIF b) env = b"


64 
"valif (VIF x) env = env x"


65 
"valif (IF b t e) env = (if valif b env then valif t env


66 
else valif e env)";


67 


68 
text{*


69 
\subsubsection{Transformation into and of Ifexpressions}


70 

9792

71 
The type @{typ"boolex"} is close to the customary representation of logical


72 
formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to


73 
translate from @{typ"boolex"} into @{typ"ifex"}:

8745

74 
*}


75 


76 
consts bool2if :: "boolex \\<Rightarrow> ifex";


77 
primrec


78 
"bool2if (Const b) = CIF b"


79 
"bool2if (Var x) = VIF x"


80 
"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"


81 
"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)";


82 


83 
text{*\noindent

9792

84 
At last, we have something we can verify: that @{term"bool2if"} preserves the

8745

85 
value of its argument:


86 
*}


87 


88 
lemma "valif (bool2if b) env = value b env";


89 


90 
txt{*\noindent


91 
The proof is canonical:


92 
*}


93 


94 
apply(induct_tac b);

10171

95 
apply(auto);


96 
done

8745

97 


98 
text{*\noindent


99 
In fact, all proofs in this case study look exactly like this. Hence we do


100 
not show them below.


101 


102 
More interesting is the transformation of Ifexpressions into a normal form

9792

103 
where the first argument of @{term"IF"} cannot be another @{term"IF"} but

8745

104 
must be a constant or variable. Such a normal form can be computed by

9541

105 
repeatedly replacing a subterm of the form @{term"IF (IF b x y) z u"} by


106 
@{term"IF b (IF x z u) (IF y z u)"}, which has the same value. The following

8745

107 
primitive recursive functions perform this task:


108 
*}


109 


110 
consts normif :: "ifex \\<Rightarrow> ifex \\<Rightarrow> ifex \\<Rightarrow> ifex";


111 
primrec


112 
"normif (CIF b) t e = IF (CIF b) t e"


113 
"normif (VIF x) t e = IF (VIF x) t e"


114 
"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)";


115 


116 
consts norm :: "ifex \\<Rightarrow> ifex";


117 
primrec


118 
"norm (CIF b) = CIF b"


119 
"norm (VIF x) = VIF x"


120 
"norm (IF b t e) = normif b (norm t) (norm e)";


121 


122 
text{*\noindent


123 
Their interplay is a bit tricky, and we leave it to the reader to develop an


124 
intuitive understanding. Fortunately, Isabelle can help us to verify that the


125 
transformation preserves the value of the expression:


126 
*}


127 


128 
theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)


129 


130 
text{*\noindent


131 
The proof is canonical, provided we first show the following simplification

9792

132 
lemma (which also helps to understand what @{term"normif"} does):

8745

133 
*}


134 


135 
lemma [simp]:


136 
"\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";


137 
(*<*)


138 
apply(induct_tac b);

9458

139 
by(auto);

8745

140 


141 
theorem "valif (norm b) env = valif b env";


142 
apply(induct_tac b);

9458

143 
by(auto);

8745

144 
(*>*)


145 
text{*\noindent


146 
Note that the lemma does not have a name, but is implicitly used in the proof

9792

147 
of the theorem shown above because of the @{text"[simp]"} attribute.

8745

148 

9792

149 
But how can we be sure that @{term"norm"} really produces a normal form in

8745

150 
the above sense? We define a function that tests Ifexpressions for normality


151 
*}


152 


153 
consts normal :: "ifex \\<Rightarrow> bool";


154 
primrec


155 
"normal(CIF b) = True"


156 
"normal(VIF x) = True"


157 
"normal(IF b t e) = (normal t \\<and> normal e \\<and>


158 
(case b of CIF b \\<Rightarrow> True  VIF x \\<Rightarrow> True  IF x y z \\<Rightarrow> False))";


159 


160 
text{*\noindent

9792

161 
and prove @{term"normal(norm b)"}. Of course, this requires a lemma about


162 
normality of @{term"normif"}:

8745

163 
*}


164 

9458

165 
lemma[simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";

8771

166 
(*<*)

8745

167 
apply(induct_tac b);

9458

168 
by(auto);

8745

169 


170 
theorem "normal(norm b)";


171 
apply(induct_tac b);

9458

172 
by(auto);

9933

173 
(*>*)

8745

174 

9933

175 
text{*\medskip


176 
How does one come up with the required lemmas? Try to prove the main theorems


177 
without them and study carefully what @{text auto} leaves unproved. This has


178 
to provide the clue. The necessity of universal quantification


179 
(@{text"\<forall>t e"}) in the two lemmas is explained in


180 
\S\ref{sec:InductionHeuristics}


181 


182 
\begin{exercise}


183 
We strengthen the definition of a @{term normal} Ifexpression as follows:


184 
the first argument of all @{term IF}s must be a variable. Adapt the above


185 
development to this changed requirement. (Hint: you may need to formulate


186 
some of the goals as implications (@{text"\<longrightarrow>"}) rather than


187 
equalities (@{text"="}).)


188 
\end{exercise}


189 
*}


190 
(*<*)

8771

191 
end


192 
(*>*)
