19.1 What does this tactic ?
Ring does associative-commutative rewriting in ring and semi-ring structures. Assume you have two binary functions Å and Ä that are associative and commutative, with Å distributive on Ä, and two constants 0 and 1 that are unities for Å and Ä. A polynomial is an expression built on variables V0, V1, ... and constants by application of Å and Ä.Let an ordered product be a product of variables Vi1 Ä ... Ä Vin verifying i1 £ i2 £ ... £ in. Let a monom be the product of a constant (possibly equal to 1, in which case we omit it) and an ordered product. We can order the monoms by the lexicographic order on products of variables. Let a canonical sum be an ordered sum of monoms that are all different, i.e. each monom in the sum is strictly less than the following monom according to the lexicographic order. It is an easy theorem to show that every polynomial is equivalent (modulo the ring properties) to exactly one canonical sum. This canonical sum is called the normal form of the polynomial. So what does Ring ? It normalizes polynomials over any ring or semi-ring structure. The basic utility of Ring is to simplify ring expressions, so that the user does not have to deal manually with the theorems of associativity and commutativity.
Examples:
- In the ring of integers, the normal form of x (3 + yx + 25(1 - z)) + zx is 28x + (-24)xz + xxy.
- For the classical propositionnal calculus (or the boolean rings) the normal form is what logicians call disjunctive normal form : every formula is equivalent to a disjunction of conjunctions of atoms. (Here Å is Ú, Ä is Ù, variables are atoms and the only constants are T and F)