--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Nov 08 00:00:47 2010 +0100
@@ -38,30 +38,30 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
-\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex%
+\ 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\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}.
+\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\ {\isasymRightarrow}\ bool}, which maps variables to their
+\emph{environment} of type \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}, which maps variables to their
values:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
-\ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequoteclose}%
+\ {\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}
@@ -73,18 +73,18 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
-\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex%
+\ 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\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-{\isachardoublequoteopen}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\ {\isacharbar}\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}%
+\ 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}
@@ -94,11 +94,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{primrec}\isamarkupfalse%
-\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\ {\isacharbar}\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}\ {\isacharbar}\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}%
+\ 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
@@ -106,7 +106,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequoteclose}%
+\ {\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
@@ -119,9 +119,9 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ b{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}auto{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
@@ -139,22 +139,22 @@
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\ {\isacharparenleft}IF\ b\ x\ y{\isacharparenright}\ z\ u} by
-\isa{IF\ b\ {\isacharparenleft}IF\ x\ z\ u{\isacharparenright}\ {\isacharparenleft}IF\ y\ z\ u{\isacharparenright}}, which has the same value. The following
+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\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-{\isachardoublequoteopen}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequoteclose}\ {\isacharbar}\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
+\ 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\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-{\isachardoublequoteopen}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequoteclose}%
+\ 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
@@ -163,7 +163,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ {\isachardoublequoteopen}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}norm\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ valif\ b\ env{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
@@ -184,8 +184,8 @@
\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}%
+\ {\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
@@ -215,26 +215,26 @@
\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{{\isacharbrackleft}simp{\isacharbrackright}} attribute.
+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\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-{\isachardoublequoteopen}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\ {\isacharbar}\isanewline
-{\isachardoublequoteopen}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\ {\isacharbar}\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}%
+\ 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\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
+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%
-\ {\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}%
+\ {\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
@@ -266,15 +266,15 @@
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{{\isasymforall}t\ e}) in the two lemmas is explained in
+(\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{{\isasymlongrightarrow}}) rather than
- equalities (\isa{{\isacharequal}}).)
+ 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}%