src/HOL/ex/MonoidGroup.thy
 changeset 9297 bafe45732b10 parent 9279 fb4186e20148 child 10357 0d0cac129618
```--- a/src/HOL/ex/MonoidGroup.thy	Thu Jul 13 11:41:06 2000 +0200
+++ b/src/HOL/ex/MonoidGroup.thy	Thu Jul 13 11:41:40 2000 +0200
@@ -1,33 +1,31 @@
(*  Title:      HOL/ex/MonoidGroup.thy
ID:         \$Id\$
Author:     Markus Wenzel

Monoids and Groups as predicates over record schemes.
*)

-MonoidGroup = HOL + Record +
-
+theory MonoidGroup = Main:

record 'a monoid_sig =
times :: "['a, 'a] => 'a"
one :: 'a

-record 'a group_sig = 'a monoid_sig +
+record 'a group_sig = "'a monoid_sig" +
inv :: "'a => 'a"

constdefs
-  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) => bool"
+  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) => bool"
"monoid M == ALL x y z.
times M (times M x y) z = times M x (times M y z) &
times M (one M) x = x & times M x (one M) = x"

-  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more::more |) => bool"
+  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
"group G == monoid G & (ALL x. times G (inv G x) x = one G)"

-  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) =>
-    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
+  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) =>
+    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
"reverse M == M (| times := %x y. times M y x |)"

-
end```