Quelle  Ifexpr.thy

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

subsection‹Case Study: Boolean Expressions›

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

subsubsection‹Modelling Boolean Expressions›

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

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

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

 subsubsection{The Value of a Boolean Expression}

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

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}

  alternative and often more efficient (because in a certain sense
 ) representation are so-called \emph{If-expressions} built up
  constants (term‹CIF›), variables (term‹VIF›) and conditionals
 term‹IF›):
 ›

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

text‹\noindent
  evaluation of If-expressions proceeds as for typ‹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}

  type typ‹boolex› is close to the customary representation of logical
 , whereas typ‹ifex› is designed for efficiency. It is easy to
  from typ‹boolex› into typ‹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
  last, we have something we can verify: that term‹bool2if› preserves the
  of its argument:
 ›

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

txt‹\noindent
  proof is canonical:
 ›

apply(induct_tac b)
apply(auto)
done

text‹\noindent
  fact, all proofs in this case study look exactly like this. Hence we do
  show them below.

  interesting is the transformation of If-expressions into a normal form
  the first argument of term‹IF› cannot be another term‹IF› but
  be a constant or variable. Such a normal form can be computed by
  replacing a subterm of the form term‹IF (IF b x y) z u› by
 term‹IF b (IF x z u) (IF y z u)›, which has the same value. The following
  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
  interplay is tricky; we leave it to you to develop an
  understanding. Fortunately, Isabelle can help us to verify that the
  preserves the value of the expression:
 ›

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

text‹\noindent
  proof is canonical, provided we first show the following simplification
 , which also helps to understand what term‹normif› does:
 ›

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
  that the lemma does not have a name, but is implicitly used in the proof
  the theorem shown above because of the ‹[simp]› attribute.

  how can we be sure that term‹norm› really produces a normal form in
  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
  we prove term‹normal(norm b)›. Of course, this requires a lemma about
  of term‹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
  do we come up with the required lemmas? Try to prove the main theorems
  them and study carefully what ‹auto› leaves unproved. This
  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 const‹normal› If-expression as follows:
 the first argument of all term‹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
(*>*)