1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Apr 19 11:56:31 2000 +0200
1.3 @@ -0,0 +1,164 @@
1.4 +(*<*)
1.5 +theory Ifexpr = Main:;
1.6 +(*>*)
1.7 +
1.8 +text{*
1.9 +\subsubsection{How can we model boolean expressions?}
1.10 +
1.11 +We want to represent boolean expressions built up from variables and
1.12 +constants by negation and conjunction. The following datatype serves exactly
1.13 +that purpose:
1.14 +*}
1.15 +
1.16 +datatype boolex = Const bool | Var nat | Neg boolex
1.17 + | And boolex boolex;
1.18 +
1.19 +text{*\noindent
1.20 +The two constants are represented by \isa{Const~True} and
1.21 +\isa{Const~False}. Variables are represented by terms of the form
1.22 +\isa{Var~$n$}, where $n$ is a natural number (type \isa{nat}).
1.23 +For example, the formula $P@0 \land \neg P@1$ is represented by the term
1.24 +\isa{And~(Var~0)~(Neg(Var~1))}.
1.25 +
1.26 +\subsubsection{What is the value of a boolean expression?}
1.27 +
1.28 +The value of a boolean expression depends on the value of its variables.
1.29 +Hence the function \isa{value} takes an additional parameter, an {\em
1.30 + environment} of type \isa{nat \isasymFun\ bool}, which maps variables to
1.31 +their values:
1.32 +*}
1.33 +
1.34 +consts value :: "boolex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
1.35 +primrec
1.36 +"value (Const b) env = b"
1.37 +"value (Var x) env = env x"
1.38 +"value (Neg b) env = (\\<not> value b env)"
1.39 +"value (And b c) env = (value b env \\<and> value c env)";
1.40 +
1.41 +text{*\noindent
1.42 +\subsubsection{If-expressions}
1.43 +
1.44 +An alternative and often more efficient (because in a certain sense
1.45 +canonical) representation are so-called \emph{If-expressions} built up
1.46 +from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
1.47 +(\isa{IF}):
1.48 +*}
1.49 +
1.50 +datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
1.51 +
1.52 +text{*\noindent
1.53 +The evaluation if If-expressions proceeds as for \isa{boolex}:
1.54 +*}
1.55 +
1.56 +consts valif :: "ifex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
1.57 +primrec
1.58 +"valif (CIF b) env = b"
1.59 +"valif (VIF x) env = env x"
1.60 +"valif (IF b t e) env = (if valif b env then valif t env
1.61 + else valif e env)";
1.62 +
1.63 +text{*
1.64 +\subsubsection{Transformation into and of If-expressions}
1.65 +
1.66 +The type \isa{boolex} is close to the customary representation of logical
1.67 +formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
1.68 +translate from \isa{boolex} into \isa{ifex}:
1.69 +*}
1.70 +
1.71 +consts bool2if :: "boolex \\<Rightarrow> ifex";
1.72 +primrec
1.73 +"bool2if (Const b) = CIF b"
1.74 +"bool2if (Var x) = VIF x"
1.75 +"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"
1.76 +"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)";
1.77 +
1.78 +text{*\noindent
1.79 +At last, we have something we can verify: that \isa{bool2if} preserves the
1.80 +value of its argument:
1.81 +*}
1.82 +
1.83 +lemma "valif (bool2if b) env = value b env";
1.84 +
1.85 +txt{*\noindent
1.86 +The proof is canonical:
1.87 +*}
1.88 +
1.89 +apply(induct_tac b);
1.90 +apply(auto).;
1.91 +
1.92 +text{*\noindent
1.93 +In fact, all proofs in this case study look exactly like this. Hence we do
1.94 +not show them below.
1.95 +
1.96 +More interesting is the transformation of If-expressions into a normal form
1.97 +where the first argument of \isa{IF} cannot be another \isa{IF} but
1.98 +must be a constant or variable. Such a normal form can be computed by
1.99 +repeatedly replacing a subterm of the form \isa{IF~(IF~b~x~y)~z~u} by
1.100 +\isa{IF b (IF x z u) (IF y z u)}, which has the same value. The following
1.101 +primitive recursive functions perform this task:
1.102 +*}
1.103 +
1.104 +consts normif :: "ifex \\<Rightarrow> ifex \\<Rightarrow> ifex \\<Rightarrow> ifex";
1.105 +primrec
1.106 +"normif (CIF b) t e = IF (CIF b) t e"
1.107 +"normif (VIF x) t e = IF (VIF x) t e"
1.108 +"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)";
1.109 +
1.110 +consts norm :: "ifex \\<Rightarrow> ifex";
1.111 +primrec
1.112 +"norm (CIF b) = CIF b"
1.113 +"norm (VIF x) = VIF x"
1.114 +"norm (IF b t e) = normif b (norm t) (norm e)";
1.115 +
1.116 +text{*\noindent
1.117 +Their interplay is a bit tricky, and we leave it to the reader to develop an
1.118 +intuitive understanding. Fortunately, Isabelle can help us to verify that the
1.119 +transformation preserves the value of the expression:
1.120 +*}
1.121 +
1.122 +theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)
1.123 +
1.124 +text{*\noindent
1.125 +The proof is canonical, provided we first show the following simplification
1.126 +lemma (which also helps to understand what \isa{normif} does):
1.127 +*}
1.128 +
1.129 +lemma [simp]:
1.130 + "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
1.131 +(*<*)
1.132 +apply(induct_tac b);
1.133 +apply(auto).;
1.134 +
1.135 +theorem "valif (norm b) env = valif b env";
1.136 +apply(induct_tac b);
1.137 +apply(auto).;
1.138 +(*>*)
1.139 +text{*\noindent
1.140 +Note that the lemma does not have a name, but is implicitly used in the proof
1.141 +of the theorem shown above because of the \isa{[simp]} attribute.
1.142 +
1.143 +But how can we be sure that \isa{norm} really produces a normal form in
1.144 +the above sense? We define a function that tests If-expressions for normality
1.145 +*}
1.146 +
1.147 +consts normal :: "ifex \\<Rightarrow> bool";
1.148 +primrec
1.149 +"normal(CIF b) = True"
1.150 +"normal(VIF x) = True"
1.151 +"normal(IF b t e) = (normal t \\<and> normal e \\<and>
1.152 + (case b of CIF b \\<Rightarrow> True | VIF x \\<Rightarrow> True | IF x y z \\<Rightarrow> False))";
1.153 +
1.154 +text{*\noindent
1.155 +and prove \isa{normal(norm b)}. Of course, this requires a lemma about
1.156 +normality of \isa{normif}:
1.157 +*}
1.158 +
1.159 +lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*)
1.160 +apply(induct_tac b);
1.161 +apply(auto).;
1.162 +
1.163 +theorem "normal(norm b)";
1.164 +apply(induct_tac b);
1.165 +apply(auto).;
1.166 +
1.167 +end(*>*)