%

\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 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 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-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.

  From a software engeneering 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 theoretic 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

      (aka locales \cite{kammueller-locales}).

  \end{enumerate}

  \noindent Isar type classes also directly support code generation

  in a 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{isa-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-Wenzel:2006:classes} 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 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}}}} allows to define 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 boils down an instance judgement to the relevant primitive

  proof goals and should conveniently always be 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} are 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 instantiate on type constructor

  \isa{{\isasymkappa}} are 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 giving on 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 from 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 facts 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 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 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%

%

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

\end{isamarkuptext}%

\isamarkuptrue%

\ %

\isadeliminvisible

%

\endisadeliminvisible

%

\isataginvisible

%

\endisataginvisible

{\isafoldinvisible}%

%

\isadeliminvisible

%

\endisadeliminvisible

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{axclass}\isamarkupfalse%

\ idem\ {\isacharless}\ type\isanewline

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

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

\isacommand{proof}\isamarkupfalse%

\ \isacommand{qed}\isamarkupfalse%

\ {\isacharparenleft}rule\ idem{\isacharparenright}%

\endisatagquote

{\isafoldquote}%

%

\isadelimquote

%

\endisadelimquote

%

\begin{isamarkuptext}%

\noindent This gives 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%

\ %

\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 (e.g. \cite{krauss2006}).%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{A functor analogy%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

We introduced Isar classes by analogy to type classes

  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 which have

  a canonical interpretation as type classes.

  Anyway, there is also the possibility of other interpretations.

  For example, also \isa{list}s 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 simply can do a particular interpretation

  of monoids for lists:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimquote

%

\endisadelimquote

%

\isatagquote

\isacommand{interpretation}\isamarkupfalse%

\ list{\isacharunderscore}monoid{\isacharbang}{\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{\isacharbang}{\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

%

\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

  (cf.\ \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}}}