Fn-is-body
Prove that a function called on its formals equals its body
General Form:
(fn-is-body fn &key hints thm-name rule-classes)
Evaluation of the form above generates a defthm event whose name is
thm-name — by default, the result of adding the suffix "$IS-BODY"
to fn, which is a function symbol. To obtain that name
programmatically:
ACL2 !>(fn-is-body-name 'foo)
FOO$IS-BODY
ACL2 !>
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 unnormalized body of fn. If
:hints or :rule-classes are supplied, they will be attached to the
generated defthm form.
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 normalized body, which may differ from its
unnormalized body.
For a somewhat related utility, see install-not-normalized.
For examples, see the Community Book
misc/install-not-normalized.lisp.
