doc-src/Locales/Locales/Examples3.thy
author ballarin
Sat, 17 Oct 2009 22:58:18 +0200
changeset 32983 a6914429005b
parent 32982 40810d98f4c9
child 33867 52643d0f856d
permissions -rw-r--r--
Finished revisions of locales tutorial.
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     4
text {* \vspace{-5ex} *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     5
subsection {* Third Version: Local Interpretation
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     6
  \label{sec:local-interpretation} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     7
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
     8
text {* 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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    13
  context of the locale.  Therefore is would be convenient to have the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    14
  interpreted locale conclusions temporary available in the proof.
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
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    17
  repeat the example from the previous section to illustrate this. *}
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"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    20
    where "partial_order.less op \<le> (x::int) 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" .
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    25
    show "partial_order.less op \<le> (x::int) y = (x < y)"
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    29
text {* The inner interpretation is immediate from the preceding fact
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    36
  \isakeyword{next} or \isakeyword{qed} statement. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    37
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    38
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    39
subsection {* Further Interpretations *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    40
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    41
text {* 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
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    47
  so they can be used in a later example.  *}
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"
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    50
    where int_min_eq: "lattice.meet op \<le> (x::int) y = min x y"
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    51
      and int_max_eq: "lattice.join op \<le> (x::int) 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)"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    54
      txt {* \normalsize We have already shown that this is a partial
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    55
	order, *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    56
      apply unfold_locales
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    57
      txt {* \normalsize hence only the lattice axioms remain to be
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    58
	shown.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    59
        @{subgoals [display]}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    60
	By @{text is_inf} and @{text is_sup}, *}
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)
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    62
      txt {* \normalsize the goals are transformed to these
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    63
	statements:
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    64
	@{subgoals [display]}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    65
	This is Presburger arithmetic, which can be solved by the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    66
	method @{text arith}. *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    67
      by arith+
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    68
    txt {* \normalsize In order to show the equations, we put ourselves
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
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    70
      convenient way. *}
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" .
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    72
    show "lattice.meet op \<le> (x::int) y = min x y"
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    73
      by (bestsimp simp: int.meet_def int.is_inf_def)
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    74
    show "lattice.join op \<le> (x::int) y = max x y"
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
    78
text {* Next follows that @{text "op \<le>"} is a total order, again for
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    79
  the integers. *}
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
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    84
text {* 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}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   126
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   127
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   128
text {* The interpretations for a locale $n$ within the current
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 ``!''.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   147
*}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   148
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   149
27077
f64166dd92f0 moved labels into actual sections;
wenzelm
parents: 27075
diff changeset
   150
section {* Locale Expressions \label{sec:expressions} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   151
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   152
text {*
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   209
  declaration. *}
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   217
text (in order_preserving) {* Here are examples of theorems that are
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>}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   231
  with the following declaration: *}
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
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   236
text (in order_preserving) {* 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}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   238
  @{thm [display, indent=2] le'.less_le_trans} *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   239
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   240
text {* There are short notations for locale expressions.  These are
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   241
  discussed in the following. *}
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
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   244
subsection {* Default Instantiations *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   245
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   246
text {* 
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   253
  Section~\ref{sec:changing-the-hierarchy}. *}
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
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   256
subsection {* Implicit Parameters \label{sec:implicit-parameters} *}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   257
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   258
text {* In a locale expression that occurs within a locale
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}.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   284
 *}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   285
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   286
text{*
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
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   289
  join. *}
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
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   297
text {* The parameter instantiation in the first instance of @{term
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.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   305
*}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   306
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   307
  context lattice_hom begin
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   308
  abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   309
  abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   310
  end
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   311
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   312
text {* The next example makes radical use of the short hand
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   313
  facilities.  A homomorphism is an endomorphism if both orders
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   314
  coincide. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   315
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   316
  locale lattice_end = lattice_hom _ le
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   317
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   318
text {* The notation~@{text _} enables to omit a parameter in a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   319
  positional instantiation.  The omitted parameter,~@{text le} becomes
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   320
  the parameter of the declared locale and is, in the following
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   321
  position, used to instantiate the second parameter of @{text
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   322
  lattice_hom}.  The effect is that of identifying the first in second
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   323
  parameter of the homomorphism locale. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   324
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   325
text {* The inheritance diagram of the situation we have now is shown
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   326
  in Figure~\ref{fig:hom}, where the dashed line depicts an
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   327
  interpretation which is introduced below.  Parameter instantiations
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   328
  are indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   329
  the inheritance diagram it would seem
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   330
  that two identical copies of each of the locales @{text
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   331
  partial_order} and @{text lattice} are imported by @{text
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   332
  lattice_end}.  This is not the case!  Inheritance paths with
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   333
  identical morphisms are automatically detected and
27503
a019d6568a3c fix typo
huffman
parents: 27081
diff changeset
   334
  the conclusions of the respective locales appear only once.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   335
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   336
\begin{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   337
\hrule \vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   338
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   339
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   340
  \node (o) at (0,0) {@{text partial_order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   341
  \node (oh) at (1.5,-2) {@{text order_preserving}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   342
  \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   343
  \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   344
  \node (l) at (-1.5,-2) {@{text lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   345
  \node (lh) at (0,-4) {@{text lattice_hom}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   346
  \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   347
  \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   348
  \node (le) at (0,-6) {@{text lattice_end}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   349
  \node (le1) at (0,-4.8)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   350
    [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   351
  \node (le2) at (0,-5.2)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   352
    [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   353
  \draw (o) -- (l);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   354
  \draw[dashed] (oh) -- (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   355
  \draw (lh) -- (le);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   356
  \draw (o) .. controls (oh1.south west) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   357
  \draw (o) .. controls (oh2.north east) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   358
  \draw (l) .. controls (lh1.south west) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   359
  \draw (l) .. controls (lh2.north east) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   360
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   361
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   362
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   363
\caption{Hierarchy of Homomorphism Locales.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   364
\label{fig:hom}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   365
\end{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   366
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   367
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   368
text {* It can be shown easily that a lattice homomorphism is order
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   369
  preserving.  As the final example of this section, a locale
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   370
  interpretation is used to assert this: *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   371
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   372
  sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   373
    fix x y
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   374
    assume "x \<sqsubseteq> y"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   375
    then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   376
    then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   377
    then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   378
  qed
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   379
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   380
text (in lattice_hom) {*
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   381
  Theorems and other declarations --- syntax, in particular --- from
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   382
  the locale @{text order_preserving} are now active in @{text
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   383
  lattice_hom}, for example
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   384
  @{thm [source] hom_le}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   385
  @{thm [display, indent=2] hom_le}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   386
  This theorem will be useful in the following section.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   387
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   388
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   389
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   390
section {* Conditional Interpretation *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   391
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   392
text {* There are situations where an interpretation is not possible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   393
  in the general case since the desired property is only valid if
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   394
  certain conditions are fulfilled.  Take, for example, the function
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   395
  @{text "\<lambda>i. n * i"} that scales its argument by a constant factor.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   396
  This function is order preserving (and even a lattice endomorphism)
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   397
  with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   398
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   399
  It is not possible to express this using a global interpretation,
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   400
  because it is in general unspecified whether~@{term n} is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   401
  non-negative, but one may make an interpretation in an inner context
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   402
  of a proof where full information is available.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   403
  This is not fully satisfactory either, since potentially
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   404
  interpretations may be required to make interpretations in many
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   405
  contexts.  What is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   406
  required is an interpretation that depends on the condition --- and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   407
  this can be done with the \isakeyword{sublocale} command.  For this
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   408
  purpose, we introduce a locale for the condition. *}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   409
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   410
  locale non_negative =
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   411
    fixes n :: int
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   412
    assumes non_neg: "0 \<le> n"
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   413
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   414
text {* It is again convenient to make the interpretation in an
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   415
  incremental fashion, first for order preserving maps, the for
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   416
  lattice endomorphisms. *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   417
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   418
  sublocale non_negative \<subseteq>
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   419
      order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   420
    using non_neg by unfold_locales (rule mult_left_mono)
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   421
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   422
text {* While the proof of the previous interpretation
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   423
  is straightforward from monotonicity lemmas for~@{term "op *"}, the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   424
  second proof follows a useful pattern. *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   425
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   426
  sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   427
  proof (unfold_locales, unfold int_min_eq int_max_eq)
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   428
    txt {* \normalsize Unfolding the locale predicates \emph{and} the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   429
      interpretation equations immediately yields two subgoals that
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   430
      reflect the core conjecture.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   431
      @{subgoals [display]}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   432
      It is now necessary to show, in the context of @{term
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   433
      non_negative}, that multiplication by~@{term n} commutes with
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   434
      @{term min} and @{term max}. *}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   435
  qed (auto simp: hom_le)
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   436
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   437
text (in order_preserving) {* The lemma @{thm [source] hom_le}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   438
  simplifies a proof that would have otherwise been lengthy and we may
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   439
  consider making it a default rule for the simplifier: *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   440
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   441
  lemmas (in order_preserving) hom_le [simp]
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   442
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   443
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   444
subsection {* Avoiding Infinite Chains of Interpretations
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   445
  \label{sec:infinite-chains} *}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   446
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   447
text {* Similar situations arise frequently in formalisations of
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   448
  abstract algebra where it is desirable to express that certain
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   449
  constructions preserve certain properties.  For example, polynomials
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   450
  over rings are rings, or --- an example from the domain where the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   451
  illustrations of this tutorial are taken from --- a partial order
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   452
  may be obtained for a function space by point-wise lifting of the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   453
  partial order of the co-domain.  This corresponds to the following
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   454
  interpretation: *}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   455
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   456
  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
   457
    oops
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   458
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   459
text {* Unfortunately this is a cyclic interpretation that leads to an
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   460
  infinite chain, namely
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   461
  @{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
   462
  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
   463
  and the interpretation is rejected.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   464
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   465
  Instead it is necessary to declare a locale that is logically
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   466
  equivalent to @{term partial_order} but serves to collect facts
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   467
  about functions spaces where the co-domain is a partial order, and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   468
  to make the interpretation in its context: *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   469
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   470
  locale fun_partial_order = partial_order
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   471
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   472
  sublocale fun_partial_order \<subseteq>
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   473
      f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   474
    by unfold_locales (fast,rule,fast,blast intro: trans)
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   475
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   476
text {* It is quite common in abstract algebra that such a construction
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   477
  maps a hierarchy of algebraic structures (or specifications) to a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   478
  related hierarchy.  By means of the same lifting, a function space
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   479
  is a lattice if its co-domain is a lattice: *}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   480
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   481
  locale fun_lattice = fun_partial_order + lattice
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   482
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   483
  sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   484
    proof unfold_locales
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   485
    fix f g
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   486
    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
   487
      apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   488
    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
   489
      by fast
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   490
  next
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   491
    fix f g
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   492
    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
   493
      apply (rule is_supI) apply rule+ apply (drule spec, assumption)+ done
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   494
    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
   495
      by fast
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   496
  qed
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   497
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   498
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   499
section {* Further Reading *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   500
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   501
text {* More information on locales and their interpretation is
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   502
  available.  For the locale hierarchy of import and interpretation
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   503
  dependencies see~\cite{Ballarin2006a}; interpretations in theories
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   504
  and proofs are covered in~\cite{Ballarin2006b}.  In the latter, I
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   505
  show how interpretation in proofs enables to reason about families
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   506
  of algebraic structures, which cannot be expressed with locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   507
  directly.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   508
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   509
  Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   510
  of axiomatic type classes through a combination with locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   511
  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
   512
  facility to generate ML and Haskell code.  Classes are sufficient for
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   513
  simple specifications with a single type parameter.  The locales for
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   514
  orders and lattices presented in this tutorial fall into this
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   515
  category.  Order preserving maps, homomorphisms and vector spaces,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   516
  on the other hand, do not.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   517
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   518
  The locales reimplementation for Isabelle 2009 provides, among other
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   519
  improvements, a clean integration with Isabelle/Isar's local theory
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   520
  mechanisms, which are described in another paper by Haftmann and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   521
  Wenzel~\cite{HaftmannWenzel2009}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   522
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   523
  The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   524
  may be of interest from a historical perspective.  My previous
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   525
  report on locales and locale expressions~\cite{Ballarin2004a}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   526
  describes a simpler form of expressions than available now and is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   527
  outdated. The mathematical background on orders and lattices is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   528
  taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   529
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   530
  The sources of this tutorial, which include all proofs, are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   531
  available with the Isabelle distribution at
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   532
  \url{http://isabelle.in.tum.de}.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   533
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   534
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   535
text {*
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   536
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   537
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   538
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   539
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   540
\begin{tabular}{l>$c<$l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   541
  \multicolumn{3}{l}{Miscellaneous} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   542
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   543
  \textit{attr-name} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   544
  & \textit{name} $|$ \textit{attribute} $|$
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   545
    \textit{name} \textit{attribute} \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   546
  \textit{qualifier} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   547
  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   548
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   549
  \multicolumn{3}{l}{Context Elements} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   550
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   551
  \textit{fixes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   552
  & \textit{name} [ ``\textbf{::}'' \textit{type} ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   553
    [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   554
    \textit{mixfix} ] \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   555
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   556
  \textit{constrains} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   557
  & \textit{name} ``\textbf{::}'' \textit{type} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   558
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   559
  \textit{assumes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   560
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   561
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   562
  \textit{defines} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   563
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   564
  \textit{notes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   565
  & [ \textit{attr-name} ``\textbf{=}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   566
    ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   567
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   568
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   569
  \textit{element} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   570
  & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   571
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   572
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   573
  & \textbf{constrains} \textit{constrains}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   574
    ( \textbf{and} \textit{constrains} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   575
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   576
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   577
  & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   578
%\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   579
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   580
%  & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   581
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   582
%  & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   583
%\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   584
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   585
  \multicolumn{3}{l}{Locale Expressions} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   586
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   587
  \textit{pos-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   588
  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   589
  \textit{named-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   590
  & \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
   591
  ( \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
   592
  \textit{instance} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   593
  & [ \textit{qualifier} ``\textbf{:}'' ]
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   594
    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   595
  \textit{expression}  & ::= 
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   596
  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   597
    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   598
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   599
  \multicolumn{3}{l}{Declaration of Locales} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   600
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   601
  \textit{locale} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   602
  & \textit{element}$^+$ \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   603
  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   604
  \textit{toplevel} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   605
  & \textbf{locale} \textit{name} [ ``\textbf{=}''
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   606
    \textit{locale} ] \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   607
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   608
  \multicolumn{3}{l}{Interpretation} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   609
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   610
  \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   611
    \textit{prop} \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   612
  \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
   613
    \textit{equation} )$^*$  \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   614
  \textit{toplevel} & ::=
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   615
  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   616
    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   617
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   618
  & \textbf{interpretation}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   619
    \textit{expression} [ \textit{equations} ] \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   620
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   621
  & \textbf{interpret}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 27595
diff changeset
   622
    \textit{expression} \textit{proof} \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   623
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   624
  \multicolumn{3}{l}{Diagnostics} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   625
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   626
  \textit{toplevel} & ::=
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   627
  & \textbf{print\_locales} \\
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   628
  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   629
  & | & \textbf{print\_interps} \textit{locale}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   630
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   631
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   632
\hrule
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   633
\caption{Syntax of Locale Commands.}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   634
\label{tab:commands}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   635
\end{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   636
  *}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   637
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   638
text {* \textbf{Revision History.}  For the present third revision of
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   639
  the tutorial, much of the explanatory text
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   640
  was rewritten.  Inheritance of interpretation equations is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   641
  available with the forthcoming release of Isabelle, which at the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   642
  time of editing these notes is expected for the end of 2009.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   643
  The second revision accommodates changes introduced by the locales
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   644
  reimplementation for Isabelle 2009.  Most notably locale expressions
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   645
  have been generalised from renaming to instantiation.  *}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   646
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   647
text {* \textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32804
diff changeset
   648
  Randy Pollack, Christian Sternagel and Makarius Wenzel have made
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   649
  useful comments on earlier versions of this document.  The section
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   650
  on conditional interpretation was inspired by a number of e-mail
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   651
  enquiries the author received from locale users, and which suggested
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   652
  that this use case is important enough to deserve explicit
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   653
  explanation.  The term \emph{conditional interpretation} is due to
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   654
  Larry Paulson. *}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   655
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   656
end