src/HOL/ex/MonoidGroup.thy
changeset 5199 be986f7a6def
child 9279 fb4186e20148
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/MonoidGroup.thy	Fri Jul 24 17:55:57 1998 +0200
     1.3 @@ -0,0 +1,33 @@
     1.4 +(*  Title:      HOL/ex/MonoidGroup.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel
     1.7 +    Copyright   1996 TU Muenchen
     1.8 +
     1.9 +Monoids and Groups as predicates over record schemes.
    1.10 +*)
    1.11 +
    1.12 +MonoidGroup = HOL + Record +
    1.13 +
    1.14 +
    1.15 +record 'a monoid_sig =
    1.16 +  times :: "['a, 'a] => 'a"
    1.17 +  one :: 'a
    1.18 +
    1.19 +record 'a group_sig = 'a monoid_sig +
    1.20 +  inv :: "'a => 'a"
    1.21 +
    1.22 +constdefs
    1.23 +  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) => bool"
    1.24 +  "monoid M == ALL x y z.
    1.25 +    times M (times M x y) z = times M x (times M y z) &
    1.26 +    times M (one M) x & times M x (one M) = x"
    1.27 +
    1.28 +  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
    1.29 +  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
    1.30 +
    1.31 +  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
    1.32 +    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
    1.33 +  "reverse M == M (| times := %x y. times M y x |)"
    1.34 +
    1.35 +
    1.36 +end