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
5 subsection \<open>Third Version: Local Interpretation
6   \label{sec:local-interpretation}\<close>
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>
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
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>
39 subsection \<open>Further Interpretations\<close>
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>
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
78 text \<open>Next follows that @{text "op \<le>"} is a total order, again for
79   the integers.\<close>
81   interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
82     by unfold_locales arith
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:
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}: \\
94   @{thm [source] int.meet_left} from locale @{text lattice}: \\
96   @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
98   @{thm [source] int.less_total} from locale @{text total_order}: \\
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}
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>
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>
148 section \<open>Locale Expressions \label{sec:expressions}\<close>
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.
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.
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.
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.
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.
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.
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>
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"
213 text (in order_preserving) \<open>Here are examples of theorems that are
214   available in the locale:
216   \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le}
218   \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans}
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>
228   notation (in order_preserving) le'.less (infixl "\<prec>" 50)
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>
234 text \<open>There are short notations for locale expressions.  These are
235   discussed in the following.\<close>
238 subsection \<open>Default Instantiations\<close>
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>
250 subsection \<open>Implicit Parameters \label{sec:implicit-parameters}\<close>
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.
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.
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>
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>
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)"
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>}.
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>
301   context lattice_hom
302   begin
303   notation le'.meet (infixl "\<sqinter>''" 50)
304   notation le'.join (infixl "\<squnion>''" 50)
305   end
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>
311   locale lattice_end = lattice_hom _ le
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>
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.
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>
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>
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
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>
386 section \<open>Conditional Interpretation\<close>
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"}.
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>
406   locale non_negative =
407     fixes n :: int
408     assumes non_neg: "0 \<le> n"
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>
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)
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>
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)
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>
437   lemmas (in order_preserving) hom_le [simp]
440 subsection \<open>Avoiding Infinite Chains of Interpretations
441   \label{sec:infinite-chains}\<close>
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>
452   sublocale %visible partial_order \<subseteq> f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
453     oops
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.
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>
466   locale fun_partial_order = partial_order
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)
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>
477   locale fun_lattice = fun_partial_order + lattice
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
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.
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.
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}.
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}.
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>
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} \\
539   \textit{attr-name} & ::=
540   & \textit{name} $|$ \textit{attribute} $|$
541     \textit{name} \textit{attribute} \\
542   \textit{qualifier} & ::=
543   & \textit{name} [\textbf{?}''] \\[2ex]
545   \multicolumn{3}{l}{Context Elements} \\
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}
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}
581   \multicolumn{3}{l}{Locale Expressions} \\
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]
595   \multicolumn{3}{l}{Declaration of Locales} \\
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]
604   \multicolumn{3}{l}{Interpretation} \\
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]
620   \multicolumn{3}{l}{Diagnostics} \\
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>
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>
644 text \<open>\textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
645   Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel