author  ballarin 
Mon, 19 Jan 2009 20:37:08 +0100  
changeset 29566  937baa077df2 
parent 27595  3ac9e3cd1fa3 
child 29567  286c01be90cb 
permissions  rwrr 
27081  1 
(* $Id$ *) 
2 

27063  3 
theory Examples3 
4 
imports Examples 

5 
begin 

6 

7 
subsection {* Third Version: Local Interpretation *} 

8 

9 
text {* In the above example, the fact that @{text \<le>} is a partial 

10 
order for the natural numbers was used in the proof of the 

11 
second goal. In general, proofs of the equations may involve 

12 
theorems implied by the fact the assumptions of the instantiated 

13 
locale hold for the instantiating structure. If these theorems have 

14 
been shown abstractly in the locale they can be made available 

15 
conveniently in the context through an auxiliary local interpretation (keyword 

16 
\isakeyword{interpret}). This interpretation is inside the proof of the global 

17 
interpretation. The third revision of the example illustrates this. *} 

18 

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

19 
interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" 
27063  20 
where "partial_order.less (op \<le>) (x::nat) y = (x < y)" 
21 
proof  

22 
show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" 

23 
by unfold_locales auto 

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

24 
then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" . 
27063  25 
show "partial_order.less (op \<le>) (x::nat) y = (x < y)" 
26 
unfolding nat.less_def by auto 

27 
qed 

28 

29 
text {* The inner interpretation does not require an 

30 
elaborate new proof, it is immediate from the preceeding fact and 

31 
proved with ``.''. 

32 
This interpretation enriches the local proof context by 

33 
the very theorems also obtained in the interpretation from 

34 
Section~\ref{sec:pofirst}, and @{text nat.less_def} may directly be 

35 
used to unfold the definition. Theorems from the local 

36 
interpretation disappear after leaving the proof context  that 

37 
is, after the closing \isakeyword{qed}  and are 

38 
then replaced by those with the desired substitutions of the strict 

39 
order. *} 

40 

41 

42 
subsection {* Further Interpretations *} 

43 

44 
text {* Further interpretations are necessary to reuse theorems from 

45 
the other locales. In @{text lattice} the operations @{text \<sqinter>} and 

46 
@{text \<squnion>} are substituted by @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} and 

47 
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"}. The entire proof for the 

48 
interpretation is reproduced in order to give an example of a more 

49 
elaborate interpretation proof. *} 

50 

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

51 
interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" 
27063  52 
where "lattice.meet op \<le> (x::nat) y = min x y" 
53 
and "lattice.join op \<le> (x::nat) y = max x y" 

54 
proof  

55 
show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)" 

56 
txt {* We have already shown that this is a partial order, *} 

57 
apply unfold_locales 

58 
txt {* hence only the lattice axioms remain to be shown: @{subgoals 

59 
[display]} After unfolding @{text is_inf} and @{text is_sup}, *} 

60 
apply (unfold nat.is_inf_def nat.is_sup_def) 

61 
txt {* the goals become @{subgoals [display]} which can be solved 

62 
by Presburger arithmetic. *} 

63 
by arith+ 

64 
txt {* In order to show the equations, we put ourselves in a 

65 
situation where the lattice theorems can be used in a convenient way. *} 

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

66 
then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" . 
27063  67 
show "lattice.meet op \<le> (x::nat) y = min x y" 
68 
by (bestsimp simp: nat.meet_def nat.is_inf_def) 

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

70 
by (bestsimp simp: nat.join_def nat.is_sup_def) 

71 
qed 

72 

73 
text {* That the relation @{text \<le>} is a total order completes this 

74 
sequence of interpretations. *} 

75 

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

76 
interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" 
27063  77 
by unfold_locales arith 
78 

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

80 
Table~\ref{tab:natlattice}. 

81 

82 
\begin{table} 

83 
\hrule 

84 
\vspace{2ex} 

85 
\begin{center} 

86 
\begin{tabular}{l} 

87 
@{thm [source] nat.less_def} from locale @{text partial_order}: \\ 

88 
\quad @{thm nat.less_def} \\ 

89 
@{thm [source] nat.meet_left} from locale @{text lattice}: \\ 

90 
\quad @{thm nat.meet_left} \\ 

91 
@{thm [source] nat.join_distr} from locale @{text distrib_lattice}: \\ 

92 
\quad @{thm nat.join_distr} \\ 

93 
@{thm [source] nat.less_total} from locale @{text total_order}: \\ 

94 
\quad @{thm nat.less_total} 

95 
\end{tabular} 

96 
\end{center} 

97 
\hrule 

98 
\caption{Interpreted theorems for @{text \<le>} on the natural numbers.} 

99 
\label{tab:natlattice} 

100 
\end{table} 

101 

102 
Note that since the locale hierarchy reflects that total orders are 

103 
distributive lattices, an explicit interpretation of distributive 

104 
lattices for the order relation on natural numbers is not neccessary. 

105 

106 
Why not push this idea further and just give the last interpretation 

107 
as a single interpretation instead of the sequence of three? The 

108 
reasons for this are twofold: 

109 
\begin{itemize} 

110 
\item 

111 
Often it is easier to work in an incremental fashion, because later 

112 
interpretations require theorems provided by earlier 

113 
interpretations. 

114 
\item 

115 
Assume that a definition is made in some locale $l_1$, and that $l_2$ 

116 
imports $l_1$. Let an equation for the definition be 

117 
proved in an interpretation of $l_2$. The equation will be unfolded 

118 
in interpretations of theorems added to $l_2$ or below in the import 

119 
hierarchy, but not for theorems added above $l_2$. 

120 
Hence, an equation interpreting a definition should always be given in 

121 
an interpretation of the locale where the definition is made, not in 

122 
an interpretation of a locale further down the hierarchy. 

123 
\end{itemize} 

124 
*} 

125 

126 

127 
subsection {* Lattice @{text "dvd"} on @{typ nat} *} 

128 

129 
text {* Divisibility on the natural numbers is a distributive lattice 

130 
but not a total order. Interpretation again proceeds 

131 
incrementally. *} 

132 

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

133 
interpretation nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" 
27063  134 
where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)" 
135 
proof  

136 
show "partial_order (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" 

137 
by unfold_locales (auto simp: dvd_def) 

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

138 
then interpret nat_dvd: partial_order "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" . 
27063  139 
show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)" 
140 
apply (unfold nat_dvd.less_def) 

141 
apply auto 

142 
done 

143 
qed 

144 

145 
text {* Note that there is no symbol for strict divisibility. Instead, 

146 
interpretation substitutes @{term "x dvd y \<and> x \<noteq> y"}. *} 

147 

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

148 
interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" 
27063  149 
where nat_dvd_meet_eq: 
27595  150 
"lattice.meet op dvd = gcd" 
27063  151 
and nat_dvd_join_eq: 
27595  152 
"lattice.join op dvd = lcm" 
27063  153 
proof  
154 
show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)" 

155 
apply unfold_locales 

156 
apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def) 

27595  157 
apply (rule_tac x = "gcd x y" in exI) 
27063  158 
apply auto [1] 
27595  159 
apply (rule_tac x = "lcm x y" in exI) 
27063  160 
apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) 
161 
done 

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

162 
then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" . 
27595  163 
show "lattice.meet op dvd = gcd" 
164 
apply (auto simp add: expand_fun_eq) 

27063  165 
apply (unfold nat_dvd.meet_def) 
166 
apply (rule the_equality) 

167 
apply (unfold nat_dvd.is_inf_def) 

168 
by auto 

27595  169 
show "lattice.join op dvd = lcm" 
170 
apply (auto simp add: expand_fun_eq) 

27063  171 
apply (unfold nat_dvd.join_def) 
172 
apply (rule the_equality) 

173 
apply (unfold nat_dvd.is_sup_def) 

174 
by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least) 

175 
qed 

176 

177 
text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source] 

178 
nat_dvd_join_eq} are named since they are handy in the proof of 

179 
the subsequent interpretation. *} 

180 

181 
ML %invisible {* set quick_and_dirty *} 

182 

183 
(* 

184 
definition 

185 
is_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where 

186 
"is_lcm p m n \<longleftrightarrow> m dvd p \<and> n dvd p \<and> 

187 
(\<forall>d. m dvd d \<longrightarrow> n dvd d \<longrightarrow> p dvd d)" 

188 

189 
lemma is_gcd: "is_lcm (lcm (m, n)) m n" 

190 
by (simp add: is_lcm_def lcm_least) 

191 

192 
lemma gcd_lcm_distr_lemma: 

193 
"[ is_gcd g1 x l1; is_lcm l1 y z; is_gcd g2 x y; is_gcd g3 x z ] ==> is_lcm g1 g2 g3" 

194 
apply (unfold is_gcd_def is_lcm_def dvd_def) 

195 
apply (clarsimp simp: mult_ac) 

196 
apply (blast intro: mult_is_0) 

197 
thm mult_is_0 [THEN iffD1] 

198 
*) 

199 

200 
lemma %invisible gcd_lcm_distr: 

27595  201 
"gcd x (lcm y z) = lcm (gcd x y) (gcd x z)" sorry 
27063  202 

203 
ML %invisible {* reset quick_and_dirty *} 

204 

205 
interpretation %visible nat_dvd: 

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

206 
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" 
27063  207 
apply unfold_locales 
208 
txt {* @{subgoals [display]} *} 

209 
apply (unfold nat_dvd_meet_eq nat_dvd_join_eq) 

210 
txt {* @{subgoals [display]} *} 

211 
apply (rule gcd_lcm_distr) done 

212 

213 

214 
text {* Theorems that are available in the theory after these 

215 
interpretations are shown in Table~\ref{tab:natdvdlattice}. 

216 

217 
\begin{table} 

218 
\hrule 

219 
\vspace{2ex} 

220 
\begin{center} 

221 
\begin{tabular}{l} 

222 
@{thm [source] nat_dvd.less_def} from locale @{text partial_order}: \\ 

223 
\quad @{thm nat_dvd.less_def} \\ 

224 
@{thm [source] nat_dvd.meet_left} from locale @{text lattice}: \\ 

225 
\quad @{thm nat_dvd.meet_left} \\ 

226 
@{thm [source] nat_dvd.join_distr} from locale @{text distrib_lattice}: \\ 

227 
\quad @{thm nat_dvd.join_distr} \\ 

228 
\end{tabular} 

229 
\end{center} 

230 
\hrule 

231 
\caption{Interpreted theorems for @{text dvd} on the natural numbers.} 

232 
\label{tab:natdvdlattice} 

233 
\end{table} 

234 
*} 

235 

236 
text {* 

237 
The full syntax of the interpretation commands is shown in 

238 
Table~\ref{tab:commands}. The grammar refers to 

239 
\textit{expr}, which stands for a \emph{locale} expression. Locale 

240 
expressions are discussed in Section~\ref{sec:expressions}. 

241 
*} 

242 

243 

27077  244 
section {* Locale Expressions \label{sec:expressions} *} 
27063  245 

246 
text {* 

247 
A map @{term \<phi>} between partial orders @{text \<sqsubseteq>} and @{text \<preceq>} 

248 
is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq> 

249 
\<phi> y"}. This situation is more complex than those encountered so 

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

251 
existing locale for both. 

252 

253 
Inspecting the grammar of locale commands in 

254 
Table~\ref{tab:commands} reveals that the import of a locale can be 

255 
more than just a single locale. In general, the import is a 

256 
\emph{locale expression}. Locale expressions enable to combine locales 

257 
and rename parameters. A locale name is a locale expression. If 

258 
$e_1$ and $e_2$ are locale expressions then $e_1 + e_2$ is their 

27075
34005fa42128
renamed expression: plain ~ (space) instead of \colon;
wenzelm
parents:
27073
diff
changeset

259 
\emph{merge}. If $e$ is an expression, then $e~q_1 \ldots q_n$ is 
27063  260 
a \emph{renamed expression} where the parameters in $e$ are renamed 
261 
to $q_1 \ldots q_n$. Using a locale expression, a locale for order 

262 
preserving maps can be declared in the following way. *} 

263 

264 
locale order_preserving = 

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

265 
le: partial_order + le': partial_order le' for le' (infixl "\<preceq>" 50) + 
27063  266 
fixes \<phi> :: "'a \<Rightarrow> 'b" 
267 
assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y" 

268 

269 
text {* The second line contains the expression, which is the 

270 
merge of two partial order locales. The parameter of the second one 

271 
is @{text le'} with new infix syntax @{text \<preceq>}. The 

272 
parameters of the entire locale are @{text le}, @{text le'} and 

273 
@{text \<phi>}. This is their \emph{canonical order}, 

274 
which is obtained by a lefttoright traversal of the expression, 

275 
where only the new parameters are appended to the end of the list. The 

276 
parameters introduced in the locale elements of the declaration 

277 
follow. 

278 

279 
In renamings parameters are referred to by position in the canonical 

280 
order; an underscore is used to skip a parameter position, which is 

281 
then not renamed. Renaming deletes the syntax of a parameter unless 

282 
a new mixfix annotation is given. 

283 

284 
Parameter renamings are morphisms between locales. These can be 

285 
lifted to terms and theorems and thus be applied to assumptions and 

286 
conclusions. The assumption of a merge is the conjunction of the 

287 
assumptions of the merged locale. The conclusions of a merge are 

288 
obtained by appending the conclusions of the left locale and of the 

289 
right locale. *} 

290 

291 
text {* The locale @{text order_preserving} contains theorems for both 

292 
orders @{text \<sqsubseteq>} and @{text \<preceq>}. How can one refer to a theorem for 

293 
a particular order, @{text \<sqsubseteq>} or @{text \<preceq>}? Names in locales are 

294 
qualified by the locale parameters. More precisely, a name is 

295 
qualified by the parameters of the locale in which its declaration 

296 
occurs. Here are examples: *} 

297 

298 
context %invisible order_preserving begin 

299 

300 
text {* 

301 
@{thm [source] le.less_le_trans}: @{thm le.less_le_trans} 

302 

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

303 
@{thm [source] hom_le}: @{thm hom_le} 
27063  304 
*} 
305 

306 
text {* When renaming a locale, the morphism is also applied 

307 
to the qualifiers. Hence theorems for the partial order @{text \<preceq>} 

308 
are qualified by @{text le'}. For example, @{thm [source] 

309 
le'.less_le_trans}: @{thm [display, indent=2] le'.less_le_trans} *} 

310 

311 
end %invisible 

312 

313 
text {* This example reveals that there is no infix syntax for the strict 

314 
version of @{text \<preceq>}! This can, of course, not be introduced 

315 
automatically, but it can be declared manually through an abbreviation. 

316 
*} 

317 

318 
abbreviation (in order_preserving) 

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

320 

321 
text {* Now the theorem is displayed nicely as 

322 
@{thm [locale=order_preserving] le'.less_le_trans}. *} 

323 

324 
text {* Not only names of theorems are qualified. In fact, all names 

325 
are qualified, in particular names introduced by definitions and 

326 
abbreviations. The name of the strict order of @{text \<sqsubseteq>} is @{text 

327 
le.less} and therefore @{text le'.less} is the name of the strict 

328 
order of @{text \<preceq>}. Hence, the equation in the above abbreviation 

329 
could have been written as @{text "less' \<equiv> le'.less"}. *} 

330 

331 
text {* Two more locales illustrate working with locale expressions. 

332 
A map @{text \<phi>} is a lattice homomorphism if it preserves meet and join. *} 

333 

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

334 
locale lattice_hom = le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) + 
27063  335 
fixes \<phi> 
336 
assumes hom_meet: 

337 
"\<phi> (lattice.meet le x y) = lattice.meet le' (\<phi> x) (\<phi> y)" 

338 
and hom_join: 

339 
"\<phi> (lattice.join le x y) = lattice.join le' (\<phi> x) (\<phi> y)" 

340 

341 
abbreviation (in lattice_hom) 

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

343 
abbreviation (in lattice_hom) 

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

345 

346 
text {* A homomorphism is an endomorphism if both orders coincide. *} 

347 

348 
locale lattice_end = 

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

349 
lattice_hom le le for le (infixl "\<sqsubseteq>" 50) 
27063  350 

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

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

353 
interpretation which is introduced below. Renamings are 

354 
indicated by $\sqsubseteq \mapsto \preceq$ etc. The expression 

355 
imported by @{text lattice_end} identifies the first and second 

356 
parameter of @{text lattice_hom}. By looking at the inheritance diagram it would seem 

357 
that two identical copies of each of the locales @{text 

358 
partial_order} and @{text lattice} are imported. This is not the 

359 
case! Inheritance paths with identical morphisms are detected and 

27503  360 
the conclusions of the respective locales appear only once. 
27063  361 

362 
\begin{figure} 

363 
\hrule \vspace{2ex} 

364 
\begin{center} 

365 
\begin{tikzpicture} 

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

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

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

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

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

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

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

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

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

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

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

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

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

379 
\draw (o)  (l); 

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

381 
\draw (lh)  (le); 

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

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

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

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

386 
\end{tikzpicture} 

387 
\end{center} 

388 
\hrule 

389 
\caption{Hierarchy of Homomorphism Locales.} 

390 
\label{fig:hom} 

391 
\end{figure} 

392 
*} 

393 

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

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

396 
interpretation is used to assert this. *} 

397 

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

398 
sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales 
27063  399 
fix x y 
400 
assume "x \<sqsubseteq> y" 

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

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

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

404 
qed 

405 

406 
text {* Theorems and other declarations  syntax, in particular  

407 
from the locale @{text order_preserving} are now active in @{text 

408 
lattice_hom}, for example 

409 

410 
@{thm [locale=lattice_hom, source] le'.less_le_trans}: 

411 
@{thm [locale=lattice_hom] le'.less_le_trans} 

412 
*} 

413 

414 

415 

416 
section {* Further Reading *} 

417 

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

419 
available. For the locale hierarchy of import and interpretation 

420 
dependencies see \cite{Ballarin2006a}; interpretations in theories 

421 
and proofs are covered in \cite{Ballarin2006b}. In the latter, we 

422 
show how interpretation in proofs enables to reason about families 

423 
of algebraic structures, which cannot be expressed with locales 

424 
directly. 

425 

426 
Haftmann and Wenzel \cite{HaftmannWenzel2007} overcome a restriction 

427 
of axiomatic type classes through a combination with locale 

428 
interpretation. The result is a Haskellstyle class system with a 

429 
facility to generate Haskell code. Classes are sufficient for 

430 
simple specifications with a single type parameter. The locales for 

431 
orders and lattices presented in this tutorial fall into this 

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

433 
on the other hand, do not. 

434 

435 
The original work of Kamm\"uller on locales \cite{KammullerEtAl1999} 

436 
may be of interest from a historical perspective. The mathematical 

437 
background on orders and lattices is taken from Jacobson's textbook 

438 
on algebra \cite[Chapter~8]{Jacobson1985}. 

439 
*} 

440 

441 
text {* 

442 
\begin{table} 

443 
\hrule 

444 
\vspace{2ex} 

445 
\begin{center} 

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

447 
\multicolumn{3}{l}{Miscellaneous} \\ 

448 

449 
\textit{attrname} & ::= 

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

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

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

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

453 
& \textit{name} [``\textbf{!}''] \\[2ex] 
27063  454 

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

456 

457 
\textit{fixes} & ::= 

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

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

460 
\textit{mixfix} ] \\ 

461 
\begin{comment} 

462 
\textit{constrains} & ::= 

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

464 
\end{comment} 

465 
\textit{assumes} & ::= 

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

467 
\begin{comment} 

468 
\textit{defines} & ::= 

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

470 
\textit{notes} & ::= 

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

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

473 
\end{comment} 

474 

475 
\textit{element} & ::= 

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

477 
\begin{comment} 

478 
&  

479 
& \textbf{constrains} \textit{constrains} 

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

481 
\end{comment} 

482 
&  

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

484 
%\begin{comment} 

485 
% &  

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

487 
% &  

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

489 
%\end{comment} 

490 

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

492 

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

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

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

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

496 
& \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

497 
( \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

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

499 
& [ \textit{qualifier} \textbf{:} ] 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

500 
\textit{qualifiedname} ( \textit{posinsts} $$ \textit{namedinst} ) \\ 
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27595
diff
changeset

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

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

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

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

506 

507 
\textit{locale} & ::= 

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

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

509 
&  & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ 
27063  510 
\textit{toplevel} & ::= 
511 
& \textbf{locale} \textit{name} [ ``\textbf{=}'' 

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

513 

514 
\multicolumn{3}{l}{Interpretation} \\ 

515 

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

517 
\textit{prop} \\ 

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

518 
\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

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

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

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

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

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

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

528 
\textit{expression} \textit{proof} \\[2ex] 
27063  529 

530 
\multicolumn{3}{l}{Diagnostics} \\ 

531 

532 
\textit{toplevel} & ::= 

533 
& \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ 

534 
&  & \textbf{print\_locales} 

535 
\end{tabular} 

536 
\end{center} 

537 
\hrule 

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

538 
\caption{Syntax of Locale Commands (abrigded).} 
27063  539 
\label{tab:commands} 
540 
\end{table} 

541 
*} 

542 

543 
text {* \textbf{Acknowledgements.} Alexander Krauss, Tobias Nipkow, 

544 
Christian Sternagel and Makarius Wenzel have made useful comments on 

545 
a draft of this document. *} 

546 

547 
end 