REFINEMENT

record that one equivalence relation refines another
```Major Section:  RULE-CLASSES
```

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. An example `:``corollary` formula from which a `:refinement` rule might be built is:

```Example:
(implies (bag-equal x y) (set-equal y x)).
```
Also see defrefinement.

```General Form:
(implies (equiv1 x y) (equiv2 x y))
```
`Equiv1` and `equiv2` must be known equivalence relations. The effect of such a rule is to record that `equiv1` is a refinement of `equiv2`. This means that `equiv1` `:``rewrite` rules may be used while trying to maintain `equiv2`. See equivalence for a general discussion of the issues.

The macro form `(defrefinement equiv1 equiv2)` is an abbreviation for a `defthm` of rule-class `:refinement` that establishes that `equiv1` is a refinement of `equiv2`. See defrefinement.

Suppose we have the `:``rewrite` rule

```(bag-equal (append a b) (append b a))
```
which states that `append` is commutative modulo bag-equality. Suppose further we have established that bag-equality refines set-equality. Then when we are simplifying `append` expressions while maintaining set-equality we use `append`'s commutativity property, even though it was proved for bag-equality.

Equality is known to be a refinement of all equivalence relations. The transitive closure of the refinement relation is maintained, so if `set-equality`, say, is shown to be a refinement of some third sense of equivalence, then `bag-equality` will automatially be known as a refinement of that third equivalence.

`:refinement` lemmas cannot be disabled. That is, once one equivalence relation has been shown to be a refinement of another, there is no way to prevent the system from using that information. Of course, individual `:``rewrite` rules can be disabled.

More will be written about this as we develop the techniques.