src/HOL/ex/MonoidGroup.thy
author wenzelm
Fri, 24 Jul 1998 17:55:57 +0200
changeset 5199 be986f7a6def
child 9279 fb4186e20148
permissions -rw-r--r--
added ex/MonoidGroups (record example); moved Bin and String examples to ex;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/MonoidGroup.thy
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     4
    Copyright   1996 TU Muenchen
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     5
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     6
Monoids and Groups as predicates over record schemes.
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     7
*)
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     8
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     9
MonoidGroup = HOL + Record +
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    10
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    11
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    12
record 'a monoid_sig =
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    13
  times :: "['a, 'a] => 'a"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    14
  one :: 'a
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    15
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    16
record 'a group_sig = 'a monoid_sig +
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    17
  inv :: "'a => 'a"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    18
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    19
constdefs
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    20
  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) => bool"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    21
  "monoid M == ALL x y z.
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    22
    times M (times M x y) z = times M x (times M y z) &
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    23
    times M (one M) x & times M x (one M) = x"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    24
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    25
  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    26
  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    27
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    28
  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    29
    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    30
  "reverse M == M (| times := %x y. times M y x |)"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    31
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    32
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    33
end