Remove trivial calls from a term

For many rule-classes, the process of converting terms to rules includes the removal of certain trivial calls from the term. Such removal is performed in some other settings as well, including hints processing, generating proof obligations for guards and termination, and the storing of induction schemes and constraints.

In all such cases, the resulting term is provably equivalent to the input
term. A common example is to replace the term `return-last` is replaced by its last argument.
ACL2 identifies certain such transformations, from a term to a trivial
simplification of it, such that the input and output are provably equal. We
historically have referred to the process of making such replacements as
``removing guard holders.'' (For a discussion of the connection to guards,
see the ``Essay on the Removal of Guard Holders'' in the ACL2 sources.)

The process of removing guard-holders includes the transformations below.
That process is also applied to each argument of a function call and to the
bodies of lambda expressions (see term), usually including
quoted lambda expressions that appear in an argument position with ilk

(return-last term0 term1 term2) ==> term2 (mv-list n term) ==> term (cons-with-hint x y) ==> (cons x y) (the-check guard x y) ==> y (from-df x) ==> x (to-df 'r) ==> 'r ; only when r satisfies dfp (df0) ==> 0 (df1) ==> 1 (do$ x1 x2 x3 x4 x5 'u1 'u2) ==> (do$ x1 x2 x3 x4 x5 'nil 'nil) ; only when u1 and u2 are non-nil ; For replacing a term (the type term) by term: ((lambda (y) (the-check guard x y)) val) ==> val ; For replacing equality aliases; for example, this transforms ; the macroexpansion of (member x y) to (member-equal x y): (('LAMBDA (f1 ... fk) ('RETURN-LAST ''MBE1-RAW exec logic)) a1 ... ak) ==> logic ; For other than measure theorems and induction schemes, remove lambda ; applications that are ``trivial'' in either of the following two senses. ; For replacing a term (let ((v term)) v) by term: (('LAMBDA (v) v) term) ==> term ; When each formal is equal to the corresponding actual: (('LAMBDA (f1 ... fk) body) f1 ... fk) ==> body

Because of how `mbe` and `ec-call` are defined in terms of
`return-last`, the expressions

The final two classes of simplification above (removal of ``trivial''
lambda applications) may be removed by executing the following form, which is
`local` to an `encapsulate` form and to books.

(defattach-system remove-guard-holders-lamp constant-nil-function-arity-0)

Here is how to restore the default behavior.

(defattach-system remove-guard-holders-lamp constant-t-function-arity-0)

Note that by default, guard-holders are not removed inside calls of `hide`. You can however cause them to be removed inside such calls after all,
as was the case through Version 8.2, as follows.

(defattach-system ; generates (local (defattach ...)) remove-guard-holders-blocked-by-hide-p constant-nil-function-arity-0)