src/HOL/ex/MonoidGroup.thy
author wenzelm
Mon Oct 30 18:24:42 2000 +0100 (2000-10-30)
changeset 10357 0d0cac129618
parent 9297 bafe45732b10
child 11019 e968e5bfe98d
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/ex/MonoidGroup.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Monoids and Groups as predicates over record schemes.
     7 *)
     8 
     9 header {* Monoids and Groups *}
    10 
    11 theory MonoidGroup = Main:
    12 
    13 record 'a monoid_sig =
    14   times :: "['a, 'a] => 'a"
    15   one :: 'a
    16 
    17 record 'a group_sig = "'a monoid_sig" +
    18   inv :: "'a => 'a"
    19 
    20 constdefs
    21   monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) => bool"
    22   "monoid M == ALL x y z.
    23     times M (times M x y) z = times M x (times M y z) &
    24     times M (one M) x = x & times M x (one M) = x"
    25 
    26   group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
    27   "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
    28 
    29   reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) =>
    30     (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
    31   "reverse M == M (| times := %x y. times M y x |)"
    32 
    33 end