haftmann@20967: % haftmann@20967: \begin{isabellebody}% haftmann@20967: \def\isabellecontext{Classes}% haftmann@20967: % haftmann@20967: \isadelimtheory haftmann@20967: \isanewline haftmann@20967: \isanewline haftmann@20967: \isanewline haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: % haftmann@20967: \isatagtheory haftmann@20967: \isacommand{theory}\isamarkupfalse% haftmann@20967: \ Classes\isanewline haftmann@20967: \isakeyword{imports}\ Main\isanewline haftmann@22317: \isakeyword{begin}% haftmann@20967: \endisatagtheory haftmann@20967: {\isafoldtheory}% haftmann@20967: % haftmann@20967: \isadelimtheory haftmann@22317: \isanewline haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: % haftmann@20967: \isadelimML haftmann@22317: \isanewline haftmann@22317: % haftmann@22317: \endisadelimML haftmann@22317: % haftmann@22317: \isatagML haftmann@22317: \isacommand{ML}\isamarkupfalse% haftmann@22317: \ {\isacharverbatimopen}\isanewline haftmann@22317: CodegenSerializer{\isachardot}code{\isacharunderscore}width\ {\isacharcolon}{\isacharequal}\ {\isadigit{7}}{\isadigit{4}}{\isacharsemicolon}\isanewline haftmann@22317: {\isacharverbatimclose}\isanewline haftmann@22317: % haftmann@22317: \endisatagML haftmann@22317: {\isafoldML}% haftmann@22317: % haftmann@22317: \isadelimML haftmann@22317: % haftmann@22317: \endisadelimML haftmann@22317: % haftmann@22317: \isadelimML haftmann@20967: % haftmann@20967: \endisadelimML haftmann@20967: % haftmann@20967: \isatagML haftmann@20967: % haftmann@20967: \endisatagML haftmann@20967: {\isafoldML}% haftmann@20967: % haftmann@20967: \isadelimML haftmann@20967: % haftmann@20967: \endisadelimML haftmann@20967: % haftmann@20967: \isamarkupchapter{Haskell-style classes with Isabelle/Isar% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \isamarkupsection{Introduction% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@22317: Type classes were introduces by Wadler and Blott \cite{wadler89how} haftmann@22317: into the Haskell language, to allow for a reasonable implementation haftmann@22317: of overloading\footnote{throughout this tutorial, we are referring haftmann@22317: to classical Haskell 1.0 type classes, not considering haftmann@22317: later additions in expressiveness}. haftmann@22317: As a canonical example, a polymorphic equality function haftmann@22317: \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different haftmann@22317: types for \isa{{\isasymalpha}}, which is achieves by splitting introduction haftmann@22317: of the \isa{eq} function from its overloaded definitions by means haftmann@22317: of \isa{class} and \isa{instance} declarations: haftmann@20967: haftmann@22317: \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\ haftmann@22317: \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} haftmann@22317: haftmann@22317: \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\ haftmann@22317: \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\ haftmann@22317: \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\ haftmann@22317: \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\ haftmann@22317: \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m} haftmann@22317: haftmann@22317: \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\ haftmann@22317: \hspace*{4ex}\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}}\ {\isacharampersand}{\isacharampersand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}} haftmann@22317: haftmann@22317: \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\ haftmann@22317: \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ haftmann@22317: \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} haftmann@22317: haftmann@22317: \medskip Type variables are annotated with (finitly many) classes; haftmann@22317: these annotations are assertions that a particular polymorphic type haftmann@22317: provides definitions for overloaded functions. haftmann@22317: haftmann@22317: Indeed, type classes not only allow for simple overloading haftmann@22317: but form a generic calculus, an instance of order-sorted haftmann@22317: algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}. haftmann@22317: haftmann@22317: From a software enigineering point of view, type classes haftmann@22317: correspond to interfaces in object-oriented languages like Java; haftmann@22317: so, it is naturally desirable that type classes do not only haftmann@22317: provide functions (class operations) but also state specifications haftmann@22317: implementations must obey. For example, the \isa{class\ eq} haftmann@22317: above could be given the following specification: haftmann@22317: haftmann@22317: \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\ haftmann@22317: \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ haftmann@22317: \hspace*{2ex}\isa{satisfying} \\ haftmann@22317: \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\ haftmann@22317: \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\ haftmann@22317: \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z} haftmann@22317: haftmann@22317: \medskip From a theoretic point of view, type classes are leightweight haftmann@22317: modules; indeed, Haskell type classes may be emulated by haftmann@22317: SML functors \cite{classes_modules}. haftmann@22317: Isabelle/Isar offers a discipline of type classes which brings haftmann@22317: all those aspects together: haftmann@22317: haftmann@22317: \begin{enumerate} haftmann@22317: \item specifying abstract operations togehter with haftmann@22317: corresponding specifications, haftmann@22317: \item instantating those abstract operations by a particular haftmann@22317: type haftmann@22317: \item in connection with a ``less ad-hoc'' approach to overloading, haftmann@22317: \item with a direct link to the Isabelle module system (aka locales). haftmann@22317: \end{enumerate} haftmann@22317: haftmann@22317: Isar type classes also directly support code generation haftmann@22317: in as Haskell like fashion. haftmann@22317: haftmann@22317: This tutorial demonstrates common elements of structured specifications haftmann@22317: and abstract reasoning with type classes by the algebraic hierarchy of haftmann@22317: semigroups, monoids and groups. Our background theory is that of haftmann@22317: Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some haftmann@22317: familiarity is assumed. haftmann@22317: haftmann@22317: Here we merely present the look-and-feel for end users. haftmann@22317: Internally, those are mapped to more primitive Isabelle concepts. haftmann@22317: See \cite{haftmann_wenzel2006classes} for more detail.% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \isamarkupsection{A simple algebra example \label{sec:example}% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \isamarkupsubsection{Class definition% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@20967: Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is haftmann@20967: assumed to be associative:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{class}\isamarkupfalse% haftmann@20967: \ semigroup\ {\isacharequal}\isanewline haftmann@20967: \ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline haftmann@20967: \ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}% haftmann@20967: \begin{isamarkuptext}% haftmann@20967: \noindent This \isa{{\isasymCLASS}} specification consists of two haftmann@20967: parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them haftmann@20967: (\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global haftmann@20967: operation \isa{{\isachardoublequote}mult\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the haftmann@20967: global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \isamarkupsubsection{Class instantiation \label{sec:class_inst}% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@20967: The concrete type \isa{int} is made a \isa{semigroup} haftmann@20967: instance by providing a suitable definition for the class operation haftmann@20967: \isa{mult} and a proof for the specification of \isa{assoc}.% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@20967: \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline haftmann@22317: \ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@22317: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@22317: \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% haftmann@20967: \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% haftmann@20967: \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@20967: \noindent From now on, the type-checker will consider \isa{int} haftmann@20967: as a \isa{semigroup} automatically, i.e.\ any general results haftmann@20967: are immediately available on concrete instances. haftmann@20967: haftmann@22317: Note that the first proof step is the \isa{default} method, haftmann@22317: which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method. haftmann@22317: This boils down an instantiation judgement to the relevant primitive haftmann@22317: proof goals and should conveniently always be the first method applied haftmann@22317: in an instantiation proof. haftmann@22317: haftmann@20967: Another instance of \isa{semigroup} are the natural numbers:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@20967: \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline haftmann@22317: \ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% haftmann@22317: \ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@20967: Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as haftmann@20967: operation:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@20967: \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline haftmann@22317: \ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% haftmann@20967: \ {\isacharminus}\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% haftmann@22317: \ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse% haftmann@20967: \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isamarkupsubsection{Subclasses% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@22317: We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral) haftmann@20967: by extending \isa{semigroup} haftmann@20967: with one additional operation \isa{neutral} together haftmann@20967: with its property:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{class}\isamarkupfalse% haftmann@20967: \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline haftmann@20967: \ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline haftmann@20967: \ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}% haftmann@20967: \begin{isamarkuptext}% haftmann@20967: \noindent Again, we make some instances, by haftmann@20967: providing suitable operation definitions and proofs for the haftmann@20967: additional specifications.% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@20967: \ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline haftmann@22317: \ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% haftmann@20967: \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \isanewline haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@20967: \ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline haftmann@22317: \ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% haftmann@20967: \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \isanewline haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@20967: \ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline haftmann@22317: \ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% haftmann@20967: \ {\isacharminus}\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% haftmann@20967: \ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isacharprime}a\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse% haftmann@20967: \ \isacommand{from}\isamarkupfalse% haftmann@20967: \ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse% haftmann@20967: \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@22317: \noindent Fully-fledged monoids are modelled by another subclass haftmann@22317: which does not add new operations but tightens the specification:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{class}\isamarkupfalse% haftmann@20967: \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline haftmann@22317: \ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}% haftmann@22317: \begin{isamarkuptext}% haftmann@22317: \noindent Instantiations may also be given simultaneously for different haftmann@22317: type constructors:% haftmann@22317: \end{isamarkuptext}% haftmann@22317: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@22317: \ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% haftmann@20967: \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@22317: \ \ \ \ \isacommand{next}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% haftmann@20967: \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@22317: \ \ \ \ \isacommand{next}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% haftmann@20967: \ {\isacharminus}\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% haftmann@20967: \ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse% haftmann@20967: \ \isacommand{from}\isamarkupfalse% haftmann@20967: \ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse% haftmann@20967: \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@22317: % haftmann@22317: \begin{isamarkuptext}% haftmann@22317: \noindent To finish our small algebra example, we add a \isa{group} class haftmann@22317: with a corresponding instance:% haftmann@22317: \end{isamarkuptext}% haftmann@22317: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{class}\isamarkupfalse% haftmann@20967: \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline haftmann@20967: \ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline haftmann@20967: \ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{instance}\isamarkupfalse% haftmann@20967: \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline haftmann@22317: \ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% haftmann@20967: \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% haftmann@20967: \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% haftmann@20967: \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@22317: \isamarkupsection{Type classes as locales% haftmann@22317: } haftmann@22317: \isamarkuptrue% haftmann@22317: % haftmann@22317: \isamarkupsubsection{A look behind the scene% haftmann@22317: } haftmann@22317: \isamarkuptrue% haftmann@22317: % haftmann@22317: \begin{isamarkuptext}% haftmann@22317: % haftmann@22317: \end{isamarkuptext}% haftmann@22317: \isamarkuptrue% haftmann@22317: % haftmann@20967: \isamarkupsubsection{Abstract reasoning% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@20967: Abstract theories enable reasoning at a general level, while results haftmann@20967: are implicitly transferred to all instances. For example, we can haftmann@20967: now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which haftmann@20967: states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: \ \ \ \ \isacommand{lemma}\isamarkupfalse% haftmann@20967: \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: \ \ \ \ % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \isatagproof haftmann@20967: \isacommand{proof}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{assume}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% haftmann@20967: \ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% haftmann@20967: \ \isacommand{have}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% haftmann@20967: \ assoc\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% haftmann@20967: \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% haftmann@20967: \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \isacommand{next}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{assume}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% haftmann@20967: \ \isacommand{show}\isamarkupfalse% haftmann@20967: \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% haftmann@20967: \ simp\isanewline haftmann@20967: \ \ \ \ \isacommand{qed}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagproof haftmann@20967: {\isafoldproof}% haftmann@20967: % haftmann@20967: \isadelimproof haftmann@20967: % haftmann@20967: \endisadelimproof haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@20967: \noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification haftmann@20967: indicates that the result is recorded within that context for later haftmann@20967: use. This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of haftmann@20967: \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@22317: \isamarkupsection{Further issues% haftmann@22317: } haftmann@22317: \isamarkuptrue% haftmann@22317: % haftmann@22317: \isamarkupsubsection{Code generation% haftmann@20967: } haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \begin{isamarkuptext}% haftmann@22317: Turning back to the first motivation for type classes, haftmann@22317: namely overloading, it is obvious that overloading haftmann@22317: stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}} haftmann@22317: statements naturally maps to Haskell type classes. haftmann@22317: The code generator framework \cite{isabelle-codegen} haftmann@22317: takes this into account. Concerning target languages haftmann@22317: lacking type classes (e.g.~SML), type classes haftmann@22317: are implemented by explicit dictionary construction. haftmann@22317: As example, the natural power function on groups:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@22317: \ \ \ \ \isacommand{fun}\isamarkupfalse% haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline haftmann@20967: \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline haftmann@20967: \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{definition}\isamarkupfalse% haftmann@20967: \isanewline haftmann@22317: \ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline haftmann@20967: \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline haftmann@20967: \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline haftmann@20967: \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline haftmann@20967: \isanewline haftmann@20967: \ \ \ \ \isacommand{definition}\isamarkupfalse% haftmann@20967: \isanewline haftmann@22317: \ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline haftmann@20967: \ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}% haftmann@20967: \begin{isamarkuptext}% haftmann@22317: \noindent This maps to Haskell as:% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@22317: \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% haftmann@22317: \ example\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}% haftmann@20967: \begin{isamarkuptext}% haftmann@22317: \lsthaskell{Thy/code_examples/Classes.hs} haftmann@22317: haftmann@22317: \noindent (we have left out all other modules). haftmann@22317: haftmann@22317: \noindent The whole code in SML with explicit dictionary passing:% haftmann@22317: \end{isamarkuptext}% haftmann@22317: \isamarkuptrue% haftmann@22317: \isacommand{code{\isacharunderscore}gen}\isamarkupfalse% haftmann@22317: \ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}% haftmann@22317: \begin{isamarkuptext}% haftmann@22317: \lstsml{Thy/code_examples/classes.ML}% haftmann@20967: \end{isamarkuptext}% haftmann@20967: \isamarkuptrue% haftmann@20967: % haftmann@20967: \isadelimtheory haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: % haftmann@20967: \isatagtheory haftmann@20967: \isacommand{end}\isamarkupfalse% haftmann@20967: % haftmann@20967: \endisatagtheory haftmann@20967: {\isafoldtheory}% haftmann@20967: % haftmann@20967: \isadelimtheory haftmann@20967: % haftmann@20967: \endisadelimtheory haftmann@20967: \isanewline haftmann@20967: \end{isabellebody}% haftmann@20967: %%% Local Variables: haftmann@20967: %%% mode: latex haftmann@20967: %%% TeX-master: "root" haftmann@20967: %%% End: