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 = Main + |
|
10 |
|
11 (* additive semigroups *) |
|
12 |
|
13 axclass add_semigroup < plus |
|
14 plus_assoc "(x + y) + z = x + (y + z)" |
|
15 |
|
16 |
|
17 (* additive monoids *) |
|
18 |
|
19 axclass add_monoid < add_semigroup, zero |
|
20 zeroL "0 + x = x" |
|
21 zeroR "x + 0 = x" |
|
22 |
|
23 (* additive groups *) |
|
24 (* |
|
25 The inverse is the binary `-'. Groups with unary and binary inverse are |
|
26 interdefinable: x-y := x+(0-y) and -x := 0-x. The law left_inv is |
|
27 simply the translation of (-x)+x = 0. This characterizes groups already, |
|
28 provided we only allow (0-x). Law minus_inv `defines' the general x-y in |
|
29 terms of the specific 0-y. |
|
30 *) |
|
31 axclass add_group < add_monoid, minus |
|
32 left_inv "(0-x)+x = 0" |
|
33 minus_inv "x-y = x + (0-y)" |
|
34 |
|
35 (* additive abelian groups *) |
|
36 |
|
37 axclass add_agroup < add_group |
|
38 plus_commute "x + y = y + x" |
|
39 |
|
40 end |
|