author  wenzelm 
Mon, 01 Mar 2010 21:41:35 +0100  
changeset 35423  6ef9525a5727 
parent 33867  52643d0f856d 
child 37206  7f2a6f3143ad 
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 
32981  13 
context of the locale. Therefore is would be convenient to have the 
14 
interpreted locale conclusions temporary available in the proof. 

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" 
20 
where "partial_order.less op \<le> (x::int) 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" . 
25 
show "partial_order.less op \<le> (x::int) y = (x < y)" 

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" 
32983  50 
where int_min_eq: "lattice.meet op \<le> (x::int) y = min x y" 
51 
and int_max_eq: "lattice.join op \<le> (x::int) 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 
55 
order, *} 

56 
apply unfold_locales 

57 
txt {* \normalsize hence only the lattice axioms remain to be 

32983  58 
shown. 
59 
@{subgoals [display]} 

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 
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" . 
72 
show "lattice.meet op \<le> (x::int) y = min x y" 

73 
by (bestsimp simp: int.meet_def int.is_inf_def) 

74 
show "lattice.join op \<le> (x::int) y = max x y" 

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 

307 
context lattice_hom begin 

308 
abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet" 

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

310 
end 

311 

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

314 
coincide. *} 

27063  315 

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

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

317 

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

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

27063  324 

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

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

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

329 
the inheritance diagram it would seem 

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

333 
identical morphisms are automatically detected and 

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

336 
\begin{figure} 

337 
\hrule \vspace{2ex} 

338 
\begin{center} 

339 
\begin{tikzpicture} 

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

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

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

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

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

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

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

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

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

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

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

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

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

353 
\draw (o)  (l); 

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

355 
\draw (lh)  (le); 

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

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

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

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

360 
\end{tikzpicture} 

361 
\end{center} 

362 
\hrule 

363 
\caption{Hierarchy of Homomorphism Locales.} 

364 
\label{fig:hom} 

365 
\end{figure} 

366 
*} 

367 

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

369 
preserving. As the final example of this section, a locale 

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

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

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

372 
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales 
27063  373 
fix x y 
374 
assume "x \<sqsubseteq> y" 

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

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

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

378 
qed 

379 

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

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

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

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

32983  386 
This theorem will be useful in the following section. 
27063  387 
*} 
388 

32983  389 

32981  390 
section {* Conditional Interpretation *} 
27063  391 

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

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

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

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

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

398 

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

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

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

402 
of a proof where full information is available. 

403 
This is not fully satisfactory either, since potentially 

404 
interpretations may be required to make interpretations in many 

405 
contexts. What is 

406 
required is an interpretation that depends on the condition  and 

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

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

409 

32981  410 
locale non_negative = 
411 
fixes n :: int 

32983  412 
assumes non_neg: "0 \<le> n" 
413 

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

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

416 
lattice endomorphisms. *} 

32981  417 

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

420 
using non_neg by unfold_locales (rule mult_left_mono) 

421 

422 
text {* While the proof of the previous interpretation 

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

424 
second proof follows a useful pattern. *} 

32981  425 

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

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

429 
interpretation equations immediately yields two subgoals that 

430 
reflect the core conjecture. 

431 
@{subgoals [display]} 

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

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

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

435 
qed (auto simp: hom_le) 

32981  436 

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

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

32981  440 

32983  441 
lemmas (in order_preserving) hom_le [simp] 
32981  442 

443 

32983  444 
subsection {* Avoiding Infinite Chains of Interpretations 
445 
\label{sec:infinitechains} *} 

446 

447 
text {* Similar situations arise frequently in formalisations of 

448 
abstract algebra where it is desirable to express that certain 

449 
constructions preserve certain properties. For example, polynomials 

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

451 
illustrations of this tutorial are taken from  a partial order 

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

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

454 
interpretation: *} 

455 

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

457 
oops 

458 

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

460 
infinite chain, namely 

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

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

463 
and the interpretation is rejected. 

464 

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

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

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

468 
to make the interpretation in its context: *} 

32981  469 

32983  470 
locale fun_partial_order = partial_order 
471 

472 
sublocale fun_partial_order \<subseteq> 

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

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

475 

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

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

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

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

480 

481 
locale fun_lattice = fun_partial_order + lattice 

32981  482 

32983  483 
sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 
484 
proof unfold_locales 

485 
fix f g 

486 
have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)" 

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

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

489 
by fast 

490 
next 

491 
fix f g 

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

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

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

495 
by fast 

496 
qed 

497 

27063  498 

499 
section {* Further Reading *} 

500 

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

502 
available. For the locale hierarchy of import and interpretation 

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

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

507 
directly. 

508 

32983  509 
Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction 
27063  510 
of axiomatic type classes through a combination with locale 
511 
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

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

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

516 
on the other hand, do not. 

517 

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

521 
Wenzel~\cite{HaftmannWenzel2009}. 

32981  522 

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

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

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

527 
outdated. The mathematical background on orders and lattices is 

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

32981  529 

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

531 
available with the Isabelle distribution at 

532 
\url{http://isabelle.in.tum.de}. 

27063  533 
*} 
534 

535 
text {* 

536 
\begin{table} 

537 
\hrule 

538 
\vspace{2ex} 

539 
\begin{center} 

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

541 
\multicolumn{3}{l}{Miscellaneous} \\ 

542 

543 
\textit{attrname} & ::= 

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

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

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

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

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

550 

551 
\textit{fixes} & ::= 

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

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

554 
\textit{mixfix} ] \\ 

555 
\begin{comment} 

556 
\textit{constrains} & ::= 

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

558 
\end{comment} 

559 
\textit{assumes} & ::= 

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

561 
\begin{comment} 

562 
\textit{defines} & ::= 

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

564 
\textit{notes} & ::= 

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

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

567 
\end{comment} 

568 

569 
\textit{element} & ::= 

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

571 
\begin{comment} 

572 
&  

573 
& \textbf{constrains} \textit{constrains} 

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

575 
\end{comment} 

576 
&  

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

578 
%\begin{comment} 

579 
% &  

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

581 
% &  

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

583 
%\end{comment} 

584 

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

586 

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

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

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

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

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

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

592 
\textit{instance} & ::= 
30751  593 
& [ \textit{qualifier} ``\textbf{:}'' ] 
33867  594 
\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

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

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

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

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

600 

601 
\textit{locale} & ::= 

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

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

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

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

607 

608 
\multicolumn{3}{l}{Interpretation} \\ 

609 

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

611 
\textit{prop} \\ 

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

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

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

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

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

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

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

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

622 
\textit{expression} \textit{proof} \\[2ex] 
27063  623 

624 
\multicolumn{3}{l}{Diagnostics} \\ 

625 

626 
\textit{toplevel} & ::= 

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

27063  630 
\end{tabular} 
631 
\end{center} 

632 
\hrule 

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

636 
*} 

637 

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

640 
was rewritten. Inheritance of interpretation equations is 

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

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

643 
The second revision accommodates changes introduced by the locales 

644 
reimplementation for Isabelle 2009. Most notably locale expressions 

645 
have been generalised from renaming to instantiation. *} 

32981  646 

27063  647 
text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, 
32981  648 
Randy Pollack, Christian Sternagel and Makarius Wenzel have made 
32983  649 
useful comments on earlier versions of this document. The section 
650 
on conditional interpretation was inspired by a number of email 

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

652 
that this use case is important enough to deserve explicit 

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

654 
Larry Paulson. *} 

27063  655 

656 
end 