To instruct GL to symbolically execute

(defthm filter1-for-gl (equal (filter1 x) (filter2 x)) :rule-classes nil) (gl::set-preferred-def filter1 filter1-for-gl)

The

When GL encounters a call of a function in this table, it replaces the call
with the right-hand side of the theorem, which is justified by the theorem. So
after the above event, GL will replace calls of

As another example of a preferred definition, GL automatically optimizes the definition of evenp, which ACL2 defines as follows:

(evenp x) = (integerp (* x (/ 2)))

This definition is basically unworkable since GL provides little support for
rational numbers. However, GL has an efficient, built-in implementation of
logbitp. So to permit the efficient execution of

(defthm evenp-is-logbitp (equal (evenp x) (or (not (acl2-numberp x)) (and (integerp x) (equal (logbitp 0 x) nil)))))