|
2281
|
1 |
(* Title: HOL/Integ/Group.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1996 TU Muenchen
|
|
|
5 |
|
|
|
6 |
A little bit of group theory leading up to rings. Hence groups are additive.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Group = Set +
|
|
|
10 |
|
|
|
11 |
(* 0 already used in Nat *)
|
|
|
12 |
axclass zero < term
|
|
|
13 |
consts zero :: "'a::zero"
|
|
|
14 |
|
|
|
15 |
(* additive semigroups *)
|
|
|
16 |
|
|
|
17 |
axclass add_semigroup < plus
|
|
|
18 |
plus_assoc "(x + y) + z = x + (y + z)"
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
(* additive monoids *)
|
|
|
22 |
|
|
|
23 |
axclass add_monoid < add_semigroup, zero
|
|
|
24 |
zeroL "zero + x = x"
|
|
|
25 |
zeroR "x + zero = x"
|
|
|
26 |
|
|
|
27 |
(* additive groups *)
|
|
|
28 |
|
|
|
29 |
axclass add_group < add_monoid, minus
|
|
|
30 |
left_inv "(zero-x)+x = zero"
|
|
|
31 |
minus_inv "x-y = x + (zero-y)"
|
|
|
32 |
|
|
|
33 |
(* additive abelian groups *)
|
|
|
34 |
|
|
|
35 |
axclass add_agroup < add_group
|
|
|
36 |
plus_commute "x + y = y + x"
|
|
|
37 |
|
|
|
38 |
end
|