src/HOL/ex/MonoidGroup.thy
 author wenzelm Tue Oct 06 17:47:28 2015 +0200 (2015-10-06) changeset 61343 5b5656a63bd6 parent 58889 5b7a9633cfa8 permissions -rw-r--r--
isabelle update_cartouches;
 wenzelm@5199 1 (* Title: HOL/ex/MonoidGroup.thy wenzelm@5199 2 Author: Markus Wenzel wenzelm@5199 3 *) wenzelm@5199 4 wenzelm@61343 5 section \Monoids and Groups as predicates over record schemes\ wenzelm@10357 6 haftmann@16417 7 theory MonoidGroup imports Main begin wenzelm@5199 8 wenzelm@5199 9 record 'a monoid_sig = wenzelm@11019 10 times :: "'a => 'a => 'a" wenzelm@5199 11 one :: 'a wenzelm@5199 12 wenzelm@9297 13 record 'a group_sig = "'a monoid_sig" + wenzelm@5199 14 inv :: "'a => 'a" wenzelm@5199 15 wenzelm@19736 16 definition wenzelm@21404 17 monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" where wenzelm@19736 18 "monoid M = (\x y z. wenzelm@11019 19 times M (times M x y) z = times M x (times M y z) \ wenzelm@19736 20 times M (one M) x = x \ times M x (one M) = x)" wenzelm@5199 21 wenzelm@21404 22 definition wenzelm@21404 23 group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" where wenzelm@19736 24 "group G = (monoid G \ (\x. times G (inv G x) x = one G))" wenzelm@5199 25 wenzelm@21404 26 definition wenzelm@11939 27 reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => wenzelm@21404 28 (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" where wenzelm@19736 29 "reverse M = M (| times := \x y. times M y x |)" wenzelm@5199 30 wenzelm@5199 31 end