1 theory Examples3 |
|
2 imports Examples |
|
3 begin |
|
4 text {* \vspace{-5ex} *} |
|
5 subsection {* Third Version: Local Interpretation |
|
6 \label{sec:local-interpretation} *} |
|
7 |
|
8 text {* In the above example, the fact that @{term "op \<le>"} is a partial |
|
9 order for the integers was used in the second goal to |
|
10 discharge the premise in the definition of @{text "op \<sqsubset>"}. In |
|
11 general, proofs of the equations not only may involve definitions |
|
12 from the interpreted locale but arbitrarily complex arguments in the |
|
13 context of the locale. Therefore it would be convenient to have the |
|
14 interpreted locale conclusions temporarily 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. *} |
|
18 |
|
19 interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" |
|
20 where "int.less x y = (x < y)" |
|
21 proof - |
|
22 show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" |
|
23 by unfold_locales auto |
|
24 then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" . |
|
25 show "int.less x y = (x < y)" |
|
26 unfolding int.less_def by auto |
|
27 qed |
|
28 |
|
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 |
|
32 also obtained in the interpretation from Section~\ref{sec:po-first}, |
|
33 and @{text int.less_def} may directly be used to unfold the |
|
34 definition. Theorems from the local interpretation disappear after |
|
35 leaving the proof context --- that is, after the succeeding |
|
36 \isakeyword{next} or \isakeyword{qed} statement. *} |
|
37 |
|
38 |
|
39 subsection {* Further Interpretations *} |
|
40 |
|
41 text {* Further interpretations are necessary for |
|
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 |
|
45 interpretation is reproduced to give an example of a more |
|
46 elaborate interpretation proof. Note that the equations are named |
|
47 so they can be used in a later example. *} |
|
48 |
|
49 interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" |
|
50 where int_min_eq: "int.meet x y = min x y" |
|
51 and int_max_eq: "int.join x y = max x y" |
|
52 proof - |
|
53 show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)" |
|
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 |
|
58 shown. |
|
59 @{subgoals [display]} |
|
60 By @{text is_inf} and @{text is_sup}, *} |
|
61 apply (unfold int.is_inf_def int.is_sup_def) |
|
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 |
|
66 method @{text arith}. *} |
|
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. *} |
|
71 then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" . |
|
72 show "int.meet x y = min x y" |
|
73 by (bestsimp simp: int.meet_def int.is_inf_def) |
|
74 show "int.join x y = max x y" |
|
75 by (bestsimp simp: int.join_def int.is_sup_def) |
|
76 qed |
|
77 |
|
78 text {* Next follows that @{text "op \<le>"} is a total order, again for |
|
79 the integers. *} |
|
80 |
|
81 interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" |
|
82 by unfold_locales arith |
|
83 |
|
84 text {* Theorems that are available in the theory at this point are shown in |
|
85 Table~\ref{tab:int-lattice}. Two points are worth noting: |
|
86 |
|
87 \begin{table} |
|
88 \hrule |
|
89 \vspace{2ex} |
|
90 \begin{center} |
|
91 \begin{tabular}{l} |
|
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} |
|
100 \end{tabular} |
|
101 \end{center} |
|
102 \hrule |
|
103 \caption{Interpreted theorems for~@{text \<le>} on the integers.} |
|
104 \label{tab:int-lattice} |
|
105 \end{table} |
|
106 |
|
107 \begin{itemize} |
|
108 \item |
|
109 Locale @{text distrib_lattice} was also interpreted. Since the |
|
110 locale hierarchy reflects that total orders are distributive |
|
111 lattices, the interpretation of the latter was inserted |
|
112 automatically with the interpretation of the former. In general, |
|
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. |
|
117 \item |
|
118 The predicate @{term "op <"} appears in theorem @{thm [source] |
|
119 int.less_total} |
|
120 although an equation for the replacement of @{text "op \<sqsubset>"} was only |
|
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. |
|
125 \end{itemize} |
|
126 *} |
|
127 |
|
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: |
|
133 \begin{small} |
|
134 \begin{alltt} |
|
135 int! : partial_order "op \(\le\)" |
|
136 \end{alltt} |
|
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 |
|
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 |
|
144 prevent accidental hiding of names, while optional qualifiers can be |
|
145 more convenient to use. For \isakeyword{interpretation}, the |
|
146 default is ``!''. |
|
147 *} |
|
148 |
|
149 |
|
150 section {* Locale Expressions \label{sec:expressions} *} |
|
151 |
|
152 text {* |
|
153 A map~@{term \<phi>} between partial orders~@{text \<sqsubseteq>} and~@{text \<preceq>} |
|
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 |
|
159 A locale for order preserving maps requires three parameters: @{text |
|
160 le}~(\isakeyword{infixl}~@{text \<sqsubseteq>}) and @{text |
|
161 le'}~(\isakeyword{infixl}~@{text \<preceq>}) for the orders and~@{text \<phi>} |
|
162 for the map. |
|
163 |
|
164 In order to reuse the existing locale for partial orders, which has |
|
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 |
|
168 expression. |
|
169 |
|
170 In general, a locale expression is a sequence of \emph{locale instances} |
|
171 separated by~``$\textbf{+}$'' and followed by a \isakeyword{for} |
|
172 clause. |
|
173 An instance has the following format: |
|
174 \begin{quote} |
|
175 \textit{qualifier} \textbf{:} \textit{locale-name} |
|
176 \textit{parameter-instantiation} |
|
177 \end{quote} |
|
178 We have already seen locale instances as arguments to |
|
179 \isakeyword{interpretation} in Section~\ref{sec:interpretation}. |
|
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. |
|
185 |
|
186 Since the parameters~@{text le} and~@{text le'} are to be partial |
|
187 orders, our locale for order preserving maps will import the these |
|
188 instances: |
|
189 \begin{small} |
|
190 \begin{alltt} |
|
191 le: partial_order le |
|
192 le': partial_order le' |
|
193 \end{alltt} |
|
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 |
|
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 |
|
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 |
|
205 parameters is declared. |
|
206 |
|
207 Two context elements for the map parameter~@{text \<phi>} and the |
|
208 assumptions that it is order preserving complete the locale |
|
209 declaration. *} |
|
210 |
|
211 locale order_preserving = |
|
212 le: partial_order le + le': partial_order le' |
|
213 for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) + |
|
214 fixes \<phi> |
|
215 assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y" |
|
216 |
|
217 text (in order_preserving) {* Here are examples of theorems that are |
|
218 available in the locale: |
|
219 |
|
220 \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le} |
|
221 |
|
222 \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans} |
|
223 |
|
224 \hspace*{1em}@{thm [source] le'.less_le_trans}: |
|
225 @{thm [display, indent=4] le'.less_le_trans} |
|
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 |
|
230 introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>} |
|
231 with the following declaration: *} |
|
232 |
|
233 abbreviation (in order_preserving) |
|
234 less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'" |
|
235 |
|
236 text (in order_preserving) {* Now the theorem is displayed nicely as |
|
237 @{thm [source] le'.less_le_trans}: |
|
238 @{thm [display, indent=2] le'.less_le_trans} *} |
|
239 |
|
240 text {* There are short notations for locale expressions. These are |
|
241 discussed in the following. *} |
|
242 |
|
243 |
|
244 subsection {* Default Instantiations *} |
|
245 |
|
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 |
|
250 partial_order} is short for @{text "partial_order le"}, since the |
|
251 locale's single parameter is~@{text le}. We took advantage of this |
|
252 in the \isakeyword{sublocale} declarations of |
|
253 Section~\ref{sec:changing-the-hierarchy}. *} |
|
254 |
|
255 |
|
256 subsection {* Implicit Parameters \label{sec:implicit-parameters} *} |
|
257 |
|
258 text {* In a locale expression that occurs within a locale |
|
259 declaration, omitted parameters additionally extend the (possibly |
|
260 empty) \isakeyword{for} clause. |
|
261 |
|
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. |
|
270 |
|
271 There is an exception to this rule in locale declarations, where the |
|
272 \isakeyword{for} clause serves to declare locale parameters. Here, |
|
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 |
|
277 \begin{small} |
|
278 \begin{alltt} |
|
279 partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.} |
|
280 \end{alltt} |
|
281 \end{small} |
|
282 This short hand was used in the locale declarations throughout |
|
283 Section~\ref{sec:import}. |
|
284 *} |
|
285 |
|
286 text{* |
|
287 The following locale declarations provide more examples. A |
|
288 map~@{text \<phi>} is a lattice homomorphism if it preserves meet and |
|
289 join. *} |
|
290 |
|
291 locale lattice_hom = |
|
292 le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) + |
|
293 fixes \<phi> |
|
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)" |
|
296 |
|
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>}. |
|
301 |
|
302 Before turning to the second example, we complete the locale by |
|
303 providing infix syntax for the meet and join operations of the |
|
304 second lattice. |
|
305 *} |
|
306 |
|
307 context lattice_hom |
|
308 begin |
|
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 |
|
313 text {* The next example makes radical use of the short hand |
|
314 facilities. A homomorphism is an endomorphism if both orders |
|
315 coincide. *} |
|
316 |
|
317 locale lattice_end = lattice_hom _ le |
|
318 |
|
319 text {* The notation~@{text _} enables to omit a parameter in a |
|
320 positional instantiation. The omitted parameter,~@{text le} becomes |
|
321 the parameter of the declared locale and is, in the following |
|
322 position, used to instantiate the second parameter of @{text |
|
323 lattice_hom}. The effect is that of identifying the first in second |
|
324 parameter of the homomorphism locale. *} |
|
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 |
|
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 |
|
331 that two identical copies of each of the locales @{text |
|
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 |
|
335 the conclusions of the respective locales appear only once. |
|
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 |
|
371 interpretation is used to assert this: *} |
|
372 |
|
373 sublocale lattice_hom \<subseteq> order_preserving |
|
374 proof unfold_locales |
|
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 |
|
382 text (in lattice_hom) {* |
|
383 Theorems and other declarations --- syntax, in particular --- from |
|
384 the locale @{text order_preserving} are now active in @{text |
|
385 lattice_hom}, for example |
|
386 @{thm [source] hom_le}: |
|
387 @{thm [display, indent=2] hom_le} |
|
388 This theorem will be useful in the following section. |
|
389 *} |
|
390 |
|
391 |
|
392 section {* Conditional Interpretation *} |
|
393 |
|
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 non-negative, 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 |
|
412 locale non_negative = |
|
413 fixes n :: int |
|
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. *} |
|
419 |
|
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. *} |
|
427 |
|
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) |
|
438 |
|
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: *} |
|
442 |
|
443 lemmas (in order_preserving) hom_le [simp] |
|
444 |
|
445 |
|
446 subsection {* Avoiding Infinite Chains of Interpretations |
|
447 \label{sec:infinite-chains} *} |
|
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 point-wise lifting of the |
|
455 partial order of the co-domain. 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 co-domain is a partial order, and |
|
470 to make the interpretation in its context: *} |
|
471 |
|
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 co-domain is a lattice: *} |
|
482 |
|
483 locale fun_lattice = fun_partial_order + lattice |
|
484 |
|
485 sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" |
|
486 proof unfold_locales |
|
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 |
|
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 |
|
505 dependencies see~\cite{Ballarin2006a}; interpretations in theories |
|
506 and proofs are covered in~\cite{Ballarin2006b}. In the latter, I |
|
507 show how interpretation in proofs enables to reason about families |
|
508 of algebraic structures, which cannot be expressed with locales |
|
509 directly. |
|
510 |
|
511 Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction |
|
512 of axiomatic type classes through a combination with locale |
|
513 interpretation. The result is a Haskell-style class system with a |
|
514 facility to generate ML and Haskell code. Classes are sufficient for |
|
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 |
|
520 The locales reimplementation for Isabelle 2009 provides, among other |
|
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}. |
|
524 |
|
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}. |
|
531 |
|
532 The sources of this tutorial, which include all proofs, are |
|
533 available with the Isabelle distribution at |
|
534 \url{http://isabelle.in.tum.de}. |
|
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{attr-name} & ::= |
|
546 & \textit{name} $|$ \textit{attribute} $|$ |
|
547 \textit{name} \textit{attribute} \\ |
|
548 \textit{qualifier} & ::= |
|
549 & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex] |
|
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{attr-name} ``\textbf{:}'' ] \textit{proposition} \\ |
|
563 \begin{comment} |
|
564 \textit{defines} & ::= |
|
565 & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\ |
|
566 \textit{notes} & ::= |
|
567 & [ \textit{attr-name} ``\textbf{=}'' ] |
|
568 ( \textit{qualified-name} [ \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 |
|
589 \textit{pos-insts} & ::= |
|
590 & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\ |
|
591 \textit{named-insts} & ::= |
|
592 & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} |
|
593 ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ |
|
594 \textit{instance} & ::= |
|
595 & [ \textit{qualifier} ``\textbf{:}'' ] |
|
596 \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ |
|
597 \textit{expression} & ::= |
|
598 & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ |
|
599 [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] |
|
600 |
|
601 \multicolumn{3}{l}{Declaration of Locales} \\ |
|
602 |
|
603 \textit{locale} & ::= |
|
604 & \textit{element}$^+$ \\ |
|
605 & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ |
|
606 \textit{toplevel} & ::= |
|
607 & \textbf{locale} \textit{name} [ ``\textbf{=}'' |
|
608 \textit{locale} ] \\[2ex] |
|
609 |
|
610 \multicolumn{3}{l}{Interpretation} \\ |
|
611 |
|
612 \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ] |
|
613 \textit{prop} \\ |
|
614 \textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and} |
|
615 \textit{equation} )$^*$ \\ |
|
616 \textit{toplevel} & ::= |
|
617 & \textbf{sublocale} \textit{name} ( ``$<$'' $|$ |
|
618 ``$\subseteq$'' ) \textit{expression} \textit{proof} \\ |
|
619 & | |
|
620 & \textbf{interpretation} |
|
621 \textit{expression} [ \textit{equations} ] \textit{proof} \\ |
|
622 & | |
|
623 & \textbf{interpret} |
|
624 \textit{expression} \textit{proof} \\[2ex] |
|
625 |
|
626 \multicolumn{3}{l}{Diagnostics} \\ |
|
627 |
|
628 \textit{toplevel} & ::= |
|
629 & \textbf{print\_locales} \\ |
|
630 & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\ |
|
631 & | & \textbf{print\_interps} \textit{name} |
|
632 \end{tabular} |
|
633 \end{center} |
|
634 \hrule |
|
635 \caption{Syntax of Locale Commands.} |
|
636 \label{tab:commands} |
|
637 \end{table} |
|
638 *} |
|
639 |
|
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. *} |
|
648 |
|
649 text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, |
|
650 Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel |
|
651 have made |
|
652 useful comments on earlier versions of this document. The section |
|
653 on conditional interpretation was inspired by a number of e-mail |
|
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. *} |
|
658 |
|
659 end |
|