src/HOL/ex/MonoidGroup.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 11939 c5e69470f03b
child 16417 9bc16273c2d4
permissions -rw-r--r--
Merged in license change from Isabelle2004
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
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     5
Monoids and Groups as predicates over record schemes.
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     6
*)
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
     7
10357
wenzelm
parents: 9297
diff changeset
     8
header {* Monoids and Groups *}
wenzelm
parents: 9297
diff changeset
     9
9297
wenzelm
parents: 9279
diff changeset
    10
theory MonoidGroup = Main:
5199
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 =
11019
wenzelm
parents: 10357
diff changeset
    13
  times :: "'a => 'a => 'a"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    14
  one :: 'a
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    15
9297
wenzelm
parents: 9279
diff changeset
    16
record 'a group_sig = "'a monoid_sig" +
5199
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
11939
c5e69470f03b updated records;
wenzelm
parents: 11019
diff changeset
    20
  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"
11019
wenzelm
parents: 10357
diff changeset
    21
  "monoid M == \<forall>x y z.
wenzelm
parents: 10357
diff changeset
    22
    times M (times M x y) z = times M x (times M y z) \<and>
wenzelm
parents: 10357
diff changeset
    23
    times M (one M) x = x \<and> times M x (one M) = x"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    24
11939
c5e69470f03b updated records;
wenzelm
parents: 11019
diff changeset
    25
  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"
11019
wenzelm
parents: 10357
diff changeset
    26
  "group G == monoid G \<and> (\<forall>x. times G (inv G x) x = one G)"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    27
11939
c5e69470f03b updated records;
wenzelm
parents: 11019
diff changeset
    28
  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
11019
wenzelm
parents: 10357
diff changeset
    29
    (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"
wenzelm
parents: 10357
diff changeset
    30
  "reverse M == M (| times := \<lambda>x y. times M y x |)"
5199
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    31
be986f7a6def added ex/MonoidGroups (record example);
wenzelm
parents:
diff changeset
    32
end