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\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
296 \isacommand{instance}\isamarkupfalse%
297 \ \isacommand{proof}\isamarkupfalse%
299 \ \ \isacommand{fix}\isamarkupfalse%
300 \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
301 \ \ \isacommand{show}\isamarkupfalse%
302 \ {\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
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 type class%
650 \endisadeliminvisible
659 \endisadeliminvisible
666 \isacommand{classes}\isamarkupfalse%
667 \ idem\ {\isacharless}\ type%
677 \endisadeliminvisible
686 \endisadeliminvisible
688 \begin{isamarkuptext}%
689 \noindent together with a corresponding interpretation:%
698 \isacommand{interpretation}\isamarkupfalse%
699 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline
700 \ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
708 \begin{isamarkuptext}%
709 \noindent This gives you the full power of the Isabelle module system;
710 conclusions in locale \isa{idem} are implicitly propagated
711 to class \isa{idem}.%
717 \endisadeliminvisible
726 \endisadeliminvisible
728 \isamarkupsubsection{Abstract reasoning%
732 \begin{isamarkuptext}%
733 Isabelle locales enable reasoning at a general level, while results
734 are implicitly transferred to all instances. For example, we can
735 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
736 states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:%
745 \isacommand{lemma}\isamarkupfalse%
746 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
747 \isacommand{proof}\isamarkupfalse%
749 \ \ \isacommand{assume}\isamarkupfalse%
750 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
751 \ \ \isacommand{then}\isamarkupfalse%
752 \ \isacommand{have}\isamarkupfalse%
753 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
755 \ \ \isacommand{then}\isamarkupfalse%
756 \ \isacommand{have}\isamarkupfalse%
757 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
758 \ assoc\ \isacommand{by}\isamarkupfalse%
760 \ \ \isacommand{then}\isamarkupfalse%
761 \ \isacommand{show}\isamarkupfalse%
762 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
763 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
765 \isacommand{next}\isamarkupfalse%
767 \ \ \isacommand{assume}\isamarkupfalse%
768 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
769 \ \ \isacommand{then}\isamarkupfalse%
770 \ \isacommand{show}\isamarkupfalse%
771 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
773 \isacommand{qed}\isamarkupfalse%
782 \begin{isamarkuptext}%
783 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
784 indicates that the result is recorded within that context for later
785 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
786 \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}}.%
790 \isamarkupsubsection{Derived definitions%
794 \begin{isamarkuptext}%
795 Isabelle locales are targets which support local definitions:%
804 \isacommand{primrec}\isamarkupfalse%
805 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
806 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
807 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
815 \begin{isamarkuptext}%
816 \noindent If the locale \isa{group} is also a class, this local
817 definition is propagated onto a global definition of
818 \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
819 with corresponding theorems
821 \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
822 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
824 \noindent As you can see from this example, for local
825 definitions you may use any specification tool
826 which works together with locales, such as Krauss's recursive function package
831 \isamarkupsubsection{A functor analogy%
835 \begin{isamarkuptext}%
836 We introduced Isar classes by analogy to type classes in
837 functional programming; if we reconsider this in the
838 context of what has been said about type classes and locales,
839 we can drive this analogy further by stating that type
840 classes essentially correspond to functors that have
841 a canonical interpretation as type classes.
842 There is also the possibility of other interpretations.
843 For example, \isa{list}s also form a monoid with
844 \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
845 seems inappropriate to apply to lists
846 the same operations as for genuinely algebraic types.
847 In such a case, we can simply make a particular interpretation
848 of monoids for lists:%
857 \isacommand{interpretation}\isamarkupfalse%
858 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
859 \ \ \isacommand{proof}\isamarkupfalse%
860 \ \isacommand{qed}\isamarkupfalse%
869 \begin{isamarkuptext}%
870 \noindent This enables us to apply facts on monoids
871 to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
873 When using this interpretation pattern, it may also
874 be appropriate to map derived definitions accordingly:%
883 \isacommand{primrec}\isamarkupfalse%
884 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
885 \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
886 \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
888 \isacommand{interpretation}\isamarkupfalse%
889 \ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
890 \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
891 \isacommand{proof}\isamarkupfalse%
892 \ {\isacharminus}\isanewline
893 \ \ \isacommand{interpret}\isamarkupfalse%
894 \ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
896 \ \ \isacommand{show}\isamarkupfalse%
897 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
898 \ \ \isacommand{proof}\isamarkupfalse%
900 \ \ \ \ \isacommand{fix}\isamarkupfalse%
902 \ \ \ \ \isacommand{show}\isamarkupfalse%
903 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
904 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
905 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
906 \ \ \isacommand{qed}\isamarkupfalse%
908 \isacommand{qed}\isamarkupfalse%
909 \ intro{\isacharunderscore}locales%
917 \begin{isamarkuptext}%
918 \noindent This pattern is also helpful to reuse abstract
919 specifications on the \emph{same} type. For example, think of a
920 class \isa{preorder}; for type \isa{nat}, there are at least two
921 possible instances: the natural order or the order induced by the
922 divides relation. But only one of these instances can be used for
923 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract
924 specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.%
928 \isamarkupsubsection{Additional subclass relations%
932 \begin{isamarkuptext}%
933 Any \isa{group} is also a \isa{monoid}; this can be made
934 explicit by claiming an additional subclass relation, together with
935 a proof of the logical difference:%
944 \isacommand{subclass}\isamarkupfalse%
945 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
946 \isacommand{proof}\isamarkupfalse%
948 \ \ \isacommand{fix}\isamarkupfalse%
950 \ \ \isacommand{from}\isamarkupfalse%
951 \ invl\ \isacommand{have}\isamarkupfalse%
952 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
954 \ \ \isacommand{with}\isamarkupfalse%
955 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
956 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
958 \ \ \isacommand{with}\isamarkupfalse%
959 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
960 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
962 \isacommand{qed}\isamarkupfalse%
971 \begin{isamarkuptext}%
972 The logical proof is carried out on the locale level.
973 Afterwards it is propagated
974 to the type system, making \isa{group} an instance of
975 \isa{monoid} by adding an additional edge
976 to the graph of subclass relations
977 (\figref{fig:subclass}).
983 \begin{picture}(40,60)(0,0)
984 \put(20,60){\makebox(0,0){\isa{semigroup}}}
985 \put(20,40){\makebox(0,0){\isa{monoidl}}}
986 \put(00,20){\makebox(0,0){\isa{monoid}}}
987 \put(40,00){\makebox(0,0){\isa{group}}}
988 \put(20,55){\vector(0,-1){10}}
989 \put(15,35){\vector(-1,-1){10}}
990 \put(25,35){\vector(1,-3){10}}
993 \begin{picture}(40,60)(0,0)
994 \put(20,60){\makebox(0,0){\isa{semigroup}}}
995 \put(20,40){\makebox(0,0){\isa{monoidl}}}
996 \put(00,20){\makebox(0,0){\isa{monoid}}}
997 \put(40,00){\makebox(0,0){\isa{group}}}
998 \put(20,55){\vector(0,-1){10}}
999 \put(15,35){\vector(-1,-1){10}}
1000 \put(05,15){\vector(3,-1){30}}
1002 \caption{Subclass relationship of monoids and groups:
1003 before and after establishing the relationship
1004 \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
1005 \label{fig:subclass}
1009 For illustration, a derived definition
1010 in \isa{group} using \isa{pow{\isacharunderscore}nat}%
1011 \end{isamarkuptext}%
1019 \isacommand{definition}\isamarkupfalse%
1020 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1021 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
1022 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
1023 \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
1031 \begin{isamarkuptext}%
1032 \noindent yields the global definition of
1033 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
1034 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}}.%
1035 \end{isamarkuptext}%
1038 \isamarkupsubsection{A note on syntax%
1042 \begin{isamarkuptext}%
1043 As a convenience, class context syntax allows references
1044 to local class operations and their global counterparts
1045 uniformly; type inference resolves ambiguities. For example:%
1046 \end{isamarkuptext}%
1054 \isacommand{context}\isamarkupfalse%
1055 \ semigroup\isanewline
1056 \isakeyword{begin}\isanewline
1058 \isacommand{term}\isamarkupfalse%
1059 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1060 \isamarkupcmt{example 1%
1063 \isacommand{term}\isamarkupfalse%
1064 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1065 \isamarkupcmt{example 2%
1069 \isacommand{end}\isamarkupfalse%
1072 \isacommand{term}\isamarkupfalse%
1073 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
1074 \isamarkupcmt{example 3%
1084 \begin{isamarkuptext}%
1085 \noindent Here in example 1, the term refers to the local class operation
1086 \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
1087 enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
1088 In the global context in example 3, the reference is
1089 to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
1090 \end{isamarkuptext}%
1093 \isamarkupsection{Further issues%
1097 \isamarkupsubsection{Type classes and code generation%
1101 \begin{isamarkuptext}%
1102 Turning back to the first motivation for type classes,
1103 namely overloading, it is obvious that overloading
1104 stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
1105 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
1106 targets naturally maps to Haskell type classes.
1107 The code generator framework \cite{isabelle-codegen}
1108 takes this into account. If the target language (e.g.~SML)
1109 lacks type classes, then they
1110 are implemented by an explicit dictionary construction.
1111 As example, let's go back to the power function:%
1112 \end{isamarkuptext}%
1120 \isacommand{definition}\isamarkupfalse%
1121 \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
1122 \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
1130 \begin{isamarkuptext}%
1131 \noindent This maps to Haskell as follows:%
1132 \end{isamarkuptext}%
1141 \begin{isamarkuptext}%
1144 \hspace*{0pt}module Example where {\char123}\\
1146 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
1148 \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
1149 \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
1151 \hspace*{0pt}nat ::~Integer -> Nat;\\
1152 \hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
1154 \hspace*{0pt}class Semigroup a where {\char123}\\
1155 \hspace*{0pt} ~mult ::~a -> a -> a;\\
1156 \hspace*{0pt}{\char125};\\
1158 \hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
1159 \hspace*{0pt} ~neutral ::~a;\\
1160 \hspace*{0pt}{\char125};\\
1162 \hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
1163 \hspace*{0pt}{\char125};\\
1165 \hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
1166 \hspace*{0pt} ~inverse ::~a -> a;\\
1167 \hspace*{0pt}{\char125};\\
1169 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
1170 \hspace*{0pt}inverse{\char95}int i = negate i;\\
1172 \hspace*{0pt}neutral{\char95}int ::~Integer;\\
1173 \hspace*{0pt}neutral{\char95}int = 0;\\
1175 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
1176 \hspace*{0pt}mult{\char95}int i j = i + j;\\
1178 \hspace*{0pt}instance Semigroup Integer where {\char123}\\
1179 \hspace*{0pt} ~mult = mult{\char95}int;\\
1180 \hspace*{0pt}{\char125};\\
1182 \hspace*{0pt}instance Monoidl Integer where {\char123}\\
1183 \hspace*{0pt} ~neutral = neutral{\char95}int;\\
1184 \hspace*{0pt}{\char125};\\
1186 \hspace*{0pt}instance Monoid Integer where {\char123}\\
1187 \hspace*{0pt}{\char125};\\
1189 \hspace*{0pt}instance Group Integer where {\char123}\\
1190 \hspace*{0pt} ~inverse = inverse{\char95}int;\\
1191 \hspace*{0pt}{\char125};\\
1193 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1194 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
1195 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
1197 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
1198 \hspace*{0pt}pow{\char95}int k x =\\
1199 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
1200 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
1202 \hspace*{0pt}example ::~Integer;\\
1203 \hspace*{0pt}example = pow{\char95}int 10 (-2);\\
1205 \hspace*{0pt}{\char125}%
1206 \end{isamarkuptext}%
1216 \begin{isamarkuptext}%
1217 \noindent The code in SML has explicit dictionary passing:%
1218 \end{isamarkuptext}%
1227 \begin{isamarkuptext}%
1230 \hspace*{0pt}structure Example :~sig\\
1231 \hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
1232 \hspace*{0pt} ~val nat{\char95}aux :~IntInf.int -> nat -> nat\\
1233 \hspace*{0pt} ~val nat :~IntInf.int -> nat\\
1234 \hspace*{0pt} ~type 'a semigroup\\
1235 \hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
1236 \hspace*{0pt} ~type 'a monoidl\\
1237 \hspace*{0pt} ~val semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup\\
1238 \hspace*{0pt} ~val neutral :~'a monoidl -> 'a\\
1239 \hspace*{0pt} ~type 'a monoid\\
1240 \hspace*{0pt} ~val monoidl{\char95}monoid :~'a monoid -> 'a monoidl\\
1241 \hspace*{0pt} ~type 'a group\\
1242 \hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\
1243 \hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\
1244 \hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\
1245 \hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\
1246 \hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\
1247 \hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\
1248 \hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\
1249 \hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\
1250 \hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\
1251 \hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\
1252 \hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\
1253 \hspace*{0pt} ~val example :~IntInf.int\\
1254 \hspace*{0pt}end = struct\\
1256 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1258 \hspace*{0pt}fun nat{\char95}aux i n =\\
1259 \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
1260 \hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\
1262 \hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
1264 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
1265 \hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
1267 \hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
1268 \hspace*{0pt}val semigroup{\char95}monoidl = {\char35}semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup;\\
1269 \hspace*{0pt}val neutral = {\char35}neutral :~'a monoidl -> 'a;\\
1271 \hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
1272 \hspace*{0pt}val monoidl{\char95}monoid = {\char35}monoidl{\char95}monoid :~'a monoid -> 'a monoidl;\\
1274 \hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
1275 \hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\
1276 \hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\
1278 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
1280 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
1282 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
1284 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
1286 \hspace*{0pt}val monoidl{\char95}int =\\
1287 \hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
1288 \hspace*{0pt} ~IntInf.int monoidl;\\
1290 \hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
1292 \hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
1293 \hspace*{0pt} ~IntInf.int group;\\
1295 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
1296 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
1297 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
1299 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
1300 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
1301 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
1302 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
1304 \hspace*{0pt}val example :~IntInf.int =\\
1305 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
1307 \hspace*{0pt}end;~(*struct Example*)%
1308 \end{isamarkuptext}%
1318 \isamarkupsubsection{Inspecting the type class universe%
1322 \begin{isamarkuptext}%
1323 To facilitate orientation in complex subclass structures,
1324 two diagnostics commands are provided:
1328 \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] print a list of all classes
1329 together with associated operations etc.
1331 \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation
1332 between all classes as a Hasse diagram.
1335 \end{isamarkuptext}%
1343 \isacommand{end}\isamarkupfalse%
1353 %%% Local Variables:
1355 %%% TeX-master: "root"