equal
deleted
inserted
replaced
|
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 The inverse is the binary `-'. Groups with unary and binary inverse are |
|
30 interdefinable: x-y := x+(zero-y) and -x := zero-x. The law left_inv is |
|
31 simply the translation of (-x)+x = zero. This characterizes groups already, |
|
32 provided we only allow (zero-x). Law minus_inv `defines' the general x-y in |
|
33 terms of the specific zero-y. |
|
34 *) |
|
35 axclass add_group < add_monoid, minus |
|
36 left_inv "(zero-x)+x = zero" |
|
37 minus_inv "x-y = x + (zero-y)" |
|
38 |
|
39 (* additive abelian groups *) |
|
40 |
|
41 axclass add_agroup < add_group |
|
42 plus_commute "x + y = y + x" |
|
43 |
|
44 end |