src/HOL/ex/MonoidGroup.thy
 author bulwahn Fri Jan 07 14:46:28 2011 +0100 (2011-01-07) changeset 41460 ea56b98aee83 parent 21404 eb85850d3eb7 child 58889 5b7a9633cfa8 permissions -rw-r--r--
removing obselete Id comments from HOL/ex theories
1 (*  Title:      HOL/ex/MonoidGroup.thy
2     Author:     Markus Wenzel
3 *)
5 header {* Monoids and Groups as predicates over record schemes *}
7 theory MonoidGroup imports Main begin
9 record 'a monoid_sig =
10   times :: "'a => 'a => 'a"
11   one :: 'a
13 record 'a group_sig = "'a monoid_sig" +
14   inv :: "'a => 'a"
16 definition
17   monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" where
18   "monoid M = (\<forall>x y z.
19     times M (times M x y) z = times M x (times M y z) \<and>
20     times M (one M) x = x \<and> times M x (one M) = x)"
22 definition
23   group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" where
24   "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
26 definition
27   reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
28     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" where
29   "reverse M = M (| times := \<lambda>x y. times M y x |)"
31 end