author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8936  a1c426541757 
permissions  rwrr 
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: xy := x+(0y) and x := 0x. 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 (0x). Law minus_inv `defines' the general xy 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 0y. 
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 "(0x)+x = 0" 
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

33 
minus_inv "xy = x + (0y)" 
5078  34 

35 
(* additive abelian groups *) 

36 

37 
axclass add_agroup < add_group 

38 
plus_commute "x + y = y + x" 

39 

40 
end 