doc-src/Locales/Locales/document/Examples3.tex
author wenzelm
Mon, 01 Mar 2010 21:41:35 +0100
changeset 35423 6ef9525a5727
parent 33868 62251d6b0038
child 37206 7f2a6f3143ad
permissions -rw-r--r--
eliminated hard tabs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     1
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     2
\begin{isabellebody}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     3
\def\isabellecontext{Examples{\isadigit{3}}}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     4
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     5
\isadelimtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     6
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     7
\endisadelimtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     8
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
     9
\isatagtheory
27080
0ee385433247 updated generated file;
wenzelm
parents: 27079
diff changeset
    10
\isacommand{theory}\isamarkupfalse%
0ee385433247 updated generated file;
wenzelm
parents: 27079
diff changeset
    11
\ Examples{\isadigit{3}}\isanewline
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    12
\isakeyword{imports}\ Examples\isanewline
27080
0ee385433247 updated generated file;
wenzelm
parents: 27079
diff changeset
    13
\isakeyword{begin}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    14
\endisatagtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    15
{\isafoldtheory}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    16
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    17
\isadelimtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    18
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    19
\endisadelimtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    20
%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    21
\begin{isamarkuptext}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    22
\vspace{-5ex}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    23
\end{isamarkuptext}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    24
\isamarkuptrue%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    25
%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    26
\isamarkupsubsection{Third Version: Local Interpretation
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    27
  \label{sec:local-interpretation}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    28
}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    29
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    30
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    31
\begin{isamarkuptext}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    32
In the above example, the fact that \isa{op\ {\isasymle}} is a partial
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    33
  order for the integers was used in the second goal to
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    34
  discharge the premise in the definition of \isa{op\ {\isasymsqsubset}}.  In
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    35
  general, proofs of the equations not only may involve definitions
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    36
  from the interpreted locale but arbitrarily complex arguments in the
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    37
  context of the locale.  Therefore is would be convenient to have the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    38
  interpreted locale conclusions temporary available in the proof.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    39
  This can be achieved by a locale interpretation in the proof body.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    40
  The command for local interpretations is \isakeyword{interpret}.  We
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    41
  repeat the example from the previous section to illustrate this.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    42
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    43
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    44
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    45
\isadelimvisible
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    46
\ \ %
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    47
\endisadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    48
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    49
\isatagvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    50
\isacommand{interpretation}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    51
\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    52
\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    53
\ \ \isacommand{proof}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    54
\ {\isacharminus}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    55
\ \ \ \ \isacommand{show}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    56
\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    57
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    58
\ unfold{\isacharunderscore}locales\ auto\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    59
\ \ \ \ \isacommand{then}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    60
\ \isacommand{interpret}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    61
\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}int{\isacharcomma}\ int{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    62
\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    63
\ \ \ \ \isacommand{show}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    64
\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    65
\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
    66
\ int{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    67
\ auto\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    68
\ \ \isacommand{qed}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    69
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    70
\endisatagvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    71
{\isafoldvisible}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    72
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    73
\isadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    74
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    75
\endisadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    76
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    77
\begin{isamarkuptext}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    78
The inner interpretation is immediate from the preceding fact
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    79
  and proved by assumption (Isar short hand ``.'').  It enriches the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    80
  local proof context by the theorems
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    81
  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
    82
  and \isa{int{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
    83
  definition.  Theorems from the local interpretation disappear after
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    84
  leaving the proof context --- that is, after the succeeding
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    85
  \isakeyword{next} or \isakeyword{qed} statement.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    86
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    87
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    88
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    89
\isamarkupsubsection{Further Interpretations%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    90
}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    91
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    92
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
    93
\begin{isamarkuptext}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    94
Further interpretations are necessary for
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    95
  the other locales.  In \isa{lattice} the operations~\isa{{\isasymsqinter}}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    96
  and~\isa{{\isasymsqunion}} are substituted by \isa{min}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    97
  and \isa{max}.  The entire proof for the
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
    98
  interpretation is reproduced to give an example of a more
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
    99
  elaborate interpretation proof.  Note that the equations are named
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   100
  so they can be used in a later example.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   101
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   102
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   103
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   104
\isadelimvisible
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   105
\ \ %
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   106
\endisadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   107
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   108
\isatagvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   109
\isacommand{interpretation}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   110
\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   111
\ \ \ \ \isakeyword{where}\ int{\isacharunderscore}min{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   112
\ \ \ \ \ \ \isakeyword{and}\ int{\isacharunderscore}max{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   113
\ \ \isacommand{proof}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   114
\ {\isacharminus}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   115
\ \ \ \ \isacommand{show}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   116
\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   117
\begin{isamarkuptxt}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   118
\normalsize We have already shown that this is a partial
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   119
	order,%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   120
\end{isamarkuptxt}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   121
\isamarkuptrue%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   122
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   123
\ unfold{\isacharunderscore}locales%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   124
\begin{isamarkuptxt}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   125
\normalsize hence only the lattice axioms remain to be
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   126
	shown.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   127
        \begin{isabelle}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   128
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ op\ {\isasymle}\ x\ y\ inf\isanewline
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   129
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ op\ {\isasymle}\ x\ y\ sup%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   130
\end{isabelle}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   131
	By \isa{is{\isacharunderscore}inf} and \isa{is{\isacharunderscore}sup},%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   132
\end{isamarkuptxt}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   133
\isamarkuptrue%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   134
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   135
\ {\isacharparenleft}unfold\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   136
\begin{isamarkuptxt}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   137
\normalsize the goals are transformed to these
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   138
	statements:
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   139
	\begin{isabelle}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   140
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isasymle}x{\isachardot}\ inf\ {\isasymle}\ y\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ z\ {\isasymle}\ x\ {\isasymand}\ z\ {\isasymle}\ y\ {\isasymlongrightarrow}\ z\ {\isasymle}\ inf{\isacharparenright}\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   141
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   142
\end{isabelle}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   143
	This is Presburger arithmetic, which can be solved by the
35423
6ef9525a5727 eliminated hard tabs;
wenzelm
parents: 33868
diff changeset
   144
        method \isa{arith}.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   145
\end{isamarkuptxt}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   146
\isamarkuptrue%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   147
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   148
\ arith{\isacharplus}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   149
\begin{isamarkuptxt}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   150
\normalsize In order to show the equations, we put ourselves
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   151
      in a situation where the lattice theorems can be used in a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   152
      convenient way.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   153
\end{isamarkuptxt}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   154
\isamarkuptrue%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   155
\ \ \ \ \isacommand{then}\isamarkupfalse%
32836
4c6e3e7ac2bf updated generated files;
wenzelm
parents: 31960
diff changeset
   156
\ \isacommand{interpret}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   157
\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   158
\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   159
\ \ \ \ \isacommand{show}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   160
\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   161
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   162
\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}meet{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   163
\ \ \ \ \isacommand{show}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   164
\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   165
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   166
\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}join{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   167
\ \ \isacommand{qed}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   168
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   169
\endisatagvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   170
{\isafoldvisible}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   171
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   172
\isadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   173
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   174
\endisadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   175
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   176
\begin{isamarkuptext}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   177
Next follows that \isa{op\ {\isasymle}} is a total order, again for
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   178
  the integers.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   179
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   180
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   181
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   182
\isadelimvisible
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   183
\ \ %
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   184
\endisadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   185
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   186
\isatagvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   187
\isacommand{interpretation}\isamarkupfalse%
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   188
\ int{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   189
\ \ \ \ \isacommand{by}\isamarkupfalse%
32836
4c6e3e7ac2bf updated generated files;
wenzelm
parents: 31960
diff changeset
   190
\ unfold{\isacharunderscore}locales\ arith%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   191
\endisatagvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   192
{\isafoldvisible}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   193
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   194
\isadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   195
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   196
\endisadelimvisible
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   197
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   198
\begin{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   199
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
   200
  Table~\ref{tab:int-lattice}.  Two points are worth noting:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   201
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   202
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   203
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   204
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   205
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   206
\begin{tabular}{l}
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   207
  \isa{int{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   208
  \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   209
  \isa{int{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   210
  \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   211
  \isa{int{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   212
  \quad \isa{max\ {\isacharquery}x\ {\isacharparenleft}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ min\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   213
  \isa{int{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
30782
38e477e8524f In interpretation: equations are not propagated through the hierarchy automatically.
ballarin
parents: 30780
diff changeset
   214
  \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   215
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   216
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   217
\hrule
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   218
\caption{Interpreted theorems for~\isa{{\isasymle}} on the integers.}
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   219
\label{tab:int-lattice}
32836
4c6e3e7ac2bf updated generated files;
wenzelm
parents: 31960
diff changeset
   220
\end{table}
4c6e3e7ac2bf updated generated files;
wenzelm
parents: 31960
diff changeset
   221
4c6e3e7ac2bf updated generated files;
wenzelm
parents: 31960
diff changeset
   222
\begin{itemize}
4c6e3e7ac2bf updated generated files;
wenzelm
parents: 31960
diff changeset
   223
\item
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   224
  Locale \isa{distrib{\isacharunderscore}lattice} was also interpreted.  Since the
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   225
  locale hierarchy reflects that total orders are distributive
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   226
  lattices, the interpretation of the latter was inserted
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   227
  automatically with the interpretation of the former.  In general,
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   228
  interpretation traverses the locale hierarchy upwards and interprets
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   229
  all encountered locales, regardless whether imported or proved via
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   230
  the \isakeyword{sublocale} command.  Existing interpretations are
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   231
  skipped avoiding duplicate work.
32836
4c6e3e7ac2bf updated generated files;
wenzelm
parents: 31960
diff changeset
   232
\item
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   233
  The predicate \isa{op\ {\isacharless}} appears in theorem \isa{int{\isachardot}less{\isacharunderscore}total}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   234
  although an equation for the replacement of \isa{op\ {\isasymsqsubset}} was only
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   235
  given in the interpretation of \isa{partial{\isacharunderscore}order}.  The
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   236
  interpretation equations are pushed downwards the hierarchy for
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   237
  related interpretations --- that is, for interpretations that share
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   238
  the instances of parameters they have in common.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   239
\end{itemize}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   240
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   241
\isamarkuptrue%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   242
%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   243
\begin{isamarkuptext}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   244
The interpretations for a locale $n$ within the current
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   245
  theory may be inspected with \isakeyword{print\_interps}~$n$.  This
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   246
  prints the list of instances of $n$, for which interpretations exist.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   247
  For example, \isakeyword{print\_interps} \isa{partial{\isacharunderscore}order}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   248
  outputs the following:
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   249
\begin{small}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   250
\begin{alltt}
32982
40810d98f4c9 Changed part of the examples to int.
ballarin
parents: 32981
diff changeset
   251
  int! : partial_order "op \(\le\)"
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   252
\end{alltt}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   253
\end{small}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   254
  Of course, there is only one interpretation.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   255
  The interpretation qualifier on the left is decorated with an
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   256
  exclamation point.  This means that it is mandatory.  Qualifiers
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   257
  can either be \emph{mandatory} or \emph{optional}, designated by
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   258
  ``!'' or ``?'' respectively.  Mandatory qualifiers must occur in a
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   259
  name reference while optional ones need not.  Mandatory qualifiers
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   260
  prevent accidental hiding of names, while optional qualifiers can be
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   261
  more convenient to use.  For \isakeyword{interpretation}, the
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   262
  default is ``!''.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   263
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   264
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   265
%
27079
61ac01ff0aa9 updated generated file;
wenzelm
parents: 27075
diff changeset
   266
\isamarkupsection{Locale Expressions \label{sec:expressions}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   267
}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   268
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   269
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   270
\begin{isamarkuptext}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   271
A map~\isa{{\isasymphi}} between partial orders~\isa{{\isasymsqsubseteq}} and~\isa{{\isasympreceq}}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   272
  is called order preserving if \isa{x\ {\isasymsqsubseteq}\ y} implies \isa{{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y}.  This situation is more complex than those encountered so
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   273
  far: it involves two partial orders, and it is desirable to use the
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   274
  existing locale for both.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   275
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   276
  A locale for order preserving maps requires three parameters: \isa{le}~(\isakeyword{infixl}~\isa{{\isasymsqsubseteq}}) and \isa{le{\isacharprime}}~(\isakeyword{infixl}~\isa{{\isasympreceq}}) for the orders and~\isa{{\isasymphi}}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   277
  for the map.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   278
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   279
  In order to reuse the existing locale for partial orders, which has
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   280
  the single parameter~\isa{le}, it must be imported twice, once
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   281
  mapping its parameter to~\isa{le} from the new locale and once
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   282
  to~\isa{le{\isacharprime}}.  This can be achieved with a compound locale
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   283
  expression.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   284
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   285
  In general, a locale expression is a sequence of \emph{locale instances}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   286
  separated by~``$\textbf{+}$'' and followed by a \isakeyword{for}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   287
  clause.
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   288
  An instance has the following format:
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   289
\begin{quote}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   290
  \textit{qualifier} \textbf{:} \textit{locale-name}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   291
  \textit{parameter-instantiation}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   292
\end{quote}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   293
  We have already seen locale instances as arguments to
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   294
  \isakeyword{interpretation} in Section~\ref{sec:interpretation}.
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   295
  As before, the qualifier serves to disambiguate names from
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   296
  different instances of the same locale.  While in
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   297
  \isakeyword{interpretation} qualifiers default to mandatory, in
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   298
  import and in the \isakeyword{sublocale} command, they default to
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   299
  optional.
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   300
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   301
  Since the parameters~\isa{le} and~\isa{le{\isacharprime}} are to be partial
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   302
  orders, our locale for order preserving maps will import the these
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   303
  instances:
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   304
\begin{small}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   305
\begin{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   306
  le: partial_order le
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   307
  le': partial_order le'
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   308
\end{alltt}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   309
\end{small}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   310
  For matter of convenience we choose to name parameter names and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   311
  qualifiers alike.  This is an arbitrary decision.  Technically, qualifiers
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   312
  and parameters are unrelated.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   313
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   314
  Having determined the instances, let us turn to the \isakeyword{for}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   315
  clause.  It serves to declare locale parameters in the same way as
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   316
  the context element \isakeyword{fixes} does.  Context elements can
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   317
  only occur after the import section, and therefore the parameters
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   318
  referred to in the instances must be declared in the \isakeyword{for}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   319
  clause.  The \isakeyword{for} clause is also where the syntax of these
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   320
  parameters is declared.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   321
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   322
  Two context elements for the map parameter~\isa{{\isasymphi}} and the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   323
  assumptions that it is order preserving complete the locale
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   324
  declaration.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   325
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   326
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   327
\ \ \isacommand{locale}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   328
\ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   329
\ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ le\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\isanewline
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   330
\ \ \ \ \ \ \isakeyword{for}\ le\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqsubseteq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   331
\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   332
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   333
\begin{isamarkuptext}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   334
Here are examples of theorems that are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   335
  available in the locale:
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   336
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   337
  \hspace*{1em}\isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   338
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   339
  \hspace*{1em}\isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   340
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   341
  \hspace*{1em}\isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   342
  \begin{isabelle}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   343
\ \ \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   344
\isaindent{\ \ \ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   345
\end{isabelle}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   346
  While there is infix syntax for the strict operation associated to
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   347
  \isa{op\ {\isasymsqsubseteq}}, there is none for the strict version of \isa{op\ {\isasympreceq}}.  The abbreviation \isa{less} with its infix syntax is only
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   348
  available for the original instance it was declared for.  We may
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   349
  introduce the abbreviation \isa{less{\isacharprime}} with infix syntax~\isa{{\isasymprec}}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   350
  with the following declaration:%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   351
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   352
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   353
\ \ \isacommand{abbreviation}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   354
\ {\isacharparenleft}\isakeyword{in}\ order{\isacharunderscore}preserving{\isacharparenright}\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   355
\ \ \ \ less{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymprec}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}less{\isacharprime}\ {\isasymequiv}\ partial{\isacharunderscore}order{\isachardot}less\ le{\isacharprime}{\isachardoublequoteclose}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   356
\begin{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   357
Now the theorem is displayed nicely as
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   358
  \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   359
  \begin{isabelle}%
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   360
\ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z%
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   361
\end{isabelle}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   362
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   363
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   364
%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   365
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   366
There are short notations for locale expressions.  These are
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   367
  discussed in the following.%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   368
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   369
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   370
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   371
\isamarkupsubsection{Default Instantiations%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   372
}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   373
\isamarkuptrue%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   374
%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   375
\begin{isamarkuptext}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   376
It is possible to omit parameter instantiations.  The
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   377
  instantiation then defaults to the name of
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   378
  the parameter itself.  For example, the locale expression \isa{partial{\isacharunderscore}order} is short for \isa{partial{\isacharunderscore}order\ le}, since the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   379
  locale's single parameter is~\isa{le}.  We took advantage of this
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   380
  in the \isakeyword{sublocale} declarations of
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   381
  Section~\ref{sec:changing-the-hierarchy}.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   382
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   383
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   384
%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   385
\isamarkupsubsection{Implicit Parameters \label{sec:implicit-parameters}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   386
}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   387
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   388
%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   389
\begin{isamarkuptext}%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   390
In a locale expression that occurs within a locale
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   391
  declaration, omitted parameters additionally extend the (possibly
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   392
  empty) \isakeyword{for} clause.
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   393
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   394
  The \isakeyword{for} clause is a general construct of Isabelle/Isar
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   395
  to mark names occurring in the preceding declaration as ``arbitrary
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   396
  but fixed''.  This is necessary for example, if the name is already
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   397
  bound in a surrounding context.  In a locale expression, names
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   398
  occurring in parameter instantiations should be bound by a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   399
  \isakeyword{for} clause whenever these names are not introduced
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   400
  elsewhere in the context --- for example, on the left hand side of a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   401
  \isakeyword{sublocale} declaration.
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   402
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   403
  There is an exception to this rule in locale declarations, where the
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   404
  \isakeyword{for} clause serves to declare locale parameters.  Here,
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   405
  locale parameters for which no parameter instantiation is given are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   406
  implicitly added, with their mixfix syntax, at the beginning of the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   407
  \isakeyword{for} clause.  For example, in a locale declaration, the
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   408
  expression \isa{partial{\isacharunderscore}order} is short for
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   409
\begin{small}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   410
\begin{alltt}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   411
  partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   412
\end{alltt}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   413
\end{small}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   414
  This short hand was used in the locale declarations throughout
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   415
  Section~\ref{sec:import}.%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   416
\end{isamarkuptext}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   417
\isamarkuptrue%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   418
%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   419
\begin{isamarkuptext}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   420
The following locale declarations provide more examples.  A
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   421
  map~\isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   422
  join.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   423
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   424
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   425
\ \ \isacommand{locale}\isamarkupfalse%
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   426
\ lattice{\isacharunderscore}hom\ {\isacharequal}\isanewline
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   427
\ \ \ \ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   428
\ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   429
\ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqinter}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}meet\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   430
\ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}\ {\isacharequal}\ le{\isacharprime}{\isachardot}join\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   431
\begin{isamarkuptext}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   432
The parameter instantiation in the first instance of \isa{lattice} is omitted.  This causes the parameter~\isa{le} to be
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   433
  added to the \isakeyword{for} clause, and the locale has
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   434
  parameters~\isa{le},~\isa{le{\isacharprime}} and, of course,~\isa{{\isasymphi}}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   435
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   436
  Before turning to the second example, we complete the locale by
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   437
  providing infix syntax for the meet and join operations of the
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   438
  second lattice.%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   439
\end{isamarkuptext}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   440
\isamarkuptrue%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   441
\ \ \isacommand{context}\isamarkupfalse%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   442
\ lattice{\isacharunderscore}hom\ \isakeyword{begin}\isanewline
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   443
\ \ \isacommand{abbreviation}\isamarkupfalse%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   444
\ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   445
\ \ \isacommand{abbreviation}\isamarkupfalse%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   446
\ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}\isanewline
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   447
\ \ \isacommand{end}\isamarkupfalse%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   448
%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   449
\begin{isamarkuptext}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   450
The next example makes radical use of the short hand
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   451
  facilities.  A homomorphism is an endomorphism if both orders
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   452
  coincide.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   453
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   454
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   455
\ \ \isacommand{locale}\isamarkupfalse%
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   456
\ lattice{\isacharunderscore}end\ {\isacharequal}\ lattice{\isacharunderscore}hom\ {\isacharunderscore}\ le%
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   457
\begin{isamarkuptext}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   458
The notation~\isa{{\isacharunderscore}} enables to omit a parameter in a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   459
  positional instantiation.  The omitted parameter,~\isa{le} becomes
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   460
  the parameter of the declared locale and is, in the following
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   461
  position, used to instantiate the second parameter of \isa{lattice{\isacharunderscore}hom}.  The effect is that of identifying the first in second
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   462
  parameter of the homomorphism locale.%
30750
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   463
\end{isamarkuptext}%
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   464
\isamarkuptrue%
3779e2158dad Update explanation of locale expressions to locale reimplementation.
ballarin
parents: 30580
diff changeset
   465
%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   466
\begin{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   467
The inheritance diagram of the situation we have now is shown
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   468
  in Figure~\ref{fig:hom}, where the dashed line depicts an
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   469
  interpretation which is introduced below.  Parameter instantiations
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   470
  are indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   471
  the inheritance diagram it would seem
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   472
  that two identical copies of each of the locales \isa{partial{\isacharunderscore}order} and \isa{lattice} are imported by \isa{lattice{\isacharunderscore}end}.  This is not the case!  Inheritance paths with
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   473
  identical morphisms are automatically detected and
27506
c99c72458ec5 updated generated file;
wenzelm
parents: 27080
diff changeset
   474
  the conclusions of the respective locales appear only once.
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   475
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   476
\begin{figure}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   477
\hrule \vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   478
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   479
\begin{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   480
  \node (o) at (0,0) {\isa{partial{\isacharunderscore}order}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   481
  \node (oh) at (1.5,-2) {\isa{order{\isacharunderscore}preserving}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   482
  \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   483
  \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   484
  \node (l) at (-1.5,-2) {\isa{lattice}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   485
  \node (lh) at (0,-4) {\isa{lattice{\isacharunderscore}hom}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   486
  \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   487
  \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   488
  \node (le) at (0,-6) {\isa{lattice{\isacharunderscore}end}};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   489
  \node (le1) at (0,-4.8)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   490
    [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   491
  \node (le2) at (0,-5.2)
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   492
    [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$};
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   493
  \draw (o) -- (l);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   494
  \draw[dashed] (oh) -- (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   495
  \draw (lh) -- (le);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   496
  \draw (o) .. controls (oh1.south west) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   497
  \draw (o) .. controls (oh2.north east) .. (oh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   498
  \draw (l) .. controls (lh1.south west) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   499
  \draw (l) .. controls (lh2.north east) .. (lh);
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   500
\end{tikzpicture}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   501
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   502
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   503
\caption{Hierarchy of Homomorphism Locales.}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   504
\label{fig:hom}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   505
\end{figure}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   506
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   507
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   508
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   509
\begin{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   510
It can be shown easily that a lattice homomorphism is order
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   511
  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
   512
  interpretation is used to assert this:%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   513
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   514
\isamarkuptrue%
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   515
\ \ \isacommand{sublocale}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   516
\ lattice{\isacharunderscore}hom\ {\isasymsubseteq}\ order{\isacharunderscore}preserving%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   517
\isadelimproof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   518
\ %
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   519
\endisadelimproof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   520
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   521
\isatagproof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   522
\isacommand{proof}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   523
\ unfold{\isacharunderscore}locales\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   524
\ \ \ \ \isacommand{fix}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   525
\ x\ y\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   526
\ \ \ \ \isacommand{assume}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   527
\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y{\isachardoublequoteclose}\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   528
\ \ \ \ \isacommand{then}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   529
\ \isacommand{have}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   530
\ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   531
\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   532
\ \ \ \ \isacommand{then}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   533
\ \isacommand{have}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   534
\ {\isachardoublequoteopen}{\isasymphi}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymphi}\ x\ {\isasymsqunion}{\isacharprime}\ {\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   535
\ {\isacharparenleft}simp\ add{\isacharcolon}\ hom{\isacharunderscore}join\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   536
\ \ \ \ \isacommand{then}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   537
\ \isacommand{show}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   538
\ {\isachardoublequoteopen}{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   539
\ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   540
\ \ \isacommand{qed}\isamarkupfalse%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   541
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   542
\endisatagproof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   543
{\isafoldproof}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   544
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   545
\isadelimproof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   546
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   547
\endisadelimproof
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   548
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   549
\begin{isamarkuptext}%
30393
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   550
Theorems and other declarations --- syntax, in particular --- from
aa6f42252bf6 replaced old locale option by proper "text (in locale)";
wenzelm
parents: 29568
diff changeset
   551
  the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   552
  \isa{hom{\isacharunderscore}le}:
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   553
  \begin{isabelle}%
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   554
\ \ {\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   555
\end{isabelle}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   556
  This theorem will be useful in the following section.%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   557
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   558
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   559
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   560
\isamarkupsection{Conditional Interpretation%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   561
}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   562
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   563
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   564
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   565
There are situations where an interpretation is not possible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   566
  in the general case since the desired property is only valid if
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   567
  certain conditions are fulfilled.  Take, for example, the function
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   568
  \isa{{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i} that scales its argument by a constant factor.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   569
  This function is order preserving (and even a lattice endomorphism)
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   570
  with respect to \isa{op\ {\isasymle}} provided \isa{n\ {\isasymge}\ {\isadigit{0}}}.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   571
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   572
  It is not possible to express this using a global interpretation,
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   573
  because it is in general unspecified whether~\isa{n} is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   574
  non-negative, but one may make an interpretation in an inner context
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   575
  of a proof where full information is available.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   576
  This is not fully satisfactory either, since potentially
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   577
  interpretations may be required to make interpretations in many
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   578
  contexts.  What is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   579
  required is an interpretation that depends on the condition --- and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   580
  this can be done with the \isakeyword{sublocale} command.  For this
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   581
  purpose, we introduce a locale for the condition.%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   582
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   583
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   584
\ \ \isacommand{locale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   585
\ non{\isacharunderscore}negative\ {\isacharequal}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   586
\ \ \ \ \isakeyword{fixes}\ n\ {\isacharcolon}{\isacharcolon}\ int\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   587
\ \ \ \ \isakeyword{assumes}\ non{\isacharunderscore}neg{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymle}\ n{\isachardoublequoteclose}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   588
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   589
It is again convenient to make the interpretation in an
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   590
  incremental fashion, first for order preserving maps, the for
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   591
  lattice endomorphisms.%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   592
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   593
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   594
\ \ \isacommand{sublocale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   595
\ non{\isacharunderscore}negative\ {\isasymsubseteq}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   596
\ \ \ \ \ \ order{\isacharunderscore}preserving\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   597
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   598
\isadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   599
\ \ \ \ %
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   600
\endisadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   601
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   602
\isatagproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   603
\isacommand{using}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   604
\ non{\isacharunderscore}neg\ \isacommand{by}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   605
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ mult{\isacharunderscore}left{\isacharunderscore}mono{\isacharparenright}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   606
\endisatagproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   607
{\isafoldproof}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   608
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   609
\isadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   610
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   611
\endisadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   612
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   613
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   614
While the proof of the previous interpretation
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   615
  is straightforward from monotonicity lemmas for~\isa{op\ {\isacharasterisk}}, the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   616
  second proof follows a useful pattern.%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   617
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   618
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   619
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   620
\isadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   621
\ \ %
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   622
\endisadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   623
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   624
\isatagvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   625
\isacommand{sublocale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   626
\ non{\isacharunderscore}negative\ {\isasymsubseteq}\ lattice{\isacharunderscore}end\ {\isachardoublequoteopen}op\ {\isasymle}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isasymlambda}i{\isachardot}\ n\ {\isacharasterisk}\ i{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   627
\ \ \isacommand{proof}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   628
\ {\isacharparenleft}unfold{\isacharunderscore}locales{\isacharcomma}\ unfold\ int{\isacharunderscore}min{\isacharunderscore}eq\ int{\isacharunderscore}max{\isacharunderscore}eq{\isacharparenright}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   629
\begin{isamarkuptxt}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   630
\normalsize Unfolding the locale predicates \emph{and} the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   631
      interpretation equations immediately yields two subgoals that
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   632
      reflect the core conjecture.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   633
      \begin{isabelle}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   634
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ n\ {\isacharasterisk}\ min\ x\ y\ {\isacharequal}\ min\ {\isacharparenleft}n\ {\isacharasterisk}\ x{\isacharparenright}\ {\isacharparenleft}n\ {\isacharasterisk}\ y{\isacharparenright}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   635
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ n\ {\isacharasterisk}\ max\ x\ y\ {\isacharequal}\ max\ {\isacharparenleft}n\ {\isacharasterisk}\ x{\isacharparenright}\ {\isacharparenleft}n\ {\isacharasterisk}\ y{\isacharparenright}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   636
\end{isabelle}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   637
      It is now necessary to show, in the context of \isa{non{\isacharunderscore}negative}, that multiplication by~\isa{n} commutes with
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   638
      \isa{min} and \isa{max}.%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   639
\end{isamarkuptxt}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   640
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   641
\ \ \isacommand{qed}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   642
\ {\isacharparenleft}auto\ simp{\isacharcolon}\ hom{\isacharunderscore}le{\isacharparenright}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   643
\endisatagvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   644
{\isafoldvisible}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   645
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   646
\isadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   647
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   648
\endisadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   649
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   650
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   651
The lemma \isa{hom{\isacharunderscore}le}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   652
  simplifies a proof that would have otherwise been lengthy and we may
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   653
  consider making it a default rule for the simplifier:%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   654
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   655
\isamarkuptrue%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   656
\ \ \isacommand{lemmas}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   657
\ {\isacharparenleft}\isakeyword{in}\ order{\isacharunderscore}preserving{\isacharparenright}\ hom{\isacharunderscore}le\ {\isacharbrackleft}simp{\isacharbrackright}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   658
\isamarkupsubsection{Avoiding Infinite Chains of Interpretations
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   659
  \label{sec:infinite-chains}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   660
}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   661
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   662
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   663
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   664
Similar situations arise frequently in formalisations of
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   665
  abstract algebra where it is desirable to express that certain
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   666
  constructions preserve certain properties.  For example, polynomials
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   667
  over rings are rings, or --- an example from the domain where the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   668
  illustrations of this tutorial are taken from --- a partial order
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   669
  may be obtained for a function space by point-wise lifting of the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   670
  partial order of the co-domain.  This corresponds to the following
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   671
  interpretation:%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   672
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   673
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   674
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   675
\isadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   676
\ \ %
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   677
\endisadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   678
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   679
\isatagvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   680
\isacommand{sublocale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   681
\ partial{\isacharunderscore}order\ {\isasymsubseteq}\ f{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   682
\ \ \ \ \isacommand{oops}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   683
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   684
\endisatagvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   685
{\isafoldvisible}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   686
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   687
\isadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   688
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   689
\endisadelimvisible
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   690
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   691
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   692
Unfortunately this is a cyclic interpretation that leads to an
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   693
  infinite chain, namely
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   694
  \begin{isabelle}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   695
\ \ partial{\isacharunderscore}order\ {\isasymsubseteq}\ partial{\isacharunderscore}order\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ {\isasymsubseteq}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   696
\isaindent{\ \ }\ \ partial{\isacharunderscore}order\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ f\ x\ y\ {\isasymsqsubseteq}\ g\ x\ y{\isacharparenright}\ {\isasymsubseteq}\ \ {\isasymdots}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   697
\end{isabelle}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   698
  and the interpretation is rejected.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   699
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   700
  Instead it is necessary to declare a locale that is logically
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   701
  equivalent to \isa{partial{\isacharunderscore}order} but serves to collect facts
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   702
  about functions spaces where the co-domain is a partial order, and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   703
  to make the interpretation in its context:%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   704
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   705
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   706
\ \ \isacommand{locale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   707
\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isacharequal}\ partial{\isacharunderscore}order\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   708
\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   709
\ \ \isacommand{sublocale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   710
\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isasymsubseteq}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   711
\ \ \ \ \ \ f{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   712
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   713
\isadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   714
\ \ \ \ %
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   715
\endisadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   716
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   717
\isatagproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   718
\isacommand{by}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   719
\ unfold{\isacharunderscore}locales\ {\isacharparenleft}fast{\isacharcomma}rule{\isacharcomma}fast{\isacharcomma}blast\ intro{\isacharcolon}\ trans{\isacharparenright}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   720
\endisatagproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   721
{\isafoldproof}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   722
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   723
\isadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   724
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   725
\endisadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   726
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   727
\begin{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   728
It is quite common in abstract algebra that such a construction
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   729
  maps a hierarchy of algebraic structures (or specifications) to a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   730
  related hierarchy.  By means of the same lifting, a function space
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   731
  is a lattice if its co-domain is a lattice:%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   732
\end{isamarkuptext}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   733
\isamarkuptrue%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   734
\ \ \isacommand{locale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   735
\ fun{\isacharunderscore}lattice\ {\isacharequal}\ fun{\isacharunderscore}partial{\isacharunderscore}order\ {\isacharplus}\ lattice\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   736
\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   737
\ \ \isacommand{sublocale}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   738
\ fun{\isacharunderscore}lattice\ {\isasymsubseteq}\ f{\isacharcolon}\ lattice\ {\isachardoublequoteopen}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   739
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   740
\isadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   741
\ \ \ \ %
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   742
\endisadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   743
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   744
\isatagproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   745
\isacommand{proof}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   746
\ unfold{\isacharunderscore}locales\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   747
\ \ \ \ \isacommand{fix}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   748
\ f\ g\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   749
\ \ \ \ \isacommand{have}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   750
\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x\ {\isasymsqinter}\ g\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   751
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   752
\ {\isacharparenleft}rule\ is{\isacharunderscore}infI{\isacharparenright}\ \isacommand{apply}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   753
\ rule{\isacharplus}\ \isacommand{apply}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   754
\ {\isacharparenleft}drule\ spec{\isacharcomma}\ assumption{\isacharparenright}{\isacharplus}\ \isacommand{done}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   755
\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   756
\ \ \ \ \isacommand{then}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   757
\ \isacommand{show}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   758
\ {\isachardoublequoteopen}{\isasymexists}inf{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}inf\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ inf{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   759
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   760
\ fast\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   761
\ \ \isacommand{next}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   762
\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   763
\ \ \ \ \isacommand{fix}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   764
\ f\ g\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   765
\ \ \ \ \isacommand{have}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   766
\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x\ {\isasymsqunion}\ g\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   767
\ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   768
\ {\isacharparenleft}rule\ is{\isacharunderscore}supI{\isacharparenright}\ \isacommand{apply}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   769
\ rule{\isacharplus}\ \isacommand{apply}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   770
\ {\isacharparenleft}drule\ spec{\isacharcomma}\ assumption{\isacharparenright}{\isacharplus}\ \isacommand{done}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   771
\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   772
\ \ \ \ \isacommand{then}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   773
\ \isacommand{show}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   774
\ {\isachardoublequoteopen}{\isasymexists}sup{\isachardot}\ partial{\isacharunderscore}order{\isachardot}is{\isacharunderscore}sup\ {\isacharparenleft}{\isasymlambda}f\ g{\isachardot}\ {\isasymforall}x{\isachardot}\ f\ x\ {\isasymsqsubseteq}\ g\ x{\isacharparenright}\ f\ g\ sup{\isachardoublequoteclose}\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   775
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   776
\ fast\isanewline
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   777
\ \ \isacommand{qed}\isamarkupfalse%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   778
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   779
\endisatagproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   780
{\isafoldproof}%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   781
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   782
\isadelimproof
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   783
%
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   784
\endisadelimproof
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   785
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   786
\isamarkupsection{Further Reading%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   787
}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   788
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   789
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   790
\begin{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   791
More information on locales and their interpretation is
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   792
  available.  For the locale hierarchy of import and interpretation
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   793
  dependencies see~\cite{Ballarin2006a}; interpretations in theories
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   794
  and proofs are covered in~\cite{Ballarin2006b}.  In the latter, I
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   795
  show how interpretation in proofs enables to reason about families
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   796
  of algebraic structures, which cannot be expressed with locales
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   797
  directly.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   798
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   799
  Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   800
  of axiomatic type classes through a combination with locale
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   801
  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
   802
  facility to generate ML and Haskell code.  Classes are sufficient for
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   803
  simple specifications with a single type parameter.  The locales for
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   804
  orders and lattices presented in this tutorial fall into this
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   805
  category.  Order preserving maps, homomorphisms and vector spaces,
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   806
  on the other hand, do not.
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   807
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   808
  The locales reimplementation for Isabelle 2009 provides, among other
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   809
  improvements, a clean integration with Isabelle/Isar's local theory
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   810
  mechanisms, which are described in another paper by Haftmann and
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   811
  Wenzel~\cite{HaftmannWenzel2009}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   812
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   813
  The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   814
  may be of interest from a historical perspective.  My previous
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   815
  report on locales and locale expressions~\cite{Ballarin2004a}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   816
  describes a simpler form of expressions than available now and is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   817
  outdated. The mathematical background on orders and lattices is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   818
  taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}.
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   819
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   820
  The sources of this tutorial, which include all proofs, are
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   821
  available with the Isabelle distribution at
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   822
  \url{http://isabelle.in.tum.de}.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   823
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   824
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   825
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   826
\begin{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   827
\begin{table}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   828
\hrule
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   829
\vspace{2ex}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   830
\begin{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   831
\begin{tabular}{l>$c<$l}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   832
  \multicolumn{3}{l}{Miscellaneous} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   833
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   834
  \textit{attr-name} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   835
  & \textit{name} $|$ \textit{attribute} $|$
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   836
    \textit{name} \textit{attribute} \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   837
  \textit{qualifier} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   838
  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   839
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   840
  \multicolumn{3}{l}{Context Elements} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   841
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   842
  \textit{fixes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   843
  & \textit{name} [ ``\textbf{::}'' \textit{type} ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   844
    [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   845
    \textit{mixfix} ] \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   846
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   847
  \textit{constrains} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   848
  & \textit{name} ``\textbf{::}'' \textit{type} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   849
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   850
  \textit{assumes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   851
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   852
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   853
  \textit{defines} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   854
  & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   855
  \textit{notes} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   856
  & [ \textit{attr-name} ``\textbf{=}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   857
    ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   858
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   859
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   860
  \textit{element} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   861
  & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   862
\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   863
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   864
  & \textbf{constrains} \textit{constrains}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   865
    ( \textbf{and} \textit{constrains} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   866
\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   867
  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   868
  & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   869
%\begin{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   870
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   871
%  & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   872
%  & |
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   873
%  & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   874
%\end{comment}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   875
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   876
  \multicolumn{3}{l}{Locale Expressions} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   877
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   878
  \textit{pos-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   879
  & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   880
  \textit{named-insts} & ::=
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   881
  & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   882
  ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   883
  \textit{instance} & ::=
30751
36a255c2e428 Corrections to locale syntax.
ballarin
parents: 30750
diff changeset
   884
  & [ \textit{qualifier} ``\textbf{:}'' ]
33868
62251d6b0038 Generated files.
ballarin
parents: 32983
diff changeset
   885
    \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   886
  \textit{expression}  & ::= 
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   887
  & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   888
    [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   889
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   890
  \multicolumn{3}{l}{Declaration of Locales} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   891
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   892
  \textit{locale} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   893
  & \textit{element}$^+$ \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   894
  & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   895
  \textit{toplevel} & ::=
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   896
  & \textbf{locale} \textit{name} [ ``\textbf{=}''
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   897
    \textit{locale} ] \\[2ex]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   898
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   899
  \multicolumn{3}{l}{Interpretation} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   900
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   901
  \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ]
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   902
    \textit{prop} \\
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   903
  \textit{equations} & ::= &  \textbf{where} \textit{equation} ( \textbf{and}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   904
    \textit{equation} )$^*$  \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   905
  \textit{toplevel} & ::=
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   906
  & \textbf{sublocale} \textit{name} ( ``$<$'' $|$
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   907
    ``$\subseteq$'' ) \textit{expression} \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   908
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   909
  & \textbf{interpretation}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   910
    \textit{expression} [ \textit{equations} ] \textit{proof} \\
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   911
  & |
29566
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   912
  & \textbf{interpret}
937baa077df2 Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents: 28259
diff changeset
   913
    \textit{expression} \textit{proof} \\[2ex]
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   914
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   915
  \multicolumn{3}{l}{Diagnostics} \\
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   916
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   917
  \textit{toplevel} & ::=
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   918
  & \textbf{print\_locales} \\
33868
62251d6b0038 Generated files.
ballarin
parents: 32983
diff changeset
   919
  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
62251d6b0038 Generated files.
ballarin
parents: 32983
diff changeset
   920
  & | & \textbf{print\_interps} \textit{name}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   921
\end{tabular}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   922
\end{center}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   923
\hrule
30826
a53f4872400e Improvements to the text.
ballarin
parents: 30782
diff changeset
   924
\caption{Syntax of Locale Commands.}
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   925
\label{tab:commands}
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   926
\end{table}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   927
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   928
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   929
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   930
\begin{isamarkuptext}%
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   931
\textbf{Revision History.}  For the present third revision of
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   932
  the tutorial, much of the explanatory text
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   933
  was rewritten.  Inheritance of interpretation equations is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   934
  available with the forthcoming release of Isabelle, which at the
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   935
  time of editing these notes is expected for the end of 2009.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   936
  The second revision accommodates changes introduced by the locales
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   937
  reimplementation for Isabelle 2009.  Most notably locale expressions
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   938
  have been generalised from renaming to instantiation.%
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   939
\end{isamarkuptext}%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   940
\isamarkuptrue%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   941
%
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   942
\begin{isamarkuptext}%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   943
\textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 32836
diff changeset
   944
  Randy Pollack, Christian Sternagel and Makarius Wenzel have made
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   945
  useful comments on earlier versions of this document.  The section
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   946
  on conditional interpretation was inspired by a number of e-mail
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   947
  enquiries the author received from locale users, and which suggested
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   948
  that this use case is important enough to deserve explicit
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   949
  explanation.  The term \emph{conditional interpretation} is due to
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32982
diff changeset
   950
  Larry Paulson.%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   951
\end{isamarkuptext}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   952
\isamarkuptrue%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   953
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   954
\isadelimtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   955
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   956
\endisadelimtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   957
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   958
\isatagtheory
27080
0ee385433247 updated generated file;
wenzelm
parents: 27079
diff changeset
   959
\isacommand{end}\isamarkupfalse%
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   960
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   961
\endisatagtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   962
{\isafoldtheory}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   963
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   964
\isadelimtheory
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   965
%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   966
\endisadelimtheory
27080
0ee385433247 updated generated file;
wenzelm
parents: 27079
diff changeset
   967
\isanewline
27063
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   968
\end{isabellebody}%
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   969
%%% Local Variables:
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   970
%%% mode: latex
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   971
%%% TeX-master: "root"
d1d35284542f New version covering interpretation.
ballarin
parents:
diff changeset
   972
%%% End: