src/HOL/AxClasses/Tutorial/Semigroups.thy
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1573 6d66b59f94a9
child 8920 af5e09b6c208
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
     1 (*  Title:      HOL/AxClasses/Tutorial/Semigroups.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Semigroups with different 'signatures'.
     6 *)
     7 
     8 Semigroups = HOL +
     9 
    10 consts
    11   "<+>"         :: "['a, 'a] => 'a"             (infixl 65)
    12   "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
    13 
    14 constdefs
    15   assoc         :: "(['a, 'a] => 'a) => bool"
    16   "assoc f == ALL x y z. f (f x y) z = f x (f y z)"
    17 
    18 
    19 (* semigroups with op <+> *)
    20 
    21 axclass
    22   plus_sg < term
    23   plus_assoc    "assoc (op <+>)"
    24 
    25 
    26 (* semigroups with op <*> *)
    27 
    28 axclass
    29   times_sg < term
    30   times_assoc   "assoc (op <*>)"
    31 
    32 end