| author | paulson |
| Tue, 06 Jan 2004 10:50:36 +0100 | |
| changeset 14342 | 6e564092d72d |
| parent 11868 | 56db9f3a6b3e |
| permissions | -rw-r--r-- |
| 5078 | 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 |
||
|
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
6921
diff
changeset
|
10 |
IntRing = Ring + Lagrange + |
| 5078 | 11 |
|
12 |
instance int :: add_semigroup (zadd_assoc) |
|
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset
|
13 |
instance int :: add_monoid (zadd_0,zadd_0_right) |
|
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
6921
diff
changeset
|
14 |
instance int :: add_group {|Auto_tac|}
|
| 5078 | 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 |