Changed part of the examples to int.
%
\begin{isabellebody}%
\def\isabellecontext{Examples{\isadigit{1}}}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Examples{\isadigit{1}}\isanewline
\isakeyword{imports}\ Examples\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{Use of Locales in Theories and Proofs
\label{sec:interpretation}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Locales can also be interpreted in the contexts of theories and
structured proofs. These interpretations are dynamic, too.
Conclusions of locales will be propagated to the current theory or
the current proof context.%
\footnote{Strictly speaking, only interpretation in theories is
dynamic since it is not possible to change locales or the locale
hierarchy from within a proof.}
The focus of this section is on
interpretation in theories, but we will also encounter
interpretations in proofs, in
Section~\ref{sec:local-interpretation}.
As an example, consider the type of integers \isa{int}. The
relation \isa{op\ {\isasymle}} is a total order over \isa{int},
divisibility \isa{op\ dvd} forms a distributive lattice. We start with the
interpretation that \isa{op\ {\isasymle}} is a partial order. The facilities of
the interpretation command are explored gradually in three versions.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{First Version: Replacement of Parameters Only
\label{sec:po-first}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The command \isakeyword{interpretation} is for the interpretation of
locale in theories. In the following example, the parameter of locale
\isa{partial{\isacharunderscore}order} is replaced by \isa{op\ {\isasymle}} and the locale instance is interpreted in the current
theory.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimvisible
\ \ %
\endisadelimvisible
%
\isatagvisible
\isacommand{interpretation}\isamarkupfalse%
\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
\begin{isamarkuptxt}%
\normalsize
The argument of the command is a simple \emph{locale expression}
consisting of the name of the interpreted locale, which is
preceded by the qualifier \isa{int{\isacharcolon}} and succeeded by a
white-space-separated list of terms, which provide a full
instantiation of the locale parameters. The parameters are referred
to by order of declaration, which is also the order in which
\isakeyword{print\_locale} outputs them.
[TODO: Introduce morphisms. Reference to \ref{sec:locale-expressions}.]
The command creates the goal
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ partial{\isacharunderscore}order\ op\ {\isasymle}%
\end{isabelle} which can be shown easily:%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ unfold{\isacharunderscore}locales\ auto%
\endisatagvisible
{\isafoldvisible}%
%
\isadelimvisible
%
\endisadelimvisible
%
\begin{isamarkuptext}%
The effect of the command is that instances of all
conclusions of the locale are available in the theory, where names
are prefixed by the qualifier. For example, transitivity for \isa{int} is named \isa{int{\isachardot}trans} and is the following
theorem:
\begin{isabelle}%
\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z%
\end{isabelle}
It is not possible to reference this theorem simply as \isa{trans}, which prevents unwanted hiding of existing theorems of the
theory by an interpretation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Second Version: Replacement of Definitions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Not only does the above interpretation qualify theorem names.
The prefix \isa{int} is applied to all names introduced in locale
conclusions including names introduced in definitions. The
qualified name \isa{int{\isachardot}less} refers to
the interpretation of the definition, which is \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}}.
Qualified name and expanded form may be used almost
interchangeably.%
\footnote{Since \isa{op\ {\isasymle}} is polymorphic, for \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}} a
more general type will be inferred than for \isa{int{\isachardot}less} which
is over type \isa{int}.}
The latter is preferred on output, as for example in the theorem
\isa{int{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
\ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\isanewline
\isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z%
\end{isabelle}
Both notations for the strict order are not satisfactory. The
constant \isa{op\ {\isacharless}} is the strict order for \isa{int}.
In order to allow for the desired replacement, interpretation
accepts \emph{equations} in addition to the parameter instantiation.
These follow the locale expression and are indicated with the
keyword \isakeyword{where}. The revised interpretation follows.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: