author | paulson |
Tue, 23 May 2000 18:08:52 +0200 | |
changeset 8936 | a1c426541757 |
parent 5078 | 7b5ea59c0275 |
permissions | -rw-r--r-- |
5078 | 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 |
||
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
9 |
Group = Main + |
5078 | 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 |
|
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
20 |
zeroL "0 + x = x" |
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
21 |
zeroR "x + 0 = x" |
5078 | 22 |
|
23 |
(* additive groups *) |
|
24 |
(* |
|
25 |
The inverse is the binary `-'. Groups with unary and binary inverse are |
|
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
26 |
interdefinable: x-y := x+(0-y) and -x := 0-x. The law left_inv is |
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
27 |
simply the translation of (-x)+x = 0. This characterizes groups already, |
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
28 |
provided we only allow (0-x). Law minus_inv `defines' the general x-y in |
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
29 |
terms of the specific 0-y. |
5078 | 30 |
*) |
31 |
axclass add_group < add_monoid, minus |
|
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
32 |
left_inv "(0-x)+x = 0" |
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset
|
33 |
minus_inv "x-y = x + (0-y)" |
5078 | 34 |
|
35 |
(* additive abelian groups *) |
|
36 |
||
37 |
axclass add_agroup < add_group |
|
38 |
plus_commute "x + y = y + x" |
|
39 |
||
40 |
end |