src/HOL/ex/MonoidGroup.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 14981 e73f8140af78
child 17388 495c799df31d
permissions -rw-r--r--
migrated theory headers to new format
wenzelm@5199
     1
(*  Title:      HOL/ex/MonoidGroup.thy
wenzelm@5199
     2
    ID:         $Id$
wenzelm@5199
     3
    Author:     Markus Wenzel
wenzelm@5199
     4
wenzelm@5199
     5
Monoids and Groups as predicates over record schemes.
wenzelm@5199
     6
*)
wenzelm@5199
     7
wenzelm@10357
     8
header {* Monoids and Groups *}
wenzelm@10357
     9
haftmann@16417
    10
theory MonoidGroup imports Main begin
wenzelm@5199
    11
wenzelm@5199
    12
record 'a monoid_sig =
wenzelm@11019
    13
  times :: "'a => 'a => 'a"
wenzelm@5199
    14
  one :: 'a
wenzelm@5199
    15
wenzelm@9297
    16
record 'a group_sig = "'a monoid_sig" +
wenzelm@5199
    17
  inv :: "'a => 'a"
wenzelm@5199
    18
wenzelm@5199
    19
constdefs
wenzelm@11939
    20
  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
wenzelm@11019
    21
  "monoid M == \<forall>x y z.
wenzelm@11019
    22
    times M (times M x y) z = times M x (times M y z) \<and>
wenzelm@11019
    23
    times M (one M) x = x \<and> times M x (one M) = x"
wenzelm@5199
    24
wenzelm@11939
    25
  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
wenzelm@11019
    26
  "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
wenzelm@5199
    27
wenzelm@11939
    28
  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
wenzelm@11019
    29
    (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
wenzelm@11019
    30
  "reverse M == M (| times := \<lambda>x y. times M y x |)"
wenzelm@5199
    31
wenzelm@5199
    32
end