|
2281
|
1 |
(* Title: HOL/Integ/IntRing.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow and Markus Wenzel
|
|
|
4 |
Copyright 1996 TU Muenchen
|
|
|
5 |
|
|
|
6 |
The integers form a commutative ring.
|
|
|
7 |
With an application of Lagrange's lemma.
|
|
|
8 |
*)
|
|
|
9 |
|
|
|
10 |
IntRing = IntRingDefs + Lagrange +
|
|
|
11 |
|
|
|
12 |
instance int :: add_semigroup (zadd_assoc)
|
|
|
13 |
instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right)
|
|
|
14 |
instance int :: add_group (left_inv_int,minus_inv_int)
|
|
|
15 |
instance int :: add_agroup (zadd_commute)
|
|
|
16 |
instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
|
|
|
17 |
instance int :: cring (zmult_commute)
|
|
|
18 |
|
|
|
19 |
end
|