src/HOL/ex/MonoidGroup.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61343 5b5656a63bd6
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/ex/MonoidGroup.thy
     2     Author:     Markus Wenzel
     3 *)
     4 
     5 section {* Monoids and Groups as predicates over record schemes *}
     6 
     7 theory MonoidGroup imports Main begin
     8 
     9 record 'a monoid_sig =
    10   times :: "'a => 'a => 'a"
    11   one :: 'a
    12 
    13 record 'a group_sig = "'a monoid_sig" +
    14   inv :: "'a => 'a"
    15 
    16 definition
    17   monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" where
    18   "monoid M = (\<forall>x y z.
    19     times M (times M x y) z = times M x (times M y z) \<and>
    20     times M (one M) x = x \<and> times M x (one M) = x)"
    21 
    22 definition
    23   group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" where
    24   "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
    25 
    26 definition
    27   reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
    28     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" where
    29   "reverse M = M (| times := \<lambda>x y. times M y x |)"
    30 
    31 end