5199

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


2 
ID: $Id$


3 
Author: Markus Wenzel


4 
*)


5 

17388

6 
header {* Monoids and Groups as predicates over record schemes *}

10357

7 

16417

8 
theory MonoidGroup imports Main begin

5199

9 


10 
record 'a monoid_sig =

11019

11 
times :: "'a => 'a => 'a"

5199

12 
one :: 'a


13 

9297

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

5199

15 
inv :: "'a => 'a"


16 

19736

17 
definition

11939

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

19736

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

11019

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

19736

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

5199

22 

11939

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

19736

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

5199

25 

11939

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

11019

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

19736

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

5199

29 


30 
end
