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.