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