3 \def\isabellecontext{Classes}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Main\ Setup\isanewline
21 \isamarkupchapter{Haskell-style classes with Isabelle/Isar%
25 \isamarkupsection{Introduction%
29 \begin{isamarkuptext}%
30 Type classes were introduces by Wadler and Blott \cite{wadler89how}
31 into the Haskell language, to allow for a reasonable implementation
32 of overloading\footnote{throughout this tutorial, we are referring
33 to classical Haskell 1.0 type classes, not considering
34 later additions in expressiveness}.
35 As a canonical example, a polymorphic equality function
36 \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different
37 types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
38 of the \isa{eq} function from its overloaded definitions by means
39 of \isa{class} and \isa{instance} declarations:
43 \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
44 \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
46 \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
47 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
48 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
49 \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
50 \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
52 \medskip\noindent\\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
53 \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}}}
55 \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
56 \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
57 \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
61 \noindent Type variables are annotated with (finitely many) classes;
62 these annotations are assertions that a particular polymorphic type
63 provides definitions for overloaded functions.
65 Indeed, type classes not only allow for simple overloading
66 but form a generic calculus, an instance of order-sorted
67 algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
69 From a software engeneering point of view, type classes
70 roughly correspond to interfaces in object-oriented languages like Java;
71 so, it is naturally desirable that type classes do not only
72 provide functions (class parameters) but also state specifications
73 implementations must obey. For example, the \isa{class\ eq}
74 above could be given the following specification, demanding that
75 \isa{class\ eq} is an equivalence relation obeying reflexivity,
76 symmetry and transitivity:
80 \noindent\isa{class\ eq\ where} \\
81 \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
83 \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
84 \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
85 \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
89 \noindent From a theoretic point of view, type classes are lightweight
90 modules; Haskell type classes may be emulated by
91 SML functors \cite{classes_modules}.
92 Isabelle/Isar offers a discipline of type classes which brings
93 all those aspects together:
96 \item specifying abstract parameters together with
97 corresponding specifications,
98 \item instantiating those abstract parameters by a particular
100 \item in connection with a ``less ad-hoc'' approach to overloading,
101 \item with a direct link to the Isabelle module system
102 (aka locales \cite{kammueller-locales}).
105 \noindent Isar type classes also directly support code generation
106 in a Haskell like fashion.
108 This tutorial demonstrates common elements of structured specifications
109 and abstract reasoning with type classes by the algebraic hierarchy of
110 semigroups, monoids and groups. Our background theory is that of
111 Isabelle/HOL \cite{isa-tutorial}, for which some
112 familiarity is assumed.
114 Here we merely present the look-and-feel for end users.
115 Internally, those are mapped to more primitive Isabelle concepts.
116 See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
120 \isamarkupsection{A simple algebra example \label{sec:example}%
124 \isamarkupsubsection{Class definition%
128 \begin{isamarkuptext}%
129 Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
130 assumed to be associative:%
139 \isacommand{class}\isamarkupfalse%
140 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
141 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
142 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
150 \begin{isamarkuptext}%
151 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
152 parts: the \qn{operational} part names the class parameter
153 (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
154 (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
155 \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
157 parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
158 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}}.%
162 \isamarkupsubsection{Class instantiation \label{sec:class_inst}%
166 \begin{isamarkuptext}%
167 The concrete type \isa{int} is made a \isa{semigroup}
168 instance by providing a suitable definition for the class parameter
169 \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
170 This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
179 \isacommand{instantiation}\isamarkupfalse%
180 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
181 \isakeyword{begin}\isanewline
183 \isacommand{definition}\isamarkupfalse%
185 \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
187 \isacommand{instance}\isamarkupfalse%
188 \ \isacommand{proof}\isamarkupfalse%
190 \ \ \isacommand{fix}\isamarkupfalse%
191 \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
192 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
194 \ \ \isacommand{then}\isamarkupfalse%
195 \ \isacommand{show}\isamarkupfalse%
196 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
197 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
198 \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
200 \isacommand{qed}\isamarkupfalse%
203 \isacommand{end}\isamarkupfalse%
212 \begin{isamarkuptext}%
213 \noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
214 at a particular instance using common specification tools (here,
215 \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
216 opens a proof that the given parameters actually conform
217 to the class specification. Note that the first proof step
218 is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
219 which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
220 This boils down an instance judgement to the relevant primitive
221 proof goals and should conveniently always be the first method applied
222 in an instantiation proof.
224 From now on, the type-checker will consider \isa{int}
225 as a \isa{semigroup} automatically, i.e.\ any general results
226 are immediately available on concrete instances.
228 \medskip Another instance of \isa{semigroup} are the natural numbers:%
237 \isacommand{instantiation}\isamarkupfalse%
238 \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
239 \isakeyword{begin}\isanewline
241 \isacommand{primrec}\isamarkupfalse%
242 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
243 \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
244 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
246 \isacommand{instance}\isamarkupfalse%
247 \ \isacommand{proof}\isamarkupfalse%
249 \ \ \isacommand{fix}\isamarkupfalse%
250 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
251 \ \ \isacommand{show}\isamarkupfalse%
252 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
253 \ \ \ \ \isacommand{by}\isamarkupfalse%
254 \ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
255 \isacommand{qed}\isamarkupfalse%
258 \isacommand{end}\isamarkupfalse%
267 \begin{isamarkuptext}%
268 \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
269 in the primrec declaration; by default, the local name of
270 a class operation \isa{f} to instantiate on type constructor
271 \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
272 these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
273 or the corresponding ProofGeneral button.%
277 \isamarkupsubsection{Lifting and parametric types%
281 \begin{isamarkuptext}%
282 Overloaded definitions giving on class instantiation
283 may include recursion over the syntactic structure of types.
284 As a canonical example, we model product semigroups
285 using our simple algebra:%
294 \isacommand{instantiation}\isamarkupfalse%
295 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
296 \isakeyword{begin}\isanewline
298 \isacommand{definition}\isamarkupfalse%
300 \ \ 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
302 \isacommand{instance}\isamarkupfalse%
303 \ \isacommand{proof}\isamarkupfalse%
305 \ \ \isacommand{fix}\isamarkupfalse%
306 \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
307 \ \ \isacommand{show}\isamarkupfalse%
308 \ {\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
309 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
310 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
311 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
312 \isacommand{qed}\isamarkupfalse%
313 \ \ \ \ \ \ \isanewline
315 \isacommand{end}\isamarkupfalse%
324 \begin{isamarkuptext}%
325 \noindent Associativity from product semigroups is
327 the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
328 associativity of the type components; these hypotheses
329 are facts due to the \isa{semigroup} constraints imposed
330 on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
331 Indeed, this pattern often occurs with parametric types
336 \isamarkupsubsection{Subclassing%
340 \begin{isamarkuptext}%
341 We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
342 by extending \isa{semigroup}
343 with one additional parameter \isa{neutral} together
353 \isacommand{class}\isamarkupfalse%
354 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
355 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
356 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
364 \begin{isamarkuptext}%
365 \noindent Again, we prove some instances, by
366 providing suitable parameter definitions and proofs for the
367 additional specifications. Observe that instantiations
368 for types with the same arity may be simultaneous:%
377 \isacommand{instantiation}\isamarkupfalse%
378 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
379 \isakeyword{begin}\isanewline
381 \isacommand{definition}\isamarkupfalse%
383 \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
385 \isacommand{definition}\isamarkupfalse%
387 \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
389 \isacommand{instance}\isamarkupfalse%
390 \ \isacommand{proof}\isamarkupfalse%
392 \ \ \isacommand{fix}\isamarkupfalse%
393 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
394 \ \ \isacommand{show}\isamarkupfalse%
395 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
396 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
397 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
399 \isacommand{next}\isamarkupfalse%
401 \ \ \isacommand{fix}\isamarkupfalse%
402 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
403 \ \ \isacommand{show}\isamarkupfalse%
404 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
405 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
406 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
408 \isacommand{qed}\isamarkupfalse%
411 \isacommand{end}\isamarkupfalse%
414 \isacommand{instantiation}\isamarkupfalse%
415 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
416 \isakeyword{begin}\isanewline
418 \isacommand{definition}\isamarkupfalse%
420 \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
422 \isacommand{instance}\isamarkupfalse%
423 \ \isacommand{proof}\isamarkupfalse%
425 \ \ \isacommand{fix}\isamarkupfalse%
426 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
427 \ \ \isacommand{show}\isamarkupfalse%
428 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
429 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
430 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
431 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
432 \isacommand{qed}\isamarkupfalse%
435 \isacommand{end}\isamarkupfalse%
444 \begin{isamarkuptext}%
445 \noindent Fully-fledged monoids are modelled by another subclass
446 which does not add new parameters but tightens the specification:%
455 \isacommand{class}\isamarkupfalse%
456 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
457 \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
459 \isacommand{instantiation}\isamarkupfalse%
460 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
461 \isakeyword{begin}\isanewline
463 \isacommand{instance}\isamarkupfalse%
464 \ \isacommand{proof}\isamarkupfalse%
466 \ \ \isacommand{fix}\isamarkupfalse%
467 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
468 \ \ \isacommand{show}\isamarkupfalse%
469 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
470 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
471 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
472 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
473 \isacommand{next}\isamarkupfalse%
475 \ \ \isacommand{fix}\isamarkupfalse%
476 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
477 \ \ \isacommand{show}\isamarkupfalse%
478 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
479 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
480 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
482 \isacommand{qed}\isamarkupfalse%
485 \isacommand{end}\isamarkupfalse%
488 \isacommand{instantiation}\isamarkupfalse%
489 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
490 \isakeyword{begin}\isanewline
492 \isacommand{instance}\isamarkupfalse%
493 \ \isacommand{proof}\isamarkupfalse%
495 \ \ \isacommand{fix}\isamarkupfalse%
496 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
497 \ \ \isacommand{show}\isamarkupfalse%
498 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
499 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
500 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
501 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
502 \isacommand{qed}\isamarkupfalse%
505 \isacommand{end}\isamarkupfalse%
514 \begin{isamarkuptext}%
515 \noindent To finish our small algebra example, we add a \isa{group} class
516 with a corresponding instance:%
525 \isacommand{class}\isamarkupfalse%
526 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
527 \ \ \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
528 \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
530 \isacommand{instantiation}\isamarkupfalse%
531 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
532 \isakeyword{begin}\isanewline
534 \isacommand{definition}\isamarkupfalse%
536 \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
538 \isacommand{instance}\isamarkupfalse%
539 \ \isacommand{proof}\isamarkupfalse%
541 \ \ \isacommand{fix}\isamarkupfalse%
542 \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
543 \ \ \isacommand{have}\isamarkupfalse%
544 \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
546 \ \ \isacommand{then}\isamarkupfalse%
547 \ \isacommand{show}\isamarkupfalse%
548 \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
549 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
550 \ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
552 \isacommand{qed}\isamarkupfalse%
555 \isacommand{end}\isamarkupfalse%
564 \isamarkupsection{Type classes as locales%
568 \isamarkupsubsection{A look behind the scene%
572 \begin{isamarkuptext}%
573 The example above gives an impression how Isar type classes work
574 in practice. As stated in the introduction, classes also provide
575 a link to Isar's locale system. Indeed, the logical core of a class
576 is nothing else than a locale:%
585 \isacommand{class}\isamarkupfalse%
586 \ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
587 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
588 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
596 \begin{isamarkuptext}%
597 \noindent essentially introduces the locale%
603 \endisadeliminvisible
606 \isacommand{setup}\isamarkupfalse%
607 \ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
613 \endisadeliminvisible
622 \isacommand{locale}\isamarkupfalse%
623 \ idem\ {\isacharequal}\isanewline
624 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
625 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
633 \begin{isamarkuptext}%
634 \noindent together with corresponding constant(s):%
643 \isacommand{consts}\isamarkupfalse%
644 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
652 \begin{isamarkuptext}%
653 \noindent The connection to the type system is done by means
654 of a primitive axclass%
663 \isacommand{axclass}\isamarkupfalse%
664 \ idem\ {\isacharless}\ type\isanewline
665 \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
673 \begin{isamarkuptext}%
674 \noindent together with a corresponding interpretation:%
683 \isacommand{interpretation}\isamarkupfalse%
684 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
685 \ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
686 \isacommand{by}\isamarkupfalse%
687 \ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}%
695 \begin{isamarkuptext}%
696 \noindent This gives you at hand the full power of the Isabelle module system;
697 conclusions in locale \isa{idem} are implicitly propagated
698 to class \isa{idem}.%
704 \endisadeliminvisible
707 \isacommand{setup}\isamarkupfalse%
708 \ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
714 \endisadeliminvisible
716 \isamarkupsubsection{Abstract reasoning%
720 \begin{isamarkuptext}%
721 Isabelle locales enable reasoning at a general level, while results
722 are implicitly transferred to all instances. For example, we can
723 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
724 states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
733 \isacommand{lemma}\isamarkupfalse%
734 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
735 \isacommand{proof}\isamarkupfalse%
737 \ \ \isacommand{assume}\isamarkupfalse%
738 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
739 \ \ \isacommand{then}\isamarkupfalse%
740 \ \isacommand{have}\isamarkupfalse%
741 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
743 \ \ \isacommand{then}\isamarkupfalse%
744 \ \isacommand{have}\isamarkupfalse%
745 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
746 \ assoc\ \isacommand{by}\isamarkupfalse%
748 \ \ \isacommand{then}\isamarkupfalse%
749 \ \isacommand{show}\isamarkupfalse%
750 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
751 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
753 \isacommand{next}\isamarkupfalse%
755 \ \ \isacommand{assume}\isamarkupfalse%
756 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
757 \ \ \isacommand{then}\isamarkupfalse%
758 \ \isacommand{show}\isamarkupfalse%
759 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
761 \isacommand{qed}\isamarkupfalse%
770 \begin{isamarkuptext}%
771 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
772 indicates that the result is recorded within that context for later
773 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
774 \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}}.%
778 \isamarkupsubsection{Derived definitions%
782 \begin{isamarkuptext}%
783 Isabelle locales support a concept of local definitions
793 \isacommand{primrec}\isamarkupfalse%
794 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
795 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
796 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
804 \begin{isamarkuptext}%
805 \noindent If the locale \isa{group} is also a class, this local
806 definition is propagated onto a global definition of
807 \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
808 with corresponding theorems
810 \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
811 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
813 \noindent As you can see from this example, for local
814 definitions you may use any specification tool
815 which works together with locales (e.g. \cite{krauss2006}).%
819 \isamarkupsubsection{A functor analogy%
823 \begin{isamarkuptext}%
824 We introduced Isar classes by analogy to type classes
825 functional programming; if we reconsider this in the
826 context of what has been said about type classes and locales,
827 we can drive this analogy further by stating that type
828 classes essentially correspond to functors which have
829 a canonical interpretation as type classes.
830 Anyway, there is also the possibility of other interpretations.
831 For example, also \isa{list}s form a monoid with
832 \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
833 seems inappropriate to apply to lists
834 the same operations as for genuinely algebraic types.
835 In such a case, we simply can do a particular interpretation
836 of monoids for lists:%
845 \isacommand{interpretation}\isamarkupfalse%
846 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
847 \ \ \isacommand{by}\isamarkupfalse%
848 \ unfold{\isacharunderscore}locales\ auto%
856 \begin{isamarkuptext}%
857 \noindent This enables us to apply facts on monoids
858 to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
860 When using this interpretation pattern, it may also
861 be appropriate to map derived definitions accordingly:%
870 \isacommand{primrec}\isamarkupfalse%
871 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
872 \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
873 \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
875 \isacommand{interpretation}\isamarkupfalse%
876 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
877 \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
878 \isacommand{proof}\isamarkupfalse%
879 \ {\isacharminus}\isanewline
880 \ \ \isacommand{interpret}\isamarkupfalse%
881 \ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
883 \ \ \isacommand{show}\isamarkupfalse%
884 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
885 \ \ \isacommand{proof}\isamarkupfalse%
887 \ \ \ \ \isacommand{fix}\isamarkupfalse%
889 \ \ \ \ \isacommand{show}\isamarkupfalse%
890 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
891 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
892 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
893 \ \ \isacommand{qed}\isamarkupfalse%
895 \isacommand{qed}\isamarkupfalse%
896 \ intro{\isacharunderscore}locales%
904 \isamarkupsubsection{Additional subclass relations%
908 \begin{isamarkuptext}%
909 Any \isa{group} is also a \isa{monoid}; this
910 can be made explicit by claiming an additional
912 together with a proof of the logical difference:%
921 \isacommand{subclass}\isamarkupfalse%
922 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
923 \isacommand{proof}\isamarkupfalse%
924 \ unfold{\isacharunderscore}locales\isanewline
925 \ \ \isacommand{fix}\isamarkupfalse%
927 \ \ \isacommand{from}\isamarkupfalse%
928 \ invl\ \isacommand{have}\isamarkupfalse%
929 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
931 \ \ \isacommand{with}\isamarkupfalse%
932 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
933 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
935 \ \ \isacommand{with}\isamarkupfalse%
936 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
937 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
939 \isacommand{qed}\isamarkupfalse%
948 \begin{isamarkuptext}%
949 \noindent The logical proof is carried out on the locale level
950 and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales}
951 method which only leaves the logical differences still
952 open to proof to the user. Afterwards it is propagated
953 to the type system, making \isa{group} an instance of
954 \isa{monoid} by adding an additional edge
955 to the graph of subclass relations
956 (cf.\ \figref{fig:subclass}).
962 \begin{picture}(40,60)(0,0)
963 \put(20,60){\makebox(0,0){\isa{semigroup}}}
964 \put(20,40){\makebox(0,0){\isa{monoidl}}}
965 \put(00,20){\makebox(0,0){\isa{monoid}}}
966 \put(40,00){\makebox(0,0){\isa{group}}}
967 \put(20,55){\vector(0,-1){10}}
968 \put(15,35){\vector(-1,-1){10}}
969 \put(25,35){\vector(1,-3){10}}
972 \begin{picture}(40,60)(0,0)
973 \put(20,60){\makebox(0,0){\isa{semigroup}}}
974 \put(20,40){\makebox(0,0){\isa{monoidl}}}
975 \put(00,20){\makebox(0,0){\isa{monoid}}}
976 \put(40,00){\makebox(0,0){\isa{group}}}
977 \put(20,55){\vector(0,-1){10}}
978 \put(15,35){\vector(-1,-1){10}}
979 \put(05,15){\vector(3,-1){30}}
981 \caption{Subclass relationship of monoids and groups:
982 before and after establishing the relationship
983 \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges left out.}
988 For illustration, a derived definition
989 in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
998 \isacommand{definition}\isamarkupfalse%
999 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1000 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
1001 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
1002 \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
1010 \begin{isamarkuptext}%
1011 \noindent yields the global definition of
1012 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
1013 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}}.%
1014 \end{isamarkuptext}%
1017 \isamarkupsubsection{A note on syntax%
1021 \begin{isamarkuptext}%
1022 As a commodity, class context syntax allows to refer
1023 to local class operations and their global counterparts
1024 uniformly; type inference resolves ambiguities. For example:%
1025 \end{isamarkuptext}%
1033 \isacommand{context}\isamarkupfalse%
1034 \ semigroup\isanewline
1035 \isakeyword{begin}\isanewline
1037 \isacommand{term}\isamarkupfalse%
1038 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1039 \isamarkupcmt{example 1%
1042 \isacommand{term}\isamarkupfalse%
1043 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1044 \isamarkupcmt{example 2%
1048 \isacommand{end}\isamarkupfalse%
1051 \isacommand{term}\isamarkupfalse%
1052 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1053 \isamarkupcmt{example 3%
1063 \begin{isamarkuptext}%
1064 \noindent Here in example 1, the term refers to the local class operation
1065 \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
1066 enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
1067 In the global context in example 3, the reference is
1068 to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
1069 \end{isamarkuptext}%
1072 \isamarkupsection{Type classes and code generation%
1076 \begin{isamarkuptext}%
1077 Turning back to the first motivation for type classes,
1078 namely overloading, it is obvious that overloading
1079 stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
1080 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
1081 targets naturally maps to Haskell type classes.
1082 The code generator framework \cite{isabelle-codegen}
1083 takes this into account. Concerning target languages
1084 lacking type classes (e.g.~SML), type classes
1085 are implemented by explicit dictionary construction.
1086 As example, let's go back to the power function:%
1087 \end{isamarkuptext}%
1095 \isacommand{definition}\isamarkupfalse%
1096 \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
1097 \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
1105 \begin{isamarkuptext}%
1106 \noindent This maps to Haskell as:%
1107 \end{isamarkuptext}%
1116 \begin{isamarkuptext}%
1119 \hspace*{0pt}module Example where {\char123}\\
1122 \hspace*{0pt}data Nat = Suc Nat | Zero{\char95}nat;\\
1124 \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
1125 \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
1127 \hspace*{0pt}nat ::~Integer -> Nat;\\
1128 \hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
1130 \hspace*{0pt}class Semigroup a where {\char123}\\
1131 \hspace*{0pt} ~mult ::~a -> a -> a;\\
1132 \hspace*{0pt}{\char125};\\
1134 \hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
1135 \hspace*{0pt} ~neutral ::~a;\\
1136 \hspace*{0pt}{\char125};\\
1138 \hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
1139 \hspace*{0pt}{\char125};\\
1141 \hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
1142 \hspace*{0pt} ~inverse ::~a -> a;\\
1143 \hspace*{0pt}{\char125};\\
1145 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
1146 \hspace*{0pt}inverse{\char95}int i = negate i;\\
1148 \hspace*{0pt}neutral{\char95}int ::~Integer;\\
1149 \hspace*{0pt}neutral{\char95}int = 0;\\
1151 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
1152 \hspace*{0pt}mult{\char95}int i j = i + j;\\
1154 \hspace*{0pt}instance Semigroup Integer where {\char123}\\
1155 \hspace*{0pt} ~mult = mult{\char95}int;\\
1156 \hspace*{0pt}{\char125};\\
1158 \hspace*{0pt}instance Monoidl Integer where {\char123}\\
1159 \hspace*{0pt} ~neutral = neutral{\char95}int;\\
1160 \hspace*{0pt}{\char125};\\
1162 \hspace*{0pt}instance Monoid Integer where {\char123}\\
1163 \hspace*{0pt}{\char125};\\
1165 \hspace*{0pt}instance Group Integer where {\char123}\\
1166 \hspace*{0pt} ~inverse = inverse{\char95}int;\\
1167 \hspace*{0pt}{\char125};\\
1169 \hspace*{0pt}pow{\char95}nat ::~forall a. (Monoid a) => Nat -> a -> a;\\
1170 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
1171 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
1173 \hspace*{0pt}pow{\char95}int ::~forall a. (Group a) => Integer -> a -> a;\\
1174 \hspace*{0pt}pow{\char95}int k x =\\
1175 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
1176 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
1178 \hspace*{0pt}example ::~Integer;\\
1179 \hspace*{0pt}example = pow{\char95}int 10 (-2);\\
1181 \hspace*{0pt}{\char125}%
1182 \end{isamarkuptext}%
1192 \begin{isamarkuptext}%
1193 \noindent The whole code in SML with explicit dictionary passing:%
1194 \end{isamarkuptext}%
1203 \begin{isamarkuptext}%
1206 \hspace*{0pt}structure Example = \\
1207 \hspace*{0pt}struct\\
1209 \hspace*{0pt}datatype nat = Suc of nat | Zero{\char95}nat;\\
1211 \hspace*{0pt}fun nat{\char95}aux i n =\\
1212 \hspace*{0pt} ~(if IntInf.<= (i, (0 :~IntInf.int)) then n\\
1213 \hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i, (1 :~IntInf.int))) (Suc n));\\
1215 \hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
1217 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
1218 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
1220 \hspace*{0pt}type 'a monoidl =\\
1221 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup, neutral :~'a{\char125};\\
1222 \hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
1223 \hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
1225 \hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
1226 \hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
1228 \hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid, inverse :~'a -> 'a{\char125};\\
1229 \hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
1230 \hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
1232 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
1234 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
1236 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i, j);\\
1238 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
1240 \hspace*{0pt}val monoidl{\char95}int =\\
1241 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int, neutral = neutral{\char95}int{\char125}~:\\
1242 \hspace*{0pt} ~IntInf.int monoidl;\\
1244 \hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
1245 \hspace*{0pt} ~IntInf.int monoid;\\
1247 \hspace*{0pt}val group{\char95}int =\\
1248 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int, inverse = inverse{\char95}int{\char125}~:\\
1249 \hspace*{0pt} ~IntInf.int group;\\
1251 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
1252 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
1253 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
1255 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
1256 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int), k)\\
1257 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
1258 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
1260 \hspace*{0pt}val example :~IntInf.int =\\
1261 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
1263 \hspace*{0pt}end; (*struct Example*)%
1264 \end{isamarkuptext}%
1279 \isacommand{end}\isamarkupfalse%
1289 %%% Local Variables:
1291 %%% TeX-master: "root"