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

 \isadelimvisible
 %
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-The inner interpretation does not require an
-  elaborate new proof, it is immediate from the preceeding fact and
-  proved with ``.''.  Strict qualifiers are normally not necessary for
-  interpretations inside proofs, since these have only limited scope.
-
-  The above interpretation enriches the local proof context by
-  the very theorems also obtained in the interpretation from
-  Section~\ref{sec:po-first}, and \isa{nat{\isachardot}less{\isacharunderscore}def} may directly be
-  used to unfold the definition.  Theorems from the local
-  interpretation disappear after leaving the proof context --- that
-  is, after the closing \isakeyword{qed} --- and are
-  then replaced by those with the desired substitutions of the strict
-  order.%
+The inner interpretation does not require an elaborate new
+  proof, it is immediate from the preceding fact and proved with
+  ``.''.  It enriches the local proof context by the very theorems
+  also obtained in the interpretation from Section~\ref{sec:po-first},
+  and \isa{nat{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the
+  definition.  Theorems from the local interpretation disappear after
+  leaving the proof context --- that is, after the closing
+  \isakeyword{qed} --- and are then replaced by those with the desired
+  substitutions of the strict order.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Further Interpretations%
 }

 \isamarkuptrue%
 \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ arith{\isacharplus}%
 \begin{isamarkuptxt}%
 For the first of the equations, we refer to the theorem
-  generated in the previous interpretation.%
+  shown in the previous interpretation.%
 \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{by}\isamarkupfalse%

 \isadelimvisible
 %
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-The interpretation that the relation \isa{{\isasymle}} is a total
-  order follows next.%
+Next follows that \isa{{\isasymle}} is a total order.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimvisible
 %

 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}total{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isachardoublequoteopen}total{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ arith\isanewline
 \isacommand{qed}\isamarkupfalse%
 \ {\isacharparenleft}rule\ nat{\isacharunderscore}less{\isacharunderscore}eq\ nat{\isacharunderscore}meet{\isacharunderscore}eq\ nat{\isacharunderscore}join{\isacharunderscore}eq{\isacharparenright}{\isacharplus}%
 \endisatagvisible
 {\isafoldvisible}%

 \isadelimvisible
 %
 \endisadelimvisible
 %
 \begin{isamarkuptext}%
-Note that since the locale hierarchy reflects that total
+Since the locale hierarchy reflects that total
   orders are distributive lattices, an explicit interpretation of
   distributive lattices for the order relation on natural numbers is
   only necessary for mapping the definitions to the right operators on
   \isa{nat}.%
 \end{isamarkuptext}%

   incrementally.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{where}\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharcolon}\isanewline
+\ \ \ \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
 \endisadelimproof
 %

 \isadelimproof
 %
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-Equations \isa{nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq} and \isa{nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq} are named since they are handy in the proof of
-  the subsequent interpretation.%
+Equations \isa{nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq} and \isa{nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq} are used in the main part the subsequent
+  interpretation.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadeliminvisible
 %

 \end{table}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The full syntax of the interpretation commands is shown in
+The syntax of the interpretation commands is shown in
   Table~\ref{tab:commands}.  The grammar refers to
   \textit{expression}, which stands for a \emph{locale} expression.
   Locale expressions are discussed in the following section.%
 \end{isamarkuptext}%
 \isamarkuptrue%

   existing locale for both.
 
   Inspecting the grammar of locale commands in
   Table~\ref{tab:commands} reveals that the import of a locale can be
   more than just a single locale.  In general, the import is a
-  \emph{locale expression}.  These enable to combine locales
+  \emph{locale expression}, which enables to combine locales
   and instantiate parameters.  A locale expression is a sequence of
   locale \emph{instances} followed by an optional \isakeyword{for}
   clause.  Each instance consists of a locale reference, which may be
   preceded by a qualifer and succeeded by instantiations of the
   parameters of that locale.  Instantiations may be either positional
-  or through explicit parameter argument pairs.
+  or through explicit mappings of parameters to arguments.
 
   Using a locale expression, a locale for order
   preserving maps can be declared in the following way.%
 \end{isamarkuptext}%
 \isamarkuptrue%

 \ \ \ \ \ \ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 The second and third line contain the expression --- two
-  instances of the partial order locale with instantiations \isa{le}
+  instances of the partial order locale where the parameter is
+  instantiated to \isa{le}
   and \isa{le{\isacharprime}}, respectively.  The \isakeyword{for} clause consists
   of parameter declarations and is similar to the context element
   \isakeyword{fixes}.  The notable difference is that the
   \isakeyword{for} clause is part of the expression, and only
   parameters defined in the expression may occur in its instances.
 
-  Instances are \emph{morphisms} on locales.  Their effect on the
-  parameters is naturally lifted to terms, propositions and theorems,
+  Instances define \emph{morphisms} on locales.  Their effect on the
+  parameters is lifted to terms, propositions and theorems in the
+  canonical way,
   and thus to the assumptions and conclusions of a locale.  The
   assumption of a locale expression is the conjunction of the
   assumptions of the instances.  The conclusions of a sequence of
   instances are obtained by appending the conclusions of the
   instances in the order of the sequence.

 \isadeliminvisible
 %
 \endisadeliminvisible
 %
 \begin{isamarkuptext}%
-This example reveals that there is no infix syntax for the strict
-  version of \isa{{\isasympreceq}}!  This can be declared through an abbreviation.%
+This example reveals that there is no infix syntax for the
+  strict operation associated with \isa{{\isasympreceq}}.  This can be declared
+  through an abbreviation.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{abbreviation}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ order{\isacharunderscore}preserving{\isacharparenright}\isanewline
 \ \ \ \ less{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymprec}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}less{\isacharprime}\ {\isasymequiv}\ partial{\isacharunderscore}order{\isachardot}less\ le{\isacharprime}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 Now the theorem is displayed nicely as
-  \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}.%
+  \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
+  \begin{isabelle}%
+\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z%
+\end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Qualifiers not only apply to theorem names, but also to names
-  introduced by definitions and abbreviations.  In locale
-  \isa{partial{\isacharunderscore}order} the full name of the strict order of \isa{{\isasymsqsubseteq}} is
-  \isa{le{\isachardot}less} and therefore \isa{le{\isacharprime}{\isachardot}less} is the full name of
-  the strict order of \isa{{\isasympreceq}}.  Hence, the equation in the
-  abbreviation above could have been also written as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
+  introduced by definitions and abbreviations.  For example, in \isa{partial{\isacharunderscore}order} the name \isa{less} abbreviates \isa{op\ {\isasymsqsubset}}.  Therefore, in \isa{order{\isacharunderscore}preserving}
+  the qualified name \isa{le{\isachardot}less} abbreviates \isa{op\ {\isasymsqsubset}} and \isa{le{\isacharprime}{\isachardot}less} abbreviates \isa{op\ {\isasymprec}}.  Hence, the equation in the abbreviation
+  above could have been written more concisely as \isa{less{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}less}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Readers may find the declaration of locale \isa{order{\isacharunderscore}preserving} a little awkward, because the declaration and

   provided for it.  In positional instantiations, a parameter position
   may be skipped with an underscore, and it is allowed to give fewer
   instantiation terms than the instantiated locale's number of
   parameters.  In named instantiations, instantiation pairs for
   certain parameters may simply be omitted.  Untouched parameters are
-  declared by the locale expression and with their concrete syntax by
-  implicitly adding them to the beginning of the \isakeyword{for}
-  clause.
+  implicitly declared by the locale expression and with their concrete
+  syntax.  In the sequence of parameters, they appear before the
+  parameters from the \isakeyword{for} clause.
 
   The following locales illustrate this.  A map \isa{{\isasymphi}} is a
   lattice homomorphism if it preserves meet and join.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
 \ lattice{\isacharunderscore}hom\ {\isacharequal}\isanewline
 \ \ \ \ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
-\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
 \ \ \isacommand{abbreviation}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline
 \ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{abbreviation}\isamarkupfalse%

 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \isacommand{locale}\isamarkupfalse%
 \ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
 \begin{isamarkuptext}%
-In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and then used to instantiate
+In this declaration, the first parameter of \isa{lattice{\isacharunderscore}hom}, \isa{le}, is untouched and is then used to instantiate
   the second parameter.  Its concrete syntax is preserved.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%

 \endisadelimproof
 %
 \begin{isamarkuptext}%
 Theorems and other declarations --- syntax, in particular --- from
   the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
-
-  \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
-  \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}%
+  \isa{hom{\isacharunderscore}le}:
+  \begin{isabelle}%
+\ \ {\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y%
+\end{isabelle}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsection{Further Reading%
 }

   & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
   & | & \textbf{print\_locales} 
 \end{tabular}
 \end{center}
 \hrule
-\caption{Syntax of Locale Commands (abridged).}
+\caption{Syntax of Locale Commands.}
 \label{tab:commands}
 \end{table}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %