author | haftmann |
Wed, 05 Dec 2007 14:15:39 +0100 | |
changeset 25533 | 0140cc7b26ad |
parent 25369 | 5200374fda5d |
child 25868 | 97c6787099bc |
permissions | -rw-r--r-- |
20946 | 1 |
(* $Id$ *) |
2 |
||
22317 | 3 |
(*<*) |
20946 | 4 |
theory Classes |
24991 | 5 |
imports Main Code_Integer |
20946 | 6 |
begin |
7 |
||
22317 | 8 |
ML {* |
24628 | 9 |
CodeTarget.code_width := 74; |
22317 | 10 |
*} |
11 |
||
20946 | 12 |
syntax |
13 |
"_alpha" :: "type" ("\<alpha>") |
|
22479 | 14 |
"_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000) |
25533 | 15 |
"_beta" :: "type" ("\<beta>") |
16 |
"_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000) |
|
20946 | 17 |
|
18 |
parse_ast_translation {* |
|
19 |
let |
|
20 |
fun alpha_ast_tr [] = Syntax.Variable "'a" |
|
21 |
| alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
|
22 |
fun alpha_ofsort_ast_tr [ast] = |
|
23 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast] |
|
24 |
| alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); |
|
25533 | 25 |
fun beta_ast_tr [] = Syntax.Variable "'b" |
26 |
| beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
|
27 |
fun beta_ofsort_ast_tr [ast] = |
|
28 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast] |
|
29 |
| beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); |
|
20946 | 30 |
in [ |
25533 | 31 |
("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr), |
32 |
("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr) |
|
20946 | 33 |
] end |
34 |
*} |
|
35 |
(*>*) |
|
36 |
||
37 |
||
38 |
chapter {* Haskell-style classes with Isabelle/Isar *} |
|
39 |
||
40 |
section {* Introduction *} |
|
41 |
||
42 |
text {* |
|
22317 | 43 |
Type classes were introduces by Wadler and Blott \cite{wadler89how} |
44 |
into the Haskell language, to allow for a reasonable implementation |
|
45 |
of overloading\footnote{throughout this tutorial, we are referring |
|
46 |
to classical Haskell 1.0 type classes, not considering |
|
47 |
later additions in expressiveness}. |
|
48 |
As a canonical example, a polymorphic equality function |
|
49 |
@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different |
|
22550 | 50 |
types for @{text "\<alpha>"}, which is achieved by splitting introduction |
22317 | 51 |
of the @{text eq} function from its overloaded definitions by means |
52 |
of @{text class} and @{text instance} declarations: |
|
53 |
||
54 |
\medskip\noindent\hspace*{2ex}@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\ |
|
55 |
\hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} |
|
20946 | 56 |
|
22317 | 57 |
\medskip\noindent\hspace*{2ex}@{text "instance nat \<Colon> eq where"} \\ |
58 |
\hspace*{4ex}@{text "eq 0 0 = True"} \\ |
|
59 |
\hspace*{4ex}@{text "eq 0 _ = False"} \\ |
|
60 |
\hspace*{4ex}@{text "eq _ 0 = False"} \\ |
|
61 |
\hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"} |
|
62 |
||
63 |
\medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\ |
|
22550 | 64 |
\hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"} |
20946 | 65 |
|
22317 | 66 |
\medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\ |
67 |
\hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\ |
|
68 |
\hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} |
|
69 |
||
22550 | 70 |
\medskip\noindent Type variables are annotated with (finitly many) classes; |
22317 | 71 |
these annotations are assertions that a particular polymorphic type |
72 |
provides definitions for overloaded functions. |
|
73 |
||
74 |
Indeed, type classes not only allow for simple overloading |
|
75 |
but form a generic calculus, an instance of order-sorted |
|
23956 | 76 |
algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}. |
20946 | 77 |
|
22317 | 78 |
From a software enigineering point of view, type classes |
79 |
correspond to interfaces in object-oriented languages like Java; |
|
80 |
so, it is naturally desirable that type classes do not only |
|
24991 | 81 |
provide functions (class parameters) but also state specifications |
22317 | 82 |
implementations must obey. For example, the @{text "class eq"} |
22550 | 83 |
above could be given the following specification, demanding that |
84 |
@{text "class eq"} is an equivalence relation obeying reflexivity, |
|
85 |
symmetry and transitivity: |
|
22317 | 86 |
|
87 |
\medskip\noindent\hspace*{2ex}@{text "class eq where"} \\ |
|
88 |
\hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\ |
|
89 |
\hspace*{2ex}@{text "satisfying"} \\ |
|
90 |
\hspace*{4ex}@{text "refl: eq x x"} \\ |
|
91 |
\hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\ |
|
92 |
\hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"} |
|
93 |
||
22550 | 94 |
\medskip\noindent From a theoretic point of view, type classes are leightweight |
22347 | 95 |
modules; Haskell type classes may be emulated by |
22317 | 96 |
SML functors \cite{classes_modules}. |
97 |
Isabelle/Isar offers a discipline of type classes which brings |
|
98 |
all those aspects together: |
|
99 |
||
100 |
\begin{enumerate} |
|
24991 | 101 |
\item specifying abstract parameters together with |
22317 | 102 |
corresponding specifications, |
24991 | 103 |
\item instantating those abstract parameters by a particular |
22317 | 104 |
type |
105 |
\item in connection with a ``less ad-hoc'' approach to overloading, |
|
23956 | 106 |
\item with a direct link to the Isabelle module system |
107 |
(aka locales \cite{kammueller-locales}). |
|
22317 | 108 |
\end{enumerate} |
109 |
||
22550 | 110 |
\noindent Isar type classes also directly support code generation |
111 |
in a Haskell like fashion. |
|
22317 | 112 |
|
113 |
This tutorial demonstrates common elements of structured specifications |
|
114 |
and abstract reasoning with type classes by the algebraic hierarchy of |
|
20946 | 115 |
semigroups, monoids and groups. Our background theory is that of |
23956 | 116 |
Isabelle/HOL \cite{isa-tutorial}, for which some |
22317 | 117 |
familiarity is assumed. |
20946 | 118 |
|
22317 | 119 |
Here we merely present the look-and-feel for end users. |
20946 | 120 |
Internally, those are mapped to more primitive Isabelle concepts. |
23956 | 121 |
See \cite{Haftmann-Wenzel:2006:classes} for more detail. |
20946 | 122 |
*} |
123 |
||
22317 | 124 |
section {* A simple algebra example \label{sec:example} *} |
20946 | 125 |
|
126 |
subsection {* Class definition *} |
|
127 |
||
128 |
text {* |
|
129 |
Depending on an arbitrary type @{text "\<alpha>"}, class @{text |
|
24991 | 130 |
"semigroup"} introduces a binary operator @{text "\<otimes>"} that is |
20946 | 131 |
assumed to be associative: |
132 |
*} |
|
133 |
||
22473 | 134 |
class semigroup = type + |
25200 | 135 |
fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70) |
136 |
assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
|
20946 | 137 |
|
138 |
text {* |
|
139 |
\noindent This @{text "\<CLASS>"} specification consists of two |
|
24991 | 140 |
parts: the \qn{operational} part names the class parameter (@{text |
20946 | 141 |
"\<FIXES>"}), the \qn{logical} part specifies properties on them |
142 |
(@{text "\<ASSUMES>"}). The local @{text "\<FIXES>"} and @{text |
|
143 |
"\<ASSUMES>"} are lifted to the theory toplevel, yielding the global |
|
24991 | 144 |
parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the |
20946 | 145 |
global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y |
22479 | 146 |
z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}. |
20946 | 147 |
*} |
148 |
||
149 |
||
150 |
subsection {* Class instantiation \label{sec:class_inst} *} |
|
151 |
||
152 |
text {* |
|
153 |
The concrete type @{text "int"} is made a @{text "semigroup"} |
|
24991 | 154 |
instance by providing a suitable definition for the class parameter |
20946 | 155 |
@{text "mult"} and a proof for the specification of @{text "assoc"}. |
25533 | 156 |
This is accomplished by the @{text "\<INSTANTIATION>"} target: |
20946 | 157 |
*} |
158 |
||
25533 | 159 |
instantiation int :: semigroup |
160 |
begin |
|
161 |
||
162 |
definition |
|
163 |
mult_int_def: "i \<otimes> j = i + (j\<Colon>int)" |
|
164 |
||
165 |
instance proof |
|
22317 | 166 |
fix i j k :: int have "(i + j) + k = i + (j + k)" by simp |
25247 | 167 |
then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" |
168 |
unfolding mult_int_def . |
|
20946 | 169 |
qed |
170 |
||
25533 | 171 |
end |
172 |
||
20946 | 173 |
text {* |
25533 | 174 |
\noindent @{text "\<INSTANTIATION>"} allows to define class parameters |
175 |
at a particular instance using common specification tools (here, |
|
176 |
@{text "\<DEFINITION>"}). The concluding @{text "\<INSTANCE>"} |
|
177 |
opens a proof that the given parameters actually conform |
|
178 |
to the class specification. Note that the first proof step |
|
179 |
is the @{text default} method, |
|
180 |
which for such instance proofs maps to the @{text intro_classes} method. |
|
181 |
This boils down an instance judgement to the relevant primitive |
|
22317 | 182 |
proof goals and should conveniently always be the first method applied |
183 |
in an instantiation proof. |
|
184 |
||
25533 | 185 |
From now on, the type-checker will consider @{text "int"} |
186 |
as a @{text "semigroup"} automatically, i.e.\ any general results |
|
187 |
are immediately available on concrete instances. |
|
22550 | 188 |
\medskip Another instance of @{text "semigroup"} are the natural numbers: |
20946 | 189 |
*} |
190 |
||
25533 | 191 |
instantiation nat :: semigroup |
192 |
begin |
|
193 |
||
194 |
definition |
|
195 |
mult_nat_def: "m \<otimes> n = m + (n\<Colon>nat)" |
|
196 |
||
197 |
instance proof |
|
20946 | 198 |
fix m n q :: nat |
25247 | 199 |
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" |
200 |
unfolding mult_nat_def by simp |
|
20946 | 201 |
qed |
202 |
||
25533 | 203 |
end |
20946 | 204 |
|
25247 | 205 |
subsection {* Lifting and parametric types *} |
206 |
||
207 |
text {* |
|
208 |
Overloaded definitions giving on class instantiation |
|
209 |
may include recursion over the syntactic structure of types. |
|
210 |
As a canonical example, we model product semigroups |
|
211 |
using our simple algebra: |
|
212 |
*} |
|
213 |
||
25533 | 214 |
instantiation * :: (semigroup, semigroup) semigroup |
215 |
begin |
|
216 |
||
217 |
definition |
|
218 |
mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)" |
|
219 |
||
220 |
instance proof |
|
221 |
fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup" |
|
25247 | 222 |
show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)" |
223 |
unfolding mult_prod_def by (simp add: assoc) |
|
224 |
qed |
|
225 |
||
25533 | 226 |
end |
227 |
||
25247 | 228 |
text {* |
229 |
\noindent Associativity from product semigroups is |
|
230 |
established using |
|
231 |
the definition of @{text \<otimes>} on products and the hypothetical |
|
232 |
associativety of the type components; these hypothesis |
|
233 |
are facts due to the @{text semigroup} constraints imposed |
|
234 |
on the type components by the @{text instance} proposition. |
|
235 |
Indeed, this pattern often occurs with parametric types |
|
236 |
and type classes. |
|
237 |
*} |
|
238 |
||
239 |
||
240 |
subsection {* Subclassing *} |
|
20946 | 241 |
|
242 |
text {* |
|
22317 | 243 |
We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral) |
20946 | 244 |
by extending @{text "semigroup"} |
24991 | 245 |
with one additional parameter @{text "neutral"} together |
20946 | 246 |
with its property: |
247 |
*} |
|
248 |
||
249 |
class monoidl = semigroup + |
|
25200 | 250 |
fixes neutral :: "\<alpha>" ("\<one>") |
251 |
assumes neutl: "\<one> \<otimes> x = x" |
|
20946 | 252 |
|
253 |
text {* |
|
25247 | 254 |
\noindent Again, we prove some instances, by |
24991 | 255 |
providing suitable parameter definitions and proofs for the |
25533 | 256 |
additional specifications. Obverve that instantiations |
257 |
for types with the same arity may be simultaneous: |
|
20946 | 258 |
*} |
259 |
||
25533 | 260 |
instantiation nat and int :: monoidl |
261 |
begin |
|
262 |
||
263 |
definition |
|
264 |
neutral_nat_def: "\<one> = (0\<Colon>nat)" |
|
265 |
||
266 |
definition |
|
267 |
neutral_int_def: "\<one> = (0\<Colon>int)" |
|
268 |
||
269 |
instance proof |
|
20946 | 270 |
fix n :: nat |
25247 | 271 |
show "\<one> \<otimes> n = n" |
272 |
unfolding neutral_nat_def mult_nat_def by simp |
|
25533 | 273 |
next |
20946 | 274 |
fix k :: int |
25247 | 275 |
show "\<one> \<otimes> k = k" |
276 |
unfolding neutral_int_def mult_int_def by simp |
|
20946 | 277 |
qed |
278 |
||
25533 | 279 |
end |
280 |
||
281 |
instantiation * :: (monoidl, monoidl) monoidl |
|
282 |
begin |
|
283 |
||
284 |
definition |
|
285 |
neutral_prod_def: "\<one> = (\<one>, \<one>)" |
|
286 |
||
287 |
instance proof |
|
288 |
fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl" |
|
25247 | 289 |
show "\<one> \<otimes> p = p" |
290 |
unfolding neutral_prod_def mult_prod_def by (simp add: neutl) |
|
291 |
qed |
|
20946 | 292 |
|
25533 | 293 |
end |
294 |
||
20946 | 295 |
text {* |
22317 | 296 |
\noindent Fully-fledged monoids are modelled by another subclass |
24991 | 297 |
which does not add new parameters but tightens the specification: |
20946 | 298 |
*} |
299 |
||
300 |
class monoid = monoidl + |
|
25200 | 301 |
assumes neutr: "x \<otimes> \<one> = x" |
20946 | 302 |
|
25533 | 303 |
instantiation nat and int :: monoid |
304 |
begin |
|
305 |
||
306 |
instance proof |
|
20946 | 307 |
fix n :: nat |
25247 | 308 |
show "n \<otimes> \<one> = n" |
309 |
unfolding neutral_nat_def mult_nat_def by simp |
|
25533 | 310 |
next |
20946 | 311 |
fix k :: int |
25247 | 312 |
show "k \<otimes> \<one> = k" |
313 |
unfolding neutral_int_def mult_int_def by simp |
|
314 |
qed |
|
315 |
||
25533 | 316 |
end |
317 |
||
318 |
instantiation * :: (monoid, monoid) monoid |
|
319 |
begin |
|
320 |
||
321 |
instance proof |
|
322 |
fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid" |
|
25247 | 323 |
show "p \<otimes> \<one> = p" |
324 |
unfolding neutral_prod_def mult_prod_def by (simp add: neutr) |
|
22317 | 325 |
qed |
326 |
||
25533 | 327 |
end |
328 |
||
22317 | 329 |
text {* |
330 |
\noindent To finish our small algebra example, we add a @{text "group"} class |
|
331 |
with a corresponding instance: |
|
332 |
*} |
|
20946 | 333 |
|
334 |
class group = monoidl + |
|
25200 | 335 |
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999) |
336 |
assumes invl: "x\<div> \<otimes> x = \<one>" |
|
20946 | 337 |
|
25533 | 338 |
instantiation int :: group |
339 |
begin |
|
340 |
||
341 |
definition |
|
342 |
inverse_int_def: "i\<div> = - (i\<Colon>int)" |
|
343 |
||
344 |
instance proof |
|
20946 | 345 |
fix i :: int |
346 |
have "-i + i = 0" by simp |
|
22550 | 347 |
then show "i\<div> \<otimes> i = \<one>" |
25247 | 348 |
unfolding mult_int_def neutral_int_def inverse_int_def . |
20946 | 349 |
qed |
350 |
||
25533 | 351 |
end |
352 |
||
22317 | 353 |
section {* Type classes as locales *} |
354 |
||
355 |
subsection {* A look behind the scene *} |
|
356 |
||
22347 | 357 |
text {* |
358 |
The example above gives an impression how Isar type classes work |
|
359 |
in practice. As stated in the introduction, classes also provide |
|
360 |
a link to Isar's locale system. Indeed, the logical core of a class |
|
361 |
is nothing else than a locale: |
|
362 |
*} |
|
363 |
||
22473 | 364 |
class idem = type + |
22347 | 365 |
fixes f :: "\<alpha> \<Rightarrow> \<alpha>" |
366 |
assumes idem: "f (f x) = f x" |
|
22317 | 367 |
|
368 |
text {* |
|
22347 | 369 |
\noindent essentially introduces the locale |
370 |
*} |
|
371 |
(*<*) setup {* Sign.add_path "foo" *} (*>*) |
|
372 |
locale idem = |
|
373 |
fixes f :: "\<alpha> \<Rightarrow> \<alpha>" |
|
374 |
assumes idem: "f (f x) = f x" |
|
375 |
||
22550 | 376 |
text {* \noindent together with corresponding constant(s): *} |
22347 | 377 |
|
378 |
consts f :: "\<alpha> \<Rightarrow> \<alpha>" |
|
379 |
||
22550 | 380 |
text {* |
381 |
\noindent The connection to the type system is done by means |
|
382 |
of a primitive axclass |
|
383 |
*} |
|
384 |
||
22347 | 385 |
axclass idem < type |
386 |
idem: "f (f x) = f x" |
|
387 |
||
22550 | 388 |
text {* \noindent together with a corresponding interpretation: *} |
22347 | 389 |
|
390 |
interpretation idem_class: |
|
25533 | 391 |
idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"] |
22347 | 392 |
by unfold_locales (rule idem) |
393 |
(*<*) setup {* Sign.parent_path *} (*>*) |
|
394 |
text {* |
|
395 |
This give you at hand the full power of the Isabelle module system; |
|
396 |
conclusions in locale @{text idem} are implicitly propagated |
|
22479 | 397 |
to class @{text idem}. |
22317 | 398 |
*} |
20946 | 399 |
|
400 |
subsection {* Abstract reasoning *} |
|
401 |
||
402 |
text {* |
|
22347 | 403 |
Isabelle locales enable reasoning at a general level, while results |
20946 | 404 |
are implicitly transferred to all instances. For example, we can |
405 |
now establish the @{text "left_cancel"} lemma for groups, which |
|
25247 | 406 |
states that the function @{text "(x \<otimes>)"} is injective: |
20946 | 407 |
*} |
408 |
||
25200 | 409 |
lemma (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z" |
20946 | 410 |
proof |
25247 | 411 |
assume "x \<otimes> y = x \<otimes> z" |
25200 | 412 |
then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp |
413 |
then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp |
|
22347 | 414 |
then show "y = z" using neutl and invl by simp |
20946 | 415 |
next |
25247 | 416 |
assume "y = z" |
25200 | 417 |
then show "x \<otimes> y = x \<otimes> z" by simp |
20946 | 418 |
qed |
419 |
||
420 |
text {* |
|
421 |
\noindent Here the \qt{@{text "\<IN> group"}} target specification |
|
422 |
indicates that the result is recorded within that context for later |
|
423 |
use. This local theorem is also lifted to the global one @{text |
|
22479 | 424 |
"group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> |
20946 | 425 |
z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of |
426 |
@{text "group"} before, we may refer to that fact as well: @{prop |
|
22479 | 427 |
[source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. |
20946 | 428 |
*} |
429 |
||
430 |
||
23956 | 431 |
subsection {* Derived definitions *} |
432 |
||
433 |
text {* |
|
434 |
Isabelle locales support a concept of local definitions |
|
435 |
in locales: |
|
436 |
*} |
|
437 |
||
438 |
fun (in monoid) |
|
439 |
pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where |
|
25200 | 440 |
"pow_nat 0 x = \<one>" |
441 |
| "pow_nat (Suc n) x = x \<otimes> pow_nat n x" |
|
20946 | 442 |
|
443 |
text {* |
|
23956 | 444 |
\noindent If the locale @{text group} is also a class, this local |
445 |
definition is propagated onto a global definition of |
|
446 |
@{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} |
|
447 |
with corresponding theorems |
|
448 |
||
449 |
@{thm pow_nat.simps [no_vars]}. |
|
20946 | 450 |
|
23956 | 451 |
\noindent As you can see from this example, for local |
452 |
definitions you may use any specification tool |
|
453 |
which works together with locales (e.g. \cite{krauss2006}). |
|
454 |
*} |
|
455 |
||
456 |
||
25247 | 457 |
subsection {* A functor analogy *} |
458 |
||
459 |
text {* |
|
460 |
We introduced Isar classes by analogy to type classes |
|
461 |
functional programming; if we reconsider this in the |
|
462 |
context of what has been said about type classes and locales, |
|
463 |
we can drive this analogy further by stating that type |
|
464 |
classes essentially correspond to functors which have |
|
465 |
a canonical interpretation as type classes. |
|
466 |
Anyway, there is also the possibility of other interpretations. |
|
467 |
For example, also @{text "list"}s form a monoid with |
|
25369
5200374fda5d
replaced @{const} (allows name only) by proper @{term};
wenzelm
parents:
25247
diff
changeset
|
468 |
@{term "op @"} and @{term "[]"} as operations, but it |
25247 | 469 |
seems inappropriate to apply to lists |
470 |
the same operations as for genuinly algebraic types. |
|
471 |
In such a case, we simply can do a particular interpretation |
|
472 |
of monoids for lists: |
|
473 |
*} |
|
474 |
||
475 |
interpretation list_monoid: monoid ["op @" "[]"] |
|
476 |
by unfold_locales auto |
|
477 |
||
478 |
text {* |
|
479 |
\noindent This enables us to apply facts on monoids |
|
480 |
to lists, e.g. @{thm list_monoid.neutl [no_vars]}. |
|
481 |
||
482 |
When using this interpretation pattern, it may also |
|
483 |
be appropriate to map derived definitions accordingly: |
|
484 |
*} |
|
485 |
||
486 |
fun |
|
25533 | 487 |
replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" |
25247 | 488 |
where |
489 |
"replicate 0 _ = []" |
|
490 |
| "replicate (Suc n) xs = xs @ replicate n xs" |
|
491 |
||
492 |
interpretation list_monoid: monoid ["op @" "[]"] where |
|
493 |
"monoid.pow_nat (op @) [] = replicate" |
|
494 |
proof |
|
495 |
fix n :: nat |
|
496 |
show "monoid.pow_nat (op @) [] n = replicate n" |
|
497 |
by (induct n) auto |
|
498 |
qed |
|
499 |
||
500 |
||
24991 | 501 |
subsection {* Additional subclass relations *} |
22347 | 502 |
|
503 |
text {* |
|
504 |
Any @{text "group"} is also a @{text "monoid"}; this |
|
25247 | 505 |
can be made explicit by claiming an additional |
506 |
subclass relation, |
|
22347 | 507 |
together with a proof of the logical difference: |
508 |
*} |
|
509 |
||
24991 | 510 |
subclass (in group) monoid |
23956 | 511 |
proof unfold_locales |
22347 | 512 |
fix x |
25200 | 513 |
from invl have "x\<div> \<otimes> x = \<one>" by simp |
514 |
with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp |
|
515 |
with left_cancel show "x \<otimes> \<one> = x" by simp |
|
23956 | 516 |
qed |
517 |
||
518 |
text {* |
|
25200 | 519 |
\noindent The logical proof is carried out on the locale level |
23956 | 520 |
and thus conveniently is opened using the @{text unfold_locales} |
521 |
method which only leaves the logical differences still |
|
25200 | 522 |
open to proof to the user. Afterwards it is propagated |
23956 | 523 |
to the type system, making @{text group} an instance of |
25247 | 524 |
@{text monoid} by adding an additional edge |
525 |
to the graph of subclass relations |
|
526 |
(cf.\ \figref{fig:subclass}). |
|
527 |
||
528 |
\begin{figure}[htbp] |
|
529 |
\begin{center} |
|
530 |
\small |
|
531 |
\unitlength 0.6mm |
|
532 |
\begin{picture}(40,60)(0,0) |
|
533 |
\put(20,60){\makebox(0,0){@{text semigroup}}} |
|
534 |
\put(20,40){\makebox(0,0){@{text monoidl}}} |
|
535 |
\put(00,20){\makebox(0,0){@{text monoid}}} |
|
536 |
\put(40,00){\makebox(0,0){@{text group}}} |
|
537 |
\put(20,55){\vector(0,-1){10}} |
|
538 |
\put(15,35){\vector(-1,-1){10}} |
|
539 |
\put(25,35){\vector(1,-3){10}} |
|
540 |
\end{picture} |
|
541 |
\hspace{8em} |
|
542 |
\begin{picture}(40,60)(0,0) |
|
543 |
\put(20,60){\makebox(0,0){@{text semigroup}}} |
|
544 |
\put(20,40){\makebox(0,0){@{text monoidl}}} |
|
545 |
\put(00,20){\makebox(0,0){@{text monoid}}} |
|
546 |
\put(40,00){\makebox(0,0){@{text group}}} |
|
547 |
\put(20,55){\vector(0,-1){10}} |
|
548 |
\put(15,35){\vector(-1,-1){10}} |
|
549 |
\put(05,15){\vector(3,-1){30}} |
|
550 |
\end{picture} |
|
551 |
\caption{Subclass relationship of monoids and groups: |
|
552 |
before and after establishing the relationship |
|
553 |
@{text "group \<subseteq> monoid"}; transitive edges left out.} |
|
554 |
\label{fig:subclass} |
|
555 |
\end{center} |
|
556 |
\end{figure} |
|
557 |
||
558 |
For illustration, a derived definition |
|
24991 | 559 |
in @{text group} which uses @{text pow_nat}: |
23956 | 560 |
*} |
561 |
||
562 |
definition (in group) |
|
563 |
pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where |
|
564 |
"pow_int k x = (if k >= 0 |
|
565 |
then pow_nat (nat k) x |
|
25200 | 566 |
else (pow_nat (nat (- k)) x)\<div>)" |
23956 | 567 |
|
568 |
text {* |
|
25247 | 569 |
\noindent yields the global definition of |
23956 | 570 |
@{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} |
571 |
with the corresponding theorem @{thm pow_int_def [no_vars]}. |
|
24991 | 572 |
*} |
23956 | 573 |
|
22347 | 574 |
|
25247 | 575 |
section {* Type classes and code generation *} |
22317 | 576 |
|
577 |
text {* |
|
578 |
Turning back to the first motivation for type classes, |
|
579 |
namely overloading, it is obvious that overloading |
|
25533 | 580 |
stemming from @{text "\<CLASS>"} statements and |
581 |
@{text "\<INSTANTIATION>"} |
|
582 |
targets naturally maps to Haskell type classes. |
|
22317 | 583 |
The code generator framework \cite{isabelle-codegen} |
584 |
takes this into account. Concerning target languages |
|
585 |
lacking type classes (e.g.~SML), type classes |
|
586 |
are implemented by explicit dictionary construction. |
|
23956 | 587 |
For example, lets go back to the power function: |
22317 | 588 |
*} |
589 |
||
590 |
definition |
|
591 |
example :: int where |
|
592 |
"example = pow_int 10 (-2)" |
|
593 |
||
594 |
text {* |
|
595 |
\noindent This maps to Haskell as: |
|
596 |
*} |
|
597 |
||
24628 | 598 |
export_code example in Haskell module_name Classes file "code_examples/" |
22317 | 599 |
(* NOTE: you may use Haskell only once in this document, otherwise |
600 |
you have to work in distinct subdirectories *) |
|
601 |
||
602 |
text {* |
|
603 |
\lsthaskell{Thy/code_examples/Classes.hs} |
|
604 |
||
605 |
\noindent The whole code in SML with explicit dictionary passing: |
|
606 |
*} |
|
607 |
||
24628 | 608 |
export_code example (*<*)in SML module_name Classes(*>*)in SML module_name Classes file "code_examples/classes.ML" |
22317 | 609 |
|
610 |
text {* |
|
611 |
\lstsml{Thy/code_examples/classes.ML} |
|
612 |
*} |
|
613 |
||
614 |
||
615 |
(* subsection {* Different syntax for same specifications *} |
|
20946 | 616 |
|
617 |
text {* |
|
618 |
||
22479 | 619 |
subsection {* Syntactic classes *} |
22317 | 620 |
|
20946 | 621 |
*} *) |
622 |
||
623 |
end |