src/HOL/ex/MonoidGroup.thy
changeset 11939 c5e69470f03b
parent 11019 e968e5bfe98d
child 14981 e73f8140af78
equal deleted inserted replaced
11938:7b594aba1300 11939:c5e69470f03b
    16 
    16 
    17 record 'a group_sig = "'a monoid_sig" +
    17 record 'a group_sig = "'a monoid_sig" +
    18   inv :: "'a => 'a"
    18   inv :: "'a => 'a"
    19 
    19 
    20 constdefs
    20 constdefs
    21   monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) => bool"
    21   monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
    22   "monoid M == \<forall>x y z.
    22   "monoid M == \<forall>x y z.
    23     times M (times M x y) z = times M x (times M y z) \<and>
    23     times M (times M x y) z = times M x (times M y z) \<and>
    24     times M (one M) x = x \<and> times M x (one M) = x"
    24     times M (one M) x = x \<and> times M x (one M) = x"
    25 
    25 
    26   group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
    26   group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
    27   "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
    27   "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
    28 
    28 
    29   reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b::more |) =>
    29   reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
    30     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
    30     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
    31   "reverse M == M (| times := \<lambda>x y. times M y x |)"
    31   "reverse M == M (| times := \<lambda>x y. times M y x |)"
    32 
    32 
    33 end
    33 end