src/HOL/AxClasses/Tutorial/Group.thy
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1247 18b1441fb603
child 2907 0e272e4c7cb2
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
     1 (*  Title:      HOL/AxClasses/Tutorial/Group.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Define classes "semigroup", "group", "agroup".
     6 *)
     7 
     8 Group = Sigs +
     9 
    10 (* semigroups *)
    11 
    12 axclass
    13   semigroup < term
    14   assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
    15 
    16 
    17 (* groups *)
    18 
    19 axclass
    20   group < semigroup
    21   left_unit     "1 <*> x = x"
    22   left_inv      "inv x <*> x = 1"
    23 
    24 
    25 (* abelian groups *)
    26 
    27 axclass
    28   agroup < group
    29   commut        "x <*> y = y <*> x"
    30 
    31 end