summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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