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