Major Section: EVENTS
Example: (defrefinement equiv1 equiv2)See refinement.
is an abbreviation for (defthm equiv1-refines-equiv2 (implies (equiv1 x y) (equiv2 x y)) :rule-classes (:refinement))
General Form: (defrefinement equiv1 equiv2 :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg :event-name event-name :doc doc)where
equiv2are known equivalence relations,
event-name, if supplied, is a symbol and all other arguments are as specified in the documentation for
defrefinementmacro expands into a call of
defthm. The name supplied is
event-nameis supplied, in which case it is used as the name. The term supplied states that
equiv2. The rule-class
:refinementis added to the
rule-classesspecified, if it is not already there. All other arguments to the generated
defthmform are as specified by the other keyword arguments above.