doc-src/AxClass/generated/Semigroups.tex

tuned;

\begin{isabelle}%
%
\isamarkupheader{Semigroups}
\isacommand{theory}~Semigroups~=~Main:%
\begin{isamarkuptext}%
\medskip\noindent An axiomatic type class is simply a class of types
 that all meet certain \emph{axioms}. Thus, type classes may be also
 understood as type predicates --- i.e.\ abstractions over a single
 type argument $\alpha$.  Class axioms typically contain polymorphic
 constants that depend on this type $\alpha$.  These
 \emph{characteristic constants} behave like operations associated
 with the ``carrier'' type $\alpha$.

 We illustrate these basic concepts by the following formulation of
 semigroups.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
\isacommand{axclass}\isanewline
~~semigroup~<~{"}term{"}\isanewline
~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}%
\begin{isamarkuptext}%
\noindent Above we have first declared a polymorphic constant $\TIMES
 :: \alpha \To \alpha \To \alpha$ and then defined the class
 $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
 \To \tau$ is indeed an associative operator.  The $assoc$ axiom
 contains exactly one type variable, which is invisible in the above
 presentation, though.  Also note that free term variables (like $x$,
 $y$, $z$) are allowed for user convenience --- conceptually all of
 these are bound by outermost universal quantifiers.

 \medskip In general, type classes may be used to describe
 \emph{structures} with exactly one carrier $\alpha$ and a fixed
 \emph{signature}.  Different signatures require different classes.
 Subsequently, class $plus_semigroup$ represents semigroups of the
 form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
 to semigroups $(\tau, \TIMES^\tau)$.%
\end{isamarkuptext}%
\isacommand{consts}\isanewline
~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~70)\isanewline
\isacommand{axclass}\isanewline
~~plus\_semigroup~<~{"}term{"}\isanewline
~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}%
\begin{isamarkuptext}%
\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
 represent semigroups in a sense, they are certainly not the same!%
\end{isamarkuptext}%
\isacommand{end}\end{isabelle}%