--- a/doc-src/AxClass/Group/document/Semigroups.tex Thu Feb 26 06:39:06 2009 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Semigroups}%
-%
-\isamarkupheader{Semigroups%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\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}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}%
-\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}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
-\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}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: