# Theory MonoidGroup

Up to index of Isabelle/HOL/ex

theory MonoidGroup
imports Main
begin

    (*  Title:      HOL/ex/MonoidGroup.thy
        ID:         $Id: MonoidGroup.thy,v 1.9 2005/09/14 20:08:08 wenzelm Exp $
        Author:     Markus Wenzel
    *)

    header {* Monoids and Groups as predicates over record schemes *}

    theory MonoidGroup imports Main begin

    record 'a monoid_sig =
      times :: "'a => 'a => 'a"
      one :: 'a

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

    constdefs
      monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
      "monoid M == ∀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, ... :: 'b |) => bool"
      "group G == monoid G ∧ (∀x. times G (inv G x) x = one G)"

      reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
        (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
      "reverse M == M (| times := λx y. times M y x |)"

    end