3 \def\isabellecontext{Classes}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Main\ Setup\isanewline
21 \isamarkupsection{Introduction%
25 \begin{isamarkuptext}%
26 Type classes were introduces by Wadler and Blott \cite{wadler89how}
27 into the Haskell language, to allow for a reasonable implementation
28 of overloading\footnote{throughout this tutorial, we are referring
29 to classical Haskell 1.0 type classes, not considering
30 later additions in expressiveness}.
31 As a canonical example, a polymorphic equality function
32 \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
33 types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
34 of the \isa{eq} function from its overloaded definitions by means
35 of \isa{class} and \isa{instance} declarations:
36 \footnote{syntax here is a kind of isabellized Haskell}
40 \noindent\isa{class\ eq\ where} \\
41 \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
43 \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
44 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
45 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
46 \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
47 \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
49 \medskip\noindent\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
50 \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
52 \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
53 \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
54 \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
58 \noindent Type variables are annotated with (finitely many) classes;
59 these annotations are assertions that a particular polymorphic type
60 provides definitions for overloaded functions.
62 Indeed, type classes not only allow for simple overloading
63 but form a generic calculus, an instance of order-sorted
64 algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
66 From a software engeneering point of view, type classes
67 roughly correspond to interfaces in object-oriented languages like Java;
68 so, it is naturally desirable that type classes do not only
69 provide functions (class parameters) but also state specifications
70 implementations must obey. For example, the \isa{class\ eq}
71 above could be given the following specification, demanding that
72 \isa{class\ eq} is an equivalence relation obeying reflexivity,
73 symmetry and transitivity:
77 \noindent\isa{class\ eq\ where} \\
78 \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
80 \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
81 \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
82 \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
86 \noindent From a theoretic point of view, type classes are lightweight
87 modules; Haskell type classes may be emulated by
88 SML functors \cite{classes_modules}.
89 Isabelle/Isar offers a discipline of type classes which brings
90 all those aspects together:
93 \item specifying abstract parameters together with
94 corresponding specifications,
95 \item instantiating those abstract parameters by a particular
97 \item in connection with a ``less ad-hoc'' approach to overloading,
98 \item with a direct link to the Isabelle module system
99 (aka locales \cite{kammueller-locales}).
102 \noindent Isar type classes also directly support code generation
103 in a Haskell like fashion.
105 This tutorial demonstrates common elements of structured specifications
106 and abstract reasoning with type classes by the algebraic hierarchy of
107 semigroups, monoids and groups. Our background theory is that of
108 Isabelle/HOL \cite{isa-tutorial}, for which some
109 familiarity is assumed.
111 Here we merely present the look-and-feel for end users.
112 Internally, those are mapped to more primitive Isabelle concepts.
113 See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
117 \isamarkupsection{A simple algebra example \label{sec:example}%
121 \isamarkupsubsection{Class definition%
125 \begin{isamarkuptext}%
126 Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
127 assumed to be associative:%
136 \isacommand{class}\isamarkupfalse%
137 \ semigroup\ {\isacharequal}\isanewline
138 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
139 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
147 \begin{isamarkuptext}%
148 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
149 parts: the \qn{operational} part names the class parameter
150 (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
151 (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
152 \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
154 parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
155 global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
159 \isamarkupsubsection{Class instantiation \label{sec:class_inst}%
163 \begin{isamarkuptext}%
164 The concrete type \isa{int} is made a \isa{semigroup}
165 instance by providing a suitable definition for the class parameter
166 \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
167 This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
176 \isacommand{instantiation}\isamarkupfalse%
177 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
178 \isakeyword{begin}\isanewline
180 \isacommand{definition}\isamarkupfalse%
182 \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
184 \isacommand{instance}\isamarkupfalse%
185 \ \isacommand{proof}\isamarkupfalse%
187 \ \ \isacommand{fix}\isamarkupfalse%
188 \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
189 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
191 \ \ \isacommand{then}\isamarkupfalse%
192 \ \isacommand{show}\isamarkupfalse%
193 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
194 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
195 \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
197 \isacommand{qed}\isamarkupfalse%
200 \isacommand{end}\isamarkupfalse%
209 \begin{isamarkuptext}%
210 \noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
211 at a particular instance using common specification tools (here,
212 \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
213 opens a proof that the given parameters actually conform
214 to the class specification. Note that the first proof step
215 is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
216 which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
217 This boils down an instance judgement to the relevant primitive
218 proof goals and should conveniently always be the first method applied
219 in an instantiation proof.
221 From now on, the type-checker will consider \isa{int}
222 as a \isa{semigroup} automatically, i.e.\ any general results
223 are immediately available on concrete instances.
225 \medskip Another instance of \isa{semigroup} are the natural numbers:%
234 \isacommand{instantiation}\isamarkupfalse%
235 \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
236 \isakeyword{begin}\isanewline
238 \isacommand{primrec}\isamarkupfalse%
239 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
240 \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
241 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
243 \isacommand{instance}\isamarkupfalse%
244 \ \isacommand{proof}\isamarkupfalse%
246 \ \ \isacommand{fix}\isamarkupfalse%
247 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
248 \ \ \isacommand{show}\isamarkupfalse%
249 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
250 \ \ \ \ \isacommand{by}\isamarkupfalse%
251 \ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
252 \isacommand{qed}\isamarkupfalse%
255 \isacommand{end}\isamarkupfalse%
264 \begin{isamarkuptext}%
265 \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
266 in the primrec declaration; by default, the local name of
267 a class operation \isa{f} to instantiate on type constructor
268 \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
269 these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
270 or the corresponding ProofGeneral button.%
274 \isamarkupsubsection{Lifting and parametric types%
278 \begin{isamarkuptext}%
279 Overloaded definitions giving on class instantiation
280 may include recursion over the syntactic structure of types.
281 As a canonical example, we model product semigroups
282 using our simple algebra:%
291 \isacommand{instantiation}\isamarkupfalse%
292 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
293 \isakeyword{begin}\isanewline
295 \isacommand{definition}\isamarkupfalse%
297 \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
299 \isacommand{instance}\isamarkupfalse%
300 \ \isacommand{proof}\isamarkupfalse%
302 \ \ \isacommand{fix}\isamarkupfalse%
303 \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
304 \ \ \isacommand{show}\isamarkupfalse%
305 \ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
306 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
307 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
308 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
309 \isacommand{qed}\isamarkupfalse%
310 \ \ \ \ \ \ \isanewline
312 \isacommand{end}\isamarkupfalse%
321 \begin{isamarkuptext}%
322 \noindent Associativity from product semigroups is
324 the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
325 associativity of the type components; these hypotheses
326 are facts due to the \isa{semigroup} constraints imposed
327 on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
328 Indeed, this pattern often occurs with parametric types
333 \isamarkupsubsection{Subclassing%
337 \begin{isamarkuptext}%
338 We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
339 by extending \isa{semigroup}
340 with one additional parameter \isa{neutral} together
350 \isacommand{class}\isamarkupfalse%
351 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
352 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
353 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
361 \begin{isamarkuptext}%
362 \noindent Again, we prove some instances, by
363 providing suitable parameter definitions and proofs for the
364 additional specifications. Observe that instantiations
365 for types with the same arity may be simultaneous:%
374 \isacommand{instantiation}\isamarkupfalse%
375 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
376 \isakeyword{begin}\isanewline
378 \isacommand{definition}\isamarkupfalse%
380 \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
382 \isacommand{definition}\isamarkupfalse%
384 \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
386 \isacommand{instance}\isamarkupfalse%
387 \ \isacommand{proof}\isamarkupfalse%
389 \ \ \isacommand{fix}\isamarkupfalse%
390 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
391 \ \ \isacommand{show}\isamarkupfalse%
392 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
393 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
394 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
396 \isacommand{next}\isamarkupfalse%
398 \ \ \isacommand{fix}\isamarkupfalse%
399 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
400 \ \ \isacommand{show}\isamarkupfalse%
401 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
402 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
403 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
405 \isacommand{qed}\isamarkupfalse%
408 \isacommand{end}\isamarkupfalse%
411 \isacommand{instantiation}\isamarkupfalse%
412 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
413 \isakeyword{begin}\isanewline
415 \isacommand{definition}\isamarkupfalse%
417 \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
419 \isacommand{instance}\isamarkupfalse%
420 \ \isacommand{proof}\isamarkupfalse%
422 \ \ \isacommand{fix}\isamarkupfalse%
423 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
424 \ \ \isacommand{show}\isamarkupfalse%
425 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
426 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
427 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
428 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
429 \isacommand{qed}\isamarkupfalse%
432 \isacommand{end}\isamarkupfalse%
441 \begin{isamarkuptext}%
442 \noindent Fully-fledged monoids are modelled by another subclass
443 which does not add new parameters but tightens the specification:%
452 \isacommand{class}\isamarkupfalse%
453 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
454 \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
456 \isacommand{instantiation}\isamarkupfalse%
457 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
458 \isakeyword{begin}\isanewline
460 \isacommand{instance}\isamarkupfalse%
461 \ \isacommand{proof}\isamarkupfalse%
463 \ \ \isacommand{fix}\isamarkupfalse%
464 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
465 \ \ \isacommand{show}\isamarkupfalse%
466 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
467 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
468 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
469 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
470 \isacommand{next}\isamarkupfalse%
472 \ \ \isacommand{fix}\isamarkupfalse%
473 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
474 \ \ \isacommand{show}\isamarkupfalse%
475 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
476 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
477 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
479 \isacommand{qed}\isamarkupfalse%
482 \isacommand{end}\isamarkupfalse%
485 \isacommand{instantiation}\isamarkupfalse%
486 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
487 \isakeyword{begin}\isanewline
489 \isacommand{instance}\isamarkupfalse%
490 \ \isacommand{proof}\isamarkupfalse%
492 \ \ \isacommand{fix}\isamarkupfalse%
493 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
494 \ \ \isacommand{show}\isamarkupfalse%
495 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
496 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
497 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
498 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
499 \isacommand{qed}\isamarkupfalse%
502 \isacommand{end}\isamarkupfalse%
511 \begin{isamarkuptext}%
512 \noindent To finish our small algebra example, we add a \isa{group} class
513 with a corresponding instance:%
522 \isacommand{class}\isamarkupfalse%
523 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
524 \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
525 \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
527 \isacommand{instantiation}\isamarkupfalse%
528 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
529 \isakeyword{begin}\isanewline
531 \isacommand{definition}\isamarkupfalse%
533 \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
535 \isacommand{instance}\isamarkupfalse%
536 \ \isacommand{proof}\isamarkupfalse%
538 \ \ \isacommand{fix}\isamarkupfalse%
539 \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
540 \ \ \isacommand{have}\isamarkupfalse%
541 \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
543 \ \ \isacommand{then}\isamarkupfalse%
544 \ \isacommand{show}\isamarkupfalse%
545 \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
546 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
547 \ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
549 \isacommand{qed}\isamarkupfalse%
552 \isacommand{end}\isamarkupfalse%
561 \isamarkupsection{Type classes as locales%
565 \isamarkupsubsection{A look behind the scene%
569 \begin{isamarkuptext}%
570 The example above gives an impression how Isar type classes work
571 in practice. As stated in the introduction, classes also provide
572 a link to Isar's locale system. Indeed, the logical core of a class
573 is nothing else than a locale:%
582 \isacommand{class}\isamarkupfalse%
583 \ idem\ {\isacharequal}\isanewline
584 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
585 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
593 \begin{isamarkuptext}%
594 \noindent essentially introduces the locale%
600 \endisadeliminvisible
609 \endisadeliminvisible
616 \isacommand{locale}\isamarkupfalse%
617 \ idem\ {\isacharequal}\isanewline
618 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
619 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
627 \begin{isamarkuptext}%
628 \noindent together with corresponding constant(s):%
637 \isacommand{consts}\isamarkupfalse%
638 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
646 \begin{isamarkuptext}%
647 \noindent The connection to the type system is done by means
648 of a primitive axclass%
654 \endisadeliminvisible
663 \endisadeliminvisible
670 \isacommand{axclass}\isamarkupfalse%
671 \ idem\ {\isacharless}\ type\isanewline
672 \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
682 \endisadeliminvisible
691 \endisadeliminvisible
693 \begin{isamarkuptext}%
694 \noindent together with a corresponding interpretation:%
703 \isacommand{interpretation}\isamarkupfalse%
704 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
705 \ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
706 \isacommand{proof}\isamarkupfalse%
707 \ \isacommand{qed}\isamarkupfalse%
708 \ {\isacharparenleft}rule\ idem{\isacharparenright}%
716 \begin{isamarkuptext}%
717 \noindent This gives you at hand the full power of the Isabelle module system;
718 conclusions in locale \isa{idem} are implicitly propagated
719 to class \isa{idem}.%
725 \endisadeliminvisible
734 \endisadeliminvisible
736 \isamarkupsubsection{Abstract reasoning%
740 \begin{isamarkuptext}%
741 Isabelle locales enable reasoning at a general level, while results
742 are implicitly transferred to all instances. For example, we can
743 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
744 states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
753 \isacommand{lemma}\isamarkupfalse%
754 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
755 \isacommand{proof}\isamarkupfalse%
757 \ \ \isacommand{assume}\isamarkupfalse%
758 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
759 \ \ \isacommand{then}\isamarkupfalse%
760 \ \isacommand{have}\isamarkupfalse%
761 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
763 \ \ \isacommand{then}\isamarkupfalse%
764 \ \isacommand{have}\isamarkupfalse%
765 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
766 \ assoc\ \isacommand{by}\isamarkupfalse%
768 \ \ \isacommand{then}\isamarkupfalse%
769 \ \isacommand{show}\isamarkupfalse%
770 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
771 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
773 \isacommand{next}\isamarkupfalse%
775 \ \ \isacommand{assume}\isamarkupfalse%
776 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
777 \ \ \isacommand{then}\isamarkupfalse%
778 \ \isacommand{show}\isamarkupfalse%
779 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
781 \isacommand{qed}\isamarkupfalse%
790 \begin{isamarkuptext}%
791 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
792 indicates that the result is recorded within that context for later
793 use. This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
794 \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
798 \isamarkupsubsection{Derived definitions%
802 \begin{isamarkuptext}%
803 Isabelle locales support a concept of local definitions
813 \isacommand{primrec}\isamarkupfalse%
814 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
815 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
816 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
824 \begin{isamarkuptext}%
825 \noindent If the locale \isa{group} is also a class, this local
826 definition is propagated onto a global definition of
827 \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
828 with corresponding theorems
830 \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
831 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
833 \noindent As you can see from this example, for local
834 definitions you may use any specification tool
835 which works together with locales (e.g. \cite{krauss2006}).%
839 \isamarkupsubsection{A functor analogy%
843 \begin{isamarkuptext}%
844 We introduced Isar classes by analogy to type classes
845 functional programming; if we reconsider this in the
846 context of what has been said about type classes and locales,
847 we can drive this analogy further by stating that type
848 classes essentially correspond to functors which have
849 a canonical interpretation as type classes.
850 Anyway, there is also the possibility of other interpretations.
851 For example, also \isa{list}s form a monoid with
852 \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
853 seems inappropriate to apply to lists
854 the same operations as for genuinely algebraic types.
855 In such a case, we simply can do a particular interpretation
856 of monoids for lists:%
865 \isacommand{interpretation}\isamarkupfalse%
866 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
867 \ \ \isacommand{proof}\isamarkupfalse%
868 \ \isacommand{qed}\isamarkupfalse%
877 \begin{isamarkuptext}%
878 \noindent This enables us to apply facts on monoids
879 to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
881 When using this interpretation pattern, it may also
882 be appropriate to map derived definitions accordingly:%
891 \isacommand{primrec}\isamarkupfalse%
892 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
893 \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
894 \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
896 \isacommand{interpretation}\isamarkupfalse%
897 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
898 \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
899 \isacommand{proof}\isamarkupfalse%
900 \ {\isacharminus}\isanewline
901 \ \ \isacommand{interpret}\isamarkupfalse%
902 \ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
904 \ \ \isacommand{show}\isamarkupfalse%
905 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
906 \ \ \isacommand{proof}\isamarkupfalse%
908 \ \ \ \ \isacommand{fix}\isamarkupfalse%
910 \ \ \ \ \isacommand{show}\isamarkupfalse%
911 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
912 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
913 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
914 \ \ \isacommand{qed}\isamarkupfalse%
916 \isacommand{qed}\isamarkupfalse%
917 \ intro{\isacharunderscore}locales%
925 \isamarkupsubsection{Additional subclass relations%
929 \begin{isamarkuptext}%
930 Any \isa{group} is also a \isa{monoid}; this
931 can be made explicit by claiming an additional
933 together with a proof of the logical difference:%
942 \isacommand{subclass}\isamarkupfalse%
943 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
944 \isacommand{proof}\isamarkupfalse%
946 \ \ \isacommand{fix}\isamarkupfalse%
948 \ \ \isacommand{from}\isamarkupfalse%
949 \ invl\ \isacommand{have}\isamarkupfalse%
950 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
952 \ \ \isacommand{with}\isamarkupfalse%
953 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
954 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
956 \ \ \isacommand{with}\isamarkupfalse%
957 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
958 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
960 \isacommand{qed}\isamarkupfalse%
969 \begin{isamarkuptext}%
970 The logical proof is carried out on the locale level.
971 Afterwards it is propagated
972 to the type system, making \isa{group} an instance of
973 \isa{monoid} by adding an additional edge
974 to the graph of subclass relations
975 (cf.\ \figref{fig:subclass}).
981 \begin{picture}(40,60)(0,0)
982 \put(20,60){\makebox(0,0){\isa{semigroup}}}
983 \put(20,40){\makebox(0,0){\isa{monoidl}}}
984 \put(00,20){\makebox(0,0){\isa{monoid}}}
985 \put(40,00){\makebox(0,0){\isa{group}}}
986 \put(20,55){\vector(0,-1){10}}
987 \put(15,35){\vector(-1,-1){10}}
988 \put(25,35){\vector(1,-3){10}}
991 \begin{picture}(40,60)(0,0)
992 \put(20,60){\makebox(0,0){\isa{semigroup}}}
993 \put(20,40){\makebox(0,0){\isa{monoidl}}}
994 \put(00,20){\makebox(0,0){\isa{monoid}}}
995 \put(40,00){\makebox(0,0){\isa{group}}}
996 \put(20,55){\vector(0,-1){10}}
997 \put(15,35){\vector(-1,-1){10}}
998 \put(05,15){\vector(3,-1){30}}
1000 \caption{Subclass relationship of monoids and groups:
1001 before and after establishing the relationship
1002 \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
1003 \label{fig:subclass}
1007 For illustration, a derived definition
1008 in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
1009 \end{isamarkuptext}%
1017 \isacommand{definition}\isamarkupfalse%
1018 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1019 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
1020 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
1021 \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
1029 \begin{isamarkuptext}%
1030 \noindent yields the global definition of
1031 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
1032 with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
1033 \end{isamarkuptext}%
1036 \isamarkupsubsection{A note on syntax%
1040 \begin{isamarkuptext}%
1041 As a commodity, class context syntax allows to refer
1042 to local class operations and their global counterparts
1043 uniformly; type inference resolves ambiguities. For example:%
1044 \end{isamarkuptext}%
1052 \isacommand{context}\isamarkupfalse%
1053 \ semigroup\isanewline
1054 \isakeyword{begin}\isanewline
1056 \isacommand{term}\isamarkupfalse%
1057 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1058 \isamarkupcmt{example 1%
1061 \isacommand{term}\isamarkupfalse%
1062 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1063 \isamarkupcmt{example 2%
1067 \isacommand{end}\isamarkupfalse%
1070 \isacommand{term}\isamarkupfalse%
1071 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1072 \isamarkupcmt{example 3%
1082 \begin{isamarkuptext}%
1083 \noindent Here in example 1, the term refers to the local class operation
1084 \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
1085 enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
1086 In the global context in example 3, the reference is
1087 to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
1088 \end{isamarkuptext}%
1091 \isamarkupsection{Further issues%
1095 \isamarkupsubsection{Type classes and code generation%
1099 \begin{isamarkuptext}%
1100 Turning back to the first motivation for type classes,
1101 namely overloading, it is obvious that overloading
1102 stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
1103 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
1104 targets naturally maps to Haskell type classes.
1105 The code generator framework \cite{isabelle-codegen}
1106 takes this into account. Concerning target languages
1107 lacking type classes (e.g.~SML), type classes
1108 are implemented by explicit dictionary construction.
1109 As example, let's go back to the power function:%
1110 \end{isamarkuptext}%
1118 \isacommand{definition}\isamarkupfalse%
1119 \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
1120 \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
1128 \begin{isamarkuptext}%
1129 \noindent This maps to Haskell as:%
1130 \end{isamarkuptext}%
1139 \begin{isamarkuptext}%
1142 \hspace*{0pt}module Example where {\char123}\\
1145 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
1147 \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
1148 \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
1150 \hspace*{0pt}nat ::~Integer -> Nat;\\
1151 \hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
1153 \hspace*{0pt}class Semigroup a where {\char123}\\
1154 \hspace*{0pt} ~mult ::~a -> a -> a;\\
1155 \hspace*{0pt}{\char125};\\
1157 \hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
1158 \hspace*{0pt} ~neutral ::~a;\\
1159 \hspace*{0pt}{\char125};\\
1161 \hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
1162 \hspace*{0pt}{\char125};\\
1164 \hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
1165 \hspace*{0pt} ~inverse ::~a -> a;\\
1166 \hspace*{0pt}{\char125};\\
1168 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
1169 \hspace*{0pt}inverse{\char95}int i = negate i;\\
1171 \hspace*{0pt}neutral{\char95}int ::~Integer;\\
1172 \hspace*{0pt}neutral{\char95}int = 0;\\
1174 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
1175 \hspace*{0pt}mult{\char95}int i j = i + j;\\
1177 \hspace*{0pt}instance Semigroup Integer where {\char123}\\
1178 \hspace*{0pt} ~mult = mult{\char95}int;\\
1179 \hspace*{0pt}{\char125};\\
1181 \hspace*{0pt}instance Monoidl Integer where {\char123}\\
1182 \hspace*{0pt} ~neutral = neutral{\char95}int;\\
1183 \hspace*{0pt}{\char125};\\
1185 \hspace*{0pt}instance Monoid Integer where {\char123}\\
1186 \hspace*{0pt}{\char125};\\
1188 \hspace*{0pt}instance Group Integer where {\char123}\\
1189 \hspace*{0pt} ~inverse = inverse{\char95}int;\\
1190 \hspace*{0pt}{\char125};\\
1192 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1193 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
1194 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
1196 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
1197 \hspace*{0pt}pow{\char95}int k x =\\
1198 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
1199 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
1201 \hspace*{0pt}example ::~Integer;\\
1202 \hspace*{0pt}example = pow{\char95}int 10 (-2);\\
1204 \hspace*{0pt}{\char125}%
1205 \end{isamarkuptext}%
1215 \begin{isamarkuptext}%
1216 \noindent The whole code in SML with explicit dictionary passing:%
1217 \end{isamarkuptext}%
1226 \begin{isamarkuptext}%
1229 \hspace*{0pt}structure Example = \\
1230 \hspace*{0pt}struct\\
1232 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1234 \hspace*{0pt}fun nat{\char95}aux i n =\\
1235 \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
1236 \hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\
1238 \hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
1240 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
1241 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
1243 \hspace*{0pt}type 'a monoidl =\\
1244 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
1245 \hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
1246 \hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
1248 \hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
1249 \hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
1251 \hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
1252 \hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
1253 \hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
1255 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
1257 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\
1259 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
1261 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
1263 \hspace*{0pt}val monoidl{\char95}int =\\
1264 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
1265 \hspace*{0pt} ~IntInf.int monoidl;\\
1267 \hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
1268 \hspace*{0pt} ~IntInf.int monoid;\\
1270 \hspace*{0pt}val group{\char95}int =\\
1271 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
1272 \hspace*{0pt} ~IntInf.int group;\\
1274 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
1275 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
1276 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
1278 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
1279 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
1280 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
1281 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
1283 \hspace*{0pt}val example :~IntInf.int =\\
1284 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\
1286 \hspace*{0pt}end;~(*struct Example*)%
1287 \end{isamarkuptext}%
1297 \isamarkupsubsection{Inspecting the type class universe%
1301 \begin{isamarkuptext}%
1302 To facilitate orientation in complex subclass structures,
1303 two diagnostics commands are provided:
1307 \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] print a list of all classes
1308 together with associated operations etc.
1310 \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation
1311 between all classes as a Hasse diagram.
1314 \end{isamarkuptext}%
1322 \isacommand{end}\isamarkupfalse%
1332 %%% Local Variables:
1334 %%% TeX-master: "root"