doc-src/Locales/Locales/Examples3.thy
changeset 32981 0114e04a0d64
parent 32804 ca430e6aee1c
child 32982 40810d98f4c9
--- a/doc-src/Locales/Locales/Examples3.thy	Thu Oct 15 22:06:43 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Thu Oct 15 22:07:18 2009 +0200
@@ -1,77 +1,86 @@
 theory Examples3
-imports Examples
+imports Examples "~~/src/HOL/Number_Theory/UniqueFactorization"
 begin
-subsection {* Third Version: Local Interpretation *}
+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 @{text \<le>} is a partial
-  order for the natural numbers was used in the proof of the
-  second goal.  In general, proofs of the equations may involve
-  theorems implied by the fact the assumptions of the instantiated
-  locale hold for the instantiating structure.  If these theorems have
-  been shown abstractly in the locale they can be made available
-  conveniently in the context through an auxiliary local interpretation (keyword
-  \isakeyword{interpret}).  This interpretation is inside the proof of the global
-  interpretation.  The third revision of the example illustrates this.  *}
+text {* In the above example, the fact that @{term "op \<le>"} is a partial
+  order for the natural numbers 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
+  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. *}
 
-interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "partial_order.less op \<le> (x::nat) y = (x < y)"
-proof -
-  show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-    by unfold_locales auto
-  then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
-  show "partial_order.less op \<le> (x::nat) y = (x < y)"
-    unfolding nat.less_def by auto
-qed
+  interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+    where "partial_order.less op \<le> (x::nat) y = (x < y)"
+  proof -
+    show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+      by unfold_locales auto
+    then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
+    show "partial_order.less op \<le> (x::nat) y = (x < y)"
+      unfolding nat.less_def by auto
+  qed
 
-text {* 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
+text {* The inner interpretation is immediate from the preceding fact
+  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 nat.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
-  \isakeyword{qed} --- and are then replaced by those with the desired
-  substitutions of the strict order.  *}
+  leaving the proof context --- that is, after the closing a
+  \isakeyword{next} or \isakeyword{qed} statement. *}
 
 
 subsection {* Further Interpretations *}
 
-text {* Further interpretations are necessary to reuse theorems from
+text {* Further interpretations are necessary for
   the other locales.  In @{text lattice} the operations @{text \<sqinter>} and
   @{text \<squnion>} are substituted by @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} and
   @{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"}.  The entire proof for the
-  interpretation is reproduced in order to give an example of a more
+  interpretation is reproduced to give an example of a more
   elaborate interpretation proof.  *}
 
-interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  where "lattice.meet op \<le> (x::nat) y = min x y"
-    and "lattice.join op \<le> (x::nat) y = max x y"
-proof -
-  show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
-    txt {* We have already shown that this is a partial order, *}
-    apply unfold_locales
-    txt {* hence only the lattice axioms remain to be shown: @{subgoals
-      [display]}  After unfolding @{text is_inf} and @{text is_sup}, *}
-    apply (unfold nat.is_inf_def nat.is_sup_def)
-    txt {* the goals become @{subgoals [display]} which can be solved
-      by Presburger arithmetic. *}
-    by arith+
-  txt {* 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 nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
-  show "lattice.meet op \<le> (x::nat) y = min x y"
-    by (bestsimp simp: nat.meet_def nat.is_inf_def)
-  show "lattice.join op \<le> (x::nat) y = max x y"
-    by (bestsimp simp: nat.join_def nat.is_sup_def)
-qed
+  interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+    where "lattice.meet op \<le> (x::nat) y = min x y"
+      and "lattice.join op \<le> (x::nat) y = max x y"
+  proof -
+    show "lattice (op \<le> :: nat \<Rightarrow> nat \<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}, *}
+      apply (unfold nat.is_inf_def nat.is_sup_def)
+      txt {* \normalsize the goals become @{subgoals [display]}
+	This can be solved by Presburger arithmetic, which is contained
+	in @{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 nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
+    show "lattice.meet op \<le> (x::nat) y = min x y"
+      by (bestsimp simp: nat.meet_def nat.is_inf_def)
+    show "lattice.join op \<le> (x::nat) y = max x y"
+      by (bestsimp simp: nat.join_def nat.is_sup_def)
+  qed
 
-text {* Next follows that @{text \<le>} is a total order. *}
+text {* Next follows that @{text "op \<le>"} is a total order, again for
+  the natural numbers. *}
 
-interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  by unfold_locales arith
+  interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+    by unfold_locales arith
 
 text {* Theorems that are available in the theory at this point are shown in
-  Table~\ref{tab:nat-lattice}.
+  Table~\ref{tab:nat-lattice}.  Two points are worth noting:
 
 \begin{table}
 \hrule
@@ -93,113 +102,101 @@
 \label{tab:nat-lattice}
 \end{table}
 
-  Note that 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 not neccessary.
-
-  Why not push this idea further and just give the last interpretation
-  as a single interpretation instead of the sequence of three?  The
-  reasons for this are twofold:
 \begin{itemize}
 \item
-  Often it is easier to work in an incremental fashion, because later
-  interpretations require theorems provided by earlier
-  interpretations.
+  Locale @{text distrib_lattice} was also interpreted.  Since the
+  locale hierarcy 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.
 \item
-  Assume that a definition is made in some locale $l_1$, and that $l_2$
-  imports $l_1$.  Let an equation for the definition be
-  proved in an interpretation of $l_2$.  The equation will be unfolded
-  in interpretations of theorems added to $l_2$ or below in the import
-  hierarchy, but not for theorems added above $l_2$.
-  Hence, an equation interpreting a definition should always be given in
-  an interpretation of the locale where the definition is made, not in
-  an interpretation of a locale further down the hierarchy.
+  Theorem @{thm [source] nat.less_total} makes use of @{term "op <"}
+  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.
 \end{itemize}
+  In the next section, the divisibility relation on the natural
+  numbers will be explored.
   *}
 
 
-subsection {* Lattice @{text "dvd"} on @{typ nat} *}
+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. *}
 
-text {* Divisibility on the natural numbers is a distributive lattice
-  but not a total order.  Interpretation again proceeds
-  incrementally. *}
+  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: 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
+  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 {* Note that in Isabelle/HOL there is no symbol for strict
-  divisibility.  Instead, interpretation substitutes @{term "x dvd y \<and>
-  x \<noteq> y"}.  *}
+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 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)"
+  interpretation %visible nat_dvd:
+    distrib_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 {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
-  nat_dvd_join_eq} are used in the main part the subsequent
-  interpretation. *}
-
-(*
-definition
-  is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
-  "is_lcm p m n \<longleftrightarrow> m dvd p \<and> n dvd p \<and>
-    (\<forall>d. m dvd d \<longrightarrow> n dvd d \<longrightarrow> p dvd d)"
-
-lemma is_gcd: "is_lcm (lcm (m, n)) m n"
-  by (simp add: is_lcm_def lcm_least)
-
-lemma gcd_lcm_distr_lemma:
-  "[| is_gcd g1 x l1; is_lcm l1 y z; is_gcd g2 x y; is_gcd g3 x z |] ==> is_lcm g1 g2 g3"
-apply (unfold is_gcd_def is_lcm_def dvd_def)
-apply (clarsimp simp: mult_ac)
-apply (blast intro: mult_is_0)
-thm mult_is_0 [THEN iffD1]
-*)
-
-lemma %invisible gcd_lcm_distr:
-  "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry
-
-interpretation %visible nat_dvd:
-  distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
-  apply unfold_locales
-  txt {* @{subgoals [display]} *}
-  apply (unfold nat_dvd_meet_eq nat_dvd_join_eq)
-  txt {* @{subgoals [display]} *}
-  apply (rule gcd_lcm_distr) done
-
+    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}.
@@ -223,12 +220,27 @@
 \end{table}
   *}
 
-text {*
-  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.
-  *}
+
+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{alltt}
+  nat! : 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
+  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
+  more convenient to use.  For \isakeyword{interpretation}, the
+  default for qualifiers without an explicit designator is ``!''.
+*}
 
 
 section {* Locale Expressions \label{sec:expressions} *}
@@ -240,70 +252,81 @@
   far: it involves two partial orders, and it is desirable to use the
   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}, 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 mappings of parameters to arguments.
+  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.
+
+  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
+  expression.
+
+  A \emph{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:
+\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.
 
-  Using a locale expression, a locale for order
-  preserving maps can be declared in the following way.  *}
+  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{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
+  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
+  parameters is declared.
+
+  Two context elements for the map parameter @{text \<phi>} and the
+  assumptions that it is order perserving 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) +
-    fixes \<phi> :: "'a \<Rightarrow> 'b"
+    fixes \<phi>
     assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
 
-text {* The second and third line contain the expression --- two
-  instances of the partial order locale where the parameter is
-  instantiated to @{text le}
-  and @{text le'}, 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.
+text (in order_preserving) {* Here are examples of theorems that are
+  available in the locale:
 
-  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.
+  @{thm [source] hom_le}: @{thm hom_le}
 
-  The qualifiers in the expression are already a familiar concept from
-  the \isakeyword{interpretation} command
-  (Section~\ref{sec:po-first}).  Here, they serve to distinguish names
-  (in particular theorem names) for the two partial orders within the
-  locale.  Qualifiers in the \isakeyword{locale} command (and in
-  \isakeyword{sublocale}) default to optional --- that is, they need
-  not occur in references to the qualified names.  Here are examples
-  of theorems in locale @{text order_preserving}: *}
-
-context %invisible order_preserving begin
-
-text {*
   @{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
 
-  @{thm [source] hom_le}: @{thm hom_le}
-  *}
+  @{thm [source] le'.less_le_trans}:
+  @{thm [display, indent=2] le'.less_le_trans}
 
-text {* The theorems for the partial order @{text \<preceq>}
-  are qualified by @{text le'}.  For example, @{thm [source]
-  le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *}
-
-end %invisible
-
-text {* This example reveals that there is no infix syntax for the
-  strict operation associated with @{text \<preceq>}.  This can be declared
-  through an abbreviation.  *}
+  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: *}
 
   abbreviation (in order_preserving)
     less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
@@ -312,33 +335,48 @@
   @{thm [source]  le'.less_le_trans}:
   @{thm [display, indent=2] le'.less_le_trans} *}
 
-text (in order_preserving)  {* Qualifiers not only apply to theorem names, but also to names
-  introduced by definitions and abbreviations.  For example, in @{text
-  partial_order} the name @{text less} abbreviates @{term
-  "partial_order.less le"}.  Therefore, in @{text order_preserving}
-  the qualified name @{text le.less} abbreviates @{term
-  "partial_order.less le"} and @{text le'.less} abbreviates @{term
-  "partial_order.less le'"}.  Hence, the equation in the abbreviation
-  above could have been written more concisely as @{text "less' \<equiv>
-  le'.less"}. *}
+
+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
+  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
+  Section~\ref{sec:changing-the-hierarchy}. *}
+
+
+text {* In a locale expression that occurs within a locale
+  declaration, omitted parameters additionally extend the (possibly
+  empty) \isakeyword{for} clause.
 
-text {* Readers may find the declaration of locale @{text
-  order_preserving} a little awkward, because the declaration and
-  concrete syntax for @{text le} from @{text partial_order} are
-  repeated in the declaration of @{text order_preserving}.  Locale
-  expressions provide a convenient short hand for this.  A parameter
-  in an instance is \emph{untouched} if no instantiation term is
-  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
-  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 \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 following locales illustrate this.  A map @{text \<phi>} is a
-  lattice homomorphism if it preserves meet and join. *}
+  There is an exception to this rule in locale declarations, where the
+  \isakeyword{for} clause servers 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{alltt}
+  partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
+\end{alltt}
+  This short hand was used in the locale declarations of
+  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
+  join. *}
 
   locale lattice_hom =
     le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
@@ -346,29 +384,42 @@
     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)"
 
-  abbreviation (in lattice_hom)
-    meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
-  abbreviation (in lattice_hom)
-    join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
+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 {* A homomorphism is an endomorphism if both orders coincide. *}
+  Before turning to the second example, we complete the locale by
+  provinding 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. *}
 
   locale lattice_end = lattice_hom _ le
 
-text {* In this declaration, the first parameter of @{text
-  lattice_hom}, @{text le}, is untouched and is then used to instantiate
-  the second parameter.  Its concrete syntax is preserved. *}
-
+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
+  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.  The expression
-  imported by @{text lattice_end} identifies the first and second
-  parameter of @{text lattice_hom}.  By looking at the inheritance diagram it would seem
+  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.  This is not the
-  case!  Inheritance paths with identical morphisms are detected and
+  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.
 
 \begin{figure}
@@ -423,14 +474,50 @@
   @{thm [display, indent=2] hom_le}
   *}
 
+(*
+section {* Conditional Interpretation *}
 
+  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
+
+*)
 
 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, we
+  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.
@@ -444,10 +531,18 @@
   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}.
+
+  The sources of this tutorial, which include all proofs, are
+  available with the Isabelle distribution at
+  \url{http://isabelle.in.tum.de}.
   *}
 
 text {*
@@ -542,8 +637,9 @@
   \multicolumn{3}{l}{Diagnostics} \\
 
   \textit{toplevel} & ::=
-  & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
-  & | & \textbf{print\_locales} 
+  & \textbf{print\_locales} \\
+  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
+  & | & \textbf{print\_interps} \textit{locale}
 \end{tabular}
 \end{center}
 \hrule
@@ -552,8 +648,18 @@
 \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{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
-  Christian Sternagel and Makarius Wenzel have made useful comments on
-  a draft of this document. *}
+  Randy Pollack, Christian Sternagel and Makarius Wenzel have made
+  useful comments on earlier versions of this document. *}
 
 end