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))
The macro form
Suppose we have the
(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
More will be written about this as we develop the techniques.