src/HOL/ex/MonoidGroup.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 21404 eb85850d3eb7
child 41460 ea56b98aee83
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/MonoidGroup.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel
     4 *)
     5 
     6 header {* Monoids and Groups as predicates over record schemes *}
     7 
     8 theory MonoidGroup imports Main begin
     9 
    10 record 'a monoid_sig =
    11   times :: "'a => 'a => 'a"
    12   one :: 'a
    13 
    14 record 'a group_sig = "'a monoid_sig" +
    15   inv :: "'a => 'a"
    16 
    17 definition
    18   monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" where
    19   "monoid M = (\<forall>x y z.
    20     times M (times M x y) z = times M x (times M y z) \<and>
    21     times M (one M) x = x \<and> times M x (one M) = x)"
    22 
    23 definition
    24   group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" where
    25   "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
    26 
    27 definition
    28   reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
    29     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" where
    30   "reverse M = M (| times := \<lambda>x y. times M y x |)"
    31 
    32 end