%

\begin{isabellebody}%

\def\isabellecontext{Classes}%

%

\isadelimtheory

\isanewline

\isanewline

%

\endisadelimtheory

%

\isatagtheory

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isadelimML

%

\endisadelimML

%

\isatagML

%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isadelimML

%

\endisadelimML

%

\isatagML

%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupchapter{Haskell-style classes with Isabelle/Isar%

}

\isamarkuptrue%

%

\isamarkupsection{Introduction%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Type classes were introduces by Wadler and Blott \cite{wadler89how}

  into the Haskell language, to allow for a reasonable implementation

  of overloading\footnote{throughout this tutorial, we are referring

  to classical Haskell 1.0 type classes, not considering

  later additions in expressiveness}.

  As a canonical example, a polymorphic equality function

  \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different

  types for \isa{{\isasymalpha}}, which is achieves by splitting introduction

  of the \isa{eq} function from its overloaded definitions by means

  of \isa{class} and \isa{instance} declarations:

  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\

  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}

  \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\

  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\

  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\

  \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\

  \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}

  \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\

  \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}}}

  \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\

  \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\

  \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}

  \medskip Type variables are annotated with (finitly many) classes;

  these annotations are assertions that a particular polymorphic type

  provides definitions for overloaded functions.

  Indeed, type classes not only allow for simple overloading

  but form a generic calculus, an instance of order-sorted

  algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.

  From a software enigineering point of view, type classes

  correspond to interfaces in object-oriented languages like Java;

  so, it is naturally desirable that type classes do not only

  provide functions (class operations) but also state specifications

  implementations must obey.  For example, the \isa{class\ eq}

  above could be given the following specification:

  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\

  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\

  \hspace*{2ex}\isa{satisfying} \\

  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\

  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\

  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}

  \medskip From a theoretic point of view, type classes are leightweight

  modules; Haskell type classes may be emulated by

  SML functors \cite{classes_modules}. 

  Isabelle/Isar offers a discipline of type classes which brings

  all those aspects together:

  \begin{enumerate}

    \item specifying abstract operations togehter with

       corresponding specifications,

    \item instantating those abstract operations by a particular

       type

    \item in connection with a ``less ad-hoc'' approach to overloading,

    \item with a direct link to the Isabelle module system (aka locales).

  \end{enumerate}

  Isar type classes also directly support code generation

  in as Haskell like fashion.

  This tutorial demonstrates common elements of structured specifications

  and abstract reasoning with type classes by the algebraic hierarchy of

  semigroups, monoids and groups.  Our background theory is that of

  Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some

  familiarity is assumed.

  Here we merely present the look-and-feel for end users.

  Internally, those are mapped to more primitive Isabelle concepts.

  See \cite{haftmann_wenzel2006classes} for more detail.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsection{A simple algebra example \label{sec:example}%

}

\isamarkuptrue%

%

\isamarkupsubsection{Class definition%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operation \isa{{\isasymcirc}} that is

  assumed to be associative:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{class}\isamarkupfalse%

\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline

\ \ \ \ \ \ \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

\ \ \ \ \ \ \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}%

\begin{isamarkuptext}%

\noindent This \isa{{\isasymCLASS}} specification consists of two

  parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them

  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global

  operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the

  global theorem \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}}.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Class instantiation \label{sec:class_inst}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The concrete type \isa{int} is made a \isa{semigroup}

  instance by providing a suitable definition for the class operation

  \isa{mult} and a proof for the specification of \isa{assoc}.%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline

\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%

\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent From now on, the type-checker will consider \isa{int}

  as a \isa{semigroup} automatically, i.e.\ any general results

  are immediately available on concrete instances.

  Note that the first proof step is the \isa{default} method,

  which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method.

  This boils down an instantiation judgement to the relevant primitive

  proof goals and should conveniently always be the first method applied

  in an instantiation proof.

  Another instance of \isa{semigroup} are the natural numbers:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline

\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%

\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as

  operation:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline

\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%

\ {\isacharminus}\isanewline

\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%

\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%

\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isamarkupsubsection{Subclasses%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)

  by extending \isa{semigroup}

  with one additional operation \isa{neutral} together

  with its property:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{class}\isamarkupfalse%

\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline

\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline

\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent Again, we make some instances, by

  providing suitable operation definitions and proofs for the

  additional specifications.%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline

\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%

\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline

\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%

\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

\isanewline

%

\endisadelimproof

\isanewline

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline

\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%

\ {\isacharminus}\isanewline

\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%

\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%

\ \isacommand{from}\isamarkupfalse%

\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Fully-fledged monoids are modelled by another subclass

  which does not add new operations but tightens the specification:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{class}\isamarkupfalse%

\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline

\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent Instantiations may also be given simultaneously for different

  type constructors:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%

\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \isacommand{next}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%

\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \isacommand{next}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%

\ {\isacharminus}\isanewline

\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%

\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%

\ \isacommand{from}\isamarkupfalse%

\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent To finish our small algebra example, we add a \isa{group} class

  with a corresponding instance:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{class}\isamarkupfalse%

\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline

\ \ \ \ \ \ \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

\ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline

\isanewline

\ \ \ \ \isacommand{instance}\isamarkupfalse%

\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline

\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%

\ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline

\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%

\ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse%

\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isamarkupsection{Type classes as locales%

}

\isamarkuptrue%

%

\isamarkupsubsection{A look behind the scene%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The example above gives an impression how Isar type classes work

  in practice.  As stated in the introduction, classes also provide

  a link to Isar's locale system.  Indeed, the logical core of a class

  is nothing else than a locale:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{class}\isamarkupfalse%

\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline

\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline

\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent essentially introduces the locale%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

\isanewline

\isacommand{locale}\isamarkupfalse%

\ idem\ {\isacharequal}\isanewline

\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline

\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent together with corresponding constant(s) and axclass%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{consts}\isamarkupfalse%

\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline

\isanewline

\isacommand{axclass}\isamarkupfalse%

\ idem\ {\isacharless}\ type\isanewline

\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%

\begin{isamarkuptext}%

This axclass is coupled to the locale by means of an interpretation:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{interpretation}\isamarkupfalse%

\ idem{\isacharunderscore}class{\isacharcolon}\isanewline

\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

\isacommand{by}\isamarkupfalse%

\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}\isanewline

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimML

%

\endisadelimML

%

\isatagML

%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

This give you at hand the full power of the Isabelle module system;

  conclusions in locale \isa{idem} are implicitly propagated

  to class \isa{idem}.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Abstract reasoning%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Isabelle locales enable reasoning at a general level, while results

  are implicitly transferred to all instances.  For example, we can

  now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which

  states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{lemma}\isamarkupfalse%

\ {\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

%

\isadelimproof

\ \ \ \ %

\endisadelimproof

%

\isatagproof

\isacommand{proof}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{assume}\isamarkupfalse%

\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\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%

\ simp\isanewline

\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{have}\isamarkupfalse%

\ {\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%

\ assoc\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%

\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \isacommand{next}\isamarkupfalse%

\isanewline

\ \ \ \ \isacommand{assume}\isamarkupfalse%

\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%

\ \isacommand{show}\isamarkupfalse%

\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%

\ simp\isanewline

\ \ \ \ \isacommand{qed}\isamarkupfalse%

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\begin{isamarkuptext}%

\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification

  indicates that the result is recorded within that context for later

  use.  This local theorem is also lifted to the global one \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

  \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}}.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsection{Further issues%

}

\isamarkuptrue%

%

\isamarkupsubsection{Code generation%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Turning back to the first motivation for type classes,

  namely overloading, it is obvious that overloading

  stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}}

  statements naturally maps to Haskell type classes.

  The code generator framework \cite{isabelle-codegen} 

  takes this into account.  Concerning target languages

  lacking type classes (e.g.~SML), type classes

  are implemented by explicit dictionary construction.

  As example, the natural power function on groups:%

\end{isamarkuptext}%

\isamarkuptrue%

\ \ \ \ \isacommand{fun}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline

\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline

\isanewline

\ \ \ \ \isacommand{definition}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline

\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline

\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline

\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline

\isanewline

\ \ \ \ \isacommand{definition}\isamarkupfalse%

\isanewline

\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline

\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%

\begin{isamarkuptext}%

\noindent This maps to Haskell as:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%

\ example\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%

\begin{isamarkuptext}%

\lsthaskell{Thy/code_examples/Classes.hs}

  \noindent (we have left out all other modules).

  \noindent The whole code in SML with explicit dictionary passing:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%

\ example\ {\isacharparenleft}SML\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%

\begin{isamarkuptext}%

\lstsml{Thy/code_examples/classes.ML}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{end}\isamarkupfalse%

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

\isanewline

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: