3 \def\isabellecontext{Classes}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Main\ Setup\isanewline
21 \isamarkupsection{Introduction%
25 \begin{isamarkuptext}%
26 Type classes were introduced 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-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
66 From a software engineering 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 theoretical 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 locales \cite{kammueller-locales}.
102 \noindent Isar type classes also directly support code generation
103 in a Haskell like fashion. Internally, they are mapped to more primitive
104 Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
106 This tutorial demonstrates common elements of structured specifications
107 and abstract reasoning with type classes by the algebraic hierarchy of
108 semigroups, monoids and groups. Our background theory is that of
109 Isabelle/HOL \cite{isa-tutorial}, for which some
110 familiarity is assumed.%
114 \isamarkupsection{A simple algebra example \label{sec:example}%
118 \isamarkupsubsection{Class definition%
122 \begin{isamarkuptext}%
123 Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
124 assumed to be associative:%
133 \isacommand{class}\isamarkupfalse%
134 \ semigroup\ {\isacharequal}\isanewline
135 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
136 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
144 \begin{isamarkuptext}%
145 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
146 parts: the \qn{operational} part names the class parameter
147 (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
148 (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
149 \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
151 parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
152 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}}.%
156 \isamarkupsubsection{Class instantiation \label{sec:class_inst}%
160 \begin{isamarkuptext}%
161 The concrete type \isa{int} is made a \isa{semigroup}
162 instance by providing a suitable definition for the class parameter
163 \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
164 This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
173 \isacommand{instantiation}\isamarkupfalse%
174 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
175 \isakeyword{begin}\isanewline
177 \isacommand{definition}\isamarkupfalse%
179 \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
181 \isacommand{instance}\isamarkupfalse%
182 \ \isacommand{proof}\isamarkupfalse%
184 \ \ \isacommand{fix}\isamarkupfalse%
185 \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
186 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
188 \ \ \isacommand{then}\isamarkupfalse%
189 \ \isacommand{show}\isamarkupfalse%
190 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
191 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
192 \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
194 \isacommand{qed}\isamarkupfalse%
197 \isacommand{end}\isamarkupfalse%
206 \begin{isamarkuptext}%
207 \noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters
208 at a particular instance using common specification tools (here,
209 \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
210 opens a proof that the given parameters actually conform
211 to the class specification. Note that the first proof step
212 is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
213 which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
214 This reduces an instance judgement to the relevant primitive
215 proof goals; typically it is the first method applied
216 in an instantiation proof.
218 From now on, the type-checker will consider \isa{int}
219 as a \isa{semigroup} automatically, i.e.\ any general results
220 are immediately available on concrete instances.
222 \medskip Another instance of \isa{semigroup} yields the natural numbers:%
231 \isacommand{instantiation}\isamarkupfalse%
232 \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
233 \isakeyword{begin}\isanewline
235 \isacommand{primrec}\isamarkupfalse%
236 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
237 \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
238 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
240 \isacommand{instance}\isamarkupfalse%
241 \ \isacommand{proof}\isamarkupfalse%
243 \ \ \isacommand{fix}\isamarkupfalse%
244 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
245 \ \ \isacommand{show}\isamarkupfalse%
246 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
247 \ \ \ \ \isacommand{by}\isamarkupfalse%
248 \ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
249 \isacommand{qed}\isamarkupfalse%
252 \isacommand{end}\isamarkupfalse%
261 \begin{isamarkuptext}%
262 \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
263 in the primrec declaration; by default, the local name of
264 a class operation \isa{f} to be instantiated on type constructor
265 \isa{{\isasymkappa}} is mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
266 these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
267 or the corresponding ProofGeneral button.%
271 \isamarkupsubsection{Lifting and parametric types%
275 \begin{isamarkuptext}%
276 Overloaded definitions given at a class instantiation
277 may include recursion over the syntactic structure of types.
278 As a canonical example, we model product semigroups
279 using our simple algebra:%
288 \isacommand{instantiation}\isamarkupfalse%
289 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
290 \isakeyword{begin}\isanewline
292 \isacommand{definition}\isamarkupfalse%
294 \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p{\isadigit{1}}\ {\isasymotimes}\ fst\ p{\isadigit{2}}{\isacharcomma}\ snd\ p{\isadigit{1}}\ {\isasymotimes}\ snd\ p{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
296 \isacommand{instance}\isamarkupfalse%
297 \ \isacommand{proof}\isamarkupfalse%
299 \ \ \isacommand{fix}\isamarkupfalse%
300 \ p{\isadigit{1}}\ p{\isadigit{2}}\ p{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
301 \ \ \isacommand{show}\isamarkupfalse%
302 \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}\ {\isacharequal}\ p{\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
303 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
304 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
305 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
306 \isacommand{qed}\isamarkupfalse%
307 \ \ \ \ \ \ \isanewline
309 \isacommand{end}\isamarkupfalse%
318 \begin{isamarkuptext}%
319 \noindent Associativity of product semigroups is established using
320 the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
321 associativity of the type components; these hypotheses
322 are legitimate due to the \isa{semigroup} constraints imposed
323 on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
324 Indeed, this pattern often occurs with parametric types
329 \isamarkupsubsection{Subclassing%
333 \begin{isamarkuptext}%
334 We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
335 by extending \isa{semigroup}
336 with one additional parameter \isa{neutral} together
337 with its characteristic property:%
346 \isacommand{class}\isamarkupfalse%
347 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
348 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
349 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
357 \begin{isamarkuptext}%
358 \noindent Again, we prove some instances, by
359 providing suitable parameter definitions and proofs for the
360 additional specifications. Observe that instantiations
361 for types with the same arity may be simultaneous:%
370 \isacommand{instantiation}\isamarkupfalse%
371 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
372 \isakeyword{begin}\isanewline
374 \isacommand{definition}\isamarkupfalse%
376 \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
378 \isacommand{definition}\isamarkupfalse%
380 \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
382 \isacommand{instance}\isamarkupfalse%
383 \ \isacommand{proof}\isamarkupfalse%
385 \ \ \isacommand{fix}\isamarkupfalse%
386 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
387 \ \ \isacommand{show}\isamarkupfalse%
388 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
389 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
390 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
392 \isacommand{next}\isamarkupfalse%
394 \ \ \isacommand{fix}\isamarkupfalse%
395 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
396 \ \ \isacommand{show}\isamarkupfalse%
397 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
398 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
399 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
401 \isacommand{qed}\isamarkupfalse%
404 \isacommand{end}\isamarkupfalse%
407 \isacommand{instantiation}\isamarkupfalse%
408 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
409 \isakeyword{begin}\isanewline
411 \isacommand{definition}\isamarkupfalse%
413 \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
415 \isacommand{instance}\isamarkupfalse%
416 \ \isacommand{proof}\isamarkupfalse%
418 \ \ \isacommand{fix}\isamarkupfalse%
419 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
420 \ \ \isacommand{show}\isamarkupfalse%
421 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
422 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
423 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
424 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
425 \isacommand{qed}\isamarkupfalse%
428 \isacommand{end}\isamarkupfalse%
437 \begin{isamarkuptext}%
438 \noindent Fully-fledged monoids are modelled by another subclass,
439 which does not add new parameters but tightens the specification:%
448 \isacommand{class}\isamarkupfalse%
449 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
450 \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
452 \isacommand{instantiation}\isamarkupfalse%
453 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
454 \isakeyword{begin}\isanewline
456 \isacommand{instance}\isamarkupfalse%
457 \ \isacommand{proof}\isamarkupfalse%
459 \ \ \isacommand{fix}\isamarkupfalse%
460 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
461 \ \ \isacommand{show}\isamarkupfalse%
462 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
463 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
464 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
465 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
466 \isacommand{next}\isamarkupfalse%
468 \ \ \isacommand{fix}\isamarkupfalse%
469 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
470 \ \ \isacommand{show}\isamarkupfalse%
471 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
472 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
473 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
475 \isacommand{qed}\isamarkupfalse%
478 \isacommand{end}\isamarkupfalse%
481 \isacommand{instantiation}\isamarkupfalse%
482 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
483 \isakeyword{begin}\isanewline
485 \isacommand{instance}\isamarkupfalse%
486 \ \isacommand{proof}\isamarkupfalse%
488 \ \ \isacommand{fix}\isamarkupfalse%
489 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
490 \ \ \isacommand{show}\isamarkupfalse%
491 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
492 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
493 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
494 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
495 \isacommand{qed}\isamarkupfalse%
498 \isacommand{end}\isamarkupfalse%
507 \begin{isamarkuptext}%
508 \noindent To finish our small algebra example, we add a \isa{group} class
509 with a corresponding instance:%
518 \isacommand{class}\isamarkupfalse%
519 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
520 \ \ \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
521 \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
523 \isacommand{instantiation}\isamarkupfalse%
524 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
525 \isakeyword{begin}\isanewline
527 \isacommand{definition}\isamarkupfalse%
529 \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
531 \isacommand{instance}\isamarkupfalse%
532 \ \isacommand{proof}\isamarkupfalse%
534 \ \ \isacommand{fix}\isamarkupfalse%
535 \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline
536 \ \ \isacommand{have}\isamarkupfalse%
537 \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
539 \ \ \isacommand{then}\isamarkupfalse%
540 \ \isacommand{show}\isamarkupfalse%
541 \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
542 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
543 \ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
545 \isacommand{qed}\isamarkupfalse%
548 \isacommand{end}\isamarkupfalse%
557 \isamarkupsection{Type classes as locales%
561 \isamarkupsubsection{A look behind the scenes%
565 \begin{isamarkuptext}%
566 The example above gives an impression how Isar type classes work
567 in practice. As stated in the introduction, classes also provide
568 a link to Isar's locale system. Indeed, the logical core of a class
569 is nothing other than a locale:%
578 \isacommand{class}\isamarkupfalse%
579 \ idem\ {\isacharequal}\isanewline
580 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
581 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
589 \begin{isamarkuptext}%
590 \noindent essentially introduces the locale%
596 \endisadeliminvisible
605 \endisadeliminvisible
612 \isacommand{locale}\isamarkupfalse%
613 \ idem\ {\isacharequal}\isanewline
614 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
615 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
623 \begin{isamarkuptext}%
624 \noindent together with corresponding constant(s):%
633 \isacommand{consts}\isamarkupfalse%
634 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
642 \begin{isamarkuptext}%
643 \noindent The connection to the type system is done by means
644 of a primitive axclass%
650 \endisadeliminvisible
659 \endisadeliminvisible
666 \isacommand{axclass}\isamarkupfalse%
667 \ idem\ {\isacharless}\ type\isanewline
668 \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
678 \endisadeliminvisible
687 \endisadeliminvisible
689 \begin{isamarkuptext}%
690 \noindent together with a corresponding interpretation:%
699 \isacommand{interpretation}\isamarkupfalse%
700 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
701 \ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
702 \isacommand{proof}\isamarkupfalse%
703 \ \isacommand{qed}\isamarkupfalse%
704 \ {\isacharparenleft}rule\ idem{\isacharparenright}%
712 \begin{isamarkuptext}%
713 \noindent This gives you the full power of the Isabelle module system;
714 conclusions in locale \isa{idem} are implicitly propagated
715 to class \isa{idem}.%
721 \endisadeliminvisible
730 \endisadeliminvisible
732 \isamarkupsubsection{Abstract reasoning%
736 \begin{isamarkuptext}%
737 Isabelle locales enable reasoning at a general level, while results
738 are implicitly transferred to all instances. For example, we can
739 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
740 states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
749 \isacommand{lemma}\isamarkupfalse%
750 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
751 \isacommand{proof}\isamarkupfalse%
753 \ \ \isacommand{assume}\isamarkupfalse%
754 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
755 \ \ \isacommand{then}\isamarkupfalse%
756 \ \isacommand{have}\isamarkupfalse%
757 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
759 \ \ \isacommand{then}\isamarkupfalse%
760 \ \isacommand{have}\isamarkupfalse%
761 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
762 \ assoc\ \isacommand{by}\isamarkupfalse%
764 \ \ \isacommand{then}\isamarkupfalse%
765 \ \isacommand{show}\isamarkupfalse%
766 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
767 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
769 \isacommand{next}\isamarkupfalse%
771 \ \ \isacommand{assume}\isamarkupfalse%
772 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
773 \ \ \isacommand{then}\isamarkupfalse%
774 \ \isacommand{show}\isamarkupfalse%
775 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
777 \isacommand{qed}\isamarkupfalse%
786 \begin{isamarkuptext}%
787 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
788 indicates that the result is recorded within that context for later
789 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
790 \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}}.%
794 \isamarkupsubsection{Derived definitions%
798 \begin{isamarkuptext}%
799 Isabelle locales support a concept of local definitions
809 \isacommand{primrec}\isamarkupfalse%
810 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
811 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
812 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
820 \begin{isamarkuptext}%
821 \noindent If the locale \isa{group} is also a class, this local
822 definition is propagated onto a global definition of
823 \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
824 with corresponding theorems
826 \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
827 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
829 \noindent As you can see from this example, for local
830 definitions you may use any specification tool
831 which works together with locales, such as Krauss's recursive function package
836 \isamarkupsubsection{A functor analogy%
840 \begin{isamarkuptext}%
841 We introduced Isar classes by analogy to type classes in
842 functional programming; if we reconsider this in the
843 context of what has been said about type classes and locales,
844 we can drive this analogy further by stating that type
845 classes essentially correspond to functors that have
846 a canonical interpretation as type classes.
847 There is also the possibility of other interpretations.
848 For example, \isa{list}s also form a monoid with
849 \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
850 seems inappropriate to apply to lists
851 the same operations as for genuinely algebraic types.
852 In such a case, we can simply make a particular interpretation
853 of monoids for lists:%
862 \isacommand{interpretation}\isamarkupfalse%
863 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
864 \ \ \isacommand{proof}\isamarkupfalse%
865 \ \isacommand{qed}\isamarkupfalse%
874 \begin{isamarkuptext}%
875 \noindent This enables us to apply facts on monoids
876 to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
878 When using this interpretation pattern, it may also
879 be appropriate to map derived definitions accordingly:%
888 \isacommand{primrec}\isamarkupfalse%
889 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
890 \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
891 \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
893 \isacommand{interpretation}\isamarkupfalse%
894 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
895 \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
896 \isacommand{proof}\isamarkupfalse%
897 \ {\isacharminus}\isanewline
898 \ \ \isacommand{interpret}\isamarkupfalse%
899 \ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
901 \ \ \isacommand{show}\isamarkupfalse%
902 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
903 \ \ \isacommand{proof}\isamarkupfalse%
905 \ \ \ \ \isacommand{fix}\isamarkupfalse%
907 \ \ \ \ \isacommand{show}\isamarkupfalse%
908 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
909 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
910 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
911 \ \ \isacommand{qed}\isamarkupfalse%
913 \isacommand{qed}\isamarkupfalse%
914 \ intro{\isacharunderscore}locales%
922 \begin{isamarkuptext}%
923 \noindent This pattern is also helpful to reuse abstract
924 specifications on the \emph{same} type. For example, think of a
925 class \isa{preorder}; for type \isa{nat}, there are at least two
926 possible instances: the natural order or the order induced by the
927 divides relation. But only one of these instances can be used for
928 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract
929 specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.%
933 \isamarkupsubsection{Additional subclass relations%
937 \begin{isamarkuptext}%
938 Any \isa{group} is also a \isa{monoid}; this can be made
939 explicit by claiming an additional subclass relation, together with
940 a proof of the logical difference:%
949 \isacommand{subclass}\isamarkupfalse%
950 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
951 \isacommand{proof}\isamarkupfalse%
953 \ \ \isacommand{fix}\isamarkupfalse%
955 \ \ \isacommand{from}\isamarkupfalse%
956 \ invl\ \isacommand{have}\isamarkupfalse%
957 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
959 \ \ \isacommand{with}\isamarkupfalse%
960 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
961 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
963 \ \ \isacommand{with}\isamarkupfalse%
964 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
965 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
967 \isacommand{qed}\isamarkupfalse%
976 \begin{isamarkuptext}%
977 The logical proof is carried out on the locale level.
978 Afterwards it is propagated
979 to the type system, making \isa{group} an instance of
980 \isa{monoid} by adding an additional edge
981 to the graph of subclass relations
982 (\figref{fig:subclass}).
988 \begin{picture}(40,60)(0,0)
989 \put(20,60){\makebox(0,0){\isa{semigroup}}}
990 \put(20,40){\makebox(0,0){\isa{monoidl}}}
991 \put(00,20){\makebox(0,0){\isa{monoid}}}
992 \put(40,00){\makebox(0,0){\isa{group}}}
993 \put(20,55){\vector(0,-1){10}}
994 \put(15,35){\vector(-1,-1){10}}
995 \put(25,35){\vector(1,-3){10}}
998 \begin{picture}(40,60)(0,0)
999 \put(20,60){\makebox(0,0){\isa{semigroup}}}
1000 \put(20,40){\makebox(0,0){\isa{monoidl}}}
1001 \put(00,20){\makebox(0,0){\isa{monoid}}}
1002 \put(40,00){\makebox(0,0){\isa{group}}}
1003 \put(20,55){\vector(0,-1){10}}
1004 \put(15,35){\vector(-1,-1){10}}
1005 \put(05,15){\vector(3,-1){30}}
1007 \caption{Subclass relationship of monoids and groups:
1008 before and after establishing the relationship
1009 \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
1010 \label{fig:subclass}
1014 For illustration, a derived definition
1015 in \isa{group} using \isa{pow{\isacharunderscore}nat}%
1016 \end{isamarkuptext}%
1024 \isacommand{definition}\isamarkupfalse%
1025 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1026 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
1027 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
1028 \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
1036 \begin{isamarkuptext}%
1037 \noindent yields the global definition of
1038 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
1039 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}}.%
1040 \end{isamarkuptext}%
1043 \isamarkupsubsection{A note on syntax%
1047 \begin{isamarkuptext}%
1048 As a convenience, class context syntax allows references
1049 to local class operations and their global counterparts
1050 uniformly; type inference resolves ambiguities. For example:%
1051 \end{isamarkuptext}%
1059 \isacommand{context}\isamarkupfalse%
1060 \ semigroup\isanewline
1061 \isakeyword{begin}\isanewline
1063 \isacommand{term}\isamarkupfalse%
1064 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1065 \isamarkupcmt{example 1%
1068 \isacommand{term}\isamarkupfalse%
1069 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1070 \isamarkupcmt{example 2%
1074 \isacommand{end}\isamarkupfalse%
1077 \isacommand{term}\isamarkupfalse%
1078 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1079 \isamarkupcmt{example 3%
1089 \begin{isamarkuptext}%
1090 \noindent Here in example 1, the term refers to the local class operation
1091 \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
1092 enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
1093 In the global context in example 3, the reference is
1094 to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
1095 \end{isamarkuptext}%
1098 \isamarkupsection{Further issues%
1102 \isamarkupsubsection{Type classes and code generation%
1106 \begin{isamarkuptext}%
1107 Turning back to the first motivation for type classes,
1108 namely overloading, it is obvious that overloading
1109 stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
1110 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
1111 targets naturally maps to Haskell type classes.
1112 The code generator framework \cite{isabelle-codegen}
1113 takes this into account. If the target language (e.g.~SML)
1114 lacks type classes, then they
1115 are implemented by an explicit dictionary construction.
1116 As example, let's go back to the power function:%
1117 \end{isamarkuptext}%
1125 \isacommand{definition}\isamarkupfalse%
1126 \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
1127 \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
1135 \begin{isamarkuptext}%
1136 \noindent This maps to Haskell as follows:%
1137 \end{isamarkuptext}%
1146 \begin{isamarkuptext}%
1149 \hspace*{0pt}module Example where {\char123}\\
1152 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
1154 \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
1155 \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
1157 \hspace*{0pt}nat ::~Integer -> Nat;\\
1158 \hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
1160 \hspace*{0pt}class Semigroup a where {\char123}\\
1161 \hspace*{0pt} ~mult ::~a -> a -> a;\\
1162 \hspace*{0pt}{\char125};\\
1164 \hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
1165 \hspace*{0pt} ~neutral ::~a;\\
1166 \hspace*{0pt}{\char125};\\
1168 \hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
1169 \hspace*{0pt}{\char125};\\
1171 \hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
1172 \hspace*{0pt} ~inverse ::~a -> a;\\
1173 \hspace*{0pt}{\char125};\\
1175 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
1176 \hspace*{0pt}inverse{\char95}int i = negate i;\\
1178 \hspace*{0pt}neutral{\char95}int ::~Integer;\\
1179 \hspace*{0pt}neutral{\char95}int = 0;\\
1181 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
1182 \hspace*{0pt}mult{\char95}int i j = i + j;\\
1184 \hspace*{0pt}instance Semigroup Integer where {\char123}\\
1185 \hspace*{0pt} ~mult = mult{\char95}int;\\
1186 \hspace*{0pt}{\char125};\\
1188 \hspace*{0pt}instance Monoidl Integer where {\char123}\\
1189 \hspace*{0pt} ~neutral = neutral{\char95}int;\\
1190 \hspace*{0pt}{\char125};\\
1192 \hspace*{0pt}instance Monoid Integer where {\char123}\\
1193 \hspace*{0pt}{\char125};\\
1195 \hspace*{0pt}instance Group Integer where {\char123}\\
1196 \hspace*{0pt} ~inverse = inverse{\char95}int;\\
1197 \hspace*{0pt}{\char125};\\
1199 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1200 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
1201 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
1203 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
1204 \hspace*{0pt}pow{\char95}int k x =\\
1205 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
1206 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
1208 \hspace*{0pt}example ::~Integer;\\
1209 \hspace*{0pt}example = pow{\char95}int 10 (-2);\\
1211 \hspace*{0pt}{\char125}%
1212 \end{isamarkuptext}%
1222 \begin{isamarkuptext}%
1223 \noindent The code in SML has explicit dictionary passing:%
1224 \end{isamarkuptext}%
1233 \begin{isamarkuptext}%
1236 \hspace*{0pt}structure Example = \\
1237 \hspace*{0pt}struct\\
1239 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1241 \hspace*{0pt}fun nat{\char95}aux i n =\\
1242 \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
1243 \hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\
1245 \hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
1247 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
1248 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
1250 \hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
1251 \hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}semigroup{\char95}monoidl A{\char95};\\
1252 \hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
1254 \hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
1255 \hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}monoidl{\char95}monoid A{\char95};\\
1257 \hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
1258 \hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}monoid{\char95}group A{\char95};\\
1259 \hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
1261 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
1263 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\
1265 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
1267 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
1269 \hspace*{0pt}val monoidl{\char95}int =\\
1270 \hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
1271 \hspace*{0pt} ~IntInf.int monoidl;\\
1273 \hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
1275 \hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
1276 \hspace*{0pt} ~IntInf.int group;\\
1278 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
1279 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
1280 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
1282 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
1283 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
1284 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
1285 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
1287 \hspace*{0pt}val example :~IntInf.int =\\
1288 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\
1290 \hspace*{0pt}end;~(*struct Example*)%
1291 \end{isamarkuptext}%
1301 \isamarkupsubsection{Inspecting the type class universe%
1305 \begin{isamarkuptext}%
1306 To facilitate orientation in complex subclass structures,
1307 two diagnostics commands are provided:
1311 \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] print a list of all classes
1312 together with associated operations etc.
1314 \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation
1315 between all classes as a Hasse diagram.
1318 \end{isamarkuptext}%
1326 \isacommand{end}\isamarkupfalse%
1336 %%% Local Variables:
1338 %%% TeX-master: "root"