src/HOL/ex/MonoidGroup.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10357 0d0cac129618
child 11019 e968e5bfe98d
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  Title:      HOL/ex/MonoidGroup.thy
    ID:         $Id$
    Author:     Markus Wenzel
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Monoids and Groups as predicates over record schemes.
*)

header {* Monoids and Groups *}

theory MonoidGroup = Main:

record 'a monoid_sig =
  times :: "['a, 'a] => 'a"
  one :: 'a

record 'a group_sig = "'a monoid_sig" +
  inv :: "'a => 'a"

constdefs
  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) => bool"
  "monoid M == ALL x y z.
    times M (times M x y) z = times M x (times M y z) &
    times M (one M) x = x & times M x (one M) = x"

  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"

  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) =>
    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
  "reverse M == M (| times := %x y. times M y x |)"

end