summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ex/Group.thy

changeset 8936 | a1c426541757 |

parent 5078 | 7b5ea59c0275 |

--- a/src/HOL/ex/Group.thy Tue May 23 18:06:22 2000 +0200 +++ b/src/HOL/ex/Group.thy Tue May 23 18:08:52 2000 +0200 @@ -6,11 +6,7 @@ A little bit of group theory leading up to rings. Hence groups are additive. *) -Group = Set + - -(* 0 already used in Nat *) -axclass zero < term -consts zero :: "'a::zero" +Group = Main + (* additive semigroups *) @@ -21,20 +17,20 @@ (* additive monoids *) axclass add_monoid < add_semigroup, zero - zeroL "zero + x = x" - zeroR "x + zero = x" + zeroL "0 + x = x" + zeroR "x + 0 = x" (* additive groups *) (* The inverse is the binary `-'. Groups with unary and binary inverse are -interdefinable: x-y := x+(zero-y) and -x := zero-x. The law left_inv is -simply the translation of (-x)+x = zero. This characterizes groups already, -provided we only allow (zero-x). Law minus_inv `defines' the general x-y in -terms of the specific zero-y. +interdefinable: x-y := x+(0-y) and -x := 0-x. The law left_inv is +simply the translation of (-x)+x = 0. This characterizes groups already, +provided we only allow (0-x). Law minus_inv `defines' the general x-y in +terms of the specific 0-y. *) axclass add_group < add_monoid, minus - left_inv "(zero-x)+x = zero" - minus_inv "x-y = x + (zero-y)" + left_inv "(0-x)+x = 0" + minus_inv "x-y = x + (0-y)" (* additive abelian groups *)