Defrefinement
Prove that equiv1 refines equiv2
Example:
(defrefinement equiv1 equiv2)
is an abbreviation for
(defthm equiv1-refines-equiv2
(implies (equiv1 x y) (equiv2 x y))
:rule-classes (:refinement))
See refinement.
General Form:
(defrefinement equiv1 equiv2
:package package
:event-name event-name
:rule-classes rule-classes
:instructions instructions
:hints hints
:otf-flg otf-flg)
where equiv1 and equiv2 are known equivalence relations;
package, if supplied, is one of :current, :equiv1, :equiv2
or :legacy; event-name, if supplied, is a symbol; and all other
arguments are as specified in the documentation for defthm. The
defrefinement macro expands into a call of defthm. The name of
the defthm event is equiv1-refines-equiv2, unless an
:event-name keyword argument is supplied, in which case event-name
is used as the name. The package of symbols generated, such as variables
and defthm names, is determined by the package argument: if it is
not supplied or its value is :current, then the current-package
is used; if its value is :equiv1 or :legacy, then the package of
:equiv1 is used; if its value is :equiv2, then the package of
:equiv2 is used. The rule-class :refinement is added to the
rule-classes specified, if it is not already there. All other
arguments to the generated defthm form are as specified by the other
keyword arguments above. The term generated for the defthm event
states that equiv1 refines equiv2.
