Defequiv
Prove that a function is an equivalence relation
Example:
(defequiv set-equal)
is an abbreviation for
(defthm set-equal-is-an-equivalence
(and (booleanp (set-equal x y))
(set-equal x x)
(implies (set-equal x y) (set-equal y x))
(implies (and (set-equal x y)
(set-equal y z))
(set-equal x z)))
:rule-classes (:equivalence))
See equivalence.
General Form:
(defequiv equiv
:package package
:event-name event-name
:rule-classes rule-classes
:instructions instructions
:hints hints
:otf-flg otf-flg)
where equiv is a function symbol of arity 2; package, if
supplied, is one of :current, :equiv or :legacy;
event-name, if supplied, is a symbol; and all other arguments are as
specified in the documentation for defthm. The defequiv macro
expands into a call of defthm. The name of the defthm is
equiv-is-an-equivalence, unless an :event-name keyword argument is
supplied, in which case event-name is used. 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 :equiv or
:legacy (which are treated identically), then the package of :equiv
is used. All other arguments to the generated defthm form are as
specified by the other keyword arguments above. The rule-class :equivalence is added to the rule-classes specified, if it is not
already there. The term generated for the defthm event states that
equiv is Boolean, reflexive, symmetric, and transitive.
Subtopics
- Equiv
- A macro to prove that a universally quantified formula is a paramaterized equivalence relation
