--- a/src/HOL/ex/MonoidGroup.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/MonoidGroup.thy Fri Nov 17 02:20:03 2006 +0100
@@ -15,16 +15,18 @@
inv :: "'a => 'a"
definition
- monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
+ monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" where
"monoid M = (\<forall>x y z.
times M (times M x y) z = times M x (times M y z) \<and>
times M (one M) x = x \<and> times M x (one M) = x)"
- group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
+definition
+ group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" where
"group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
+definition
reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
- (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
+ (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" where
"reverse M = M (| times := \<lambda>x y. times M y x |)"
end