1theory Examples3 2imports Examples 3begin 4 5subsection \<open>Third Version: Local Interpretation 6 \label{sec:local-interpretation}\<close> 7 8text \<open>In the above example, the fact that @{term "(\<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 "(\<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.\<close> 18 19 interpretation %visible int: partial_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 20 rewrites "int.less x y = (x < y)" 21 proof - 22 show "partial_order ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)" 23 by unfold_locales auto 24 then interpret int: partial_order "(\<le>) :: [int, int] \<Rightarrow> bool" . 25 show "int.less x y = (x < y)" 26 unfolding int.less_def by auto 27 qed 28 29text \<open>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.\<close> 37 38 39subsection \<open>Further Interpretations\<close> 40 41text \<open>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.\<close> 48 49 interpretation %visible int: lattice "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 50 rewrites 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 ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)" 54 txt \<open>\normalsize We have already shown that this is a partial 55 order,\<close> 56 apply unfold_locales 57 txt \<open>\normalsize hence only the lattice axioms remain to be 58 shown. 59 @{subgoals [display]} 60 By @{text is_inf} and @{text is_sup},\<close> 61 apply (unfold int.is_inf_def int.is_sup_def) 62 txt \<open>\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}.\<close> 67 by arith+ 68 txt \<open>\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.\<close> 71 then interpret int: lattice "(\<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 78text \<open>Next follows that @{text "(\<le>)"} is a total order, again for 79 the integers.\<close> 80 81 interpretation %visible int: total_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 82 by unfold_locales arith 83 84text \<open>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 "(<)"} appears in theorem @{thm [source] 119 int.less_total} 120 although an equation for the replacement of @{text "(\<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\<close> 127 128text \<open>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 "(\(\le\))" 136\end{alltt} 137\end{small} 138 Of course, there is only one interpretation. 139 The interpretation qualifier on the left is mandatory. Qualifiers 140 can either be \emph{mandatory} or \emph{optional}. Optional qualifiers 141 are designated by ``?''. Mandatory qualifiers must occur in 142 name references while optional ones need not. Mandatory qualifiers 143 prevent accidental hiding of names, while optional qualifiers can be 144 more convenient to use. The default is mandatory. 145\<close> 146 147 148section \<open>Locale Expressions \label{sec:expressions}\<close> 149 150text \<open> 151 A map~@{term \<phi>} between partial orders~@{text \<sqsubseteq>} and~@{text \<preceq>} 152 is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq> 153 \<phi> y"}. This situation is more complex than those encountered so 154 far: it involves two partial orders, and it is desirable to use the 155 existing locale for both. 156 157 A locale for order preserving maps requires three parameters: @{text 158 le}~(\isakeyword{infixl}~@{text \<sqsubseteq>}) and @{text 159 le'}~(\isakeyword{infixl}~@{text \<preceq>}) for the orders and~@{text \<phi>} 160 for the map. 161 162 In order to reuse the existing locale for partial orders, which has 163 the single parameter~@{text le}, it must be imported twice, once 164 mapping its parameter to~@{text le} from the new locale and once 165 to~@{text le'}. This can be achieved with a compound locale 166 expression. 167 168 In general, a locale expression is a sequence of \emph{locale instances} 169 separated by~``$\textbf{+}$'' and followed by a \isakeyword{for} 170 clause. 171 An instance has the following format: 172\begin{quote} 173 \textit{qualifier} \textbf{:} \textit{locale-name} 174 \textit{parameter-instantiation} 175\end{quote} 176 We have already seen locale instances as arguments to 177 \isakeyword{interpretation} in Section~\ref{sec:interpretation}. 178 As before, the qualifier serves to disambiguate names from 179 different instances of the same locale, and unless designated with a 180 ``?'' it must occur in name references. 181 182 Since the parameters~@{text le} and~@{text le'} are to be partial 183 orders, our locale for order preserving maps will import the these 184 instances: 185\begin{small} 186\begin{alltt} 187 le: partial_order le 188 le': partial_order le' 189\end{alltt} 190\end{small} 191 For matter of convenience we choose to name parameter names and 192 qualifiers alike. This is an arbitrary decision. Technically, qualifiers 193 and parameters are unrelated. 194 195 Having determined the instances, let us turn to the \isakeyword{for} 196 clause. It serves to declare locale parameters in the same way as 197 the context element \isakeyword{fixes} does. Context elements can 198 only occur after the import section, and therefore the parameters 199 referred to in the instances must be declared in the \isakeyword{for} 200 clause. The \isakeyword{for} clause is also where the syntax of these 201 parameters is declared. 202 203 Two context elements for the map parameter~@{text \<phi>} and the 204 assumptions that it is order preserving complete the locale 205 declaration.\<close> 206 207 locale order_preserving = 208 le: partial_order le + le': partial_order le' 209 for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) + 210 fixes \<phi> 211 assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y" 212 213text (in order_preserving) \<open>Here are examples of theorems that are 214 available in the locale: 215 216 \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le} 217 218 \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans} 219 220 \hspace*{1em}@{thm [source] le'.less_le_trans}: 221 @{thm [display, indent=4] le'.less_le_trans} 222 While there is infix syntax for the strict operation associated with 223 @{term "(\<sqsubseteq>)"}, there is none for the strict version of @{term 224 "(\<preceq>)"}. The syntax @{text "\<sqsubset>"} for @{text less} is only 225 available for the original instance it was declared for. We may 226 introduce infix syntax for @{text le'.less} with the following declaration:\<close> 227 228 notation (in order_preserving) le'.less (infixl "\<prec>" 50) 229 230text (in order_preserving) \<open>Now the theorem is displayed nicely as 231 @{thm [source] le'.less_le_trans}: 232 @{thm [display, indent=2] le'.less_le_trans}\<close> 233 234text \<open>There are short notations for locale expressions. These are 235 discussed in the following.\<close> 236 237 238subsection \<open>Default Instantiations\<close> 239 240text \<open> 241 It is possible to omit parameter instantiations. The 242 instantiation then defaults to the name of 243 the parameter itself. For example, the locale expression @{text 244 partial_order} is short for @{text "partial_order le"}, since the 245 locale's single parameter is~@{text le}. We took advantage of this 246 in the \isakeyword{sublocale} declarations of 247 Section~\ref{sec:changing-the-hierarchy}.\<close> 248 249 250subsection \<open>Implicit Parameters \label{sec:implicit-parameters}\<close> 251 252text \<open>In a locale expression that occurs within a locale 253 declaration, omitted parameters additionally extend the (possibly 254 empty) \isakeyword{for} clause. 255 256 The \isakeyword{for} clause is a general construct of Isabelle/Isar 257 to mark names occurring in the preceding declaration as ``arbitrary 258 but fixed''. This is necessary for example, if the name is already 259 bound in a surrounding context. In a locale expression, names 260 occurring in parameter instantiations should be bound by a 261 \isakeyword{for} clause whenever these names are not introduced 262 elsewhere in the context --- for example, on the left hand side of a 263 \isakeyword{sublocale} declaration. 264 265 There is an exception to this rule in locale declarations, where the 266 \isakeyword{for} clause serves to declare locale parameters. Here, 267 locale parameters for which no parameter instantiation is given are 268 implicitly added, with their mixfix syntax, at the beginning of the 269 \isakeyword{for} clause. For example, in a locale declaration, the 270 expression @{text partial_order} is short for 271\begin{small} 272\begin{alltt} 273 partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.} 274\end{alltt} 275\end{small} 276 This short hand was used in the locale declarations throughout 277 Section~\ref{sec:import}. 278\<close> 279 280text\<open> 281 The following locale declarations provide more examples. A 282 map~@{text \<phi>} is a lattice homomorphism if it preserves meet and 283 join.\<close> 284 285 locale lattice_hom = 286 le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) + 287 fixes \<phi> 288 assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)" 289 and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)" 290 291text \<open>The parameter instantiation in the first instance of @{term 292 lattice} is omitted. This causes the parameter~@{text le} to be 293 added to the \isakeyword{for} clause, and the locale has 294 parameters~@{text le},~@{text le'} and, of course,~@{text \<phi>}. 295 296 Before turning to the second example, we complete the locale by 297 providing infix syntax for the meet and join operations of the 298 second lattice. 299\<close> 300 301 context lattice_hom 302 begin 303 notation le'.meet (infixl "\<sqinter>''" 50) 304 notation le'.join (infixl "\<squnion>''" 50) 305 end 306 307text \<open>The next example makes radical use of the short hand 308 facilities. A homomorphism is an endomorphism if both orders 309 coincide.\<close> 310 311 locale lattice_end = lattice_hom _ le 312 313text \<open>The notation~@{text _} enables to omit a parameter in a 314 positional instantiation. The omitted parameter,~@{text le} becomes 315 the parameter of the declared locale and is, in the following 316 position, used to instantiate the second parameter of @{text 317 lattice_hom}. The effect is that of identifying the first in second 318 parameter of the homomorphism locale.\<close> 319 320text \<open>The inheritance diagram of the situation we have now is shown 321 in Figure~\ref{fig:hom}, where the dashed line depicts an 322 interpretation which is introduced below. Parameter instantiations 323 are indicated by $\sqsubseteq \mapsto \preceq$ etc. By looking at 324 the inheritance diagram it would seem 325 that two identical copies of each of the locales @{text 326 partial_order} and @{text lattice} are imported by @{text 327 lattice_end}. This is not the case! Inheritance paths with 328 identical morphisms are automatically detected and 329 the conclusions of the respective locales appear only once. 330 331\begin{figure} 332\hrule \vspace{2ex} 333\begin{center} 334\begin{tikzpicture} 335 \node (o) at (0,0) {@{text partial_order}}; 336 \node (oh) at (1.5,-2) {@{text order_preserving}}; 337 \node (oh1) at (1.5,-0.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 338 \node (oh2) at (0,-1.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; 339 \node (l) at (-1.5,-2) {@{text lattice}}; 340 \node (lh) at (0,-4) {@{text lattice_hom}}; 341 \node (lh1) at (0,-2.7) {$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 342 \node (lh2) at (-1.5,-3.3) {$\scriptscriptstyle \sqsubseteq \mapsto \preceq$}; 343 \node (le) at (0,-6) {@{text lattice_end}}; 344 \node (le1) at (0,-4.8) 345 [anchor=west]{$\scriptscriptstyle \sqsubseteq \mapsto \sqsubseteq$}; 346 \node (le2) at (0,-5.2) 347 [anchor=west]{$\scriptscriptstyle \preceq \mapsto \sqsubseteq$}; 348 \draw (o) -- (l); 349 \draw[dashed] (oh) -- (lh); 350 \draw (lh) -- (le); 351 \draw (o) .. controls (oh1.south west) .. (oh); 352 \draw (o) .. controls (oh2.north east) .. (oh); 353 \draw (l) .. controls (lh1.south west) .. (lh); 354 \draw (l) .. controls (lh2.north east) .. (lh); 355\end{tikzpicture} 356\end{center} 357\hrule 358\caption{Hierarchy of Homomorphism Locales.} 359\label{fig:hom} 360\end{figure} 361\<close> 362 363text \<open>It can be shown easily that a lattice homomorphism is order 364 preserving. As the final example of this section, a locale 365 interpretation is used to assert this:\<close> 366 367 sublocale lattice_hom \<subseteq> order_preserving 368 proof unfold_locales 369 fix x y 370 assume "x \<sqsubseteq> y" 371 then have "y = (x \<squnion> y)" by (simp add: le.join_connection) 372 then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric]) 373 then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection) 374 qed 375 376text (in lattice_hom) \<open> 377 Theorems and other declarations --- syntax, in particular --- from 378 the locale @{text order_preserving} are now active in @{text 379 lattice_hom}, for example 380 @{thm [source] hom_le}: 381 @{thm [display, indent=2] hom_le} 382 This theorem will be useful in the following section. 383\<close> 384 385 386section \<open>Conditional Interpretation\<close> 387 388text \<open>There are situations where an interpretation is not possible 389 in the general case since the desired property is only valid if 390 certain conditions are fulfilled. Take, for example, the function 391 @{text "\<lambda>i. n * i"} that scales its argument by a constant factor. 392 This function is order preserving (and even a lattice endomorphism) 393 with respect to @{term "(\<le>)"} provided @{text "n \<ge> 0"}. 394 395 It is not possible to express this using a global interpretation, 396 because it is in general unspecified whether~@{term n} is 397 non-negative, but one may make an interpretation in an inner context 398 of a proof where full information is available. 399 This is not fully satisfactory either, since potentially 400 interpretations may be required to make interpretations in many 401 contexts. What is 402 required is an interpretation that depends on the condition --- and 403 this can be done with the \isakeyword{sublocale} command. For this 404 purpose, we introduce a locale for the condition.\<close> 405 406 locale non_negative = 407 fixes n :: int 408 assumes non_neg: "0 \<le> n" 409 410text \<open>It is again convenient to make the interpretation in an 411 incremental fashion, first for order preserving maps, then for 412 lattice endomorphisms.\<close> 413 414 sublocale non_negative \<subseteq> 415 order_preserving "(\<le>)" "(\<le>)" "\<lambda>i. n * i" 416 using non_neg by unfold_locales (rule mult_left_mono) 417 418text \<open>While the proof of the previous interpretation 419 is straightforward from monotonicity lemmas for~@{term "( * )"}, the 420 second proof follows a useful pattern.\<close> 421 422 sublocale %visible non_negative \<subseteq> lattice_end "(\<le>)" "\<lambda>i. n * i" 423 proof (unfold_locales, unfold int_min_eq int_max_eq) 424 txt \<open>\normalsize Unfolding the locale predicates \emph{and} the 425 interpretation equations immediately yields two subgoals that 426 reflect the core conjecture. 427 @{subgoals [display]} 428 It is now necessary to show, in the context of @{term 429 non_negative}, that multiplication by~@{term n} commutes with 430 @{term min} and @{term max}.\<close> 431 qed (auto simp: hom_le) 432 433text (in order_preserving) \<open>The lemma @{thm [source] hom_le} 434 simplifies a proof that would have otherwise been lengthy and we may 435 consider making it a default rule for the simplifier:\<close> 436 437 lemmas (in order_preserving) hom_le [simp] 438 439 440subsection \<open>Avoiding Infinite Chains of Interpretations 441 \label{sec:infinite-chains}\<close> 442 443text \<open>Similar situations arise frequently in formalisations of 444 abstract algebra where it is desirable to express that certain 445 constructions preserve certain properties. For example, polynomials 446 over rings are rings, or --- an example from the domain where the 447 illustrations of this tutorial are taken from --- a partial order 448 may be obtained for a function space by point-wise lifting of the 449 partial order of the co-domain. This corresponds to the following 450 interpretation:\<close> 451 452 sublocale %visible partial_order \<subseteq> f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 453 oops 454 455text \<open>Unfortunately this is a cyclic interpretation that leads to an 456 infinite chain, namely 457 @{text [display, indent=2] "partial_order \<subseteq> partial_order (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) \<subseteq> 458 partial_order (\<lambda>f g. \<forall>x y. f x y \<sqsubseteq> g x y) \<subseteq> \<dots>"} 459 and the interpretation is rejected. 460 461 Instead it is necessary to declare a locale that is logically 462 equivalent to @{term partial_order} but serves to collect facts 463 about functions spaces where the co-domain is a partial order, and 464 to make the interpretation in its context:\<close> 465 466 locale fun_partial_order = partial_order 467 468 sublocale fun_partial_order \<subseteq> 469 f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 470 by unfold_locales (fast,rule,fast,blast intro: trans) 471 472text \<open>It is quite common in abstract algebra that such a construction 473 maps a hierarchy of algebraic structures (or specifications) to a 474 related hierarchy. By means of the same lifting, a function space 475 is a lattice if its co-domain is a lattice:\<close> 476 477 locale fun_lattice = fun_partial_order + lattice 478 479 sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x" 480 proof unfold_locales 481 fix f g 482 have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)" 483 apply (rule f.is_infI) apply rule+ apply (drule spec, assumption)+ done 484 then show "\<exists>inf. partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g inf" 485 by fast 486 next 487 fix f g 488 have "partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<squnion> g x)" 489 apply (rule f.is_supI) apply rule+ apply (drule spec, assumption)+ done 490 then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup" 491 by fast 492 qed 493 494 495section \<open>Further Reading\<close> 496 497text \<open>More information on locales and their interpretation is 498 available. For the locale hierarchy of import and interpretation 499 dependencies see~@{cite Ballarin2006a}; interpretations in theories 500 and proofs are covered in~@{cite Ballarin2006b}. In the latter, I 501 show how interpretation in proofs enables to reason about families 502 of algebraic structures, which cannot be expressed with locales 503 directly. 504 505 Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction 506 of axiomatic type classes through a combination with locale 507 interpretation. The result is a Haskell-style class system with a 508 facility to generate ML and Haskell code. Classes are sufficient for 509 simple specifications with a single type parameter. The locales for 510 orders and lattices presented in this tutorial fall into this 511 category. Order preserving maps, homomorphisms and vector spaces, 512 on the other hand, do not. 513 514 The locales reimplementation for Isabelle 2009 provides, among other 515 improvements, a clean integration with Isabelle/Isar's local theory 516 mechanisms, which are described in another paper by Haftmann and 517 Wenzel~@{cite HaftmannWenzel2009}. 518 519 The original work of Kamm\"uller on locales~@{cite KammullerEtAl1999} 520 may be of interest from a historical perspective. My previous 521 report on locales and locale expressions~@{cite Ballarin2004a} 522 describes a simpler form of expressions than available now and is 523 outdated. The mathematical background on orders and lattices is 524 taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}. 525 526 The sources of this tutorial, which include all proofs, are 527 available with the Isabelle distribution at 528 \<^url>\<open>https://isabelle.in.tum.de\<close>. 529\<close> 530 531text \<open> 532\begin{table} 533\hrule 534\vspace{2ex} 535\begin{center} 536\begin{tabular}{l>$c<$l} 537 \multicolumn{3}{l}{Miscellaneous} \\ 538 539 \textit{attr-name} & ::= 540 & \textit{name} $|$ \textit{attribute} $|$ 541 \textit{name} \textit{attribute} \\ 542 \textit{qualifier} & ::= 543 & \textit{name} [``\textbf{?}''] \\[2ex] 544 545 \multicolumn{3}{l}{Context Elements} \\ 546 547 \textit{fixes} & ::= 548 & \textit{name} [ ``\textbf{::}'' \textit{type} ] 549 [ ``\textbf{(}'' \textbf{structure} ``\textbf{)}'' $|$ 550 \textit{mixfix} ] \\ 551\begin{comment} 552 \textit{constrains} & ::= 553 & \textit{name} ``\textbf{::}'' \textit{type} \\ 554\end{comment} 555 \textit{assumes} & ::= 556 & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\ 557\begin{comment} 558 \textit{defines} & ::= 559 & [ \textit{attr-name} ``\textbf{:}'' ] \textit{proposition} \\ 560 \textit{notes} & ::= 561 & [ \textit{attr-name} ``\textbf{=}'' ] 562 ( \textit{qualified-name} [ \textit{attribute} ] )$^+$ \\ 563\end{comment} 564 565 \textit{element} & ::= 566 & \textbf{fixes} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ \\ 567\begin{comment} 568 & | 569 & \textbf{constrains} \textit{constrains} 570 ( \textbf{and} \textit{constrains} )$^*$ \\ 571\end{comment} 572 & | 573 & \textbf{assumes} \textit{assumes} ( \textbf{and} \textit{assumes} )$^*$ \\[2ex] 574%\begin{comment} 575% & | 576% & \textbf{defines} \textit{defines} ( \textbf{and} \textit{defines} )$^*$ \\ 577% & | 578% & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\ 579%\end{comment} 580 581 \multicolumn{3}{l}{Locale Expressions} \\ 582 583 \textit{pos-insts} & ::= 584 & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\ 585 \textit{named-insts} & ::= 586 & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} 587 ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ 588 \textit{instance} & ::= 589 & [ \textit{qualifier} ``\textbf{:}'' ] 590 \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ 591 \textit{expression} & ::= 592 & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ 593 [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] 594 595 \multicolumn{3}{l}{Declaration of Locales} \\ 596 597 \textit{locale} & ::= 598 & \textit{element}$^+$ \\ 599 & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ 600 \textit{toplevel} & ::= 601 & \textbf{locale} \textit{name} [ ``\textbf{=}'' 602 \textit{locale} ] \\[2ex] 603 604 \multicolumn{3}{l}{Interpretation} \\ 605 606 \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ] 607 \textit{prop} \\ 608 \textit{equations} & ::= & \textbf{rewrites} \textit{equation} ( \textbf{and} 609 \textit{equation} )$^*$ \\ 610 \textit{toplevel} & ::= 611 & \textbf{sublocale} \textit{name} ( ``$<$'' $|$ 612 ``$\subseteq$'' ) \textit{expression} \textit{proof} \\ 613 & | 614 & \textbf{interpretation} 615 \textit{expression} [ \textit{equations} ] \textit{proof} \\ 616 & | 617 & \textbf{interpret} 618 \textit{expression} \textit{proof} \\[2ex] 619 620 \multicolumn{3}{l}{Diagnostics} \\ 621 622 \textit{toplevel} & ::= 623 & \textbf{print\_locales} \\ 624 & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\ 625 & | & \textbf{print\_interps} \textit{name} 626\end{tabular} 627\end{center} 628\hrule 629\caption{Syntax of Locale Commands.} 630\label{tab:commands} 631\end{table} 632\<close> 633 634text \<open>\textbf{Revision History.} The present fourth revision of the 635 tutorial accommodates minor updates to the syntax of the locale commands 636 and the handling of notation under morphisms introduced with Isabelle 2016. 637 For the third revision of the tutorial, which corresponds to the published 638 version, much of the explanatory text was rewritten. Inheritance of 639 interpretation equations was made available with Isabelle 2009-1. 640 The second revision accommodates changes introduced by the locales 641 reimplementation for Isabelle 2009. Most notably locale expressions 642 were generalised from renaming to instantiation.\<close> 643 644text \<open>\textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, 645 Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel 646 have made 647 useful comments on earlier versions of this document. The section 648 on conditional interpretation was inspired by a number of e-mail 649 enquiries the author received from locale users, and which suggested 650 that this use case is important enough to deserve explicit 651 explanation. The term \emph{conditional interpretation} is due to 652 Larry Paulson.\<close> 653 654end 655