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 `:congruence`

rule might be built is:

Example: (implies (set-equal x y) (iff (memb e x) (memb e y))).Also see defcong and see equivalence.

General Form: (implies (equiv1 xk xk-equiv) (equiv2 (fn x1... xk ...xn) (fn x1... xk-equiv ...xn)))where

`equiv1`

and `equiv2`

are known equivalence relations, `fn`

is an
`n-ary`

function symbol and the `xi`

and `xk-equiv`

are all distinct
variables. The effect of such a rule is to record that the
`equiv2`

-equivalence of `fn`

-expressions can be maintained if, while
rewriting the `kth`

argument position, `equiv1`

-equivalence is
maintained. See equivalence for a general discussion of the
issues. We say that `equiv2`

, above, is the ``outside equivalence''
in the rule and `equiv1`

is the ``inside equivalence for the `k`

th
argument''
The macro form `(defcong equiv1 equiv2 (fn x1 ... x1) k)`

is an
abbreviation for a `defthm`

of rule-class `:congruence`

that attempts to
establish that `equiv2`

is maintained by maintaining `equiv1`

in `fn`

's
`k`

th argument. The `defcong`

macro automatically generates the general
formula shown above. See defcong.

The `memb`

example above tells us that `(memb e x)`

is propositionally
equivalent to `(memb e y)`

, provided `x`

and `y`

are `set-equal`

. The
outside equivalence is `iff`

and the inside equivalence for the second
argument is `set-equal`

. If we see a `memb`

expression in a
propositional context, e.g., as a literal of a clause or test of an
`if`

(but not, for example, as an argument to `cons`

), we can rewrite
its second argument maintaining `set-equality`

. For example, a rule
stating the commutativity of `append`

(modulo set-equality) could be
applied in this context. Since equality is a refinement of all
equivalence relations, all equality rules are always available.
See refinement.

All known `:congruence`

rules about a given outside equivalence and `fn`

can be used independently. That is, consider two `:congruence`

rules
with the same outside equivalence, `equiv`

, and about the same
function `fn`

. Suppose one says that `equiv1`

is the inside equivalence
for the first argument and the other says `equiv2`

is the inside
equivalence for the second argument. Then `(fn a b)`

is `equiv`

`(fn a' b')`

provided `a`

is `equiv1`

to `a'`

and `b`

is `equiv2`

to `b'`

. This is an easy consequence of the transitivity of
`equiv`

. It permits you to think independently about the inside
equivalences.

Furthermore, it is possible that more than one inside equivalence
for a given argument slot will maintain a given outside equivalence.
For example, `(length a)`

is equal to `(length a')`

if `a`

and `a'`

are
related either by `list-equal`

or by `string-equal`

. You may prove two
(or more) `:congruence`

rules for the same slot of a function. The
result is that the system uses a new, ``generated'' equivalence
relation for that slot with the result that rules of both (or all)
kinds are available while rewriting.

`:congruence`

rules can be disabled. For example, if you have two
different inside equivalences for a given argument position and you
find that the `:`

`rewrite`

rules for one are unexpectedly preventing the
application of the desired rule, you can disable the rule that
introduced the unwanted inside equivalence.

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