13 inverse :: "'a => 'a" |
13 inverse :: "'a => 'a" |
14 unit :: "'a" |
14 unit :: "'a" |
15 |
15 |
16 constdefs |
16 constdefs |
17 Group :: "('a, 'more) grouptype_scheme set" |
17 Group :: "('a, 'more) grouptype_scheme set" |
18 "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G & inverse G : carrier G -> carrier G |
18 "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G & |
|
19 inverse G : carrier G -> carrier G |
19 & unit G : carrier G & |
20 & unit G : carrier G & |
20 (! x: carrier G. ! y: carrier G. !z: carrier G. |
21 (! x: carrier G. ! y: carrier G. !z: carrier G. |
21 (bin_op G (inverse G x) x = unit G) |
22 (bin_op G (inverse G x) x = unit G) |
22 & (bin_op G (unit G) x = x) |
23 & (bin_op G (unit G) x = x) |
23 & (bin_op G (bin_op G x y) z = bin_op G (x) (bin_op G y z)))}" |
24 & (bin_op G (bin_op G x y) z = |
|
25 bin_op G (x) (bin_op G y z)))}" |
24 |
26 |
25 locale groups = |
27 locale groups = |
26 fixes |
28 fixes |
27 G ::"('a, 'more :: more) grouptype_scheme" |
29 G ::"('a, 'more :: more) grouptype_scheme" |
28 e :: "'a" |
30 e :: "'a" |
29 binop :: "'a => 'a => 'a" (infixr "#" 80) |
31 binop :: "'a => 'a => 'a" (infixr "#" 80) |
30 inv :: "'a => 'a" ("_ -|" [90]91) |
32 (*INV renamed from inv temporarily to avoid clash with Fun.inv*) |
|
33 INV :: "'a => 'a" ("_ -|" [90]91) |
31 assumes |
34 assumes |
32 Group_G "G: Group" |
35 Group_G "G: Group" |
33 defines |
36 defines |
34 e_def "e == unit G" |
37 e_def "e == unit G" |
35 binop_def "x # y == bin_op G x y" |
38 binop_def "x # y == bin_op G x y" |
36 inv_def "x -| == inverse G x" |
39 inv_def "INV == inverse G" |
37 |
40 |
38 end |
41 end |