src/HOL/ex/LocaleGroup.thy

added LocaleGroup, PiSets examples;

(*  Title:      HOL/ex/LocaleGroup.thy
    ID:         $Id$
    Author:     Florian Kammueller, University of Cambridge

Group theory via records and locales.
*)

LocaleGroup =   PiSets + Record +

record 'a grouptype = 
  carrier  :: "'a set"    
  bin_op   :: "['a, 'a] => 'a"
  inverse  :: "'a => 'a"
  unit     :: "'a"

constdefs
  Group :: "('a, 'more) grouptype_scheme set"
  "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G & inverse G : carrier G -> carrier G 
             & unit G : carrier G &
             (! x: carrier G. ! y: carrier G. !z: carrier G.
                       (bin_op G (inverse G x) x = unit G) 
                     & (bin_op G (unit G) x = x) 
                     & (bin_op G (bin_op G x y) z = bin_op G (x) (bin_op G y z)))}"

locale groups =
  fixes 
    G        ::"('a, 'more :: more) grouptype_scheme"
    e        :: "'a"
    binop    :: "'a => 'a => 'a" 	(infixr "#" 80)
    inv  :: "'a => 'a"              ("_ -|"      [90]91)
  assumes
    Group_G   "G: Group"
  defines
    e_def  "e == unit G"
    binop_def "x # y == bin_op G x y"
    inv_def "x -| == inverse G x"

end