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 |
|
|
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
|