Defthmr
Submit a theorem, as a rewrite rule only if possible.
Defthmr stands for ``defthm rule''. It is a macro that is
intended to be equivalent to defthm — in particular, it takes
the same arguments as defthm — but when necessary it avoids the
default of :rule-classes :rewrite. Here we also document defthmdr,
which is similar to defthmr but when a rewrite rule is created, it is
immediately disabled; thus defthmdr is to defthmd as defthmr is
to defthm.
Examples:
(defthmr symbol-name-abc
(equal (symbol-name 'abc) "ABC"))
(defthmdr symbol-name-intern$-acl2
(equal (symbol-name (intern$ name "ACL2")) name))
General Forms:
(defthmr name term ...) ; same keyword arguments accepted as for defthm
(defthmdr name term ...) ; same keyword arguments accepted as for defthm
In the first example above, the use of defthm would cause an
error:
ACL2 !>(defthm symbol-name-abc
(equal (symbol-name 'abc) "ABC"))
ACL2 Error in ( DEFTHM SYMBOL-NAME-ABC ...): A :REWRITE rule generated
from SYMBOL-NAME-ABC is illegal because it rewrites the term 'T to
itself! ....
The problem is that the internal form for the term (equal (symbol-name
'abc) "ABC") is, perhaps surprisingly, 'T. The reason is that ACL2
evaluates calls of undefined primitives, such as symbol-name and
equal, when translating to internal form.
Defthmr and defthmdr avoid this problem by adding
:rule-classes nil in such cases. The two examples above thus generate
the following events. In the first example, the addition of :rule-classes nil
avoids the error discussed above, by instructing ACL2 to avoid the default
behavior of attempting to store the theorem as a rewrite rule. The
second example has no such problem (because of the variable, name), so
ACL2 treats that defthmdr simply as defthmd.
(defthm symbol-name-abc
(equal (symbol-name 'abc) "ABC")
:rule-classes nil)
(defthmd symbol-name-intern$-acl2
(equal (symbol-name (intern$ name "ACL2")) name))
Note that if a :rule-classes keyword argument is supplied, then the
given call of defthmr or defthmdr simply expands directly to the
corresponding call of defthm or defthmd, respectively.
