The rewrite package supports rewriting with respect to both primitive and user-defined relation!equivalence . Some examples are:
, the computational equality relation ,
, the primitive equality relation of the type
theory,
, if and only if ,
, equality on the integers, modulo a
positive natural,
, equality of rationals represented as pairs of integers,
, the permutation relation on lists.
The package also supports `rewriting' with respect to any relation that is transitive but not necessarily symmetric or reflexive. This needs a bit of explaining. Proofs involving transitive relations and monotonicity properties of terms can be made very similar in structure to those involving equivalence relations and congruence properties.
For example, consider the following proof step that came up Forester's development of real analysis in Nuprl [3].
= 1
Here, the definition mono(f) is:
and the theorem monotone_le is:
The tactic
RWH 
tries to apply the conversion c once
to each subterm of clause i of the sequent and the conversion
RevLemmaC name converts lemma name into a right-to-left
rewrite rule. Other examples of monotone rewriting can be found
in Section 
.
It is interesting to note that logical implication 
can
be treated a rewrite relation, since it is transitive. When it is, we
have a generalization of forward and backward chaining.
For each user-defined relation, the user provides the rewrite package
with lemmas about transitivity, symmetry, reflexivity and strength (a
binary relation R over a type T is stronger than a relation 
over T if for all a and b in T, the relation 
implies
that 
). These lemmas are used by the package for the justification
of rewrites (see Section
).
The user also provides a declaration in an ML object that identifies relation families and extra properties of relations. These declarations are described in the next section.