5250

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


2 
ID: $Id$


3 
Author: Florian Kammueller, University of Cambridge


4 


5 
Group theory via records and locales.


6 
*)


7 


8 
LocaleGroup = PiSets + Record +


9 


10 
record 'a grouptype =


11 
carrier :: "'a set"


12 
bin_op :: "['a, 'a] => 'a"


13 
inverse :: "'a => 'a"


14 
unit :: "'a"


15 


16 
constdefs

9279

17 
Group :: "('a, 'more::more) grouptype_scheme set"

5846

18 
"Group == {G. (bin_op G): carrier G > carrier G > carrier G &


19 
inverse G : carrier G > carrier G

5250

20 
& unit G : carrier G &


21 
(! x: carrier G. ! y: carrier G. !z: carrier G.


22 
(bin_op G (inverse G x) x = unit G)


23 
& (bin_op G (unit G) x = x)

5846

24 
& (bin_op G (bin_op G x y) z =


25 
bin_op G (x) (bin_op G y z)))}"

5250

26 


27 
locale groups =


28 
fixes


29 
G ::"('a, 'more :: more) grouptype_scheme"


30 
e :: "'a"


31 
binop :: "'a => 'a => 'a" (infixr "#" 80)

5846

32 
(*INV renamed from inv temporarily to avoid clash with Fun.inv*)

5848

33 
INV :: "'a => 'a" ("i'(_')")

5250

34 
assumes


35 
Group_G "G: Group"


36 
defines

5846

37 
e_def "e == unit G"


38 
binop_def "x # y == bin_op G x y"


39 
inv_def "INV == inverse G"

5250

40 


41 
end
