
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:




