src/HOL/ex/Group.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8936 a1c426541757
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Integ/Group.thy
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     2
    ID:         $Id$
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author:     Tobias Nipkow
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   1996 TU Muenchen
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     5
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     6
A little bit of group theory leading up to rings. Hence groups are additive.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
     9
Group = Main +
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
(* additive semigroups *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    13
axclass  add_semigroup < plus
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
  plus_assoc   "(x + y) + z = x + (y + z)"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
(* additive monoids *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
axclass  add_monoid < add_semigroup, zero
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    20
  zeroL    "0 + x = x"
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    21
  zeroR    "x + 0 = x"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    22
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    23
(* additive groups *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    24
(*
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    25
The inverse is the binary `-'. Groups with unary and binary inverse are
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    26
interdefinable: x-y := x+(0-y) and -x := 0-x. The law left_inv is
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    27
simply the translation of (-x)+x = 0. This characterizes groups already,
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    28
provided we only allow (0-x). Law minus_inv `defines' the general x-y in
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    29
terms of the specific 0-y.
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    30
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    31
axclass  add_group < add_monoid, minus
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    32
  left_inv  "(0-x)+x = 0"
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    33
  minus_inv "x-y = x + (0-y)"
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    34
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    35
(* additive abelian groups *)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    36
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    37
axclass  add_agroup < add_group
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    38
  plus_commute  "x + y = y + x"
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    39
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    40
end