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