install-not-normalized

(in-package "ACL2")

(defxdoc install-not-normalized
  :parents (proof-automation)
  :short "Install an unnormalized definition"
  :long "@({
 General Form:

 (install-not-normalized NAME :allp FLG :defthm-name DNAME-SPEC)
 })

 <p>We explain the arguments of @('install-not-normalized') below, but first
 let us illustrate its use with an example.</p>

 <p>By default, ACL2 simplifies definitions by ``normalizing'' their bodies;
 see @(see normalize).  If you prefer that ACL2 avoid such simplification when
 expanding a function call, then you can assign the value of @('nil') to @(tsee
 xargs) keyword @(':normalize') (see @(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').</p>

 <p>Consider the following example from Eric Smith.</p>

 @({
 (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))))
 })

 <p>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 @(':')@(tsee
 type-prescription) rule, but we want to support development of robust tools
 that manipulate functions without needing to know anything about their callees.
 </p>

 <p>To solve this problem, we can invoke @('(install-not-normalized foo)'),
 which generates the following @(':')@(tsee definition) rule.</p>

 @({
 (DEFTHM FOO$NOT-NORMALIZED
   (EQUAL (FOO X) (RETURN-NIL X))
   :HINTS (("Goal" :BY FOO))
   :RULE-CLASSES ((:DEFINITION :INSTALL-BODY T)))
 })

 <p>Each of the following now succeeds.  For the second, note that the rule
 @('FOO$NOT-NORMALIZED') has installed a new body for @('FOO').</p>

 @({
 (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))))
 })

 <p>Let us see some more example forms; then, we discuss the general form.</p>

 @({
 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)
 })

 <p>where the keyword arguments are evaluated, but not @('NAME'), and:</p>

 <ul>

 <li>@('NAME') is the name of a function introduced by @(tsee defun) (or one of
 its variants, including @(tsee defund) and @(tsee defun-nx)), possibly using
 @(tsee mutual-recursion).</li>

 <li>@('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
 @(tsee 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').</li>

 <li>@('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 &mdash; that is, the result of modifying
 the @(tsee 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').</li>

 <li>@('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
 @(tsee defthmd), respectively.  If @('E') is omitted or is @(':auto'), then
 the generated event is a call of @('defthm') if the original @(see definition)
 of @('NAME') is @(see enable)d at the time the @('install-not-normalized')
 event is submitted, and otherwise is a call of @('defthmd').</li>

 </ul>

 <p>Any such @('defthm') event has @(':')@(tsee rule-classes)
 @('((:definition :install-body t))'), with suitable additional fields when
 appropriate for keywords @(':clique') and @(':controller-alist').  To obtain
 its default name programmatically:</p>

 @({
 ACL2 !>(install-not-normalized-name 'foo)
 FOO$NOT-NORMALIZED
 ACL2 !>
 })

 <p>Remark.  Each definition installed by @('install-not-normalized') contains
 the original body, not a translated version.  (See @(see term) for a
 discussion of the the notion of ``translated term''.)</p>

 <p>For a somewhat related utility, see @(see fn-is-body).</p>

 <p>For examples, see the Community Book
 @('misc/install-not-normalized-tests.lisp').</p>")

(defxdoc fn-is-body
  :parents (proof-automation)
  :short "Prove that a function called on its formals equals its body"
  :long "@({
 General Form:

 (fn-is-body fn &key hints thm-name rule-classes)

 })

 <p>Evaluation of the form above generates a @(tsee defthm) event whose name is
 @('thm-name') &mdash; by default, the result of adding the suffix "$IS-BODY"
 to @('fn'), which is a function symbol.  To obtain that name
 programmatically:</p>

 @({
 ACL2 !>(fn-is-body-name 'foo)
 FOO$IS-BODY
 ACL2 !>
 })

 <p>The formula of that @('defthm') event is of the form @('(equal (fn x1
 ... xn) <body>)'), where @('(x1 ... xn)') is the list of formal parameters of
 @('fn') and @('<body>') is the un@(see normalize)d body of @('fn').  If
 @(':hints') or @(':rule-classes') are supplied, they will be attached to the
 generated @('defthm') form.</p>

 <p>Note that the proof of the generated @('defthm') may not follow trivially
 from the function's @(':')@('definition') rule: by default, that rule is
 derived from the function's @(see normalize)d body, which may differ from its
 unnormalized body.</p>

 <p>For a somewhat related utility, see @(see install-not-normalized).</p>

 <p>For examples, see the Community Book
 @('misc/install-not-normalized.lisp').</p>")