author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 54703  499f92dc6e45 
child 57607  5ff0cf3f5f6f 
permissions  rwrr 
27063  1 
theory Examples3 
32983  2 
imports Examples 
27063  3 
begin 
32981  4 
text {* \vspace{5ex} *} 
5 
subsection {* Third Version: Local Interpretation 

6 
\label{sec:localinterpretation} *} 

27063  7 

32981  8 
text {* In the above example, the fact that @{term "op \<le>"} is a partial 
32982  9 
order for the integers was used in the second goal to 
32981  10 
discharge the premise in the definition of @{text "op \<sqsubset>"}. In 
11 
general, proofs of the equations not only may involve definitions 

32983  12 
from the interpreted locale but arbitrarily complex arguments in the 
46855  13 
context of the locale. Therefore it would be convenient to have the 
14 
interpreted locale conclusions temporarily available in the proof. 

32981  15 
This can be achieved by a locale interpretation in the proof body. 
16 
The command for local interpretations is \isakeyword{interpret}. We 

17 
repeat the example from the previous section to illustrate this. *} 

27063  18 

32982  19 
interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
37206
diff
changeset

20 
where "int.less x y = (x < y)" 
32981  21 
proof  
32982  22 
show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" 
32981  23 
by unfold_locales auto 
32982  24 
then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" . 
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
37206
diff
changeset

25 
show "int.less x y = (x < y)" 
32982  26 
unfolding int.less_def by auto 
32981  27 
qed 
27063  28 

32981  29 
text {* The inner interpretation is immediate from the preceding fact 
30 
and proved by assumption (Isar short hand ``.''). It enriches the 

31 
local proof context by the theorems 

30826  32 
also obtained in the interpretation from Section~\ref{sec:pofirst}, 
32982  33 
and @{text int.less_def} may directly be used to unfold the 
30826  34 
definition. Theorems from the local interpretation disappear after 
32983  35 
leaving the proof context  that is, after the succeeding 
32981  36 
\isakeyword{next} or \isakeyword{qed} statement. *} 
27063  37 

38 

39 
subsection {* Further Interpretations *} 

40 

32981  41 
text {* Further interpretations are necessary for 
32983  42 
the other locales. In @{text lattice} the operations~@{text \<sqinter>} 
43 
and~@{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"} 

44 
and @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}. The entire proof for the 

32981  45 
interpretation is reproduced to give an example of a more 
32983  46 
elaborate interpretation proof. Note that the equations are named 
47 
so they can be used in a later example. *} 

27063  48 

32982  49 
interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
37206
diff
changeset

50 
where int_min_eq: "int.meet x y = min x y" 
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
37206
diff
changeset

51 
and int_max_eq: "int.join x y = max x y" 
32981  52 
proof  
32982  53 
show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" 
32981  54 
txt {* \normalsize We have already shown that this is a partial 
43708  55 
order, *} 
32981  56 
apply unfold_locales 
57 
txt {* \normalsize hence only the lattice axioms remain to be 

43708  58 
shown. 
32983  59 
@{subgoals [display]} 
43708  60 
By @{text is_inf} and @{text is_sup}, *} 
32982  61 
apply (unfold int.is_inf_def int.is_sup_def) 
32983  62 
txt {* \normalsize the goals are transformed to these 
43708  63 
statements: 
64 
@{subgoals [display]} 

65 
This is Presburger arithmetic, which can be solved by the 

35423  66 
method @{text arith}. *} 
32981  67 
by arith+ 
68 
txt {* \normalsize In order to show the equations, we put ourselves 

69 
in a situation where the lattice theorems can be used in a 

70 
convenient way. *} 

32982  71 
then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" . 
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
37206
diff
changeset

72 
show "int.meet x y = min x y" 
32982  73 
by (bestsimp simp: int.meet_def int.is_inf_def) 
43543
eb8b4851b039
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
ballarin
parents:
37206
diff
changeset

74 
show "int.join x y = max x y" 
32982  75 
by (bestsimp simp: int.join_def int.is_sup_def) 
32981  76 
qed 
27063  77 

32981  78 
text {* Next follows that @{text "op \<le>"} is a total order, again for 
32982  79 
the integers. *} 
27063  80 

32982  81 
interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" 
32981  82 
by unfold_locales arith 
27063  83 

84 
text {* Theorems that are available in the theory at this point are shown in 

32982  85 
Table~\ref{tab:intlattice}. Two points are worth noting: 
27063  86 

87 
\begin{table} 

88 
\hrule 

89 
\vspace{2ex} 

90 
\begin{center} 

91 
\begin{tabular}{l} 

32982  92 
@{thm [source] int.less_def} from locale @{text partial_order}: \\ 
93 
\quad @{thm int.less_def} \\ 

94 
@{thm [source] int.meet_left} from locale @{text lattice}: \\ 

95 
\quad @{thm int.meet_left} \\ 

96 
@{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\ 

97 
\quad @{thm int.join_distr} \\ 

98 
@{thm [source] int.less_total} from locale @{text total_order}: \\ 

99 
\quad @{thm int.less_total} 

27063  100 
\end{tabular} 
101 
\end{center} 

102 
\hrule 

32983  103 
\caption{Interpreted theorems for~@{text \<le>} on the integers.} 
32982  104 
\label{tab:intlattice} 
27063  105 
\end{table} 
32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

106 

ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

107 
\begin{itemize} 
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

108 
\item 
32981  109 
Locale @{text distrib_lattice} was also interpreted. Since the 
32983  110 
locale hierarchy reflects that total orders are distributive 
32981  111 
lattices, the interpretation of the latter was inserted 
112 
automatically with the interpretation of the former. In general, 

32983  113 
interpretation traverses the locale hierarchy upwards and interprets 
114 
all encountered locales, regardless whether imported or proved via 

115 
the \isakeyword{sublocale} command. Existing interpretations are 

116 
skipped avoiding duplicate work. 

32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

117 
\item 
32983  118 
The predicate @{term "op <"} appears in theorem @{thm [source] 
119 
int.less_total} 

32981  120 
although an equation for the replacement of @{text "op \<sqsubset>"} was only 
32983  121 
given in the interpretation of @{text partial_order}. The 
122 
interpretation equations are pushed downwards the hierarchy for 

123 
related interpretations  that is, for interpretations that share 

124 
the instances of parameters they have in common. 

32804
ca430e6aee1c
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents:
31960
diff
changeset

125 
\end{itemize} 
27063  126 
*} 
127 

32981  128 
text {* The interpretations for a locale $n$ within the current 
129 
theory may be inspected with \isakeyword{print\_interps}~$n$. This 

130 
prints the list of instances of $n$, for which interpretations exist. 

131 
For example, \isakeyword{print\_interps} @{term partial_order} 

132 
outputs the following: 

32983  133 
\begin{small} 
32981  134 
\begin{alltt} 
32982  135 
int! : partial_order "op \(\le\)" 
32981  136 
\end{alltt} 
32983  137 
\end{small} 
138 
Of course, there is only one interpretation. 

139 
The interpretation qualifier on the left is decorated with an 

140 
exclamation point. This means that it is mandatory. Qualifiers 

32981  141 
can either be \emph{mandatory} or \emph{optional}, designated by 
142 
``!'' or ``?'' respectively. Mandatory qualifiers must occur in a 

143 
name reference while optional ones need not. Mandatory qualifiers 

32983  144 
prevent accidental hiding of names, while optional qualifiers can be 
32981  145 
more convenient to use. For \isakeyword{interpretation}, the 
32983  146 
default is ``!''. 
32981  147 
*} 
27063  148 

149 

27077  150 
section {* Locale Expressions \label{sec:expressions} *} 
27063  151 

152 
text {* 

32983  153 
A map~@{term \<phi>} between partial orders~@{text \<sqsubseteq>} and~@{text \<preceq>} 
27063  154 
is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq> 
155 
\<phi> y"}. This situation is more complex than those encountered so 

156 
far: it involves two partial orders, and it is desirable to use the 

157 
existing locale for both. 

158 

32981  159 
A locale for order preserving maps requires three parameters: @{text 
32983  160 
le}~(\isakeyword{infixl}~@{text \<sqsubseteq>}) and @{text 
161 
le'}~(\isakeyword{infixl}~@{text \<preceq>}) for the orders and~@{text \<phi>} 

162 
for the map. 

32981  163 

164 
In order to reuse the existing locale for partial orders, which has 

32983  165 
the single parameter~@{text le}, it must be imported twice, once 
166 
mapping its parameter to~@{text le} from the new locale and once 

167 
to~@{text le'}. This can be achieved with a compound locale 

32981  168 
expression. 
169 

32983  170 
In general, a locale expression is a sequence of \emph{locale instances} 
171 
separated by~``$\textbf{+}$'' and followed by a \isakeyword{for} 

32981  172 
clause. 
32983  173 
An instance has the following format: 
32981  174 
\begin{quote} 
175 
\textit{qualifier} \textbf{:} \textit{localename} 

176 
\textit{parameterinstantiation} 

177 
\end{quote} 

178 
We have already seen locale instances as arguments to 

179 
\isakeyword{interpretation} in Section~\ref{sec:interpretation}. 

32983  180 
As before, the qualifier serves to disambiguate names from 
181 
different instances of the same locale. While in 

182 
\isakeyword{interpretation} qualifiers default to mandatory, in 

183 
import and in the \isakeyword{sublocale} command, they default to 

184 
optional. 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

185 

32983  186 
Since the parameters~@{text le} and~@{text le'} are to be partial 
32981  187 
orders, our locale for order preserving maps will import the these 
188 
instances: 

32983  189 
\begin{small} 
32981  190 
\begin{alltt} 
191 
le: partial_order le 

192 
le': partial_order le' 

193 
\end{alltt} 

32983  194 
\end{small} 
195 
For matter of convenience we choose to name parameter names and 

196 
qualifiers alike. This is an arbitrary decision. Technically, qualifiers 

32981  197 
and parameters are unrelated. 
198 

199 
Having determined the instances, let us turn to the \isakeyword{for} 

200 
clause. It serves to declare locale parameters in the same way as 

201 
the context element \isakeyword{fixes} does. Context elements can 

202 
only occur after the import section, and therefore the parameters 

32983  203 
referred to in the instances must be declared in the \isakeyword{for} 
204 
clause. The \isakeyword{for} clause is also where the syntax of these 

32981  205 
parameters is declared. 
206 

32983  207 
Two context elements for the map parameter~@{text \<phi>} and the 
208 
assumptions that it is order preserving complete the locale 

32981  209 
declaration. *} 
27063  210 

211 
locale order_preserving = 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

212 
le: partial_order le + le': partial_order le' 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

213 
for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) + 
32981  214 
fixes \<phi> 
27063  215 
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y" 
216 

32981  217 
text (in order_preserving) {* Here are examples of theorems that are 
218 
available in the locale: 

27063  219 

32983  220 
\hspace*{1em}@{thm [source] hom_le}: @{thm hom_le} 
27063  221 

32983  222 
\hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans} 
27063  223 

32983  224 
\hspace*{1em}@{thm [source] le'.less_le_trans}: 
225 
@{thm [display, indent=4] le'.less_le_trans} 

32981  226 
While there is infix syntax for the strict operation associated to 
227 
@{term "op \<sqsubseteq>"}, there is none for the strict version of @{term 

228 
"op \<preceq>"}. The abbreviation @{text less} with its infix syntax is only 

229 
available for the original instance it was declared for. We may 

32983  230 
introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>} 
231 
with the following declaration: *} 

27063  232 

233 
abbreviation (in order_preserving) 

234 
less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'" 

235 

30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

236 
text (in order_preserving) {* Now the theorem is displayed nicely as 
30826  237 
@{thm [source] le'.less_le_trans}: 
238 
@{thm [display, indent=2] le'.less_le_trans} *} 

27063  239 

32983  240 
text {* There are short notations for locale expressions. These are 
241 
discussed in the following. *} 

32981  242 

32983  243 

244 
subsection {* Default Instantiations *} 

32981  245 

32983  246 
text {* 
247 
It is possible to omit parameter instantiations. The 

248 
instantiation then defaults to the name of 

249 
the parameter itself. For example, the locale expression @{text 

32981  250 
partial_order} is short for @{text "partial_order le"}, since the 
32983  251 
locale's single parameter is~@{text le}. We took advantage of this 
252 
in the \isakeyword{sublocale} declarations of 

32981  253 
Section~\ref{sec:changingthehierarchy}. *} 
254 

255 

32983  256 
subsection {* Implicit Parameters \label{sec:implicitparameters} *} 
257 

32981  258 
text {* In a locale expression that occurs within a locale 
259 
declaration, omitted parameters additionally extend the (possibly 

260 
empty) \isakeyword{for} clause. 

27063  261 

32983  262 
The \isakeyword{for} clause is a general construct of Isabelle/Isar 
263 
to mark names occurring in the preceding declaration as ``arbitrary 

264 
but fixed''. This is necessary for example, if the name is already 

265 
bound in a surrounding context. In a locale expression, names 

266 
occurring in parameter instantiations should be bound by a 

267 
\isakeyword{for} clause whenever these names are not introduced 

268 
elsewhere in the context  for example, on the left hand side of a 

269 
\isakeyword{sublocale} declaration. 

27063  270 

32981  271 
There is an exception to this rule in locale declarations, where the 
32983  272 
\isakeyword{for} clause serves to declare locale parameters. Here, 
32981  273 
locale parameters for which no parameter instantiation is given are 
274 
implicitly added, with their mixfix syntax, at the beginning of the 

275 
\isakeyword{for} clause. For example, in a locale declaration, the 

276 
expression @{text partial_order} is short for 

32983  277 
\begin{small} 
32981  278 
\begin{alltt} 
279 
partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.} 

280 
\end{alltt} 

32983  281 
\end{small} 
282 
This short hand was used in the locale declarations throughout 

32981  283 
Section~\ref{sec:import}. 
284 
*} 

285 

286 
text{* 

32983  287 
The following locale declarations provide more examples. A 
288 
map~@{text \<phi>} is a lattice homomorphism if it preserves meet and 

32981  289 
join. *} 
30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

290 

3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

291 
locale lattice_hom = 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

292 
le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) + 
27063  293 
fixes \<phi> 
30826  294 
assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)" 
295 
and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)" 

27063  296 

32983  297 
text {* The parameter instantiation in the first instance of @{term 
298 
lattice} is omitted. This causes the parameter~@{text le} to be 

299 
added to the \isakeyword{for} clause, and the locale has 

300 
parameters~@{text le},~@{text le'} and, of course,~@{text \<phi>}. 

27063  301 

32981  302 
Before turning to the second example, we complete the locale by 
32983  303 
providing infix syntax for the meet and join operations of the 
32981  304 
second lattice. 
305 
*} 

306 

46855  307 
context lattice_hom 
308 
begin 

32981  309 
abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet" 
310 
abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join" 

311 
end 

312 

32983  313 
text {* The next example makes radical use of the short hand 
314 
facilities. A homomorphism is an endomorphism if both orders 

315 
coincide. *} 

27063  316 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

317 
locale lattice_end = lattice_hom _ le 
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

318 

32983  319 
text {* The notation~@{text _} enables to omit a parameter in a 
320 
positional instantiation. The omitted parameter,~@{text le} becomes 

32981  321 
the parameter of the declared locale and is, in the following 
32983  322 
position, used to instantiate the second parameter of @{text 
32981  323 
lattice_hom}. The effect is that of identifying the first in second 
324 
parameter of the homomorphism locale. *} 

27063  325 

326 
text {* The inheritance diagram of the situation we have now is shown 

327 
in Figure~\ref{fig:hom}, where the dashed line depicts an 

32983  328 
interpretation which is introduced below. Parameter instantiations 
329 
are indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at 

330 
the inheritance diagram it would seem 

27063  331 
that two identical copies of each of the locales @{text 
32981  332 
partial_order} and @{text lattice} are imported by @{text 
333 
lattice_end}. This is not the case! Inheritance paths with 

334 
identical morphisms are automatically detected and 

27503  335 
the conclusions of the respective locales appear only once. 
27063  336 

337 
\begin{figure} 

338 
\hrule \vspace{2ex} 

339 
\begin{center} 

340 
\begin{tikzpicture} 

341 
\node (o) at (0,0) {@{text partial_order}}; 

342 
\node (oh) at (1.5,2) {@{text order_preserving}}; 

343 
\node (oh1) at (1.5,0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 

344 
\node (oh2) at (0,1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; 

345 
\node (l) at (1.5,2) {@{text lattice}}; 

346 
\node (lh) at (0,4) {@{text lattice_hom}}; 

347 
\node (lh1) at (0,2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 

348 
\node (lh2) at (1.5,3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; 

349 
\node (le) at (0,6) {@{text lattice_end}}; 

350 
\node (le1) at (0,4.8) 

351 
[anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 

352 
\node (le2) at (0,5.2) 

353 
[anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$}; 

354 
\draw (o)  (l); 

355 
\draw[dashed] (oh)  (lh); 

356 
\draw (lh)  (le); 

357 
\draw (o) .. controls (oh1.south west) .. (oh); 

358 
\draw (o) .. controls (oh2.north east) .. (oh); 

359 
\draw (l) .. controls (lh1.south west) .. (lh); 

360 
\draw (l) .. controls (lh2.north east) .. (lh); 

361 
\end{tikzpicture} 

362 
\end{center} 

363 
\hrule 

364 
\caption{Hierarchy of Homomorphism Locales.} 

365 
\label{fig:hom} 

366 
\end{figure} 

367 
*} 

368 

369 
text {* It can be shown easily that a lattice homomorphism is order 

370 
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

371 
interpretation is used to assert this: *} 
27063  372 

46855  373 
sublocale lattice_hom \<subseteq> order_preserving 
374 
proof unfold_locales 

27063  375 
fix x y 
376 
assume "x \<sqsubseteq> y" 

377 
then have "y = (x \<squnion> y)" by (simp add: le.join_connection) 

378 
then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric]) 

379 
then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection) 

380 
qed 

381 

30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

382 
text (in lattice_hom) {* 
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

383 
Theorems and other declarations  syntax, in particular  from 
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29568
diff
changeset

384 
the locale @{text order_preserving} are now active in @{text 
27063  385 
lattice_hom}, for example 
30826  386 
@{thm [source] hom_le}: 
387 
@{thm [display, indent=2] hom_le} 

32983  388 
This theorem will be useful in the following section. 
27063  389 
*} 
390 

32983  391 

32981  392 
section {* Conditional Interpretation *} 
27063  393 

32983  394 
text {* There are situations where an interpretation is not possible 
395 
in the general case since the desired property is only valid if 

396 
certain conditions are fulfilled. Take, for example, the function 

397 
@{text "\<lambda>i. n * i"} that scales its argument by a constant factor. 

398 
This function is order preserving (and even a lattice endomorphism) 

399 
with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}. 

400 

401 
It is not possible to express this using a global interpretation, 

402 
because it is in general unspecified whether~@{term n} is 

403 
nonnegative, but one may make an interpretation in an inner context 

404 
of a proof where full information is available. 

405 
This is not fully satisfactory either, since potentially 

406 
interpretations may be required to make interpretations in many 

407 
contexts. What is 

408 
required is an interpretation that depends on the condition  and 

409 
this can be done with the \isakeyword{sublocale} command. For this 

410 
purpose, we introduce a locale for the condition. *} 

411 

32981  412 
locale non_negative = 
413 
fixes n :: int 

32983  414 
assumes non_neg: "0 \<le> n" 
415 

416 
text {* It is again convenient to make the interpretation in an 

417 
incremental fashion, first for order preserving maps, the for 

418 
lattice endomorphisms. *} 

32981  419 

32983  420 
sublocale non_negative \<subseteq> 
421 
order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i" 

422 
using non_neg by unfold_locales (rule mult_left_mono) 

423 

424 
text {* While the proof of the previous interpretation 

425 
is straightforward from monotonicity lemmas for~@{term "op *"}, the 

426 
second proof follows a useful pattern. *} 

32981  427 

32983  428 
sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i" 
429 
proof (unfold_locales, unfold int_min_eq int_max_eq) 

430 
txt {* \normalsize Unfolding the locale predicates \emph{and} the 

431 
interpretation equations immediately yields two subgoals that 

432 
reflect the core conjecture. 

433 
@{subgoals [display]} 

434 
It is now necessary to show, in the context of @{term 

435 
non_negative}, that multiplication by~@{term n} commutes with 

436 
@{term min} and @{term max}. *} 

437 
qed (auto simp: hom_le) 

32981  438 

32983  439 
text (in order_preserving) {* The lemma @{thm [source] hom_le} 
440 
simplifies a proof that would have otherwise been lengthy and we may 

441 
consider making it a default rule for the simplifier: *} 

32981  442 

32983  443 
lemmas (in order_preserving) hom_le [simp] 
32981  444 

445 

32983  446 
subsection {* Avoiding Infinite Chains of Interpretations 
447 
\label{sec:infinitechains} *} 

448 

449 
text {* Similar situations arise frequently in formalisations of 

450 
abstract algebra where it is desirable to express that certain 

451 
constructions preserve certain properties. For example, polynomials 

452 
over rings are rings, or  an example from the domain where the 

453 
illustrations of this tutorial are taken from  a partial order 

454 
may be obtained for a function space by pointwise lifting of the 

455 
partial order of the codomain. This corresponds to the following 

456 
interpretation: *} 

457 

458 
sublocale %visible partial_order \<subseteq> f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 

459 
oops 

460 

461 
text {* Unfortunately this is a cyclic interpretation that leads to an 

462 
infinite chain, namely 

463 
@{text [display, indent=2] "partial_order \<subseteq> partial_order (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) \<subseteq> 

464 
partial_order (\<lambda>f g. \<forall>x y. f x y \<sqsubseteq> g x y) \<subseteq> \<dots>"} 

465 
and the interpretation is rejected. 

466 

467 
Instead it is necessary to declare a locale that is logically 

468 
equivalent to @{term partial_order} but serves to collect facts 

469 
about functions spaces where the codomain is a partial order, and 

470 
to make the interpretation in its context: *} 

32981  471 

32983  472 
locale fun_partial_order = partial_order 
473 

474 
sublocale fun_partial_order \<subseteq> 

475 
f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 

476 
by unfold_locales (fast,rule,fast,blast intro: trans) 

477 

478 
text {* It is quite common in abstract algebra that such a construction 

479 
maps a hierarchy of algebraic structures (or specifications) to a 

480 
related hierarchy. By means of the same lifting, a function space 

481 
is a lattice if its codomain is a lattice: *} 

482 

483 
locale fun_lattice = fun_partial_order + lattice 

32981  484 

32983  485 
sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 
46855  486 
proof unfold_locales 
32983  487 
fix f g 
488 
have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)" 

489 
apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done 

490 
then show "\<exists>inf. partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g inf" 

491 
by fast 

492 
next 

493 
fix f g 

494 
have "partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<squnion> g x)" 

495 
apply (rule is_supI) apply rule+ apply (drule spec, assumption)+ done 

496 
then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup" 

497 
by fast 

498 
qed 

499 

27063  500 

501 
section {* Further Reading *} 

502 

503 
text {* More information on locales and their interpretation is 

504 
available. For the locale hierarchy of import and interpretation 

32983  505 
dependencies see~\cite{Ballarin2006a}; interpretations in theories 
506 
and proofs are covered in~\cite{Ballarin2006b}. In the latter, I 

27063  507 
show how interpretation in proofs enables to reason about families 
508 
of algebraic structures, which cannot be expressed with locales 

509 
directly. 

510 

32983  511 
Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction 
27063  512 
of axiomatic type classes through a combination with locale 
513 
interpretation. The result is a Haskellstyle class system with a 

30750
3779e2158dad
Update explanation of locale expressions to locale reimplementation.
ballarin
parents:
30580
diff
changeset

514 
facility to generate ML and Haskell code. Classes are sufficient for 
27063  515 
simple specifications with a single type parameter. The locales for 
516 
orders and lattices presented in this tutorial fall into this 

517 
category. Order preserving maps, homomorphisms and vector spaces, 

518 
on the other hand, do not. 

519 

32981  520 
The locales reimplementation for Isabelle 2009 provides, among other 
32983  521 
improvements, a clean integration with Isabelle/Isar's local theory 
522 
mechanisms, which are described in another paper by Haftmann and 

523 
Wenzel~\cite{HaftmannWenzel2009}. 

32981  524 

32983  525 
The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999} 
526 
may be of interest from a historical perspective. My previous 

527 
report on locales and locale expressions~\cite{Ballarin2004a} 

528 
describes a simpler form of expressions than available now and is 

529 
outdated. The mathematical background on orders and lattices is 

530 
taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}. 

32981  531 

532 
The sources of this tutorial, which include all proofs, are 

533 
available with the Isabelle distribution at 

54703  534 
@{url "http://isabelle.in.tum.de"}. 
27063  535 
*} 
536 

537 
text {* 

538 
\begin{table} 

539 
\hrule 

540 
\vspace{2ex} 

541 
\begin{center} 

542 
\begin{tabular}{l>$c<$l} 

543 
\multicolumn{3}{l}{Miscellaneous} \\ 

544 

545 
\textit{attrname} & ::= 

546 
& \textit{name} $$ \textit{attribute} $$ 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

547 
\textit{name} \textit{attribute} \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

548 
\textit{qualifier} & ::= 
30751  549 
& \textit{name} [``\textbf{?}'' $$ ``\textbf{!}''] \\[2ex] 
27063  550 

551 
\multicolumn{3}{l}{Context Elements} \\ 

552 

553 
\textit{fixes} & ::= 

554 
& \textit{name} [ ``\textbf{::}'' \textit{type} ] 

555 
[ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $$ 

556 
\textit{mixfix} ] \\ 

557 
\begin{comment} 

558 
\textit{constrains} & ::= 

559 
& \textit{name} ``\textbf{::}'' \textit{type} \\ 

560 
\end{comment} 

561 
\textit{assumes} & ::= 

562 
& [ \textit{attrname} ``\textbf{:}'' ] \textit{proposition} \\ 

563 
\begin{comment} 

564 
\textit{defines} & ::= 

565 
& [ \textit{attrname} ``\textbf{:}'' ] \textit{proposition} \\ 

566 
\textit{notes} & ::= 

567 
& [ \textit{attrname} ``\textbf{=}'' ] 

568 
( \textit{qualifiedname} [ \textit{attribute} ] )$^+$ \\ 

569 
\end{comment} 

570 

571 
\textit{element} & ::= 

572 
& \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\ 

573 
\begin{comment} 

574 
&  

575 
& \textbf{constrains} \textit{constrains} 

576 
( \textbf{and} \textit{constrains} )$^*$ \\ 

577 
\end{comment} 

578 
&  

579 
& \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex] 

580 
%\begin{comment} 

581 
% &  

582 
% & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\ 

583 
% &  

584 
% & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\ 

585 
%\end{comment} 

586 

587 
\multicolumn{3}{l}{Locale Expressions} \\ 

588 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

589 
\textit{posinsts} & ::= 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

590 
& ( \textit{term} $$ ``\textbf{\_}'' )$^*$ \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

591 
\textit{namedinsts} & ::= 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

592 
& \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

593 
( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

594 
\textit{instance} & ::= 
30751  595 
& [ \textit{qualifier} ``\textbf{:}'' ] 
33867  596 
\textit{name} ( \textit{posinsts} $$ \textit{namedinst} ) \\ 
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

597 
\textit{expression} & ::= 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

598 
& \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

599 
[ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] 
27063  600 

601 
\multicolumn{3}{l}{Declaration of Locales} \\ 

602 

603 
\textit{locale} & ::= 

604 
& \textit{element}$^+$ \\ 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

605 
&  & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ 
27063  606 
\textit{toplevel} & ::= 
607 
& \textbf{locale} \textit{name} [ ``\textbf{=}'' 

608 
\textit{locale} ] \\[2ex] 

609 

610 
\multicolumn{3}{l}{Interpretation} \\ 

611 

612 
\textit{equation} & ::= & [ \textit{attrname} ``\textbf{:}'' ] 

613 
\textit{prop} \\ 

29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

614 
\textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

615 
\textit{equation} )$^*$ \\ 
27063  616 
\textit{toplevel} & ::= 
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

617 
& \textbf{sublocale} \textit{name} ( ``$<$'' $$ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

618 
``$\subseteq$'' ) \textit{expression} \textit{proof} \\ 
27063  619 
&  
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

620 
& \textbf{interpretation} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

621 
\textit{expression} [ \textit{equations} ] \textit{proof} \\ 
27063  622 
&  
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

623 
& \textbf{interpret} 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

624 
\textit{expression} \textit{proof} \\[2ex] 
27063  625 

626 
\multicolumn{3}{l}{Diagnostics} \\ 

627 

628 
\textit{toplevel} & ::= 

32981  629 
& \textbf{print\_locales} \\ 
33867  630 
&  & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\ 
631 
&  & \textbf{print\_interps} \textit{name} 

27063  632 
\end{tabular} 
633 
\end{center} 

634 
\hrule 

30826  635 
\caption{Syntax of Locale Commands.} 
27063  636 
\label{tab:commands} 
637 
\end{table} 

638 
*} 

639 

32983  640 
text {* \textbf{Revision History.} For the present third revision of 
641 
the tutorial, much of the explanatory text 

642 
was rewritten. Inheritance of interpretation equations is 

643 
available with the forthcoming release of Isabelle, which at the 

644 
time of editing these notes is expected for the end of 2009. 

645 
The second revision accommodates changes introduced by the locales 

646 
reimplementation for Isabelle 2009. Most notably locale expressions 

647 
have been generalised from renaming to instantiation. *} 

32981  648 

27063  649 
text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, 
37206  650 
Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel 
651 
have made 

32983  652 
useful comments on earlier versions of this document. The section 
653 
on conditional interpretation was inspired by a number of email 

654 
enquiries the author received from locale users, and which suggested 

655 
that this use case is important enough to deserve explicit 

656 
explanation. The term \emph{conditional interpretation} is due to 

657 
Larry Paulson. *} 

27063  658 

659 
end 