src/HOL/ex/MonoidGroup.thy
author wenzelm
Mon, 30 Oct 2000 18:24:42 +0100
changeset 10357 0d0cac129618
parent 9297 bafe45732b10
child 11019 e968e5bfe98d
permissions -rw-r--r--
tuned;
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
9297
wenzelm
parents: 9279
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
5199
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
10357
wenzelm
parents: 9297
diff changeset
     9
header {* Monoids and Groups *}
wenzelm
parents: 9297
diff changeset
    10
9297
wenzelm
parents: 9279
diff changeset
    11
theory MonoidGroup = Main:
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    12
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    13
record 'a monoid_sig =
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    14
  times :: "['a, 'a] => 'a"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    15
  one :: 'a
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    16
9297
wenzelm
parents: 9279
diff changeset
    17
record 'a group_sig = "'a monoid_sig" +
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    18
  inv :: "'a => 'a"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    19
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    20
constdefs
9297
wenzelm
parents: 9279
diff changeset
    21
  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) => bool"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    22
  "monoid M == ALL x y z.
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    23
    times M (times M x y) z = times M x (times M y z) &
9279
fb4186e20148 added type classes to constant's type
nipkow
parents: 5199
diff changeset
    24
    times M (one M) x = x & times M x (one M) = x"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    25
9297
wenzelm
parents: 9279
diff changeset
    26
  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b::more |) => bool"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    27
  "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    28
9297
wenzelm
parents: 9279
diff changeset
    29
  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b::more |) =>
wenzelm
parents: 9279
diff changeset
    30
    (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'b |)"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    31
  "reverse M == M (| times := %x y. times M y x |)"
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    32
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    33
end