src/Doc/Tutorial/Ifexpr/Ifexpr.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)
     2 theory Ifexpr imports Main begin
     3 (*>*)
     4 
     5 subsection{*Case Study: Boolean Expressions*}
     6 
     7 text{*\label{sec:boolex}\index{boolean expressions example|(}
     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{*Modelling Boolean Expressions*}
    14 
    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
    25 The two constants are represented by @{term"Const True"} and
    26 @{term"Const False"}. Variables are represented by terms of the form
    27 @{term"Var n"}, where @{term"n"} is a natural number (type @{typ"nat"}).
    28 For example, the formula $P@0 \land \neg P@1$ is represented by the term
    29 @{term"And (Var 0) (Neg(Var 1))"}.
    30 
    31 \subsubsection{The Value of a Boolean Expression}
    32 
    33 The value of a boolean expression depends on the value of its variables.
    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:
    37 *}
    38 
    39 primrec "value" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
    40 "value (Const b) env = b" |
    41 "value (Var x)   env = env x" |
    42 "value (Neg b)   env = (\<not> value b env)" |
    43 "value (And b c) env = (value b env \<and> value c env)"
    44 
    45 text{*\noindent
    46 \subsubsection{If-Expressions}
    47 
    48 An alternative and often more efficient (because in a certain sense
    49 canonical) representation are so-called \emph{If-expressions} built up
    50 from constants (@{term"CIF"}), variables (@{term"VIF"}) and conditionals
    51 (@{term"IF"}):
    52 *}
    53 
    54 datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
    55 
    56 text{*\noindent
    57 The evaluation of If-expressions proceeds as for @{typ"boolex"}:
    58 *}
    59 
    60 primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
    61 "valif (CIF b)    env = b" |
    62 "valif (VIF x)    env = env x" |
    63 "valif (IF b t e) env = (if valif b env then valif t env
    64                                         else valif e env)"
    65 
    66 text{*
    67 \subsubsection{Converting Boolean and If-Expressions}
    68 
    69 The type @{typ"boolex"} is close to the customary representation of logical
    70 formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to
    71 translate from @{typ"boolex"} into @{typ"ifex"}:
    72 *}
    73 
    74 primrec bool2if :: "boolex \<Rightarrow> ifex" where
    75 "bool2if (Const b) = CIF b" |
    76 "bool2if (Var x)   = VIF x" |
    77 "bool2if (Neg b)   = IF (bool2if b) (CIF False) (CIF True)" |
    78 "bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
    79 
    80 text{*\noindent
    81 At last, we have something we can verify: that @{term"bool2if"} preserves the
    82 value of its argument:
    83 *}
    84 
    85 lemma "valif (bool2if b) env = value b env"
    86 
    87 txt{*\noindent
    88 The proof is canonical:
    89 *}
    90 
    91 apply(induct_tac b)
    92 apply(auto)
    93 done
    94 
    95 text{*\noindent
    96 In fact, all proofs in this case study look exactly like this. Hence we do
    97 not show them below.
    98 
    99 More interesting is the transformation of If-expressions into a normal form
   100 where the first argument of @{term"IF"} cannot be another @{term"IF"} but
   101 must be a constant or variable. Such a normal form can be computed by
   102 repeatedly replacing a subterm of the form @{term"IF (IF b x y) z u"} by
   103 @{term"IF b (IF x z u) (IF y z u)"}, which has the same value. The following
   104 primitive recursive functions perform this task:
   105 *}
   106 
   107 primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where
   108 "normif (CIF b)    t e = IF (CIF b) t e" |
   109 "normif (VIF x)    t e = IF (VIF x) t e" |
   110 "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
   111 
   112 primrec norm :: "ifex \<Rightarrow> ifex" where
   113 "norm (CIF b)    = CIF b" |
   114 "norm (VIF x)    = VIF x" |
   115 "norm (IF b t e) = normif b (norm t) (norm e)"
   116 
   117 text{*\noindent
   118 Their interplay is tricky; we leave it to you to develop an
   119 intuitive understanding. Fortunately, Isabelle can help us to verify that the
   120 transformation preserves the value of the expression:
   121 *}
   122 
   123 theorem "valif (norm b) env = valif b env"(*<*)oops(*>*)
   124 
   125 text{*\noindent
   126 The proof is canonical, provided we first show the following simplification
   127 lemma, which also helps to understand what @{term"normif"} does:
   128 *}
   129 
   130 lemma [simp]:
   131   "\<forall>t e. valif (normif b t e) env = valif (IF b t e) env"
   132 (*<*)
   133 apply(induct_tac b)
   134 by(auto)
   135 
   136 theorem "valif (norm b) env = valif b env"
   137 apply(induct_tac b)
   138 by(auto)
   139 (*>*)
   140 text{*\noindent
   141 Note that the lemma does not have a name, but is implicitly used in the proof
   142 of the theorem shown above because of the @{text"[simp]"} attribute.
   143 
   144 But how can we be sure that @{term"norm"} really produces a normal form in
   145 the above sense? We define a function that tests If-expressions for normality:
   146 *}
   147 
   148 primrec normal :: "ifex \<Rightarrow> bool" where
   149 "normal(CIF b) = True" |
   150 "normal(VIF x) = True" |
   151 "normal(IF b t e) = (normal t \<and> normal e \<and>
   152      (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))"
   153 
   154 text{*\noindent
   155 Now we prove @{term"normal(norm b)"}. Of course, this requires a lemma about
   156 normality of @{term"normif"}:
   157 *}
   158 
   159 lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)"
   160 (*<*)
   161 apply(induct_tac b)
   162 by(auto)
   163 
   164 theorem "normal(norm b)"
   165 apply(induct_tac b)
   166 by(auto)
   167 (*>*)
   168 
   169 text{*\medskip
   170 How do we come up with the required lemmas? Try to prove the main theorems
   171 without them and study carefully what @{text auto} leaves unproved. This 
   172 can provide the clue.  The necessity of universal quantification
   173 (@{text"\<forall>t e"}) in the two lemmas is explained in
   174 \S\ref{sec:InductionHeuristics}
   175 
   176 \begin{exercise}
   177   We strengthen the definition of a @{const normal} If-expression as follows:
   178   the first argument of all @{term IF}s must be a variable. Adapt the above
   179   development to this changed requirement. (Hint: you may need to formulate
   180   some of the goals as implications (@{text"\<longrightarrow>"}) rather than
   181   equalities (@{text"="}).)
   182 \end{exercise}
   183 \index{boolean expressions example|)}
   184 *}
   185 (*<*)
   186 
   187 primrec normif2 :: "ifex => ifex => ifex => ifex" where
   188 "normif2 (CIF b)    t e = (if b then t else e)" |
   189 "normif2 (VIF x)    t e = IF (VIF x) t e" |
   190 "normif2 (IF b t e) u f = normif2 b (normif2 t u f) (normif2 e u f)"
   191 
   192 primrec norm2 :: "ifex => ifex" where
   193 "norm2 (CIF b)    = CIF b" |
   194 "norm2 (VIF x)    = VIF x" |
   195 "norm2 (IF b t e) = normif2 b (norm2 t) (norm2 e)"
   196 
   197 primrec normal2 :: "ifex => bool" where
   198 "normal2(CIF b) = True" |
   199 "normal2(VIF x) = True" |
   200 "normal2(IF b t e) = (normal2 t & normal2 e &
   201      (case b of CIF b => False | VIF x => True | IF x y z => False))"
   202 
   203 lemma [simp]:
   204   "ALL t e. valif (normif2 b t e) env = valif (IF b t e) env"
   205 apply(induct b)
   206 by(auto)
   207 
   208 theorem "valif (norm2 b) env = valif b env"
   209 apply(induct b)
   210 by(auto)
   211 
   212 lemma [simp]: "ALL t e. normal2 t & normal2 e --> normal2(normif2 b t e)"
   213 apply(induct b)
   214 by(auto)
   215 
   216 theorem "normal2(norm2 b)"
   217 apply(induct b)
   218 by(auto)
   219 
   220 end
   221 (*>*)