doc-src/Locales/Locales/document/Examples2.tex

Default mode of qualifiers in locale commands.

%
\begin{isabellebody}%
\def\isabellecontext{Examples{\isadigit{2}}}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Examples{\isadigit{2}}\isanewline
\isakeyword{imports}\ Examples\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
This is achieved by unfolding suitable equations during
  interpretation.  These equations are given after the keyword
  \isakeyword{where} and require proofs.  The revised command
  that replaces \isa{{\isasymsqsubset}} by \isa{{\isacharless}}, is:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimvisible
%
\endisadelimvisible
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}%
\begin{isamarkuptxt}%
The goals are \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}\isanewline
\ {\isadigit{2}}{\isachardot}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ x\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}%
\end{isabelle}
    The proof that \isa{{\isasymle}} is a partial order is as above.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\ auto%
\begin{isamarkuptxt}%
The second goal is shown by unfolding the
    definition of \isa{partial{\isacharunderscore}order{\isachardot}less}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def\ {\isacharbrackleft}OF\ {\isacharbackquoteopen}partial{\isacharunderscore}order\ op\ {\isasymle}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagvisible
{\isafoldvisible}%
%
\isadelimvisible
%
\endisadelimvisible
%
\begin{isamarkuptext}%
Note that the above proof is not in the context of a locale.
  Hence, the correct interpretation of \isa{partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def} is obtained manually with \isa{OF}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: