author | wenzelm |
Fri, 01 Sep 1995 14:27:36 +0200 | |
changeset 1247 | 18b1441fb603 |
child 2907 | 0e272e4c7cb2 |
permissions | -rw-r--r-- |
1247 | 1 |
(* Title: HOL/AxClasses/Tutorial/Group.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Define classes "semigroup", "group", "agroup". |
|
6 |
*) |
|
7 |
||
8 |
Group = Sigs + |
|
9 |
||
10 |
(* semigroups *) |
|
11 |
||
12 |
axclass |
|
13 |
semigroup < term |
|
14 |
assoc "(x <*> y) <*> z = x <*> (y <*> z)" |
|
15 |
||
16 |
||
17 |
(* groups *) |
|
18 |
||
19 |
axclass |
|
20 |
group < semigroup |
|
21 |
left_unit "1 <*> x = x" |
|
22 |
left_inv "inv x <*> x = 1" |
|
23 |
||
24 |
||
25 |
(* abelian groups *) |
|
26 |
||
27 |
axclass |
|
28 |
agroup < group |
|
29 |
commut "x <*> y = y <*> x" |
|
30 |
||
31 |
end |