|
8890
|
1 |
\begin{isabelle}%
|
|
8903
|
2 |
\isacommand{theory}~Semigroups~=~Main:\isanewline
|
|
|
3 |
\isanewline
|
|
8890
|
4 |
\isacommand{constdefs}\isanewline
|
|
|
5 |
~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
|
|
8903
|
6 |
~~{"}is\_assoc~f~{\isasymequiv}~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}\isanewline
|
|
|
7 |
\isanewline
|
|
8890
|
8 |
\isacommand{consts}\isanewline
|
|
|
9 |
~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline
|
|
|
10 |
\isacommand{axclass}\isanewline
|
|
|
11 |
~~plus\_semigroup~<~{"}term{"}\isanewline
|
|
8903
|
12 |
~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}\isanewline
|
|
|
13 |
\isanewline
|
|
8890
|
14 |
\isacommand{consts}\isanewline
|
|
|
15 |
~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline
|
|
|
16 |
\isacommand{axclass}\isanewline
|
|
|
17 |
~~times\_semigroup~<~{"}term{"}\isanewline
|
|
|
18 |
~~assoc:~{"}is\_assoc~(op~{\isasymOtimes}){"}\isanewline
|
|
|
19 |
\isanewline
|
|
|
20 |
\isacommand{end}\end{isabelle}%
|