## REFINEMENT

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

See rule-classes for a general discussion of rule classes, including how they
are used to build rules from formulas and a discussion of the various
keywords in a rule class description.

Example:
(defthm bag-equal-refines-set-equal
(implies (bag-equal x y)
(set-equal y x))
:rule-classes :refinement)

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.