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.