%
\begin{isabellebody}%
\def\isabellecontext{Classes}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Classes\isanewline
\isakeyword{imports}\ Main\ Setup\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{Introduction%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Type classes were introduced 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 achieved by splitting introduction
of the \isa{eq} function from its overloaded definitions by means
of \isa{class} and \isa{instance} declarations:
\footnote{syntax here is a kind of isabellized Haskell}
\begin{quote}
\noindent\isa{class\ eq\ where} \\
\hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
\medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
\hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
\hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
\hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
\hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
\medskip\noindent\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
\hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
\medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
\hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
\hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
\end{quote}
\noindent Type variables are annotated with (finitely 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-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
From a software engineering point of view, type classes
roughly correspond to interfaces in object-oriented languages like Java;
so, it is naturally desirable that type classes do not only
provide functions (class parameters) but also state specifications
implementations must obey. For example, the \isa{class\ eq}
above could be given the following specification, demanding that
\isa{class\ eq} is an equivalence relation obeying reflexivity,
symmetry and transitivity:
\begin{quote}
\noindent\isa{class\ eq\ where} \\
\hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
\isa{satisfying} \\
\hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
\hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
\hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
\end{quote}
\noindent From a theoretical point of view, type classes are lightweight
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 parameters together with
corresponding specifications,
\item instantiating those abstract parameters 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:
locales \cite{kammueller-locales}.
\end{enumerate}
\noindent Isar type classes also directly support code generation
in a Haskell like fashion. Internally, they are mapped to more primitive
Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
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{isa-tutorial}, for which some
familiarity is assumed.%
\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 operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
assumed to be associative:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{class}\isamarkupfalse%
\ semigroup\ {\isacharequal}\isanewline
\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
parts: the \qn{operational} part names the class parameter
(\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
(\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
yielding the global
parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
\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 parameter
\isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
\ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \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}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters
at a particular instance using common specification tools (here,
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
opens a proof that the given parameters actually conform
to the class specification. Note that the first proof step
is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
This reduces an instance judgement to the relevant primitive
proof goals; typically it is the first method applied
in an instantiation proof.
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.
\medskip Another instance of \isa{semigroup} yields the natural numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{primrec}\isamarkupfalse%
\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \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}\isanewline
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
in the primrec declaration; by default, the local name of
a class operation \isa{f} to be instantiated on type constructor
\isa{{\isasymkappa}} is mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
or the corresponding ProofGeneral button.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Lifting and parametric types%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Overloaded definitions given at a class instantiation
may include recursion over the syntactic structure of types.
As a canonical example, we model product semigroups
using our simple algebra:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\ \ \ \ \ \ \isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Associativity of product semigroups is established using
the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
associativity of the type components; these hypotheses
are legitimate due to the \isa{semigroup} constraints imposed
on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
Indeed, this pattern often occurs with parametric types
and type classes.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Subclassing%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
by extending \isa{semigroup}
with one additional parameter \isa{neutral} together
with its characteristic property:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{class}\isamarkupfalse%
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Again, we prove some instances, by
providing suitable parameter definitions and proofs for the
additional specifications. Observe that instantiations
for types with the same arity may be simultaneous:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
\ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
\ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\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}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
\ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Fully-fledged monoids are modelled by another subclass,
which does not add new parameters but tightens the specification:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{class}\isamarkupfalse%
\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
\ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\ \isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent To finish our small algebra example, we add a \isa{group} class
with a corresponding instance:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{class}\isamarkupfalse%
\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
\ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
\ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
\ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
\ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \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}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\isamarkupsection{Type classes as locales%
}
\isamarkuptrue%
%
\isamarkupsubsection{A look behind the scenes%
}
\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 other than a locale:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{class}\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}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent essentially introduces the locale%
\end{isamarkuptext}%
\isamarkuptrue%
\ %
\isadeliminvisible
%
\endisadeliminvisible
%
\isataginvisible
%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\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}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent together with corresponding constant(s):%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{consts}\isamarkupfalse%
\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent The connection to the type system is done by means
of a primitive type class%
\end{isamarkuptext}%
\isamarkuptrue%
\ %
\isadeliminvisible
%
\endisadeliminvisible
%
\isataginvisible
%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{classes}\isamarkupfalse%
\ idem\ {\isacharless}\ type%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\isadeliminvisible
%
\endisadeliminvisible
%
\isataginvisible
%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\begin{isamarkuptext}%
\noindent together with a corresponding interpretation:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This gives you the full power of the Isabelle module system;
conclusions in locale \isa{idem} are implicitly propagated
to class \isa{idem}.%
\end{isamarkuptext}%
\isamarkuptrue%
\ %
\isadeliminvisible
%
\endisadeliminvisible
%
\isataginvisible
%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
%
\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\ {\isasymotimes}{\isacharparenright}} is injective:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{lemma}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\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\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{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 \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
\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%
%
\isamarkupsubsection{Derived definitions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle locales support a concept of local definitions
in locales:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{primrec}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\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}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent If the locale \isa{group} is also a class, this local
definition is propagated onto a global definition of
\isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}}
with corresponding theorems
\isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline%
pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}.
\noindent As you can see from this example, for local
definitions you may use any specification tool
which works together with locales, such as Krauss's recursive function package
\cite{krauss2006}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{A functor analogy%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
We introduced Isar classes by analogy to type classes in
functional programming; if we reconsider this in the
context of what has been said about type classes and locales,
we can drive this analogy further by stating that type
classes essentially correspond to functors that have
a canonical interpretation as type classes.
There is also the possibility of other interpretations.
For example, \isa{list}s also form a monoid with
\isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
seems inappropriate to apply to lists
the same operations as for genuinely algebraic types.
In such a case, we can simply make a particular interpretation
of monoids for lists:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ \isacommand{qed}\isamarkupfalse%
\ auto%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This enables us to apply facts on monoids
to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}.
When using this interpretation pattern, it may also
be appropriate to map derived definitions accordingly:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{primrec}\isamarkupfalse%
\ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{interpretation}\isamarkupfalse%
\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
\ \ \isacommand{interpret}\isamarkupfalse%
\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ n\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
\ intro{\isacharunderscore}locales%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This pattern is also helpful to reuse abstract
specifications on the \emph{same} type. For example, think of a
class \isa{preorder}; for type \isa{nat}, there are at least two
possible instances: the natural order or the order induced by the
divides relation. But only one of these instances can be used for
\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract
specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Additional subclass relations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Any \isa{group} is also a \isa{monoid}; this can be made
explicit by claiming an additional subclass relation, together with
a proof of the logical difference:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{subclass}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ invl\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{with}\isamarkupfalse%
\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \isacommand{with}\isamarkupfalse%
\ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
The logical proof is carried out on the locale level.
Afterwards it is propagated
to the type system, making \isa{group} an instance of
\isa{monoid} by adding an additional edge
to the graph of subclass relations
(\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
\small
\unitlength 0.6mm
\begin{picture}(40,60)(0,0)
\put(20,60){\makebox(0,0){\isa{semigroup}}}
\put(20,40){\makebox(0,0){\isa{monoidl}}}
\put(00,20){\makebox(0,0){\isa{monoid}}}
\put(40,00){\makebox(0,0){\isa{group}}}
\put(20,55){\vector(0,-1){10}}
\put(15,35){\vector(-1,-1){10}}
\put(25,35){\vector(1,-3){10}}
\end{picture}
\hspace{8em}
\begin{picture}(40,60)(0,0)
\put(20,60){\makebox(0,0){\isa{semigroup}}}
\put(20,40){\makebox(0,0){\isa{monoidl}}}
\put(00,20){\makebox(0,0){\isa{monoid}}}
\put(40,00){\makebox(0,0){\isa{group}}}
\put(20,55){\vector(0,-1){10}}
\put(15,35){\vector(-1,-1){10}}
\put(05,15){\vector(3,-1){30}}
\end{picture}
\caption{Subclass relationship of monoids and groups:
before and after establishing the relationship
\isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
\label{fig:subclass}
\end{center}
\end{figure}
For illustration, a derived definition
in \isa{group} using \isa{pow{\isacharunderscore}nat}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{definition}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\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}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent yields the global definition of
\isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{A note on syntax%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
As a convenience, class context syntax allows references
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{context}\isamarkupfalse%
\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{term}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
\isamarkupcmt{example 1%
}
\isanewline
\isacommand{term}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
\isamarkupcmt{example 2%
}
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
\isanewline
\isanewline
\isacommand{term}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
\isamarkupcmt{example 3%
}
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Here in example 1, the term refers to the local class operation
\isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}.
In the global context in example 3, the reference is
to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Further issues%
}
\isamarkuptrue%
%
\isamarkupsubsection{Type classes and code generation%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Turning back to the first motivation for type classes,
namely overloading, it is obvious that overloading
stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
takes this into account. If the target language (e.g.~SML)
lacks type classes, then they
are implemented by an explicit dictionary construction.
As example, let's go back to the power function:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
\isacommand{definition}\isamarkupfalse%
\ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent This maps to Haskell as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
%
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
\hspace*{0pt}module Example where {\char123}\\
\hspace*{0pt}\\
\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
\hspace*{0pt}\\
\hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\
\hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\
\hspace*{0pt}\\
\hspace*{0pt}nat ::~Integer -> Nat;\\
\hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\
\hspace*{0pt}\\
\hspace*{0pt}class Semigroup a where {\char123}\\
\hspace*{0pt} ~mult ::~a -> a -> a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\
\hspace*{0pt} ~neutral ::~a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}class (Monoid a) => Group a where {\char123}\\
\hspace*{0pt} ~inverse ::~a -> a;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\
\hspace*{0pt}inverse{\char95}int i = negate i;\\
\hspace*{0pt}\\
\hspace*{0pt}neutral{\char95}int ::~Integer;\\
\hspace*{0pt}neutral{\char95}int = 0;\\
\hspace*{0pt}\\
\hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\
\hspace*{0pt}mult{\char95}int i j = i + j;\\
\hspace*{0pt}\\
\hspace*{0pt}instance Semigroup Integer where {\char123}\\
\hspace*{0pt} ~mult = mult{\char95}int;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}instance Monoidl Integer where {\char123}\\
\hspace*{0pt} ~neutral = neutral{\char95}int;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}instance Monoid Integer where {\char123}\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}instance Group Integer where {\char123}\\
\hspace*{0pt} ~inverse = inverse{\char95}int;\\
\hspace*{0pt}{\char125};\\
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\
\hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\
\hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\
\hspace*{0pt}\\
\hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\
\hspace*{0pt}pow{\char95}int k x =\\
\hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\
\hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\
\hspace*{0pt}\\
\hspace*{0pt}example ::~Integer;\\
\hspace*{0pt}example = pow{\char95}int 10 (-2);\\
\hspace*{0pt}\\
\hspace*{0pt}{\char125}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\begin{isamarkuptext}%
\noindent The code in SML has explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimquote
%
\endisadelimquote
%
\isatagquote
%
\begin{isamarkuptext}%
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
\hspace*{0pt} ~val nat{\char95}aux :~IntInf.int -> nat -> nat\\
\hspace*{0pt} ~val nat :~IntInf.int -> nat\\
\hspace*{0pt} ~type 'a semigroup\\
\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
\hspace*{0pt} ~type 'a monoidl\\
\hspace*{0pt} ~val semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup\\
\hspace*{0pt} ~val neutral :~'a monoidl -> 'a\\
\hspace*{0pt} ~type 'a monoid\\
\hspace*{0pt} ~val monoidl{\char95}monoid :~'a monoid -> 'a monoidl\\
\hspace*{0pt} ~type 'a group\\
\hspace*{0pt} ~val monoid{\char95}group :~'a group -> 'a monoid\\
\hspace*{0pt} ~val inverse :~'a group -> 'a -> 'a\\
\hspace*{0pt} ~val inverse{\char95}int :~IntInf.int -> IntInf.int\\
\hspace*{0pt} ~val neutral{\char95}int :~IntInf.int\\
\hspace*{0pt} ~val mult{\char95}int :~IntInf.int -> IntInf.int -> IntInf.int\\
\hspace*{0pt} ~val semigroup{\char95}int :~IntInf.int semigroup\\
\hspace*{0pt} ~val monoidl{\char95}int :~IntInf.int monoidl\\
\hspace*{0pt} ~val monoid{\char95}int :~IntInf.int monoid\\
\hspace*{0pt} ~val group{\char95}int :~IntInf.int group\\
\hspace*{0pt} ~val pow{\char95}nat :~'a monoid -> nat -> 'a -> 'a\\
\hspace*{0pt} ~val pow{\char95}int :~'a group -> IntInf.int -> 'a -> 'a\\
\hspace*{0pt} ~val example :~IntInf.int\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
\hspace*{0pt}\\
\hspace*{0pt}fun nat{\char95}aux i n =\\
\hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\
\hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\
\hspace*{0pt}\\
\hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
\hspace*{0pt}val semigroup{\char95}monoidl = {\char35}semigroup{\char95}monoidl :~'a monoidl -> 'a semigroup;\\
\hspace*{0pt}val neutral = {\char35}neutral :~'a monoidl -> 'a;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
\hspace*{0pt}val monoidl{\char95}monoid = {\char35}monoidl{\char95}monoid :~'a monoid -> 'a monoidl;\\
\hspace*{0pt}\\
\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
\hspace*{0pt}val monoid{\char95}group = {\char35}monoid{\char95}group :~'a group -> 'a monoid;\\
\hspace*{0pt}val inverse = {\char35}inverse :~'a group -> 'a -> 'a;\\
\hspace*{0pt}\\
\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
\hspace*{0pt}\\
\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
\hspace*{0pt}\\
\hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
\hspace*{0pt}\\
\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
\hspace*{0pt}\\
\hspace*{0pt}val monoidl{\char95}int =\\
\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int monoidl;\\
\hspace*{0pt}\\
\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
\hspace*{0pt}\\
\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
\hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\
\hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\
\hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\
\hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\
\hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
\hspace*{0pt}\\
\hspace*{0pt}val example :~IntInf.int =\\
\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
\hspace*{0pt}\\
\hspace*{0pt}end;~(*struct Example*)%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagquote
{\isafoldquote}%
%
\isadelimquote
%
\endisadelimquote
%
\isamarkupsubsection{Inspecting the type class universe%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
To facilitate orientation in complex subclass structures,
two diagnostics commands are provided:
\begin{description}
\item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] print a list of all classes
together with associated operations etc.
\item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation
between all classes as a Hasse diagram.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: