12 one :: 'a |
12 one :: 'a |
13 |
13 |
14 record 'a group_sig = "'a monoid_sig" + |
14 record 'a group_sig = "'a monoid_sig" + |
15 inv :: "'a => 'a" |
15 inv :: "'a => 'a" |
16 |
16 |
17 constdefs |
17 definition |
18 monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" |
18 monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" |
19 "monoid M == \<forall>x y z. |
19 "monoid M = (\<forall>x y z. |
20 times M (times M x y) z = times M x (times M y z) \<and> |
20 times M (times M x y) z = times M x (times M y z) \<and> |
21 times M (one M) x = x \<and> times M x (one M) = x" |
21 times M (one M) x = x \<and> times M x (one M) = x)" |
22 |
22 |
23 group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" |
23 group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" |
24 "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)" |
24 "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))" |
25 |
25 |
26 reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => |
26 reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => |
27 (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" |
27 (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" |
28 "reverse M == M (| times := \<lambda>x y. times M y x |)" |
28 "reverse M = M (| times := \<lambda>x y. times M y x |)" |
29 |
29 |
30 end |
30 end |