src/Doc/Locales/Examples3.thy
 author ballarin Thu Aug 25 20:08:41 2016 +0200 (2016-08-25) changeset 63724 e7df93d4d9b8 parent 63680 6e1e8b5abbfa child 67398 5eb932e604a2 permissions -rw-r--r--
Back to original example theorem.
     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