8890
|
1 |
\begin{isabelle}%
|
|
2 |
\isacommand{theory}~Semigroups~=~Main:%
|
|
3 |
\begin{isamarkuptext}%
|
|
4 |
\noindent Associativity of binary operations:%
|
|
5 |
\end{isamarkuptext}%
|
|
6 |
\isacommand{constdefs}\isanewline
|
|
7 |
~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
|
|
8 |
~~{"}is\_assoc~f~==~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}%
|
|
9 |
\begin{isamarkuptext}%
|
|
10 |
\medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}:
|
|
11 |
%term (latex xsymbols symbols) "op \<Oplus>";%
|
|
12 |
\end{isamarkuptext}%
|
|
13 |
\isacommand{consts}\isanewline
|
|
14 |
~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline
|
|
15 |
\isacommand{axclass}\isanewline
|
|
16 |
~~plus\_semigroup~<~{"}term{"}\isanewline
|
|
17 |
~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}%
|
|
18 |
\begin{isamarkuptext}%
|
|
19 |
\medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}:
|
|
20 |
%term (latex xsymbols symbols) "op \<Otimes>";%
|
|
21 |
\end{isamarkuptext}%
|
|
22 |
\isacommand{consts}\isanewline
|
|
23 |
~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline
|
|
24 |
\isacommand{axclass}\isanewline
|
|
25 |
~~times\_semigroup~<~{"}term{"}\isanewline
|
|
26 |
~~assoc:~{"}is\_assoc~(op~{\isasymOtimes}){"}\isanewline
|
|
27 |
\isanewline
|
|
28 |
\isacommand{end}\end{isabelle}%
|