--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Sep 12 15:43:15 2000 +0200
@@ -2,9 +2,18 @@
\begin{isabellebody}%
\def\isabellecontext{Ifexpr}%
%
+\isamarkupsubsection{Case study: boolean expressions}
+%
\begin{isamarkuptext}%
-\subsubsection{How can we model boolean expressions?}
-
+\label{sec:boolex}
+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.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{How can we model boolean expressions?}
+%
+\begin{isamarkuptext}%
We want to represent boolean expressions built up from variables and
constants by negation and conjunction. The following datatype serves exactly
that purpose:%
@@ -133,7 +142,24 @@
and prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
normality of \isa{normif}:%
\end{isamarkuptext}%
-\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
+\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\medskip
+How does one come up with the required lemmas? Try to prove the main theorems
+without them and study carefully what \isa{auto} leaves unproved. This has
+to provide the clue. The necessity of universal quantification
+(\isa{{\isasymforall}t\ e}) in the two lemmas is explained in
+\S\ref{sec:InductionHeuristics}
+
+\begin{exercise}
+ We strengthen the definition of a \isa{normal} If-expression as follows:
+ the first argument of all \isa{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 (\isa{{\isasymlongrightarrow}}) rather than
+ equalities (\isa{{\isacharequal}}).)
+\end{exercise}%
+\end{isamarkuptext}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"