Install-not-normalized
Install an unnormalized definition
General Form:
(install-not-normalized NAME :allp FLG :defthm-name DNAME-SPEC)
We explain the arguments of install-not-normalized below, but first
let us illustrate its use with an example.
By default, ACL2 simplifies definitions by ``normalizing'' their bodies;
see normalize. If you prefer that ACL2 avoid such simplification when
expanding a function call, then you can assign the value of nil to xargs keyword :normalize (see defun) instead of the default value
of t. But that might not be a reasonable option, for example because the
definition in question occurs in an included book that you prefer not to edit.
An alternative is to call a macro, install-not-normalized.
Consider the following example from Eric Smith.
(defun return-nil (x) (declare (ignore x)) nil)
(defun foo (x) (return-nil x))
; Fails!
(thm (equal (foo x) (return-nil x))
:hints (("Goal" :in-theory '(foo))))
; Also fails!
(thm (equal (foo x) (return-nil x))
:hints (("Goal" :expand ((foo x))
:in-theory (theory 'minimal-theory))))
The problem is that ACL2 stores nil for the body of foo, using
``type reasoning'' to deduce that return-nil always returns the value,
nil. So if foo is the only enabled rule, then we are left trying to
prove that nil equals (return-nil x). Of course, this example is
trivial to fix by enabling return-nil, or even just its :type-prescription rule, but we want to support development of robust tools
that manipulate functions without needing to know anything about their callees.
To solve this problem, we can invoke (install-not-normalized foo),
which generates the following :definition rule.
(DEFTHM FOO$NOT-NORMALIZED
(EQUAL (FOO X) (RETURN-NIL X))
:HINTS (("Goal" :BY FOO))
:RULE-CLASSES ((:DEFINITION :INSTALL-BODY T)))
Each of the following now succeeds. For the second, note that the rule
FOO$NOT-NORMALIZED has installed a new body for FOO.
(thm (equal (foo x) (return-nil x))
:hints (("Goal" :in-theory '(foo$not-normalized))))
(thm (equal (foo x) (return-nil x))
:hints (("Goal"
:expand ((foo x))
:in-theory (theory 'minimal-theory))))
Let us see some more example forms; then, we discuss the general form.
Example Forms:
(install-not-normalized NAME)
; Equivalent to the form above:
(install-not-normalized NAME :allp t)
; Generate a definition for NAME but not for others from its mutual-recursion:
(install-not-normalized NAME :allp nil)
; Give the name BAR to the new theorem:
(install-not-normalized NAME :defthm-name 'BAR)
; Give the name F1-DEF to the new theorem for F1 and
; give the name F2-DEF to the new theorem for F2:
(install-not-normalized NAME :defthm-name '((f1 f1-def) (f2 f1-def)))
General Form:
(install-not-normalized NAME :allp FLG :defthm-name DNAME-SPEC :enable E)
where the keyword arguments are evaluated, but not NAME, and:
- NAME is the name of a function introduced by defun (or one of
its variants, including defund and defun-nx), possibly using
mutual-recursion.
- FLG (if supplied) is a Boolean that is relevant only in the case that
NAME was introduced using mutual-recursion. When FLG is nil, a
defthm event is to be introduced only for NAME; otherwise, there
will be a new defthm for every function defined with the same
mutual-recursion as NAME.
- DNAME-SPEC (if supplied) is usually a symbol denoting the name of the
defthm event to be introduced for NAME, which is
NAME$NOT-NORMALIZED by default — that is, the result of modifying
the symbol-name of F by adding the suffix
"$NOT-NORMALIZED". Otherwise, of special interest when NAME was
introduced with mutual-recursion: DNAME-SPEC is a list of doublets
of the form (F G), where F is a symbol as described for NAME
above, and the symbol G is the name of the defthm event generated
for the symbol F.
- E is either :auto (the default), t, or nil. If E
is t or nil then the generated event is a call of defthm or
defthmd, respectively. If E is omitted or is :auto, then
the generated event is a call of defthm if the original definition
of NAME is enabled at the time the install-not-normalized
event is submitted, and otherwise is a call of defthmd.
Any such defthm event has :rule-classes
((:definition :install-body t)), with suitable additional fields when
appropriate for keywords :clique and :controller-alist. To obtain
its default name programmatically:
ACL2 !>(install-not-normalized-name 'foo)
FOO$NOT-NORMALIZED
ACL2 !>
Remark. Each definition installed by install-not-normalized contains
the original body, not a translated version. (See term for a
discussion of the the notion of ``translated term''.)
For a somewhat related utility, see fn-is-body.
For examples, see the Community Book
misc/install-not-normalized-tests.lisp.
Subtopics
- Install-not-normalized-event
- Create an event form to
install
the non-normalized definition
of a function,
ensuring that the name of the theorem will not cause a conflict.
- Install-not-normalized-event-lst
- Create a list of event forms to
install
the non-normalized definitions
of a list of functions,
ensuring that the names of the theorems will not cause a conflict.
- Install-not-normalized$
- Install
the non-normalized definition
of a function,
ensuring that the name of the theorem will not cause a conflict.
