Major Section: RULE-CLASSES
See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
:corollary formula from which a :refinement rule might be built is:
Example: (implies (bag-equal x y) (set-equal y x)).Also see defrefinement.
General Form: (implies (equiv1 x y) (equiv2 x y))
Equiv1 and equiv2 must be known equivalence relations. The effect
of such a rule is to record that equiv1 is a refinement of equiv2.
This means that equiv1 :rewrite rules may cking is based on untranslated bodies, this turns out to be
unsound! It is therefore now prohibited. We illustrate such an
unsoundness below. Let foo-thm1.lisp be a book with the
following contents.
(in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm1 (iff (foo x) x) :rule-classes nil)Note that the macro form
(p x) translates to (if x t nil).
The :program function p1 is used to generate this
translation. The function foo is defined so that (foo x) is
(p x) and a theorem about foo is proved, namely, that (foo x)
is true iff x is true.
Now let foo-thm2.lisp be a book with the following contents.
(in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil)In this book, the
:program function p1 is defined so that
(p x) means just the negation of what it meant in the first book,
namely, (if x nil t). The function foo is defined identically
-- more precisely, the untranslated body of foo is identical
in the two books, but because of the difference between the two
versions of the :program function p1 the axioms
defining the two foos are different. In the second book we prove
the theorem that (foo x) is true iff x is nil.Now co