--- a/doc-src/TutorialI/document/Ifexpr.tex Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Ifexpr}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsubsection{Case Study: Boolean Expressions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:boolex}\index{boolean expressions example|(}
-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}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Modelling Boolean Expressions%
-}
-\isamarkuptrue%
-%
-\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:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{datatype}\isamarkupfalse%
-\ boolex\ {\isaliteral{3D}{\isacharequal}}\ Const\ bool\ {\isaliteral{7C}{\isacharbar}}\ Var\ nat\ {\isaliteral{7C}{\isacharbar}}\ Neg\ boolex\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ And\ boolex\ boolex%
-\begin{isamarkuptext}%
-\noindent
-The two constants are represented by \isa{Const\ True} and
-\isa{Const\ False}. Variables are represented by terms of the form
-\isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}).
-For example, the formula $P@0 \land \neg P@1$ is represented by the term
-\isa{And\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Neg\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.
-
-\subsubsection{The Value of a Boolean Expression}
-
-The value of a boolean expression depends on the value of its variables.
-Hence the function \isa{value} takes an additional parameter, an
-\emph{environment} of type \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}, which maps variables to their
-values:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}value{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}boolex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Const\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ env\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ value\ b\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}And\ b\ c{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}value\ b\ env\ {\isaliteral{5C3C616E643E}{\isasymand}}\ value\ c\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-\subsubsection{If-Expressions}
-
-An alternative and often more efficient (because in a certain sense
-canonical) representation are so-called \emph{If-expressions} built up
-from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
-(\isa{IF}):%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{datatype}\isamarkupfalse%
-\ ifex\ {\isaliteral{3D}{\isacharequal}}\ CIF\ bool\ {\isaliteral{7C}{\isacharbar}}\ VIF\ nat\ {\isaliteral{7C}{\isacharbar}}\ IF\ ifex\ ifex\ ifex%
-\begin{isamarkuptext}%
-\noindent
-The evaluation of If-expressions proceeds as for \isa{boolex}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\ valif\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ \ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ \ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ env\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\subsubsection{Converting Boolean and If-Expressions}
-
-The type \isa{boolex} is close to the customary representation of logical
-formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
-translate from \isa{boolex} into \isa{ifex}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\ bool{\isadigit{2}}if\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}boolex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}Const\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CIF\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{3D}{\isacharequal}}\ VIF\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}CIF\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}CIF\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}And\ b\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}CIF\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the
-value of its argument:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ value\ b\ env{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-The proof is canonical:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-In fact, all proofs in this case study look exactly like this. Hence we do
-not show them below.
-
-More interesting is the transformation of If-expressions into a normal form
-where the first argument of \isa{IF} cannot be another \isa{IF} but
-must be a constant or variable. Such a normal form can be computed by
-repeatedly replacing a subterm of the form \isa{IF\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ x\ y{\isaliteral{29}{\isacharparenright}}\ z\ u} by
-\isa{IF\ b\ {\isaliteral{28}{\isacharparenleft}}IF\ x\ z\ u{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}IF\ y\ z\ u{\isaliteral{29}{\isacharparenright}}}, which has the same value. The following
-primitive recursive functions perform this task:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\ normif\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}normif\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ \ \ \ t\ e\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ t\ e{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}normif\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ \ \ \ t\ e\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ t\ e{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}normif\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ u\ f\ {\isaliteral{3D}{\isacharequal}}\ normif\ b\ {\isaliteral{28}{\isacharparenleft}}normif\ t\ u\ f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}normif\ e\ u\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ norm\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}norm\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ CIF\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}norm\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ VIF\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}norm\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ normif\ b\ {\isaliteral{28}{\isacharparenleft}}norm\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}norm\ e{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-Their interplay is tricky; we leave it to you to develop an
-intuitive understanding. Fortunately, Isabelle can help us to verify that the
-transformation preserves the value of the expression:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}norm\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ valif\ b\ env{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-The proof is canonical, provided we first show the following simplification
-lemma, which also helps to understand what \isa{normif} does:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ e{\isaliteral{2E}{\isachardot}}\ valif\ {\isaliteral{28}{\isacharparenleft}}normif\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ valif\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ env{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-Note that the lemma does not have a name, but is implicitly used in the proof
-of the theorem shown above because of the \isa{{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}} attribute.
-
-But how can we be sure that \isa{norm} really produces a normal form in
-the above sense? We define a function that tests If-expressions for normality:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\ normal\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}normal{\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}normal{\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}normal{\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}normal\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ normal\ e\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
-\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}case\ b\ of\ CIF\ b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ True\ {\isaliteral{7C}{\isacharbar}}\ VIF\ x\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ True\ {\isaliteral{7C}{\isacharbar}}\ IF\ x\ y\ z\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-Now we prove \isa{normal\ {\isaliteral{28}{\isacharparenleft}}norm\ b{\isaliteral{29}{\isacharparenright}}}. Of course, this requires a lemma about
-normality of \isa{normif}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ e{\isaliteral{2E}{\isachardot}}\ normal{\isaliteral{28}{\isacharparenleft}}normif\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}normal\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ normal\ e{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\medskip
-How do we come up with the required lemmas? Try to prove the main theorems
-without them and study carefully what \isa{auto} leaves unproved. This
-can provide the clue. The necessity of universal quantification
-(\isa{{\isaliteral{5C3C666F72616C6C3E}{\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{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}) rather than
- equalities (\isa{{\isaliteral{3D}{\isacharequal}}}).)
-\end{exercise}
-\index{boolean expressions example|)}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: