author  haftmann 
Fri, 23 May 2008 16:04:59 +0200  
changeset 26967  27f60aaa5a7b 
parent 25871  45753d56d935 
child 27065  f68aa7b5a0f3 
permissions  rwrr 
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 {* Haskellstyle 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 ordersorted 

23956  76 
algebra \cite{NipkowPrehofer:1993,nipkowsorts93,Wenzel:1997:TPHOL}. 
20946  77 

22317  78 
From a software enigineering point of view, type classes 
79 
correspond to interfaces in objectoriented 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 adhoc'' approach to overloading, 

23956  106 
\item with a direct link to the Isabelle module system 
107 
(aka locales \cite{kammuellerlocales}). 

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{isatutorial}, for which some 
22317  117 
familiarity is assumed. 
20946  118 

22317  119 
Here we merely present the lookandfeel for end users. 
20946  120 
Internally, those are mapped to more primitive Isabelle concepts. 
23956  121 
See \cite{HaftmannWenzel: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 typechecker 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 

25871  194 
primrec mult_nat where 
195 
"(0\<Colon>nat) \<otimes> n = n" 

196 
 "Suc m \<otimes> n = Suc (m \<otimes> n)" 

25533  197 

198 
instance proof 

20946  199 
fix m n q :: nat 
25247  200 
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" 
25871  201 
by (induct m) auto 
20946  202 
qed 
203 

25533  204 
end 
20946  205 

25871  206 
text {* 
207 
\noindent Note the occurence of the name @{text mult_nat} 

208 
in the primrec declaration; by default, the local name of 

209 
a class operation @{text f} to instantiate on type constructor 

210 
@{text \<kappa>} are mangled as @{text f_\<kappa>}. In case of uncertainty, 

211 
these names may be inspected using the @{text "\<PRINTCONTEXT>"} command 

212 
or the corresponding ProofGeneral button. 

213 
*} 

214 

25247  215 
subsection {* Lifting and parametric types *} 
216 

217 
text {* 

218 
Overloaded definitions giving on class instantiation 

219 
may include recursion over the syntactic structure of types. 

220 
As a canonical example, we model product semigroups 

221 
using our simple algebra: 

222 
*} 

223 

25533  224 
instantiation * :: (semigroup, semigroup) semigroup 
225 
begin 

226 

227 
definition 

228 
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)" 

229 

230 
instance proof 

231 
fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup" 

25247  232 
show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)" 
233 
unfolding mult_prod_def by (simp add: assoc) 

234 
qed 

235 

25533  236 
end 
237 

25247  238 
text {* 
239 
\noindent Associativity from product semigroups is 

240 
established using 

241 
the definition of @{text \<otimes>} on products and the hypothetical 

242 
associativety of the type components; these hypothesis 

243 
are facts due to the @{text semigroup} constraints imposed 

244 
on the type components by the @{text instance} proposition. 

245 
Indeed, this pattern often occurs with parametric types 

246 
and type classes. 

247 
*} 

248 

249 

250 
subsection {* Subclassing *} 

20946  251 

252 
text {* 

22317  253 
We define a subclass @{text "monoidl"} (a semigroup with a lefthand neutral) 
20946  254 
by extending @{text "semigroup"} 
24991  255 
with one additional parameter @{text "neutral"} together 
20946  256 
with its property: 
257 
*} 

258 

259 
class monoidl = semigroup + 

25200  260 
fixes neutral :: "\<alpha>" ("\<one>") 
261 
assumes neutl: "\<one> \<otimes> x = x" 

20946  262 

263 
text {* 

25247  264 
\noindent Again, we prove some instances, by 
24991  265 
providing suitable parameter definitions and proofs for the 
25533  266 
additional specifications. Obverve that instantiations 
267 
for types with the same arity may be simultaneous: 

20946  268 
*} 
269 

25533  270 
instantiation nat and int :: monoidl 
271 
begin 

272 

273 
definition 

274 
neutral_nat_def: "\<one> = (0\<Colon>nat)" 

275 

276 
definition 

277 
neutral_int_def: "\<one> = (0\<Colon>int)" 

278 

279 
instance proof 

20946  280 
fix n :: nat 
25247  281 
show "\<one> \<otimes> n = n" 
26967  282 
unfolding neutral_nat_def by simp 
25533  283 
next 
20946  284 
fix k :: int 
25247  285 
show "\<one> \<otimes> k = k" 
286 
unfolding neutral_int_def mult_int_def by simp 

20946  287 
qed 
288 

25533  289 
end 
290 

291 
instantiation * :: (monoidl, monoidl) monoidl 

292 
begin 

293 

294 
definition 

295 
neutral_prod_def: "\<one> = (\<one>, \<one>)" 

296 

297 
instance proof 

298 
fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl" 

25247  299 
show "\<one> \<otimes> p = p" 
300 
unfolding neutral_prod_def mult_prod_def by (simp add: neutl) 

301 
qed 

20946  302 

25533  303 
end 
304 

20946  305 
text {* 
22317  306 
\noindent Fullyfledged monoids are modelled by another subclass 
24991  307 
which does not add new parameters but tightens the specification: 
20946  308 
*} 
309 

310 
class monoid = monoidl + 

25200  311 
assumes neutr: "x \<otimes> \<one> = x" 
20946  312 

25533  313 
instantiation nat and int :: monoid 
314 
begin 

315 

316 
instance proof 

20946  317 
fix n :: nat 
25247  318 
show "n \<otimes> \<one> = n" 
25871  319 
unfolding neutral_nat_def by (induct n) simp_all 
25533  320 
next 
20946  321 
fix k :: int 
25247  322 
show "k \<otimes> \<one> = k" 
323 
unfolding neutral_int_def mult_int_def by simp 

324 
qed 

325 

25533  326 
end 
327 

328 
instantiation * :: (monoid, monoid) monoid 

329 
begin 

330 

331 
instance proof 

332 
fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid" 

25247  333 
show "p \<otimes> \<one> = p" 
334 
unfolding neutral_prod_def mult_prod_def by (simp add: neutr) 

22317  335 
qed 
336 

25533  337 
end 
338 

22317  339 
text {* 
340 
\noindent To finish our small algebra example, we add a @{text "group"} class 

341 
with a corresponding instance: 

342 
*} 

20946  343 

344 
class group = monoidl + 

25200  345 
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999) 
346 
assumes invl: "x\<div> \<otimes> x = \<one>" 

20946  347 

25533  348 
instantiation int :: group 
349 
begin 

350 

351 
definition 

352 
inverse_int_def: "i\<div> =  (i\<Colon>int)" 

353 

354 
instance proof 

20946  355 
fix i :: int 
356 
have "i + i = 0" by simp 

22550  357 
then show "i\<div> \<otimes> i = \<one>" 
25247  358 
unfolding mult_int_def neutral_int_def inverse_int_def . 
20946  359 
qed 
360 

25533  361 
end 
362 

22317  363 
section {* Type classes as locales *} 
364 

365 
subsection {* A look behind the scene *} 

366 

22347  367 
text {* 
368 
The example above gives an impression how Isar type classes work 

369 
in practice. As stated in the introduction, classes also provide 

370 
a link to Isar's locale system. Indeed, the logical core of a class 

371 
is nothing else than a locale: 

372 
*} 

373 

22473  374 
class idem = type + 
22347  375 
fixes f :: "\<alpha> \<Rightarrow> \<alpha>" 
376 
assumes idem: "f (f x) = f x" 

22317  377 

378 
text {* 

22347  379 
\noindent essentially introduces the locale 
380 
*} 

381 
(*<*) setup {* Sign.add_path "foo" *} (*>*) 

382 
locale idem = 

383 
fixes f :: "\<alpha> \<Rightarrow> \<alpha>" 

384 
assumes idem: "f (f x) = f x" 

385 

22550  386 
text {* \noindent together with corresponding constant(s): *} 
22347  387 

388 
consts f :: "\<alpha> \<Rightarrow> \<alpha>" 

389 

22550  390 
text {* 
391 
\noindent The connection to the type system is done by means 

392 
of a primitive axclass 

393 
*} 

394 

22347  395 
axclass idem < type 
396 
idem: "f (f x) = f x" 

397 

22550  398 
text {* \noindent together with a corresponding interpretation: *} 
22347  399 

400 
interpretation idem_class: 

25533  401 
idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"] 
22347  402 
by unfold_locales (rule idem) 
403 
(*<*) setup {* Sign.parent_path *} (*>*) 

404 
text {* 

405 
This give you at hand the full power of the Isabelle module system; 

406 
conclusions in locale @{text idem} are implicitly propagated 

22479  407 
to class @{text idem}. 
22317  408 
*} 
20946  409 

410 
subsection {* Abstract reasoning *} 

411 

412 
text {* 

22347  413 
Isabelle locales enable reasoning at a general level, while results 
20946  414 
are implicitly transferred to all instances. For example, we can 
415 
now establish the @{text "left_cancel"} lemma for groups, which 

25247  416 
states that the function @{text "(x \<otimes>)"} is injective: 
20946  417 
*} 
418 

25200  419 
lemma (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z" 
20946  420 
proof 
25247  421 
assume "x \<otimes> y = x \<otimes> z" 
25200  422 
then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp 
423 
then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp 

22347  424 
then show "y = z" using neutl and invl by simp 
20946  425 
next 
25247  426 
assume "y = z" 
25200  427 
then show "x \<otimes> y = x \<otimes> z" by simp 
20946  428 
qed 
429 

430 
text {* 

431 
\noindent Here the \qt{@{text "\<IN> group"}} target specification 

432 
indicates that the result is recorded within that context for later 

433 
use. This local theorem is also lifted to the global one @{text 

22479  434 
"group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> 
20946  435 
z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of 
436 
@{text "group"} before, we may refer to that fact as well: @{prop 

22479  437 
[source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. 
20946  438 
*} 
439 

440 

23956  441 
subsection {* Derived definitions *} 
442 

443 
text {* 

444 
Isabelle locales support a concept of local definitions 

445 
in locales: 

446 
*} 

447 

25871  448 
primrec (in monoid) 
23956  449 
pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where 
25200  450 
"pow_nat 0 x = \<one>" 
451 
 "pow_nat (Suc n) x = x \<otimes> pow_nat n x" 

20946  452 

453 
text {* 

23956  454 
\noindent If the locale @{text group} is also a class, this local 
455 
definition is propagated onto a global definition of 

456 
@{term [source] "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} 

457 
with corresponding theorems 

458 

459 
@{thm pow_nat.simps [no_vars]}. 

20946  460 

23956  461 
\noindent As you can see from this example, for local 
462 
definitions you may use any specification tool 

463 
which works together with locales (e.g. \cite{krauss2006}). 

464 
*} 

465 

466 

25247  467 
subsection {* A functor analogy *} 
468 

469 
text {* 

470 
We introduced Isar classes by analogy to type classes 

471 
functional programming; if we reconsider this in the 

472 
context of what has been said about type classes and locales, 

473 
we can drive this analogy further by stating that type 

474 
classes essentially correspond to functors which have 

475 
a canonical interpretation as type classes. 

476 
Anyway, there is also the possibility of other interpretations. 

477 
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

478 
@{term "op @"} and @{term "[]"} as operations, but it 
25247  479 
seems inappropriate to apply to lists 
480 
the same operations as for genuinly algebraic types. 

481 
In such a case, we simply can do a particular interpretation 

482 
of monoids for lists: 

483 
*} 

484 

485 
interpretation list_monoid: monoid ["op @" "[]"] 

486 
by unfold_locales auto 

487 

488 
text {* 

489 
\noindent This enables us to apply facts on monoids 

490 
to lists, e.g. @{thm list_monoid.neutl [no_vars]}. 

491 

492 
When using this interpretation pattern, it may also 

493 
be appropriate to map derived definitions accordingly: 

494 
*} 

495 

496 
fun 

25533  497 
replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" 
25247  498 
where 
499 
"replicate 0 _ = []" 

500 
 "replicate (Suc n) xs = xs @ replicate n xs" 

501 

502 
interpretation list_monoid: monoid ["op @" "[]"] where 

503 
"monoid.pow_nat (op @) [] = replicate" 

504 
proof 

505 
fix n :: nat 

506 
show "monoid.pow_nat (op @) [] n = replicate n" 

507 
by (induct n) auto 

508 
qed 

509 

510 

24991  511 
subsection {* Additional subclass relations *} 
22347  512 

513 
text {* 

514 
Any @{text "group"} is also a @{text "monoid"}; this 

25247  515 
can be made explicit by claiming an additional 
516 
subclass relation, 

22347  517 
together with a proof of the logical difference: 
518 
*} 

519 

24991  520 
subclass (in group) monoid 
23956  521 
proof unfold_locales 
22347  522 
fix x 
25200  523 
from invl have "x\<div> \<otimes> x = \<one>" by simp 
524 
with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp 

525 
with left_cancel show "x \<otimes> \<one> = x" by simp 

23956  526 
qed 
527 

528 
text {* 

25200  529 
\noindent The logical proof is carried out on the locale level 
23956  530 
and thus conveniently is opened using the @{text unfold_locales} 
531 
method which only leaves the logical differences still 

25200  532 
open to proof to the user. Afterwards it is propagated 
23956  533 
to the type system, making @{text group} an instance of 
25247  534 
@{text monoid} by adding an additional edge 
535 
to the graph of subclass relations 

536 
(cf.\ \figref{fig:subclass}). 

537 

538 
\begin{figure}[htbp] 

539 
\begin{center} 

540 
\small 

541 
\unitlength 0.6mm 

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(25,35){\vector(1,3){10}} 

550 
\end{picture} 

551 
\hspace{8em} 

552 
\begin{picture}(40,60)(0,0) 

553 
\put(20,60){\makebox(0,0){@{text semigroup}}} 

554 
\put(20,40){\makebox(0,0){@{text monoidl}}} 

555 
\put(00,20){\makebox(0,0){@{text monoid}}} 

556 
\put(40,00){\makebox(0,0){@{text group}}} 

557 
\put(20,55){\vector(0,1){10}} 

558 
\put(15,35){\vector(1,1){10}} 

559 
\put(05,15){\vector(3,1){30}} 

560 
\end{picture} 

561 
\caption{Subclass relationship of monoids and groups: 

562 
before and after establishing the relationship 

563 
@{text "group \<subseteq> monoid"}; transitive edges left out.} 

564 
\label{fig:subclass} 

565 
\end{center} 

566 
\end{figure} 

567 

568 
For illustration, a derived definition 

24991  569 
in @{text group} which uses @{text pow_nat}: 
23956  570 
*} 
571 

572 
definition (in group) 

573 
pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where 

574 
"pow_int k x = (if k >= 0 

575 
then pow_nat (nat k) x 

25200  576 
else (pow_nat (nat ( k)) x)\<div>)" 
23956  577 

578 
text {* 

25247  579 
\noindent yields the global definition of 
23956  580 
@{term [source] "pow_int \<Colon> int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} 
581 
with the corresponding theorem @{thm pow_int_def [no_vars]}. 

24991  582 
*} 
23956  583 

25868  584 
subsection {* A note on syntax *} 
585 

586 
text {* 

587 
As a commodity, class context syntax allows to refer 

588 
to local class operations and their global conuterparts 

589 
uniformly; type inference resolves ambiguities. For example: 

590 
*} 

591 

592 
context semigroup 

593 
begin 

594 

595 
term "x \<otimes> y"  {* example 1 *} 

596 
term "(x\<Colon>nat) \<otimes> y"  {* example 2 *} 

597 

598 
end 

599 

600 
term "x \<otimes> y"  {* example 3 *} 

601 

602 
text {* 

603 
\noindent Here in example 1, the term refers to the local class operation 

604 
@{text "mult [\<alpha>]"}, whereas in example 2 the type constraint 

605 
enforces the global class operation @{text "mult [nat]"}. 

606 
In the global context in example 3, the reference is 

607 
to the polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}. 

608 
*} 

22347  609 

25247  610 
section {* Type classes and code generation *} 
22317  611 

612 
text {* 

613 
Turning back to the first motivation for type classes, 

614 
namely overloading, it is obvious that overloading 

25533  615 
stemming from @{text "\<CLASS>"} statements and 
616 
@{text "\<INSTANTIATION>"} 

617 
targets naturally maps to Haskell type classes. 

22317  618 
The code generator framework \cite{isabellecodegen} 
619 
takes this into account. Concerning target languages 

620 
lacking type classes (e.g.~SML), type classes 

621 
are implemented by explicit dictionary construction. 

23956  622 
For example, lets go back to the power function: 
22317  623 
*} 
624 

625 
definition 

626 
example :: int where 

627 
"example = pow_int 10 (2)" 

628 

629 
text {* 

630 
\noindent This maps to Haskell as: 

631 
*} 

632 

24628  633 
export_code example in Haskell module_name Classes file "code_examples/" 
22317  634 
(* NOTE: you may use Haskell only once in this document, otherwise 
635 
you have to work in distinct subdirectories *) 

636 

637 
text {* 

638 
\lsthaskell{Thy/code_examples/Classes.hs} 

639 

640 
\noindent The whole code in SML with explicit dictionary passing: 

641 
*} 

642 

24628  643 
export_code example (*<*)in SML module_name Classes(*>*)in SML module_name Classes file "code_examples/classes.ML" 
22317  644 

645 
text {* 

646 
\lstsml{Thy/code_examples/classes.ML} 

647 
*} 

648 

649 

650 
(* subsection {* Different syntax for same specifications *} 

20946  651 

652 
text {* 

653 

22479  654 
subsection {* Syntactic classes *} 
22317  655 

20946  656 
*} *) 
657 

658 
end 