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.