		Search-engine friendly clone of the ACL2 documentation.

Rule-classes

Refinement

Record that one equivalence relation refines another

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 automatically be known as a refinement of that third equivalence.

A rewrite rule may fail to fire because its equivalence relation is not known to be a refinement of any of those known to be permitted. See geneqv for a discussion of how ACL2 uses congruence rules to derive the permitted equivalences and how those equivalences are represented. See refinement-failure for advice on how to use break-rewrite to determine that a rule failed the refinement check and for advice about how to ``fix'' such a problem.

: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. Furthermore, :refinement lemmas are not tracked and are thus not reported in the summary. Of course, individual :rewrite rules can be disabled.

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