src/HOL/ex/IntRing.thy
author paulson
Thu, 01 Oct 1998 18:30:05 +0200
changeset 5601 b6456ccd9e3e
parent 5078 7b5ea59c0275
child 6921 78a2ce8fb8df
permissions -rw-r--r--
revised for new treatment of integers
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/IntRing.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 and Markus Wenzel
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
The integers form a commutative ring.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
With an application of Lagrange's lemma.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     9
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
IntRing = IntRingDefs + Lagrange +
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
instance int :: add_semigroup (zadd_assoc)
5601
b6456ccd9e3e revised for new treatment of integers
paulson
parents: 5078
diff changeset
    13
instance int :: add_monoid (zero_int_def,zadd_nat0,zadd_nat0_right)
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
instance int :: add_group (left_inv_int,minus_inv_int)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
instance int :: add_agroup (zadd_commute)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
instance int :: cring (zmult_commute)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
end