1 \begin{isabelle}% |
1 \begin{isabelle}% |
2 % |
2 % |
3 \isamarkupheader{Semigroups} |
3 \isamarkupheader{Semigroups} |
4 \isacommand{theory}~Semigroups~=~Main:% |
4 \isacommand{theory}\ Semigroups\ =\ Main:% |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \medskip\noindent An axiomatic type class is simply a class of types |
6 \medskip\noindent An axiomatic type class is simply a class of types |
7 that all meet certain properties, which are also called \emph{class |
7 that all meet certain properties, which are also called \emph{class |
8 axioms}. Thus, type classes may be also understood as type predicates |
8 axioms}. Thus, type classes may be also understood as type predicates |
9 --- i.e.\ abstractions over a single type argument $\alpha$. Class |
9 --- i.e.\ abstractions over a single type argument $\alpha$. Class |
13 |
13 |
14 We illustrate these basic concepts by the following formulation of |
14 We illustrate these basic concepts by the following formulation of |
15 semigroups.% |
15 semigroups.% |
16 \end{isamarkuptext}% |
16 \end{isamarkuptext}% |
17 \isacommand{consts}\isanewline |
17 \isacommand{consts}\isanewline |
18 ~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline |
18 \ \ times\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline |
19 \isacommand{axclass}\isanewline |
19 \isacommand{axclass}\isanewline |
20 ~~semigroup~<~{"}term{"}\isanewline |
20 \ \ semigroup\ <\ {"}term{"}\isanewline |
21 ~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}% |
21 \ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}% |
22 \begin{isamarkuptext}% |
22 \begin{isamarkuptext}% |
23 \noindent Above we have first declared a polymorphic constant $\TIMES |
23 \noindent Above we have first declared a polymorphic constant $\TIMES |
24 :: \alpha \To \alpha \To \alpha$ and then defined the class |
24 :: \alpha \To \alpha \To \alpha$ and then defined the class |
25 $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau |
25 $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau |
26 \To \tau$ is indeed an associative operator. The $assoc$ axiom |
26 \To \tau$ is indeed an associative operator. The $assoc$ axiom |
35 Below, class $plus_semigroup$ represents semigroups of the form |
35 Below, class $plus_semigroup$ represents semigroups of the form |
36 $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond |
36 $(\tau, \PLUS^\tau)$, while the original $semigroup$ would correspond |
37 to semigroups $(\tau, \TIMES^\tau)$.% |
37 to semigroups $(\tau, \TIMES^\tau)$.% |
38 \end{isamarkuptext}% |
38 \end{isamarkuptext}% |
39 \isacommand{consts}\isanewline |
39 \isacommand{consts}\isanewline |
40 ~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~70)\isanewline |
40 \ \ plus\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOplus}{"}\ 70)\isanewline |
41 \isacommand{axclass}\isanewline |
41 \isacommand{axclass}\isanewline |
42 ~~plus\_semigroup~<~{"}term{"}\isanewline |
42 \ \ plus\_semigroup\ <\ {"}term{"}\isanewline |
43 ~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}% |
43 \ \ assoc:\ {"}(x\ {\isasymOplus}\ y)\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ (y\ {\isasymOplus}\ z){"}% |
44 \begin{isamarkuptext}% |
44 \begin{isamarkuptext}% |
45 \noindent Even if classes $plus_semigroup$ and $semigroup$ both |
45 \noindent Even if classes $plus_semigroup$ and $semigroup$ both |
46 represent semigroups in a sense, they are certainly not quite the |
46 represent semigroups in a sense, they are certainly not quite the |
47 same.% |
47 same.% |
48 \end{isamarkuptext}% |
48 \end{isamarkuptext}% |