changeset 5078 | 7b5ea59c0275 |
parent 5077 | 71043526295f |
child 5079 | 2a8ed71f791f |
5077:71043526295f | 5078:7b5ea59c0275 |
---|---|
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 |