src/HOL/ex/MonoidGroup.thy
 changeset 11939 c5e69470f03b parent 11019 e968e5bfe98d child 14981 e73f8140af78
equal 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`