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

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