src/HOL/ex/LocaleGroup.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9279 fb4186e20148
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/LocaleGroup.thy
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     3
    Author:     Florian Kammueller, University of Cambridge
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     4
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     5
Group theory via records and locales.
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     6
*)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     7
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     8
LocaleGroup =   PiSets + Record +
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     9
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    10
record 'a grouptype = 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    11
  carrier  :: "'a set"    
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    12
  bin_op   :: "['a, 'a] => 'a"
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    13
  inverse  :: "'a => 'a"
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    14
  unit     :: "'a"
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    15
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    16
constdefs
9279
fb4186e20148 added type classes to constant's type
nipkow
parents: 5848
diff changeset
    17
  Group :: "('a, 'more::more) grouptype_scheme set"
5846
paulson
parents: 5250
diff changeset
    18
  "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G &
paulson
parents: 5250
diff changeset
    19
	        inverse G : carrier G -> carrier G 
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    20
             & unit G : carrier G &
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    21
             (! x: carrier G. ! y: carrier G. !z: carrier G.
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    22
                       (bin_op G (inverse G x) x = unit G) 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    23
                     & (bin_op G (unit G) x = x) 
5846
paulson
parents: 5250
diff changeset
    24
                     & (bin_op G (bin_op G x y) z =
paulson
parents: 5250
diff changeset
    25
			bin_op G (x) (bin_op G y z)))}"
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    26
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    27
locale groups =
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    28
  fixes 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    29
    G        ::"('a, 'more :: more) grouptype_scheme"
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    30
    e        :: "'a"
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    31
    binop    :: "'a => 'a => 'a" 	(infixr "#" 80)
5846
paulson
parents: 5250
diff changeset
    32
	(*INV renamed from inv temporarily to avoid clash with Fun.inv*)
5848
99dea3c24efb changed inverse syntax from x-| to i(x)
paulson
parents: 5846
diff changeset
    33
    INV      :: "'a => 'a"              ("i'(_')")
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    34
  assumes
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    35
    Group_G   "G: Group"
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    36
  defines
5846
paulson
parents: 5250
diff changeset
    37
    e_def      "e == unit G"
paulson
parents: 5250
diff changeset
    38
    binop_def  "x # y == bin_op G x y"
paulson
parents: 5250
diff changeset
    39
    inv_def    "INV == inverse G"
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    40
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    41
end