diff -r 11aa41ed306d -r 1eced27ee0e1 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Sun Aug 28 19:42:10 2005 +0200 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Sun Aug 28 19:42:19 2005 +0200 @@ -7,6 +7,7 @@ \endisadelimtheory % \isatagtheory +\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -14,7 +15,6 @@ \isadelimtheory % \endisadelimtheory -\isamarkuptrue% % \isamarkupsubsection{Case Study: Boolean Expressions% } @@ -37,10 +37,10 @@ constants by negation and conjunction. The following datatype serves exactly that purpose:% \end{isamarkuptext}% -\isamarkupfalse% -\isacommand{datatype}\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex\isamarkuptrue% -% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex% \begin{isamarkuptext}% \noindent The two constants are represented by \isa{Const\ True} and @@ -56,15 +56,15 @@ \emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their values:% \end{isamarkuptext}% -\isamarkupfalse% -\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline -\isamarkupfalse% -\isacommand{primrec}\isanewline -{\isachardoublequote}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline -{\isachardoublequote}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline -{\isachardoublequote}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequote}\isanewline -{\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}\isamarkuptrue% -% +\isamarkuptrue% +\isacommand{consts}\isamarkupfalse% +\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isacommand{primrec}\isamarkupfalse% +\isanewline +{\isachardoublequoteopen}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent \subsubsection{If-Expressions} @@ -74,22 +74,22 @@ from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals (\isa{IF}):% \end{isamarkuptext}% -\isamarkupfalse% -\isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex\isamarkuptrue% -% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex% \begin{isamarkuptext}% \noindent The evaluation of If-expressions proceeds as for \isa{boolex}:% \end{isamarkuptext}% -\isamarkupfalse% -\isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline -\isamarkupfalse% -\isacommand{primrec}\isanewline -{\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline -{\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline -{\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}\isamarkuptrue% -% +\isamarkuptrue% +\isacommand{consts}\isamarkupfalse% +\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isacommand{primrec}\isamarkupfalse% +\isanewline +{\isachardoublequoteopen}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \subsubsection{Converting Boolean and If-Expressions} @@ -97,46 +97,46 @@ formulae, whereas \isa{ifex} is designed for efficiency. It is easy to translate from \isa{boolex} into \isa{ifex}:% \end{isamarkuptext}% -\isamarkupfalse% -\isacommand{consts}\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline -\isamarkupfalse% -\isacommand{primrec}\isanewline -{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline -{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline -{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequote}\isanewline -{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}bool{\isadigit{2}}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequote}\isamarkuptrue% -% +\isamarkuptrue% +\isacommand{consts}\isamarkupfalse% +\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline +\isacommand{primrec}\isamarkupfalse% +\isanewline +{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}bool{\isadigit{2}}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\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}% -\isamarkupfalse% -\isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isachardoublequoteopen}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof % \isatagproof -\isamarkuptrue% % \begin{isamarkuptxt}% \noindent The proof is canonical:% \end{isamarkuptxt}% -\isamarkupfalse% -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline -\isamarkupfalse% -\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline -\isamarkupfalse% -\isacommand{done}% +\isamarkuptrue% +\isacommand{apply}\isamarkupfalse% +{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline +\isacommand{apply}\isamarkupfalse% +{\isacharparenleft}auto{\isacharparenright}\isanewline +\isacommand{done}\isamarkupfalse% +% \endisatagproof {\isafoldproof}% % \isadelimproof % \endisadelimproof -\isamarkuptrue% % \begin{isamarkuptext}% \noindent @@ -150,57 +150,37 @@ \isa{IF\ b\ {\isacharparenleft}IF\ x\ z\ u{\isacharparenright}\ {\isacharparenleft}IF\ y\ z\ u{\isacharparenright}}, which has the same value. The following primitive recursive functions perform this task:% \end{isamarkuptext}% -\isamarkupfalse% -\isacommand{consts}\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline -\isamarkupfalse% -\isacommand{primrec}\isanewline -{\isachardoublequote}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline -{\isachardoublequote}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline -{\isachardoublequote}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequote}\isanewline +\isamarkuptrue% +\isacommand{consts}\isamarkupfalse% +\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline +\isacommand{primrec}\isamarkupfalse% \isanewline -\isamarkupfalse% -\isacommand{consts}\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline -\isamarkupfalse% -\isacommand{primrec}\isanewline -{\isachardoublequote}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline -{\isachardoublequote}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline -{\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}\isamarkuptrue% -% +{\isachardoublequoteopen}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{consts}\isamarkupfalse% +\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline +\isacommand{primrec}\isamarkupfalse% +\isanewline +{\isachardoublequoteopen}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\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}% -\isamarkupfalse% -\isacommand{theorem}\ {\isachardoublequote}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequote}% +\isamarkuptrue% +\isacommand{theorem}\isamarkupfalse% +\ {\isachardoublequoteopen}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof % \isatagproof -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -\isamarkuptrue% -% -\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}% \isamarkupfalse% -\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}% -\isadelimproof -% -\endisadelimproof -% -\isatagproof % \endisatagproof {\isafoldproof}% @@ -209,11 +189,22 @@ % \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% +\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline +\ \ {\isachardoublequoteopen}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof % \isatagproof +\isamarkupfalse% +\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -221,7 +212,22 @@ \isadelimproof % \endisadelimproof -\isamarkuptrue% +\isamarkupfalse% +% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +\isamarkupfalse% +\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof % \begin{isamarkuptext}% \noindent @@ -231,27 +237,30 @@ 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}% -\isamarkupfalse% -\isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline -\isamarkupfalse% -\isacommand{primrec}\isanewline -{\isachardoublequote}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline -{\isachardoublequote}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline -{\isachardoublequote}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline -\ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue% -% +\isamarkuptrue% +\isacommand{consts}\isamarkupfalse% +\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline +\isacommand{primrec}\isamarkupfalse% +\isanewline +{\isachardoublequoteopen}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline +{\isachardoublequoteopen}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline +\ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about normality of \isa{normif}:% \end{isamarkuptext}% -\isamarkupfalse% -\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}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequoteclose}% \isadelimproof % \endisadelimproof % \isatagproof +\isamarkupfalse% +\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -259,12 +268,15 @@ \isadelimproof % \endisadelimproof +\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof +\isamarkupfalse% +\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -272,7 +284,6 @@ \isadelimproof % \endisadelimproof -\isamarkuptrue% % \begin{isamarkuptext}% \medskip @@ -291,12 +302,22 @@ \end{exercise} \index{boolean expressions example|)}% \end{isamarkuptext}% +\isamarkuptrue% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% +\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof +\isamarkupfalse% +\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -304,12 +325,15 @@ \isadelimproof % \endisadelimproof +\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof +\isamarkupfalse% +\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -317,12 +341,15 @@ \isadelimproof % \endisadelimproof +\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof +\isamarkupfalse% +\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -330,12 +357,15 @@ \isadelimproof % \endisadelimproof +\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof +\isamarkupfalse% +\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -349,6 +379,7 @@ \endisadelimtheory % \isatagtheory +\isamarkupfalse% % \endisatagtheory {\isafoldtheory}%