5199

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


2 
ID: $Id$


3 
Author: Markus Wenzel


4 


5 
Monoids and Groups as predicates over record schemes.


6 
*)


7 

10357

8 
header {* Monoids and Groups *}


9 

9297

10 
theory MonoidGroup = Main:

5199

11 


12 
record 'a monoid_sig =

11019

13 
times :: "'a => 'a => 'a"

5199

14 
one :: 'a


15 

9297

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

5199

17 
inv :: "'a => 'a"


18 


19 
constdefs

11939

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

11019

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


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


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

5199

24 

11939

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

11019

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

5199

27 

11939

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

11019

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


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

5199

31 


32 
end
