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))
equiv2must be known equivalence relations. The effect of such a rule is to record that
equiv1is a refinement of
equiv2. This means that
rewriterules 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
defthm of rule-class
:refinement that establishes that
equiv1 is a
equiv2. See defrefinement.
Suppose we have the
(bag-equal (append a b) (append b a))which states that
appendis commutative modulo bag-equality. Suppose further we have established that bag-equality refines set-equality. Then when we are simplifying
appendexpressions 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
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.