Quelle  Ifexpr.thy

(*<*)
theory Ifexpr imports Main begin
(*>*)

subsection‹Case Study: Boolean Expressions›

text‹\label{sec:boolex}\index{boolean expressions example|(}
 The aim of this case study is twofold: it shows how to model boolean
 expressions and some algorithms for manipulating them, and it demonstrates
 the constructs introduced above.
 ›

subsubsection‹Modelling Boolean Expressions›

text‹
 We want to represent boolean expressions built up from variables and
 constants by negation and conjunction. The following datatype serves exactly
 that purpose:
 ›

datatype boolex = Const bool | Var nat | Neg boolex
                | And boolex boolex

text‹\noindent
 The two constants are represented by 🍋‹Const True› a
🍋‹Const False›. Variables are represented by terms of the form
🍋‹Var n›, where 🍋‹n› is a natural number (type 🍋‹nat›).
For example, the formula $P@0 \land \neg P@1$ is represented by the term
🍋‹And (Var 0) (Neg(Var 1))›.

\subsubsection{The Value of a Boolean Expression}

The value of a boolean expression depends on the value of its variables.
Hence the function ‹value› takes an additional parameter, an
\emph{environment} of type 🍋‹nat => bool›, which maps variables to their
values:
›

primrec "value" :: "boolex ==> (nat ==> bool) ==> bool" where
"value (Const b) env = b" |
"value (Var x) env = env x" |
"value (Neg b) env = (¬ value b env)" |
"value (And b c) env = (value b env ∧ value c env)"

text‹\noindent
 \subsubsection{If-Expressions}
 
 An alternative and often more efficient (because in a certain sense
 canonical) representation are so-called \emph{If-expressions} built up
 from constants (🍋‹CIF›),
(🍋‹IF›):
›

datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex

text‹\noindent
 The evaluation of If-expressions proceeds as for 🍋‹boolex›:
›

primrec valif :: "ifex ==> (nat ==> bool) ==> bool" where
"valif (CIF b) env = b" |
"valif (VIF x) env = env x" |
"valif (IF b t e) env = (if valif b env then valif t env
                                        else valif e env)"

text‹
 \subsubsection{Converting Boolean and If-Expressions}
 
 The type 🍋‹boolex› i
formulae, whereas 🍋‹ifex› is designed for efficiency. It is easy to
translate from 🍋‹boolex› into 🍋‹ifex›:
›

primrec bool2if :: "boolex ==> ifex" where
"bool2if (Const b) = CIF b" |
"bool2if (Var x) = VIF x" |
"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)" |
"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"

text‹\noindent
 At last, we have something we can verify: that 🍋‹bool2if› p
value of its argument:
›

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

txt‹\noindent
 The proof is canonical:
 ›

apply(induct_tac b)
apply(auto)
done

text‹\noindent
 In fact, all proofs in this case study look exactly like this. Hence we do
 not show them below.
 
 More interesting is the transformation of If-expressions into a normal form
 where the first argument of 🍋‹IF› c
must be a constant or variable. Such a normal form can be computed by
repeatedly replacing a subterm of the form 🍋‹IF (IF b x y) z u› by
🍋‹IF b (IF x z u) (IF y z u)›, which has the same value. The following
primitive recursive functions perform this task:
›

primrec normif :: "ifex ==> ifex ==> ifex ==> ifex" where
"normif (CIF b) t e = IF (CIF b) t e" |
"normif (VIF x) t e = IF (VIF x) t e" |
"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"

primrec norm :: "ifex ==> ifex" where
"norm (CIF b) = CIF b" |
"norm (VIF x) = VIF x" |
"norm (IF b t e) = normif b (norm t) (norm e)"

text‹\noindent
 Their interplay is tricky; we leave it to you to develop an
 intuitive understanding. Fortunately, Isabelle can help us to verify that the
 transformation preserves the value of the expression:
 ›

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

text‹\noindent
 The proof is canonical, provided we first show the following simplification
 lemma, which also helps to understand what 🍋‹normif› d
›

lemma [simp]:
  "∀t e. valif (normif b t e) env = valif (IF b t e) env"
(*<*)
apply(induct_tac b)
by(auto)

theorem "valif (norm b) env = valif b env"
apply(induct_tac b)
by(auto)
(*>*)
text‹\noindent
 Note that the lemma does not have a name, but is implicitly used in the proof
 of the theorem shown above because of the ‹[simp]› a

But how can we be sure that 🍋‹norm› really produces a normal form in
the above sense? We define a function that tests If-expressions for normality:
›

primrec normal :: "ifex ==> bool" where
"normal(CIF b) = True" |
"normal(VIF x) = True" |
"normal(IF b t e) = (normal t ∧ normal e ∧
     (case b of CIF b ==> True | VIF x ==> True | IF x y z ==> False))"

text‹\noindent
 Now we prove 🍋‹normal(norm b)›.
normality of 🍋‹normif›:
›

lemma [simp]: "∀t e. normal(normif b t e) = (normal t ∧ normal e)"
(*<*)
apply(induct_tac b)
by(auto)

theorem "normal(norm b)"
apply(induct_tac b)
by(auto)
(*>*)

text‹\medskip
 How do we come up with the required lemmas? Try to prove the main theorems
 without them and study carefully what ‹auto› l
can provide the clue.  The necessity of universal quantification
(‹∀t e›) in the two lemmas is explained in
\S\ref{sec:InductionHeuristics}

\begin{exercise}
  We strengthen the definition of a 🍋‹normal› If-expression as follows:
  the first argument of all 🍋‹IF›s must be a variable. Adapt the above
  development to this changed requirement. (Hint: you may need to formulate
  some of the goals as implications (‹⟶›) rather than
  equalities (‹=›).)
\end{exercise}
\index{boolean expressions example|)}
›
(*<*)

primrec normif2 :: "ifex => ifex => ifex => ifex" where
"normif2 (CIF b) t e = (if b then t else e)" |
"normif2 (VIF x) t e = IF (VIF x) t e" |
"normif2 (IF b t e) u f = normif2 b (normif2 t u f) (normif2 e u f)"

primrec norm2 :: "ifex => ifex" where
"norm2 (CIF b) = CIF b" |
"norm2 (VIF x) = VIF x" |
"norm2 (IF b t e) = normif2 b (norm2 t) (norm2 e)"

primrec normal2 :: "ifex => bool" where
"normal2(CIF b) = True" |
"normal2(VIF x) = True" |
"normal2(IF b t e) = (normal2 t & normal2 e &
     (case b of CIF b => False | VIF x => True | IF x y z => False))"

lemma [simp]:
  "∀t e. valif (normif2 b t e) env = valif (IF b t e) env"
apply(induct b)
by(auto)

theorem "valif (norm2 b) env = valif b env"
apply(induct b)
by(auto)

lemma [simp]: "∀t e. normal2 t & normal2 e --> normal2(normif2 b t e)"
apply(induct b)
by(auto)

theorem "normal2(norm2 b)"
apply(induct b)
by(auto)

end
(*>*)