src/HOL/ex/MonoidGroup.thy
changeset 5199 be986f7a6def
child 9279 fb4186e20148
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/MonoidGroup.thy	Fri Jul 24 17:55:57 1998 +0200
@@ -0,0 +1,33 @@
+(*  Title:      HOL/ex/MonoidGroup.thy
+    ID:         $Id$
+    Author:     Markus Wenzel
+    Copyright   1996 TU Muenchen
+
+Monoids and Groups as predicates over record schemes.
+*)
+
+MonoidGroup = HOL + Record +
+
+
+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, ... :: '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 & times M x (one M) = x"
+
+  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
+  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
+
+  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
+    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
+  "reverse M == M (| times := %x y. times M y x |)"
+
+
+end