author | wenzelm |
Fri, 15 May 1998 11:34:12 +0200 | |
changeset 4932 | c90411dde8e8 |
parent 4230 | eb5586526bc9 |
permissions | -rw-r--r-- |
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 *) |
|
4230
eb5586526bc9
Redesigned the decision procedures for (Abelian) groups and commutative rings.
nipkow
parents:
2281
diff
changeset
|
28 |
(* |
eb5586526bc9
Redesigned the decision procedures for (Abelian) groups and commutative rings.
nipkow
parents:
2281
diff
changeset
|
29 |
The inverse is the binary `-'. Groups with unary and binary inverse are |
eb5586526bc9
Redesigned the decision procedures for (Abelian) groups and commutative rings.
nipkow
parents:
2281
diff
changeset
|
30 |
interdefinable: x-y := x+(zero-y) and -x := zero-x. The law left_inv is |
eb5586526bc9
Redesigned the decision procedures for (Abelian) groups and commutative rings.
nipkow
parents:
2281
diff
changeset
|
31 |
simply the translation of (-x)+x = zero. This characterizes groups already, |
eb5586526bc9
Redesigned the decision procedures for (Abelian) groups and commutative rings.
nipkow
parents:
2281
diff
changeset
|
32 |
provided we only allow (zero-x). Law minus_inv `defines' the general x-y in |
eb5586526bc9
Redesigned the decision procedures for (Abelian) groups and commutative rings.
nipkow
parents:
2281
diff
changeset
|
33 |
terms of the specific zero-y. |
eb5586526bc9
Redesigned the decision procedures for (Abelian) groups and commutative rings.
nipkow
parents:
2281
diff
changeset
|
34 |
*) |
2281 | 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 |