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

src/HOL/ex/Group.thy

author | nipkow |

Fri, 24 Nov 2000 16:49:27 +0100 | |

changeset 10519 | ade64af4c57c |

parent 8936 | a1c426541757 |

permissions | -rw-r--r-- |

hide many names from Datatype_Universe.

(* Title: HOL/Integ/Group.thy ID: $Id$ Author: Tobias Nipkow Copyright 1996 TU Muenchen A little bit of group theory leading up to rings. Hence groups are additive. *) Group = Main + (* additive semigroups *) axclass add_semigroup < plus plus_assoc "(x + y) + z = x + (y + z)" (* additive monoids *) axclass add_monoid < add_semigroup, zero 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+(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 "(0-x)+x = 0" minus_inv "x-y = x + (0-y)" (* additive abelian groups *) axclass add_agroup < add_group plus_commute "x + y = y + x" end