8906
|
1 |
|
9146
|
2 |
header {* Semigroups *}
|
8906
|
3 |
|
9146
|
4 |
theory Semigroups = Main:
|
8890
|
5 |
|
8906
|
6 |
text {*
|
|
7 |
\medskip\noindent An axiomatic type class is simply a class of types
|
8907
|
8 |
that all meet certain properties, which are also called \emph{class
|
|
9 |
axioms}. Thus, type classes may be also understood as type predicates
|
|
10 |
--- i.e.\ abstractions over a single type argument $\alpha$. Class
|
|
11 |
axioms typically contain polymorphic constants that depend on this
|
|
12 |
type $\alpha$. These \emph{characteristic constants} behave like
|
|
13 |
operations associated with the ``carrier'' type $\alpha$.
|
8906
|
14 |
|
|
15 |
We illustrate these basic concepts by the following formulation of
|
|
16 |
semigroups.
|
9146
|
17 |
*}
|
8890
|
18 |
|
|
19 |
consts
|
9146
|
20 |
times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 70)
|
8906
|
21 |
axclass
|
|
22 |
semigroup < "term"
|
9146
|
23 |
assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)"
|
8906
|
24 |
|
|
25 |
text {*
|
|
26 |
\noindent Above we have first declared a polymorphic constant $\TIMES
|
|
27 |
:: \alpha \To \alpha \To \alpha$ and then defined the class
|
|
28 |
$semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
|
|
29 |
\To \tau$ is indeed an associative operator. The $assoc$ axiom
|
|
30 |
contains exactly one type variable, which is invisible in the above
|
|
31 |
presentation, though. Also note that free term variables (like $x$,
|
|
32 |
$y$, $z$) are allowed for user convenience --- conceptually all of
|
|
33 |
these are bound by outermost universal quantifiers.
|
|
34 |
|
|
35 |
\medskip In general, type classes may be used to describe
|
|
36 |
\emph{structures} with exactly one carrier $\alpha$ and a fixed
|
|
37 |
\emph{signature}. Different signatures require different classes.
|
8907
|
38 |
Below, class $plus_semigroup$ represents semigroups of the form
|
|
39 |
$(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond
|
8906
|
40 |
to semigroups $(\tau, \TIMES^\tau)$.
|
9146
|
41 |
*}
|
8906
|
42 |
|
|
43 |
consts
|
9146
|
44 |
plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Oplus>" 70)
|
8890
|
45 |
axclass
|
|
46 |
plus_semigroup < "term"
|
9146
|
47 |
assoc: "(x \<Oplus> y) \<Oplus> z = x \<Oplus> (y \<Oplus> z)"
|
8890
|
48 |
|
8906
|
49 |
text {*
|
8907
|
50 |
\noindent Even if classes $plus_semigroup$ and $semigroup$ both
|
|
51 |
represent semigroups in a sense, they are certainly not quite the
|
|
52 |
same.
|
9146
|
53 |
*}
|
8890
|
54 |
|
9146
|
55 |
end |