DEFREFINEMENT

prove that equiv1 refines equiv2 
Major Section:  EVENTS


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
  :rule-classes rule-classes
  :instructions instructions
  :hints hints
  :otf-flg otf-flg
  :event-name event-name
  :doc doc)
where equiv1 and equiv2 are known equivalence relations, 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 supplied is equiv1-refines-equiv2, unless event-name is supplied, in which case it is used as the name. The term supplied states that equiv1 refines equiv2. 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.