src/HOL/Integ/Group.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2281 e00c13a29eda
child 4230 eb5586526bc9
permissions -rw-r--r--
added AxClasses test;
nipkow@2281
     1
(*  Title:      HOL/Integ/Group.thy
nipkow@2281
     2
    ID:         $Id$
nipkow@2281
     3
    Author:     Tobias Nipkow
nipkow@2281
     4
    Copyright   1996 TU Muenchen
nipkow@2281
     5
nipkow@2281
     6
A little bit of group theory leading up to rings. Hence groups are additive.
nipkow@2281
     7
*)
nipkow@2281
     8
nipkow@2281
     9
Group = Set +
nipkow@2281
    10
nipkow@2281
    11
(* 0 already used in Nat *)
nipkow@2281
    12
axclass  zero < term
nipkow@2281
    13
consts   zero :: "'a::zero"
nipkow@2281
    14
nipkow@2281
    15
(* additive semigroups *)
nipkow@2281
    16
nipkow@2281
    17
axclass  add_semigroup < plus
nipkow@2281
    18
  plus_assoc   "(x + y) + z = x + (y + z)"
nipkow@2281
    19
nipkow@2281
    20
nipkow@2281
    21
(* additive monoids *)
nipkow@2281
    22
nipkow@2281
    23
axclass  add_monoid < add_semigroup, zero
nipkow@2281
    24
  zeroL    "zero + x = x"
nipkow@2281
    25
  zeroR    "x + zero = x"
nipkow@2281
    26
nipkow@2281
    27
(* additive groups *)
nipkow@2281
    28
nipkow@2281
    29
axclass  add_group < add_monoid, minus
nipkow@2281
    30
  left_inv  "(zero-x)+x = zero"
nipkow@2281
    31
  minus_inv "x-y = x + (zero-y)"
nipkow@2281
    32
nipkow@2281
    33
(* additive abelian groups *)
nipkow@2281
    34
nipkow@2281
    35
axclass  add_agroup < add_group
nipkow@2281
    36
  plus_commute  "x + y = y + x"
nipkow@2281
    37
nipkow@2281
    38
end