Prove that a function called on its formals equals its body
(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
ACL2 !>(fn-is-body-name 'foo)
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
For a somewhat related utility, see install-not-normalized.
For examples, see the Community Book