5199

1 
(* Title: HOL/ex/MonoidGroup.thy


2 
ID: $Id$


3 
Author: Markus Wenzel

9297

4 
License: GPL (GNU GENERAL PUBLIC LICENSE)

5199

5 


6 
Monoids and Groups as predicates over record schemes.


7 
*)


8 

10357

9 
header {* Monoids and Groups *}


10 

9297

11 
theory MonoidGroup = Main:

5199

12 


13 
record 'a monoid_sig =

11019

14 
times :: "'a => 'a => 'a"

5199

15 
one :: 'a


16 

9297

17 
record 'a group_sig = "'a monoid_sig" +

5199

18 
inv :: "'a => 'a"


19 


20 
constdefs

11939

21 
monoid :: "( times :: 'a => 'a => 'a, one :: 'a, ... :: 'b ) => bool"

11019

22 
"monoid M == \<forall>x y z.


23 
times M (times M x y) z = times M x (times M y z) \<and>


24 
times M (one M) x = x \<and> times M x (one M) = x"

5199

25 

11939

26 
group :: "( times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b ) => bool"

11019

27 
"group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"

5199

28 

11939

29 
reverse :: "( times :: 'a => 'a => 'a, one :: 'a, ... :: 'b ) =>

11019

30 
( times :: 'a => 'a => 'a, one :: 'a, ... :: 'b )"


31 
"reverse M == M ( times := \<lambda>x y. times M y x )"

5199

32 


33 
end
