| changeset 2281 | e00c13a29eda |
| 2280:eb2ba30c2981 | 2281:e00c13a29eda |
|---|---|
1 (* Title: HOL/Integ/Ring.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 Bits of rings. |
|
7 Main output: a simplification tactic for commutative rings. |
|
8 *) |
|
9 |
|
10 Ring = Group + |
|
11 |
|
12 (* Ring *) |
|
13 |
|
14 axclass ring < add_agroup, times |
|
15 times_assoc "(x*y)*z = x*(y*z)" |
|
16 distribL "x*(y+z) = x*y + x*z" |
|
17 distribR "(x+y)*z = x*z + y*z" |
|
18 |
|
19 (* Commutative ring *) |
|
20 |
|
21 axclass cring < ring |
|
22 times_commute "x*y = y*x" |
|
23 |
|
24 end |