doc-src/AxClass/Nat/document/Semigroups.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Nat/document/Semigroups.tex	Fri Aug 19 22:19:59 2005 +0200
@@ -0,0 +1,88 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Semigroups}%
+\isamarkuptrue%
+%
+\isamarkupheader{Semigroups%
+}
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{theory}\ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\medskip\noindent An axiomatic type class is simply a class of types
+  that all meet certain properties, which are also called \emph{class
+  axioms}. Thus, type classes may be also understood as type
+  predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class axioms typically contain polymorphic constants that
+  depend on this type \isa{{\isacharprime}a}.  These \emph{characteristic
+  constants} behave like operations associated with the ``carrier''
+  type \isa{{\isacharprime}a}.
+
+  We illustrate these basic concepts by the following formulation of
+  semigroups.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{consts}\isanewline
+\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
+  all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
+  associative operator.  The \isa{assoc} axiom contains exactly one
+  type variable, which is invisible in the above presentation, though.
+  Also note that free term variables (like \isa{x}, \isa{y},
+  \isa{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 \isa{{\isacharprime}a} and a fixed
+  \emph{signature}.  Different signatures require different classes.
+  Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
+  correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
+\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{consts}\isanewline
+\ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
+\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
+  not quite the same.%
+\end{isamarkuptext}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isamarkupfalse%
+\isacommand{end}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: