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"
|
2907
|
22 |
left_inverse "inverse x <*> x = 1"
|
1247
|
23 |
|
|
24 |
|
|
25 |
(* abelian groups *)
|
|
26 |
|
|
27 |
axclass
|
|
28 |
agroup < group
|
|
29 |
commut "x <*> y = y <*> x"
|
|
30 |
|
|
31 |
end
|