src/Doc/Locales/Examples3.thy
author haftmann
Mon Feb 06 20:56:34 2017 +0100 (2017-02-06)
changeset 64990 c6a7de505796
parent 63724 e7df93d4d9b8
child 67398 5eb932e604a2
permissions -rw-r--r--
more explicit errors in pathological cases
     1 theory Examples3
     2 imports Examples
     3 begin
     4 
     5 subsection \<open>Third Version: Local Interpretation
     6   \label{sec:local-interpretation}\<close>
     7 
     8 text \<open>In the above example, the fact that @{term "op \<le>"} is a partial
     9   order for the integers was used in the second goal to
    10   discharge the premise in the definition of @{text "op \<sqsubset>"}.  In
    11   general, proofs of the equations not only may involve definitions
    12   from the interpreted locale but arbitrarily complex arguments in the
    13   context of the locale.  Therefore it would be convenient to have the
    14   interpreted locale conclusions temporarily available in the proof.
    15   This can be achieved by a locale interpretation in the proof body.
    16   The command for local interpretations is \isakeyword{interpret}.  We
    17   repeat the example from the previous section to illustrate this.\<close>
    18 
    19   interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
    20     rewrites "int.less x y = (x < y)"
    21   proof -
    22     show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
    23       by unfold_locales auto
    24     then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
    25     show "int.less x y = (x < y)"
    26       unfolding int.less_def by auto
    27   qed
    28 
    29 text \<open>The inner interpretation is immediate from the preceding fact
    30   and proved by assumption (Isar short hand ``.'').  It enriches the
    31   local proof context by the theorems
    32   also obtained in the interpretation from Section~\ref{sec:po-first},
    33   and @{text int.less_def} may directly be used to unfold the
    34   definition.  Theorems from the local interpretation disappear after
    35   leaving the proof context --- that is, after the succeeding
    36   \isakeyword{next} or \isakeyword{qed} statement.\<close>
    37 
    38 
    39 subsection \<open>Further Interpretations\<close>
    40 
    41 text \<open>Further interpretations are necessary for
    42   the other locales.  In @{text lattice} the operations~@{text \<sqinter>}
    43   and~@{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"}
    44   and @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}.  The entire proof for the
    45   interpretation is reproduced to give an example of a more
    46   elaborate interpretation proof.  Note that the equations are named
    47   so they can be used in a later example.\<close>
    48 
    49   interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
    50     rewrites int_min_eq: "int.meet x y = min x y"
    51       and int_max_eq: "int.join x y = max x y"
    52   proof -
    53     show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
    54       txt \<open>\normalsize We have already shown that this is a partial
    55         order,\<close>
    56       apply unfold_locales
    57       txt \<open>\normalsize hence only the lattice axioms remain to be
    58         shown.
    59         @{subgoals [display]}
    60         By @{text is_inf} and @{text is_sup},\<close>
    61       apply (unfold int.is_inf_def int.is_sup_def)
    62       txt \<open>\normalsize the goals are transformed to these
    63         statements:
    64         @{subgoals [display]}
    65         This is Presburger arithmetic, which can be solved by the
    66         method @{text arith}.\<close>
    67       by arith+
    68     txt \<open>\normalsize In order to show the equations, we put ourselves
    69       in a situation where the lattice theorems can be used in a
    70       convenient way.\<close>
    71     then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
    72     show "int.meet x y = min x y"
    73       by (bestsimp simp: int.meet_def int.is_inf_def)
    74     show "int.join x y = max x y"
    75       by (bestsimp simp: int.join_def int.is_sup_def)
    76   qed
    77 
    78 text \<open>Next follows that @{text "op \<le>"} is a total order, again for
    79   the integers.\<close>
    80 
    81   interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
    82     by unfold_locales arith
    83 
    84 text \<open>Theorems that are available in the theory at this point are shown in
    85   Table~\ref{tab:int-lattice}.  Two points are worth noting:
    86 
    87 \begin{table}
    88 \hrule
    89 \vspace{2ex}
    90 \begin{center}
    91 \begin{tabular}{l}
    92   @{thm [source] int.less_def} from locale @{text partial_order}: \\
    93   \quad @{thm int.less_def} \\
    94   @{thm [source] int.meet_left} from locale @{text lattice}: \\
    95   \quad @{thm int.meet_left} \\
    96   @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
    97   \quad @{thm int.join_distr} \\
    98   @{thm [source] int.less_total} from locale @{text total_order}: \\
    99   \quad @{thm int.less_total}
   100 \end{tabular}
   101 \end{center}
   102 \hrule
   103 \caption{Interpreted theorems for~@{text \<le>} on the integers.}
   104 \label{tab:int-lattice}
   105 \end{table}
   106 
   107 \begin{itemize}
   108 \item
   109   Locale @{text distrib_lattice} was also interpreted.  Since the
   110   locale hierarchy reflects that total orders are distributive
   111   lattices, the interpretation of the latter was inserted
   112   automatically with the interpretation of the former.  In general,
   113   interpretation traverses the locale hierarchy upwards and interprets
   114   all encountered locales, regardless whether imported or proved via
   115   the \isakeyword{sublocale} command.  Existing interpretations are
   116   skipped avoiding duplicate work.
   117 \item
   118   The predicate @{term "op <"} appears in theorem @{thm [source]
   119   int.less_total}
   120   although an equation for the replacement of @{text "op \<sqsubset>"} was only
   121   given in the interpretation of @{text partial_order}.  The
   122   interpretation equations are pushed downwards the hierarchy for
   123   related interpretations --- that is, for interpretations that share
   124   the instances of parameters they have in common.
   125 \end{itemize}
   126 \<close>
   127 
   128 text \<open>The interpretations for a locale $n$ within the current
   129   theory may be inspected with \isakeyword{print\_interps}~$n$.  This
   130   prints the list of instances of $n$, for which interpretations exist.
   131   For example, \isakeyword{print\_interps} @{term partial_order}
   132   outputs the following:
   133 \begin{small}
   134 \begin{alltt}
   135   int : partial_order "op \(\le\)"
   136 \end{alltt}
   137 \end{small}
   138   Of course, there is only one interpretation.
   139   The interpretation qualifier on the left is mandatory.  Qualifiers
   140   can either be \emph{mandatory} or \emph{optional}.  Optional qualifiers
   141   are designated by ``?''.  Mandatory qualifiers must occur in
   142   name references while optional ones need not.  Mandatory qualifiers
   143   prevent accidental hiding of names, while optional qualifiers can be
   144   more convenient to use.  The default is mandatory.
   145 \<close>
   146 
   147 
   148 section \<open>Locale Expressions \label{sec:expressions}\<close>
   149 
   150 text \<open>
   151   A map~@{term \<phi>} between partial orders~@{text \<sqsubseteq>} and~@{text \<preceq>}
   152   is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq>
   153   \<phi> y"}.  This situation is more complex than those encountered so
   154   far: it involves two partial orders, and it is desirable to use the
   155   existing locale for both.
   156 
   157   A locale for order preserving maps requires three parameters: @{text
   158   le}~(\isakeyword{infixl}~@{text \<sqsubseteq>}) and @{text
   159   le'}~(\isakeyword{infixl}~@{text \<preceq>}) for the orders and~@{text \<phi>}
   160   for the map.
   161 
   162   In order to reuse the existing locale for partial orders, which has
   163   the single parameter~@{text le}, it must be imported twice, once
   164   mapping its parameter to~@{text le} from the new locale and once
   165   to~@{text le'}.  This can be achieved with a compound locale
   166   expression.
   167 
   168   In general, a locale expression is a sequence of \emph{locale instances}
   169   separated by~``$\textbf{+}$'' and followed by a \isakeyword{for}
   170   clause.
   171   An instance has the following format:
   172 \begin{quote}
   173   \textit{qualifier} \textbf{:} \textit{locale-name}
   174   \textit{parameter-instantiation}
   175 \end{quote}
   176   We have already seen locale instances as arguments to
   177   \isakeyword{interpretation} in Section~\ref{sec:interpretation}.
   178   As before, the qualifier serves to disambiguate names from
   179   different instances of the same locale, and unless designated with a
   180   ``?'' it must occur in name references.
   181 
   182   Since the parameters~@{text le} and~@{text le'} are to be partial
   183   orders, our locale for order preserving maps will import the these
   184   instances:
   185 \begin{small}
   186 \begin{alltt}
   187   le: partial_order le
   188   le': partial_order le'
   189 \end{alltt}
   190 \end{small}
   191   For matter of convenience we choose to name parameter names and
   192   qualifiers alike.  This is an arbitrary decision.  Technically, qualifiers
   193   and parameters are unrelated.
   194 
   195   Having determined the instances, let us turn to the \isakeyword{for}
   196   clause.  It serves to declare locale parameters in the same way as
   197   the context element \isakeyword{fixes} does.  Context elements can
   198   only occur after the import section, and therefore the parameters
   199   referred to in the instances must be declared in the \isakeyword{for}
   200   clause.  The \isakeyword{for} clause is also where the syntax of these
   201   parameters is declared.
   202 
   203   Two context elements for the map parameter~@{text \<phi>} and the
   204   assumptions that it is order preserving complete the locale
   205   declaration.\<close>
   206 
   207   locale order_preserving =
   208     le: partial_order le + le': partial_order le'
   209       for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +
   210     fixes \<phi>
   211     assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
   212 
   213 text (in order_preserving) \<open>Here are examples of theorems that are
   214   available in the locale:
   215 
   216   \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le}
   217 
   218   \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
   219 
   220   \hspace*{1em}@{thm [source] le'.less_le_trans}:
   221   @{thm [display, indent=4] le'.less_le_trans}
   222   While there is infix syntax for the strict operation associated with
   223   @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
   224   "op \<preceq>"}.  The syntax @{text "\<sqsubset>"} for @{text less} is only
   225   available for the original instance it was declared for.  We may
   226   introduce infix syntax for @{text le'.less} with the following declaration:\<close>
   227 
   228   notation (in order_preserving) le'.less (infixl "\<prec>" 50)
   229 
   230 text (in order_preserving) \<open>Now the theorem is displayed nicely as
   231   @{thm [source]  le'.less_le_trans}:
   232   @{thm [display, indent=2] le'.less_le_trans}\<close>
   233 
   234 text \<open>There are short notations for locale expressions.  These are
   235   discussed in the following.\<close>
   236 
   237 
   238 subsection \<open>Default Instantiations\<close>
   239 
   240 text \<open>
   241   It is possible to omit parameter instantiations.  The
   242   instantiation then defaults to the name of
   243   the parameter itself.  For example, the locale expression @{text
   244   partial_order} is short for @{text "partial_order le"}, since the
   245   locale's single parameter is~@{text le}.  We took advantage of this
   246   in the \isakeyword{sublocale} declarations of
   247   Section~\ref{sec:changing-the-hierarchy}.\<close>
   248 
   249 
   250 subsection \<open>Implicit Parameters \label{sec:implicit-parameters}\<close>
   251 
   252 text \<open>In a locale expression that occurs within a locale
   253   declaration, omitted parameters additionally extend the (possibly
   254   empty) \isakeyword{for} clause.
   255 
   256   The \isakeyword{for} clause is a general construct of Isabelle/Isar
   257   to mark names occurring in the preceding declaration as ``arbitrary
   258   but fixed''.  This is necessary for example, if the name is already
   259   bound in a surrounding context.  In a locale expression, names
   260   occurring in parameter instantiations should be bound by a
   261   \isakeyword{for} clause whenever these names are not introduced
   262   elsewhere in the context --- for example, on the left hand side of a
   263   \isakeyword{sublocale} declaration.
   264 
   265   There is an exception to this rule in locale declarations, where the
   266   \isakeyword{for} clause serves to declare locale parameters.  Here,
   267   locale parameters for which no parameter instantiation is given are
   268   implicitly added, with their mixfix syntax, at the beginning of the
   269   \isakeyword{for} clause.  For example, in a locale declaration, the
   270   expression @{text partial_order} is short for
   271 \begin{small}
   272 \begin{alltt}
   273   partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
   274 \end{alltt}
   275 \end{small}
   276   This short hand was used in the locale declarations throughout
   277   Section~\ref{sec:import}.
   278 \<close>
   279 
   280 text\<open>
   281   The following locale declarations provide more examples.  A
   282   map~@{text \<phi>} is a lattice homomorphism if it preserves meet and
   283   join.\<close>
   284 
   285   locale lattice_hom =
   286     le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
   287     fixes \<phi>
   288     assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
   289       and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
   290 
   291 text \<open>The parameter instantiation in the first instance of @{term
   292   lattice} is omitted.  This causes the parameter~@{text le} to be
   293   added to the \isakeyword{for} clause, and the locale has
   294   parameters~@{text le},~@{text le'} and, of course,~@{text \<phi>}.
   295 
   296   Before turning to the second example, we complete the locale by
   297   providing infix syntax for the meet and join operations of the
   298   second lattice.
   299 \<close>
   300 
   301   context lattice_hom
   302   begin
   303   notation le'.meet (infixl "\<sqinter>''" 50)
   304   notation le'.join (infixl "\<squnion>''" 50)
   305   end
   306 
   307 text \<open>The next example makes radical use of the short hand
   308   facilities.  A homomorphism is an endomorphism if both orders
   309   coincide.\<close>
   310 
   311   locale lattice_end = lattice_hom _ le
   312 
   313 text \<open>The notation~@{text _} enables to omit a parameter in a
   314   positional instantiation.  The omitted parameter,~@{text le} becomes
   315   the parameter of the declared locale and is, in the following
   316   position, used to instantiate the second parameter of @{text
   317   lattice_hom}.  The effect is that of identifying the first in second
   318   parameter of the homomorphism locale.\<close>
   319 
   320 text \<open>The inheritance diagram of the situation we have now is shown
   321   in Figure~\ref{fig:hom}, where the dashed line depicts an
   322   interpretation which is introduced below.  Parameter instantiations
   323   are indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at
   324   the inheritance diagram it would seem
   325   that two identical copies of each of the locales @{text
   326   partial_order} and @{text lattice} are imported by @{text
   327   lattice_end}.  This is not the case!  Inheritance paths with
   328   identical morphisms are automatically detected and
   329   the conclusions of the respective locales appear only once.
   330 
   331 \begin{figure}
   332 \hrule \vspace{2ex}
   333 \begin{center}
   334 \begin{tikzpicture}
   335   \node (o) at (0,0) {@{text partial_order}};
   336   \node (oh) at (1.5,-2) {@{text order_preserving}};
   337   \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
   338   \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
   339   \node (l) at (-1.5,-2) {@{text lattice}};
   340   \node (lh) at (0,-4) {@{text lattice_hom}};
   341   \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
   342   \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
   343   \node (le) at (0,-6) {@{text lattice_end}};
   344   \node (le1) at (0,-4.8)
   345     [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
   346   \node (le2) at (0,-5.2)
   347     [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
   348   \draw (o) -- (l);
   349   \draw[dashed] (oh) -- (lh);
   350   \draw (lh) -- (le);
   351   \draw (o) .. controls (oh1.south west) .. (oh);
   352   \draw (o) .. controls (oh2.north east) .. (oh);
   353   \draw (l) .. controls (lh1.south west) .. (lh);
   354   \draw (l) .. controls (lh2.north east) .. (lh);
   355 \end{tikzpicture}
   356 \end{center}
   357 \hrule
   358 \caption{Hierarchy of Homomorphism Locales.}
   359 \label{fig:hom}
   360 \end{figure}
   361 \<close>
   362 
   363 text \<open>It can be shown easily that a lattice homomorphism is order
   364   preserving.  As the final example of this section, a locale
   365   interpretation is used to assert this:\<close>
   366 
   367   sublocale lattice_hom \<subseteq> order_preserving
   368   proof unfold_locales
   369     fix x y
   370     assume "x \<sqsubseteq> y"
   371     then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
   372     then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
   373     then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
   374   qed
   375 
   376 text (in lattice_hom) \<open>
   377   Theorems and other declarations --- syntax, in particular --- from
   378   the locale @{text order_preserving} are now active in @{text
   379   lattice_hom}, for example
   380   @{thm [source] hom_le}:
   381   @{thm [display, indent=2] hom_le}
   382   This theorem will be useful in the following section.
   383 \<close>
   384 
   385 
   386 section \<open>Conditional Interpretation\<close>
   387 
   388 text \<open>There are situations where an interpretation is not possible
   389   in the general case since the desired property is only valid if
   390   certain conditions are fulfilled.  Take, for example, the function
   391   @{text "\<lambda>i. n * i"} that scales its argument by a constant factor.
   392   This function is order preserving (and even a lattice endomorphism)
   393   with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}.
   394 
   395   It is not possible to express this using a global interpretation,
   396   because it is in general unspecified whether~@{term n} is
   397   non-negative, but one may make an interpretation in an inner context
   398   of a proof where full information is available.
   399   This is not fully satisfactory either, since potentially
   400   interpretations may be required to make interpretations in many
   401   contexts.  What is
   402   required is an interpretation that depends on the condition --- and
   403   this can be done with the \isakeyword{sublocale} command.  For this
   404   purpose, we introduce a locale for the condition.\<close>
   405 
   406   locale non_negative =
   407     fixes n :: int
   408     assumes non_neg: "0 \<le> n"
   409 
   410 text \<open>It is again convenient to make the interpretation in an
   411   incremental fashion, first for order preserving maps, then for
   412   lattice endomorphisms.\<close>
   413 
   414   sublocale non_negative \<subseteq>
   415       order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
   416     using non_neg by unfold_locales (rule mult_left_mono)
   417 
   418 text \<open>While the proof of the previous interpretation
   419   is straightforward from monotonicity lemmas for~@{term "op *"}, the
   420   second proof follows a useful pattern.\<close>
   421 
   422   sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
   423   proof (unfold_locales, unfold int_min_eq int_max_eq)
   424     txt \<open>\normalsize Unfolding the locale predicates \emph{and} the
   425       interpretation equations immediately yields two subgoals that
   426       reflect the core conjecture.
   427       @{subgoals [display]}
   428       It is now necessary to show, in the context of @{term
   429       non_negative}, that multiplication by~@{term n} commutes with
   430       @{term min} and @{term max}.\<close>
   431   qed (auto simp: hom_le)
   432 
   433 text (in order_preserving) \<open>The lemma @{thm [source] hom_le}
   434   simplifies a proof that would have otherwise been lengthy and we may
   435   consider making it a default rule for the simplifier:\<close>
   436 
   437   lemmas (in order_preserving) hom_le [simp]
   438 
   439 
   440 subsection \<open>Avoiding Infinite Chains of Interpretations
   441   \label{sec:infinite-chains}\<close>
   442 
   443 text \<open>Similar situations arise frequently in formalisations of
   444   abstract algebra where it is desirable to express that certain
   445   constructions preserve certain properties.  For example, polynomials
   446   over rings are rings, or --- an example from the domain where the
   447   illustrations of this tutorial are taken from --- a partial order
   448   may be obtained for a function space by point-wise lifting of the
   449   partial order of the co-domain.  This corresponds to the following
   450   interpretation:\<close>
   451 
   452   sublocale %visible partial_order \<subseteq> f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
   453     oops
   454 
   455 text \<open>Unfortunately this is a cyclic interpretation that leads to an
   456   infinite chain, namely
   457   @{text [display, indent=2] "partial_order \<subseteq> partial_order (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) \<subseteq>
   458   partial_order (\<lambda>f g. \<forall>x y. f x y \<sqsubseteq> g x y) \<subseteq>  \<dots>"}
   459   and the interpretation is rejected.
   460 
   461   Instead it is necessary to declare a locale that is logically
   462   equivalent to @{term partial_order} but serves to collect facts
   463   about functions spaces where the co-domain is a partial order, and
   464   to make the interpretation in its context:\<close>
   465 
   466   locale fun_partial_order = partial_order
   467 
   468   sublocale fun_partial_order \<subseteq>
   469       f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
   470     by unfold_locales (fast,rule,fast,blast intro: trans)
   471 
   472 text \<open>It is quite common in abstract algebra that such a construction
   473   maps a hierarchy of algebraic structures (or specifications) to a
   474   related hierarchy.  By means of the same lifting, a function space
   475   is a lattice if its co-domain is a lattice:\<close>
   476 
   477   locale fun_lattice = fun_partial_order + lattice
   478 
   479   sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
   480   proof unfold_locales
   481     fix f g
   482     have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
   483       apply (rule f.is_infI) apply rule+ apply (drule spec, assumption)+ done
   484     then show "\<exists>inf. partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g inf"
   485       by fast
   486   next
   487     fix f g
   488     have "partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<squnion> g x)"
   489       apply (rule f.is_supI) apply rule+ apply (drule spec, assumption)+ done
   490     then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup"
   491       by fast
   492   qed
   493 
   494 
   495 section \<open>Further Reading\<close>
   496 
   497 text \<open>More information on locales and their interpretation is
   498   available.  For the locale hierarchy of import and interpretation
   499   dependencies see~@{cite Ballarin2006a}; interpretations in theories
   500   and proofs are covered in~@{cite Ballarin2006b}.  In the latter, I
   501   show how interpretation in proofs enables to reason about families
   502   of algebraic structures, which cannot be expressed with locales
   503   directly.
   504 
   505   Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction
   506   of axiomatic type classes through a combination with locale
   507   interpretation.  The result is a Haskell-style class system with a
   508   facility to generate ML and Haskell code.  Classes are sufficient for
   509   simple specifications with a single type parameter.  The locales for
   510   orders and lattices presented in this tutorial fall into this
   511   category.  Order preserving maps, homomorphisms and vector spaces,
   512   on the other hand, do not.
   513 
   514   The locales reimplementation for Isabelle 2009 provides, among other
   515   improvements, a clean integration with Isabelle/Isar's local theory
   516   mechanisms, which are described in another paper by Haftmann and
   517   Wenzel~@{cite HaftmannWenzel2009}.
   518 
   519   The original work of Kamm\"uller on locales~@{cite KammullerEtAl1999}
   520   may be of interest from a historical perspective.  My previous
   521   report on locales and locale expressions~@{cite Ballarin2004a}
   522   describes a simpler form of expressions than available now and is
   523   outdated. The mathematical background on orders and lattices is
   524   taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}.
   525 
   526   The sources of this tutorial, which include all proofs, are
   527   available with the Isabelle distribution at
   528   \<^url>\<open>http://isabelle.in.tum.de\<close>.
   529 \<close>
   530 
   531 text \<open>
   532 \begin{table}
   533 \hrule
   534 \vspace{2ex}
   535 \begin{center}
   536 \begin{tabular}{l>$c<$l}
   537   \multicolumn{3}{l}{Miscellaneous} \\
   538 
   539   \textit{attr-name} & ::=
   540   & \textit{name} $|$ \textit{attribute} $|$
   541     \textit{name} \textit{attribute} \\
   542   \textit{qualifier} & ::=
   543   & \textit{name} [``\textbf{?}''] \\[2ex]
   544 
   545   \multicolumn{3}{l}{Context Elements} \\
   546 
   547   \textit{fixes} & ::=
   548   & \textit{name} [ ``\textbf{::}'' \textit{type} ]
   549     [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
   550     \textit{mixfix} ] \\
   551 \begin{comment}
   552   \textit{constrains} & ::=
   553   & \textit{name} ``\textbf{::}'' \textit{type} \\
   554 \end{comment}
   555   \textit{assumes} & ::=
   556   & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
   557 \begin{comment}
   558   \textit{defines} & ::=
   559   & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
   560   \textit{notes} & ::=
   561   & [ \textit{attr-name} ``\textbf{=}'' ]
   562     ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
   563 \end{comment}
   564 
   565   \textit{element} & ::=
   566   & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
   567 \begin{comment}
   568   & |
   569   & \textbf{constrains} \textit{constrains}
   570     ( \textbf{and} \textit{constrains} )$^*$ \\
   571 \end{comment}
   572   & |
   573   & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]
   574 %\begin{comment}
   575 %  & |
   576 %  & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
   577 %  & |
   578 %  & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
   579 %\end{comment}
   580 
   581   \multicolumn{3}{l}{Locale Expressions} \\
   582 
   583   \textit{pos-insts} & ::=
   584   & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
   585   \textit{named-insts} & ::=
   586   & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
   587   ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
   588   \textit{instance} & ::=
   589   & [ \textit{qualifier} ``\textbf{:}'' ]
   590     \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
   591   \textit{expression}  & ::= 
   592   & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
   593     [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
   594 
   595   \multicolumn{3}{l}{Declaration of Locales} \\
   596 
   597   \textit{locale} & ::=
   598   & \textit{element}$^+$ \\
   599   & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
   600   \textit{toplevel} & ::=
   601   & \textbf{locale} \textit{name} [ ``\textbf{=}''
   602     \textit{locale} ] \\[2ex]
   603 
   604   \multicolumn{3}{l}{Interpretation} \\
   605 
   606   \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
   607     \textit{prop} \\
   608   \textit{equations} & ::= &  \textbf{rewrites} \textit{equation} ( \textbf{and}
   609     \textit{equation} )$^*$  \\
   610   \textit{toplevel} & ::=
   611   & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
   612     ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
   613   & |
   614   & \textbf{interpretation}
   615     \textit{expression} [ \textit{equations} ] \textit{proof} \\
   616   & |
   617   & \textbf{interpret}
   618     \textit{expression} \textit{proof} \\[2ex]
   619 
   620   \multicolumn{3}{l}{Diagnostics} \\
   621 
   622   \textit{toplevel} & ::=
   623   & \textbf{print\_locales} \\
   624   & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
   625   & | & \textbf{print\_interps} \textit{name}
   626 \end{tabular}
   627 \end{center}
   628 \hrule
   629 \caption{Syntax of Locale Commands.}
   630 \label{tab:commands}
   631 \end{table}
   632 \<close>
   633 
   634 text \<open>\textbf{Revision History.}  The present fourth revision of the
   635   tutorial accommodates minor updates to the syntax of the locale commands
   636   and the handling of notation under morphisms introduced with Isabelle 2016.
   637   For the third revision of the tutorial, which corresponds to the published
   638   version, much of the explanatory text was rewritten.  Inheritance of
   639   interpretation equations was made available with Isabelle 2009-1.
   640   The second revision accommodates changes introduced by the locales
   641   reimplementation for Isabelle 2009.  Most notably locale expressions
   642   were generalised from renaming to instantiation.\<close>
   643 
   644 text \<open>\textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
   645   Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel
   646   have made
   647   useful comments on earlier versions of this document.  The section
   648   on conditional interpretation was inspired by a number of e-mail
   649   enquiries the author received from locale users, and which suggested
   650   that this use case is important enough to deserve explicit
   651   explanation.  The term \emph{conditional interpretation} is due to
   652   Larry Paulson.\<close>
   653 
   654 end