doc-src/Locales/Locales/Examples3.thy

 theory Examples3
-imports Examples "~~/src/HOL/Number_Theory/UniqueFactorization"
+imports Examples
 begin
-hide %invisible const Lattices.lattice
-  (* imported again through Number_Theory *)
 text {* \vspace{-5ex} *}
 subsection {* Third Version: Local Interpretation
   \label{sec:local-interpretation} *}
 
 text {* In the above example, the fact that @{term "op \<le>"} is a partial
   order for the integers was used in the second goal to
   discharge the premise in the definition of @{text "op \<sqsubset>"}.  In
   general, proofs of the equations not only may involve definitions
-  fromthe interpreted locale but arbitrarily complex arguments in the
+  from the interpreted locale but arbitrarily complex arguments in the
   context of the locale.  Therefore is would be convenient to have the
   interpreted locale conclusions temporary available in the proof.
   This can be achieved by a locale interpretation in the proof body.
   The command for local interpretations is \isakeyword{interpret}.  We
   repeat the example from the previous section to illustrate this. *}

   and proved by assumption (Isar short hand ``.'').  It enriches the
   local proof context by the theorems
   also obtained in the interpretation from Section~\ref{sec:po-first},
   and @{text int.less_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 a
+  leaving the proof context --- that is, after the succeeding
   \isakeyword{next} or \isakeyword{qed} statement. *}
 
 
 subsection {* Further Interpretations *}
 
 text {* Further interpretations are necessary for
-  the other locales.  In @{text lattice} the operations @{text \<sqinter>} and
-  @{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"} and
-  @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}.  The entire proof for the
+  the other locales.  In @{text lattice} the operations~@{text \<sqinter>}
+  and~@{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"}
+  and @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}.  The entire proof for the
   interpretation is reproduced to give an example of a more
-  elaborate interpretation proof.  *}
+  elaborate interpretation proof.  Note that the equations are named
+  so they can be used in a later example.  *}
 
   interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where "lattice.meet op \<le> (x::int) y = min x y"
-      and "lattice.join op \<le> (x::int) y = max x y"
+    where int_min_eq: "lattice.meet op \<le> (x::int) y = min x y"
+      and int_max_eq: "lattice.join op \<le> (x::int) y = max x y"
   proof -
     show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
       txt {* \normalsize We have already shown that this is a partial
 	order, *}
       apply unfold_locales
       txt {* \normalsize hence only the lattice axioms remain to be
-	shown: @{subgoals [display]}  After unfolding @{text is_inf} and
-	@{text is_sup}, *}
+	shown.
+        @{subgoals [display]}
+	By @{text is_inf} and @{text is_sup}, *}
       apply (unfold int.is_inf_def int.is_sup_def)
-      txt {* \normalsize the goals become @{subgoals [display]}
-	This can be solved by Presburger arithmetic, which is contained
-	in @{text arith}. *}
+      txt {* \normalsize the goals are transformed to these
+	statements:
+	@{subgoals [display]}
+	This is Presburger arithmetic, which can be solved by the
+	method @{text arith}. *}
       by arith+
     txt {* \normalsize In order to show the equations, we put ourselves
       in a situation where the lattice theorems can be used in a
       convenient way. *}
     then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .

   @{thm [source] int.less_total} from locale @{text total_order}: \\
   \quad @{thm int.less_total}
 \end{tabular}
 \end{center}
 \hrule
-\caption{Interpreted theorems for @{text \<le>} on the integers.}
+\caption{Interpreted theorems for~@{text \<le>} on the integers.}
 \label{tab:int-lattice}
 \end{table}
 
 \begin{itemize}
 \item
   Locale @{text distrib_lattice} was also interpreted.  Since the
-  locale hierarcy reflects that total orders are distributive
+  locale hierarchy reflects that total orders are distributive
   lattices, the interpretation of the latter was inserted
   automatically with the interpretation of the former.  In general,
-  interpretation of a locale will also interpret all locales further
-  up in the hierarchy, regardless whether imported or proved via the
-  \isakeyword{sublocale} command.
+  interpretation traverses the locale hierarchy upwards and interprets
+  all encountered locales, regardless whether imported or proved via
+  the \isakeyword{sublocale} command.  Existing interpretations are
+  skipped avoiding duplicate work.
 \item
-  Theorem @{thm [source] int.less_total} makes use of @{term "op <"}
+  The predicate @{term "op <"} appears in theorem @{thm [source]
+  int.less_total}
   although an equation for the replacement of @{text "op \<sqsubset>"} was only
-  given in the interpretation of @{text partial_order}.  These
-  equations are pushed downwards the hierarchy for related
-  interpretations --- that is, for interpretations that share the
-  instance for parameters they have in common.
+  given in the interpretation of @{text partial_order}.  The
+  interpretation equations are pushed downwards the hierarchy for
+  related interpretations --- that is, for interpretations that share
+  the instances of parameters they have in common.
 \end{itemize}
-  In the next section, the divisibility relation on the natural
-  numbers will be explored.
   *}
-
-
-subsection {* Interpretations for Divisibility *}
-
-text {* In this section, further examples of interpretations are
-  presented.  Impatient readers may skip this section at first
-  reading.
-
-  Divisibility on the natural numbers is a distributive lattice
-  but not a total order.  Interpretation again proceeds
-  incrementally.  In order to distinguish divisibility from the order
-  relation $\le$, we use the qualifier @{text nat_dvd} for
-  divisibility. *}
-
-  interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-    where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-  proof -
-    show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-      by unfold_locales (auto simp: dvd_def)
-    then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
-    show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-      apply (unfold nat_dvd.less_def)
-      apply auto
-      done
-  qed
-
-text {* Note that in Isabelle/HOL there is no operator for strict
-  divisibility.  Instead, we substitute @{term "x dvd y \<and> x \<noteq> y"}.  *}
-
-  interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-    where nat_dvd_meet_eq:
-	"lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
-      and nat_dvd_join_eq:
-	"lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
-  proof -
-    show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-      apply unfold_locales
-      apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
-      apply (rule_tac x = "gcd x y" in exI)
-      apply auto [1]
-      apply (rule_tac x = "lcm x y" in exI)
-      apply (auto intro: lcm_least_nat)
-      done
-    then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
-    show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
-      apply (auto simp add: expand_fun_eq)
-      apply (unfold nat_dvd.meet_def)
-      apply (rule the_equality)
-      apply (unfold nat_dvd.is_inf_def)
-      by auto
-    show "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
-      apply (auto simp add: expand_fun_eq)
-      apply (unfold nat_dvd.join_def)
-      apply (rule the_equality)
-      apply (unfold nat_dvd.is_sup_def)
-      apply (auto intro: lcm_least_nat iff: lcm_unique_nat)
-      done
-  qed
-
-text {* The replacement equations @{thm [source] nat_dvd_meet_eq} and
-  @{thm [source] nat_dvd_join_eq} are theorems of current theories.
-  They are named so that they can be used in the main part of the
-  subsequent interpretation. *}
-
-  interpretation %visible nat_dvd:
-    distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-    apply unfold_locales
-    txt {* \normalsize @{subgoals [display]}
-      Distributivity of lattice meet and join needs to be shown.  This is
-      distributivity of gcd and lcm, as becomes apparent when unfolding
-      the replacement equations from the previous interpretation: *}
-    unfolding nat_dvd_meet_eq nat_dvd_join_eq
-    txt {* \normalsize @{subgoals [display]}
-      This is a result of number theory: *}
-    by (rule UniqueFactorization.gcd_lcm_distrib_nat)
-
-text {* Theorems that are available in the theory after these
-  interpretations are shown in Table~\ref{tab:nat-dvd-lattice}.
-
-\begin{table}
-\hrule
-\vspace{2ex}
-\begin{center}
-\begin{tabular}{l}
-  @{thm [source] nat_dvd.less_def} from locale @{text partial_order}: \\
-  \quad @{thm nat_dvd.less_def} \\
-  @{thm [source] nat_dvd.meet_left} from locale @{text lattice}: \\
-  \quad @{thm nat_dvd.meet_left} \\
-  @{thm [source] nat_dvd.join_distr} from locale @{text distrib_lattice}: \\
-  \quad @{thm nat_dvd.join_distr} \\
-\end{tabular}
-\end{center}
-\hrule
-\caption{Interpreted theorems for @{text dvd} on the natural numbers.}
-\label{tab:nat-dvd-lattice}
-\end{table}
-  *}
-
-
-subsection {* Inspecting Interpretations of a Locale *}
 
 text {* The interpretations for a locale $n$ within the current
   theory may be inspected with \isakeyword{print\_interps}~$n$.  This
   prints the list of instances of $n$, for which interpretations exist.
   For example, \isakeyword{print\_interps} @{term partial_order}
   outputs the following:
+\begin{small}
 \begin{alltt}
   int! : partial_order "op \(\le\)"
-  nat_dvd! : partial_order "op dvd"
 \end{alltt}
-  The interpretation qualifiers on the left are decorated with an
-  exclamation point, which means that they are mandatory.  Qualifiers
+\end{small}
+  Of course, there is only one interpretation.
+  The interpretation qualifier on the left is decorated with an
+  exclamation point.  This means that it is mandatory.  Qualifiers
   can either be \emph{mandatory} or \emph{optional}, designated by
   ``!'' or ``?'' respectively.  Mandatory qualifiers must occur in a
   name reference while optional ones need not.  Mandatory qualifiers
-  prevent accidental hiding of names, while optional qualifers can be
+  prevent accidental hiding of names, while optional qualifiers can be
   more convenient to use.  For \isakeyword{interpretation}, the
-  default for qualifiers without an explicit designator is ``!''.
+  default is ``!''.
 *}
 
 
 section {* Locale Expressions \label{sec:expressions} *}
 
 text {*
-  A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>}
+  A map~@{term \<phi>} between partial orders~@{text \<sqsubseteq>} and~@{text \<preceq>}
   is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq>
   \<phi> y"}.  This situation is more complex than those encountered so
   far: it involves two partial orders, and it is desirable to use the
   existing locale for both.
 
   A locale for order preserving maps requires three parameters: @{text
-  le} (\isakeyword{infixl}~@{text \<sqsubseteq>}), @{text le'}
-  (\isakeyword{infixl}~@{text \<preceq>}) for the orders and @{text \<phi>} for the
-  map.
+  le}~(\isakeyword{infixl}~@{text \<sqsubseteq>}) and @{text
+  le'}~(\isakeyword{infixl}~@{text \<preceq>}) for the orders and~@{text \<phi>}
+  for the map.
 
   In order to reuse the existing locale for partial orders, which has
-  the single parameter @{text le}, it must be imported twice, once
-  mapping its parameter to @{text le} (\isakeyword{infixl}~@{text \<sqsubseteq>})
-  from the new locale and once to @{text le'}
-  (\isakeyword{infixl}~@{text \<preceq>}).  This can be achieved with a locale
+  the single parameter~@{text le}, it must be imported twice, once
+  mapping its parameter to~@{text le} from the new locale and once
+  to~@{text le'}.  This can be achieved with a compound locale
   expression.
 
-  A \emph{locale expression} is a sequence of \emph{locale instances}
-  separated by ``$\textbf{+}$'' and followed by a \isakeyword{for}
+  In general, a locale expression is a sequence of \emph{locale instances}
+  separated by~``$\textbf{+}$'' and followed by a \isakeyword{for}
   clause.
-An instance has the following format:
+  An instance has the following format:
 \begin{quote}
   \textit{qualifier} \textbf{:} \textit{locale-name}
   \textit{parameter-instantiation}
 \end{quote}
   We have already seen locale instances as arguments to
   \isakeyword{interpretation} in Section~\ref{sec:interpretation}.
-  The qualifier serves to disambiguate the names from different
-  instances of the same locale.
-
-  Since the parameters @{text le} and @{text le'} are to be partial
+  As before, the qualifier serves to disambiguate names from
+  different instances of the same locale.  While in
+  \isakeyword{interpretation} qualifiers default to mandatory, in
+  import and in the \isakeyword{sublocale} command, they default to
+  optional.
+
+  Since the parameters~@{text le} and~@{text le'} are to be partial
   orders, our locale for order preserving maps will import the these
   instances:
+\begin{small}
 \begin{alltt}
   le: partial_order le
   le': partial_order le'
 \end{alltt}
-  For matter of convenience we choose the parameter names also as
-  qualifiers.  This is an arbitrary decision.  Technically, qualifiers
+\end{small}
+  For matter of convenience we choose to name parameter names and
+  qualifiers alike.  This is an arbitrary decision.  Technically, qualifiers
   and parameters are unrelated.
 
   Having determined the instances, let us turn to the \isakeyword{for}
   clause.  It serves to declare locale parameters in the same way as
   the context element \isakeyword{fixes} does.  Context elements can
   only occur after the import section, and therefore the parameters
-  referred to inthe instances must be declared in the \isakeyword{for}
-  clause.%
-\footnote{Since all parameters can be declared in the \isakeyword{for}
-  clause, the context element \isakeyword{fixes} is not needed in
-  locales.  It is provided for compatibility with the long goals
-  format, where the context element also occurs.}
-  The \isakeyword{for} clause is also where the syntax of these
+  referred to in the instances must be declared in the \isakeyword{for}
+  clause.  The \isakeyword{for} clause is also where the syntax of these
   parameters is declared.
 
-  Two context elements for the map parameter @{text \<phi>} and the
-  assumptions that it is order perserving complete the locale
+  Two context elements for the map parameter~@{text \<phi>} and the
+  assumptions that it is order preserving complete the locale
   declaration. *}
 
   locale order_preserving =
     le: partial_order le + le': partial_order le'
       for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +

     assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
 
 text (in order_preserving) {* Here are examples of theorems that are
   available in the locale:
 
-  @{thm [source] hom_le}: @{thm hom_le}
-
-  @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
-
-  @{thm [source] le'.less_le_trans}:
-  @{thm [display, indent=2] le'.less_le_trans}
-
+  \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le}
+
+  \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
+
+  \hspace*{1em}@{thm [source] le'.less_le_trans}:
+  @{thm [display, indent=4] le'.less_le_trans}
   While there is infix syntax for the strict operation associated to
   @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
   "op \<preceq>"}.  The abbreviation @{text less} with its infix syntax is only
   available for the original instance it was declared for.  We may
-  introduce the abbreviation @{text less'} with infix syntax @{text \<prec>}
-  with this declaration: *}
+  introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>}
+  with the following declaration: *}
 
   abbreviation (in order_preserving)
     less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
 
 text (in order_preserving) {* Now the theorem is displayed nicely as
   @{thm [source]  le'.less_le_trans}:
   @{thm [display, indent=2] le'.less_le_trans} *}
 
-
-subsection {* Default Instantiations and Implicit Parameters *}
-
-text {* It is possible to omit parameter instantiations in a locale
-  expression.  In that case, the instantiation defaults to the name of
-  the parameter itself.  That is, the locale expression @{text
+text {* There are short notations for locale expressions.  These are
+  discussed in the following. *}
+
+
+subsection {* Default Instantiations *}
+
+text {* 
+  It is possible to omit parameter instantiations.  The
+  instantiation then defaults to the name of
+  the parameter itself.  For example, the locale expression @{text
   partial_order} is short for @{text "partial_order le"}, since the
-  locale's single parameter is @{text le}.  We took advantage of this
-  short hand in the \isakeyword{sublocale} declarations of
+  locale's single parameter is~@{text le}.  We took advantage of this
+  in the \isakeyword{sublocale} declarations of
   Section~\ref{sec:changing-the-hierarchy}. *}
 
+
+subsection {* Implicit Parameters \label{sec:implicit-parameters} *}
 
 text {* In a locale expression that occurs within a locale
   declaration, omitted parameters additionally extend the (possibly
   empty) \isakeyword{for} clause.
 
-  The \isakeyword{for} clause is a
-  general construct of Isabelle/Isar to mark names from the preceding
-  declaration as ``arbitrary but fixed''.  This is necessary for
-  example, if the name is already bound in a surrounding context.  In
-  a locale expression, names occurring in parameter instantiations
-  should be bound by a \isakeyword{for} clause whenever these names
-  are not introduced elsewhere in the context --- for example, on the
-  left hand side of a \isakeyword{sublocale} declaration.
+  The \isakeyword{for} clause is a general construct of Isabelle/Isar
+  to mark names occurring in the preceding declaration as ``arbitrary
+  but fixed''.  This is necessary for example, if the name is already
+  bound in a surrounding context.  In a locale expression, names
+  occurring in parameter instantiations should be bound by a
+  \isakeyword{for} clause whenever these names are not introduced
+  elsewhere in the context --- for example, on the left hand side of a
+  \isakeyword{sublocale} declaration.
 
   There is an exception to this rule in locale declarations, where the
-  \isakeyword{for} clause servers to declare locale parameters.  Here,
+  \isakeyword{for} clause serves to declare locale parameters.  Here,
   locale parameters for which no parameter instantiation is given are
   implicitly added, with their mixfix syntax, at the beginning of the
   \isakeyword{for} clause.  For example, in a locale declaration, the
   expression @{text partial_order} is short for
+\begin{small}
 \begin{alltt}
   partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
 \end{alltt}
-  This short hand was used in the locale declarations of
+\end{small}
+  This short hand was used in the locale declarations throughout
   Section~\ref{sec:import}.
  *}
 
 text{*
-  The following locale declarations provide more examples.  A map
-  @{text \<phi>} is a lattice homomorphism if it preserves meet and
+  The following locale declarations provide more examples.  A
+  map~@{text \<phi>} is a lattice homomorphism if it preserves meet and
   join. *}
 
   locale lattice_hom =
     le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
     fixes \<phi>
     assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
       and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
 
-text {* We omit the parameter instantiation in the first instance of
-  @{term lattice}.  This causes the parameter @{text le} to be added
-  to the \isakeyword{for} clause, and the locale has parameters
-  @{text le} and @{text le'}.
+text {* The parameter instantiation in the first instance of @{term
+  lattice} is omitted.  This causes the parameter~@{text le} to be
+  added to the \isakeyword{for} clause, and the locale has
+  parameters~@{text le},~@{text le'} and, of course,~@{text \<phi>}.
 
   Before turning to the second example, we complete the locale by
-  provinding infix syntax for the meet and join operations of the
+  providing infix syntax for the meet and join operations of the
   second lattice.
 *}
 
   context lattice_hom begin
   abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
   abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
   end
 
-text {* The next example pushes the short hand facilities.  A
-  homomorphism is an endomorphism if both orders coincide. *}
+text {* The next example makes radical use of the short hand
+  facilities.  A homomorphism is an endomorphism if both orders
+  coincide. *}
 
   locale lattice_end = lattice_hom _ le
 
-text {* The notation @{text _} enables to omit a parameter in a
-  positional instantiation.  The omitted parameter, @{text le} becomes
+text {* The notation~@{text _} enables to omit a parameter in a
+  positional instantiation.  The omitted parameter,~@{text le} becomes
   the parameter of the declared locale and is, in the following
-  position used to instantiate the second parameter of @{text
+  position, used to instantiate the second parameter of @{text
   lattice_hom}.  The effect is that of identifying the first in second
   parameter of the homomorphism locale. *}
 
 text {* The inheritance diagram of the situation we have now is shown
   in Figure~\ref{fig:hom}, where the dashed line depicts an
-  interpretation which is introduced below.  Renamings are
-  indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at the
-  inheritance diagram it would seem
+  interpretation which is introduced below.  Parameter instantiations
+  are indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at
+  the inheritance diagram it would seem
   that two identical copies of each of the locales @{text
   partial_order} and @{text lattice} are imported by @{text
   lattice_end}.  This is not the case!  Inheritance paths with
   identical morphisms are automatically detected and
   the conclusions of the respective locales appear only once.

   Theorems and other declarations --- syntax, in particular --- from
   the locale @{text order_preserving} are now active in @{text
   lattice_hom}, for example
   @{thm [source] hom_le}:
   @{thm [display, indent=2] hom_le}
+  This theorem will be useful in the following section.
   *}
 
-(*
+
 section {* Conditional Interpretation *}
+
+text {* There are situations where an interpretation is not possible
+  in the general case since the desired property is only valid if
+  certain conditions are fulfilled.  Take, for example, the function
+  @{text "\<lambda>i. n * i"} that scales its argument by a constant factor.
+  This function is order preserving (and even a lattice endomorphism)
+  with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}.
+
+  It is not possible to express this using a global interpretation,
+  because it is in general unspecified whether~@{term n} is
+  non-negative, but one may make an interpretation in an inner context
+  of a proof where full information is available.
+  This is not fully satisfactory either, since potentially
+  interpretations may be required to make interpretations in many
+  contexts.  What is
+  required is an interpretation that depends on the condition --- and
+  this can be done with the \isakeyword{sublocale} command.  For this
+  purpose, we introduce a locale for the condition. *}
 
   locale non_negative =
     fixes n :: int
-    assumes non_negative: "0 \<le> n"
-
-  interpretation partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where "partial_order.less op \<le> (x::int) y = (x < y)"
-    sorry
-
-  sublocale non_negative \<subseteq> order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
-    apply unfold_locales using non_negative apply - by (rule mult_left_mono)
-
-  interpretation lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
-    where min_eq: "lattice.meet op \<le> (x::int) y = min x y"
-      and max_eq: "lattice.join op \<le> (x::int) y = max x y"
-    sorry
-
-    apply unfold_locales unfolding is_inf_def is_sup_def by arith+
-
-
-  sublocale non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
-    apply unfold_locales unfolding min_eq max_eq apply (case_tac "x \<le> y")
-    unfolding min_def apply auto apply arith
-    apply (rule sym)
-    apply (rule the_equality)
-  proof
-
-  locale fspace_po = partial_order
-  sublocale fspace_po \<subseteq> fspace: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
-(* fspace needed to disambiguate less etc *)
-apply unfold_locales
-apply auto
-apply (rule) apply auto apply (blast intro: trans) done
-
-*)
+    assumes non_neg: "0 \<le> n"
+
+text {* It is again convenient to make the interpretation in an
+  incremental fashion, first for order preserving maps, the for
+  lattice endomorphisms. *}
+
+  sublocale non_negative \<subseteq>
+      order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
+    using non_neg by unfold_locales (rule mult_left_mono)
+
+text {* While the proof of the previous interpretation
+  is straightforward from monotonicity lemmas for~@{term "op *"}, the
+  second proof follows a useful pattern. *}
+
+  sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
+  proof (unfold_locales, unfold int_min_eq int_max_eq)
+    txt {* \normalsize Unfolding the locale predicates \emph{and} the
+      interpretation equations immediately yields two subgoals that
+      reflect the core conjecture.
+      @{subgoals [display]}
+      It is now necessary to show, in the context of @{term
+      non_negative}, that multiplication by~@{term n} commutes with
+      @{term min} and @{term max}. *}
+  qed (auto simp: hom_le)
+
+text (in order_preserving) {* The lemma @{thm [source] hom_le}
+  simplifies a proof that would have otherwise been lengthy and we may
+  consider making it a default rule for the simplifier: *}
+
+  lemmas (in order_preserving) hom_le [simp]
+
+
+subsection {* Avoiding Infinite Chains of Interpretations
+  \label{sec:infinite-chains} *}
+
+text {* Similar situations arise frequently in formalisations of
+  abstract algebra where it is desirable to express that certain
+  constructions preserve certain properties.  For example, polynomials
+  over rings are rings, or --- an example from the domain where the
+  illustrations of this tutorial are taken from --- a partial order
+  may be obtained for a function space by point-wise lifting of the
+  partial order of the co-domain.  This corresponds to the following
+  interpretation: *}
+
+  sublocale %visible partial_order \<subseteq> f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
+    oops
+
+text {* Unfortunately this is a cyclic interpretation that leads to an
+  infinite chain, namely
+  @{text [display, indent=2] "partial_order \<subseteq> partial_order (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) \<subseteq>
+  partial_order (\<lambda>f g. \<forall>x y. f x y \<sqsubseteq> g x y) \<subseteq>  \<dots>"}
+  and the interpretation is rejected.
+
+  Instead it is necessary to declare a locale that is logically
+  equivalent to @{term partial_order} but serves to collect facts
+  about functions spaces where the co-domain is a partial order, and
+  to make the interpretation in its context: *}
+
+  locale fun_partial_order = partial_order
+
+  sublocale fun_partial_order \<subseteq>
+      f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
+    by unfold_locales (fast,rule,fast,blast intro: trans)
+
+text {* It is quite common in abstract algebra that such a construction
+  maps a hierarchy of algebraic structures (or specifications) to a
+  related hierarchy.  By means of the same lifting, a function space
+  is a lattice if its co-domain is a lattice: *}
+
+  locale fun_lattice = fun_partial_order + lattice
+
+  sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
+    proof unfold_locales
+    fix f g
+    have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
+      apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
+    then show "\<exists>inf. partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g inf"
+      by fast
+  next
+    fix f g
+    have "partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<squnion> g x)"
+      apply (rule is_supI) apply rule+ apply (drule spec, assumption)+ done
+    then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup"
+      by fast
+  qed
+
 
 section {* Further Reading *}
 
 text {* More information on locales and their interpretation is
   available.  For the locale hierarchy of import and interpretation
-  dependencies see \cite{Ballarin2006a}; interpretations in theories
-  and proofs are covered in \cite{Ballarin2006b}.  In the latter, I
+  dependencies see~\cite{Ballarin2006a}; interpretations in theories
+  and proofs are covered in~\cite{Ballarin2006b}.  In the latter, I
   show how interpretation in proofs enables to reason about families
   of algebraic structures, which cannot be expressed with locales
   directly.
 
-  Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction
+  Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction
   of axiomatic type classes through a combination with locale
   interpretation.  The result is a Haskell-style class system with a
   facility to generate ML and Haskell code.  Classes are sufficient for
   simple specifications with a single type parameter.  The locales for
   orders and lattices presented in this tutorial fall into this
   category.  Order preserving maps, homomorphisms and vector spaces,
   on the other hand, do not.
 
   The locales reimplementation for Isabelle 2009 provides, among other
-  improvements, a clean intergration with Isabelle/Isar's local theory
-  mechnisms, which are described in \cite{HaftmannWenzel2009}.
-
-  The original work of Kamm\"uller on locales \cite{KammullerEtAl1999}
-  may be of interest from a historical perspective.  The mathematical
-  background on orders and lattices is taken from Jacobson's textbook
-  on algebra \cite[Chapter~8]{Jacobson1985}.
+  improvements, a clean integration with Isabelle/Isar's local theory
+  mechanisms, which are described in another paper by Haftmann and
+  Wenzel~\cite{HaftmannWenzel2009}.
+
+  The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999}
+  may be of interest from a historical perspective.  My previous
+  report on locales and locale expressions~\cite{Ballarin2004a}
+  describes a simpler form of expressions than available now and is
+  outdated. The mathematical background on orders and lattices is
+  taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}.
 
   The sources of this tutorial, which include all proofs, are
   available with the Isabelle distribution at
   \url{http://isabelle.in.tum.de}.
   *}

 \caption{Syntax of Locale Commands.}
 \label{tab:commands}
 \end{table}
   *}
 
-text {* \textbf{Revision History.}  For the present third revision,
-  which was completed in October 2009, much of the explanatory text
-  has been rewritten.  In addition, inheritance of interpretation
-  equations, which was not available for Isabelle 2009, but in the
-  meantime has been implemented, is illustrated.  The second revision
-  accommodates changes introduced by the locales reimplementation for
-  Isabelle 2009.  Most notably, in complex specifications
-  (\emph{locale expressions}) renaming has been generalised to
-  instantiation.  *}
+text {* \textbf{Revision History.}  For the present third revision of
+  the tutorial, much of the explanatory text
+  was rewritten.  Inheritance of interpretation equations is
+  available with the forthcoming release of Isabelle, which at the
+  time of editing these notes is expected for the end of 2009.
+  The second revision accommodates changes introduced by the locales
+  reimplementation for Isabelle 2009.  Most notably locale expressions
+  have been generalised from renaming to instantiation.  *}
 
 text {* \textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
   Randy Pollack, Christian Sternagel and Makarius Wenzel have made
-  useful comments on earlier versions of this document. *}
+  useful comments on earlier versions of this document.  The section
+  on conditional interpretation was inspired by a number of e-mail
+  enquiries the author received from locale users, and which suggested
+  that this use case is important enough to deserve explicit
+  explanation.  The term \emph{conditional interpretation} is due to
+  Larry Paulson. *}
 
 end