author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 11964 | 828ea309dc21 |
child 17132 | 153fe83804c9 |
permissions | -rw-r--r-- |
9767 | 1 |
% |
2 |
\begin{isabellebody}% |
|
9921 | 3 |
\def\isabellecontext{Semigroups}% |
8906 | 4 |
% |
10395 | 5 |
\isamarkupheader{Semigroups% |
6 |
} |
|
11964 | 7 |
\isamarkuptrue% |
8 |
\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% |
|
9 |
% |
|
8906 | 10 |
\begin{isamarkuptext}% |
11 |
\medskip\noindent An axiomatic type class is simply a class of types |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
12 |
that all meet certain properties, which are also called \emph{class |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
13 |
axioms}. Thus, type classes may be also understood as type |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
14 |
predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}. Class axioms typically contain polymorphic constants that |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
15 |
depend on this type \isa{{\isacharprime}a}. These \emph{characteristic |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
16 |
constants} behave like operations associated with the ``carrier'' |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
17 |
type \isa{{\isacharprime}a}. |
8906 | 18 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
19 |
We illustrate these basic concepts by the following formulation of |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
20 |
semigroups.% |
8906 | 21 |
\end{isamarkuptext}% |
11964 | 22 |
\isamarkuptrue% |
8890 | 23 |
\isacommand{consts}\isanewline |
10207 | 24 |
\ \ 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 |
11964 | 25 |
\isamarkupfalse% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
26 |
\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline |
11964 | 27 |
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
28 |
% |
|
8906 | 29 |
\begin{isamarkuptext}% |
10140 | 30 |
\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 |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
31 |
all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
32 |
associative operator. The \isa{assoc} axiom contains exactly one |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
33 |
type variable, which is invisible in the above presentation, though. |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
34 |
Also note that free term variables (like \isa{x}, \isa{y}, |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
35 |
\isa{z}) are allowed for user convenience --- conceptually all of |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
36 |
these are bound by outermost universal quantifiers. |
8906 | 37 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
38 |
\medskip In general, type classes may be used to describe |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
39 |
\emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
40 |
\emph{signature}. Different signatures require different classes. |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
41 |
Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
42 |
correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.% |
8906 | 43 |
\end{isamarkuptext}% |
11964 | 44 |
\isamarkuptrue% |
8906 | 45 |
\isacommand{consts}\isanewline |
10207 | 46 |
\ \ 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 |
11964 | 47 |
\isamarkupfalse% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
48 |
\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline |
11964 | 49 |
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
50 |
% |
|
8906 | 51 |
\begin{isamarkuptext}% |
10140 | 52 |
\noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
53 |
not quite the same.% |
8906 | 54 |
\end{isamarkuptext}% |
11964 | 55 |
\isamarkuptrue% |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
56 |
\isacommand{end}\isanewline |
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11964
diff
changeset
|
57 |
\isamarkupfalse% |
11964 | 58 |
\end{isabellebody}% |
9145 | 59 |
%%% Local Variables: |
60 |
%%% mode: latex |
|
61 |
%%% TeX-master: "root" |
|
62 |
%%% End: |