src/HOL/ex/MonoidGroup.thy
author wenzelm
Fri Jul 24 17:55:57 1998 +0200 (1998-07-24)
changeset 5199 be986f7a6def
child 9279 fb4186e20148
permissions -rw-r--r--
added ex/MonoidGroups (record example);
moved Bin and String examples to ex;
wenzelm@5199
     1
(*  Title:      HOL/ex/MonoidGroup.thy
wenzelm@5199
     2
    ID:         $Id$
wenzelm@5199
     3
    Author:     Markus Wenzel
wenzelm@5199
     4
    Copyright   1996 TU Muenchen
wenzelm@5199
     5
wenzelm@5199
     6
Monoids and Groups as predicates over record schemes.
wenzelm@5199
     7
*)
wenzelm@5199
     8
wenzelm@5199
     9
MonoidGroup = HOL + Record +
wenzelm@5199
    10
wenzelm@5199
    11
wenzelm@5199
    12
record 'a monoid_sig =
wenzelm@5199
    13
  times :: "['a, 'a] => 'a"
wenzelm@5199
    14
  one :: 'a
wenzelm@5199
    15
wenzelm@5199
    16
record 'a group_sig = 'a monoid_sig +
wenzelm@5199
    17
  inv :: "'a => 'a"
wenzelm@5199
    18
wenzelm@5199
    19
constdefs
wenzelm@5199
    20
  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) => bool"
wenzelm@5199
    21
  "monoid M == ALL x y z.
wenzelm@5199
    22
    times M (times M x y) z = times M x (times M y z) &
wenzelm@5199
    23
    times M (one M) x & times M x (one M) = x"
wenzelm@5199
    24
wenzelm@5199
    25
  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
wenzelm@5199
    26
  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
wenzelm@5199
    27
wenzelm@5199
    28
  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
wenzelm@5199
    29
    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
wenzelm@5199
    30
  "reverse M == M (| times := %x y. times M y x |)"
wenzelm@5199
    31
wenzelm@5199
    32
wenzelm@5199
    33
end