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 (*>*)