doc-src/Locales/Locales/Examples3.thy

updated for Isabelle2009;

theory Examples3
imports Examples
begin
subsection {* Third Version: 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.  *}

interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
  where nat_less_eq: "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
  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.  *}


subsection {* Further Interpretations *}

text {* Further interpretations are necessary to reuse theorems from
  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
  elaborate interpretation proof.  *}

interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
  where "partial_order.less op \<le> (x::nat) y = (x < y)"
    and nat_meet_eq: "lattice.meet op \<le> (x::nat) y = min x y"
    and nat_join_eq: "lattice.join op \<le> (x::nat) y = max x y"
proof -
  show lattice: "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 {* For the first of the equations, we refer to the theorem
  shown in the previous interpretation. *}
  show "partial_order.less op \<le> (x::nat) y = (x < y)"
    by (rule nat_less_eq)
  txt {* In order to show the remaining equations, we put ourselves in a
    situation where the lattice theorems can be used in a convenient way. *}
  from lattice 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. *}

interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
  where "partial_order.less op \<le> (x::nat) y = (x < y)"
    and "lattice.meet op \<le> (x::nat) y = min x y"
    and "lattice.join op \<le> (x::nat) y = max x y"
proof -
  show "total_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
    by unfold_locales arith
qed (rule nat_less_eq nat_meet_eq nat_join_eq)+

text {* 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
  @{typ nat}. *}

interpretation %visible nat: distrib_lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
  where "partial_order.less op \<le> (x::nat) y = (x < y)"
    and "lattice.meet op \<le> (x::nat) y = min x y"
    and "lattice.join op \<le> (x::nat) y = max x y"
  by unfold_locales [1] (rule nat_less_eq nat_meet_eq nat_join_eq)+

text {* Theorems that are available in the theory at this point are shown in
  Table~\ref{tab:nat-lattice}.

\begin{table}
\hrule
\vspace{2ex}
\begin{center}
\begin{tabular}{l}
  @{thm [source] nat.less_def} from locale @{text partial_order}: \\
  \quad @{thm nat.less_def} \\
  @{thm [source] nat.meet_left} from locale @{text lattice}: \\
  \quad @{thm nat.meet_left} \\
  @{thm [source] nat.join_distr} from locale @{text distrib_lattice}: \\
  \quad @{thm nat.join_distr} \\
  @{thm [source] nat.less_total} from locale @{text total_order}: \\
  \quad @{thm nat.less_total}
\end{tabular}
\end{center}
\hrule
\caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
\label{tab:nat-lattice}
\end{table}
  *}


subsection {* Lattice @{text "dvd"} on @{typ nat} *}

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 nat_dvd_less_eq:
    "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 symbol for strict
  divisibility.  Instead, interpretation substitutes @{term "x dvd y \<and>
  x \<noteq> y"}.  *}

interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
    and nat_dvd_meet_eq: "lattice.meet op dvd = gcd"
    and nat_dvd_join_eq: "lattice.join op dvd = 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_dvd1 lcm_dvd2 lcm_least)
    done
  then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
  show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
    by (rule nat_dvd_less_eq)
  show "lattice.meet op dvd = 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 = 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)
    by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
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"
  where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
    and "lattice.meet op dvd = gcd"
    and "lattice.join op dvd = lcm"
proof -
  show "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
qed (rule nat_dvd_less_eq nat_dvd_meet_eq nat_dvd_join_eq)+


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}
  *}

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.
  *}


section {* Locale Expressions \label{sec:expressions} *}

text {*
  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.

  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.

  Using a locale expression, a locale for order
  preserving maps can be declared in the following way.  *}

  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"
    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.

  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.

  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}
  *}

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.  *}

  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} *}

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"}. *}

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 following locales illustrate this.  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)"

  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 {* 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 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
  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
  the conclusions of the respective locales appear only once.

\begin{figure}
\hrule \vspace{2ex}
\begin{center}
\begin{tikzpicture}
  \node (o) at (0,0) {@{text partial_order}};
  \node (oh) at (1.5,-2) {@{text order_preserving}};
  \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
  \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
  \node (l) at (-1.5,-2) {@{text lattice}};
  \node (lh) at (0,-4) {@{text lattice_hom}};
  \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
  \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
  \node (le) at (0,-6) {@{text lattice_end}};
  \node (le1) at (0,-4.8)
    [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
  \node (le2) at (0,-5.2)
    [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
  \draw (o) -- (l);
  \draw[dashed] (oh) -- (lh);
  \draw (lh) -- (le);
  \draw (o) .. controls (oh1.south west) .. (oh);
  \draw (o) .. controls (oh2.north east) .. (oh);
  \draw (l) .. controls (lh1.south west) .. (lh);
  \draw (l) .. controls (lh2.north east) .. (lh);
\end{tikzpicture}
\end{center}
\hrule
\caption{Hierarchy of Homomorphism Locales.}
\label{fig:hom}
\end{figure}
  *}

text {* It can be shown easily that a lattice homomorphism is order
  preserving.  As the final example of this section, a locale
  interpretation is used to assert this: *}

  sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
    fix x y
    assume "x \<sqsubseteq> y"
    then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
    then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
    then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
  qed

text (in lattice_hom) {*
  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}
  *}



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
  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
  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 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}.
  *}

text {*
\begin{table}
\hrule
\vspace{2ex}
\begin{center}
\begin{tabular}{l>$c<$l}
  \multicolumn{3}{l}{Miscellaneous} \\

  \textit{attr-name} & ::=
  & \textit{name} $|$ \textit{attribute} $|$
    \textit{name} \textit{attribute} \\
  \textit{qualifier} & ::=
  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]

  \multicolumn{3}{l}{Context Elements} \\

  \textit{fixes} & ::=
  & \textit{name} [ ``\textbf{::}'' \textit{type} ]
    [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
    \textit{mixfix} ] \\
\begin{comment}
  \textit{constrains} & ::=
  & \textit{name} ``\textbf{::}'' \textit{type} \\
\end{comment}
  \textit{assumes} & ::=
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
\begin{comment}
  \textit{defines} & ::=
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
  \textit{notes} & ::=
  & [ \textit{attr-name} ``\textbf{=}'' ]
    ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
\end{comment}

  \textit{element} & ::=
  & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
\begin{comment}
  & |
  & \textbf{constrains} \textit{constrains}
    ( \textbf{and} \textit{constrains} )$^*$ \\
\end{comment}
  & |
  & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]
%\begin{comment}
%  & |
%  & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
%  & |
%  & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
%\end{comment}

  \multicolumn{3}{l}{Locale Expressions} \\

  \textit{pos-insts} & ::=
  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
  \textit{named-insts} & ::=
  & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
  ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
  \textit{instance} & ::=
  & [ \textit{qualifier} ``\textbf{:}'' ]
    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
  \textit{expression}  & ::= 
  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]

  \multicolumn{3}{l}{Declaration of Locales} \\

  \textit{locale} & ::=
  & \textit{element}$^+$ \\
  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
  \textit{toplevel} & ::=
  & \textbf{locale} \textit{name} [ ``\textbf{=}''
    \textit{locale} ] \\[2ex]

  \multicolumn{3}{l}{Interpretation} \\

  \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
    \textit{prop} \\
  \textit{equations} & ::= &  \textbf{where} \textit{equation} ( \textbf{and}
    \textit{equation} )$^*$  \\
  \textit{toplevel} & ::=
  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
  & |
  & \textbf{interpretation}
    \textit{expression} [ \textit{equations} ] \textit{proof} \\
  & |
  & \textbf{interpret}
    \textit{expression} \textit{proof} \\[2ex]

  \multicolumn{3}{l}{Diagnostics} \\

  \textit{toplevel} & ::=
  & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
  & | & \textbf{print\_locales} 
\end{tabular}
\end{center}
\hrule
\caption{Syntax of Locale Commands.}
\label{tab:commands}
\end{table}
  *}

text {* \textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
  Christian Sternagel and Makarius Wenzel have made useful comments on
  a draft of this document. *}

end