Notion of definedness of functions, for some event macros.

As far as certain event macros are concerned,
an ACL2 named function is defined if and only if
it has a non-

The unnormalized body of a named function is
the `defun` event that introduces the function.
This is the case not only for user-defined functions,
but also for built-in defined ACL2 functions,
whose introducing `defun` events can be seen
via

A valid untranslated term never translates to `pseudo-termp`
(which captures a superset of the valid translated terms),
but it does not satisfy `termp`.
Therefore, the unnormalized body of a defined function cannot be

However, the built-in program-mode functions are defined but do not have an unnormalized body. Thus, the event macros that use this notion of definedness would not regard these functions as being defined. This is only an issue for program-mode functions, not for logic-mode functions (including the built-in ones); thus, if an event macro requires a function (e.g. to be transformed) to be in logic mode and to be defined, checking the unnormalized body is an accurate way to establish if the logic-mode function is defined.

The system utility `ubody` (or `ubody+`)
retrieves the unnormalized body of a function.
It is a specialization of the built-in `body` system utility,
which retrieves the unnormalized or normalized body of a function.
based on the flag passed as argument.
The normalized body of a function may differ from the unnormalized one
because the former may be obtained from the latter
via some simplifications.