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 =


14 
times :: "['a, 'a] => 'a"


15 
one :: 'a


16 

9297

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

5199

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


19 


20 
constdefs

9297

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

5199

22 
"monoid M == ALL x y z.


23 
times M (times M x y) z = times M x (times M y z) &

9279

24 
times M (one M) x = x & times M x (one M) = x"

5199

25 

9297

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

5199

27 
"group G == monoid G & (ALL x. times G (inv G x) x = one G)"


28 

9297

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


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

5199

31 
"reverse M == M ( times := %x y. times M y x )"


32 


33 
end
