A useful utility to use rewrite rules that has lambda expression on RHS for RP-Rewriter.
RP-Rewriter does not work with terms that has lambda expressions. Every rewrite rule and conjectures are beta-reduced. However, for some cases, doing beta-reduction without rewriting subterms first can cause performance issues due to repetition.
To mitigate this issue, we use a macro defthm-lambda that can retain the functionality of lambda expressions rewrite rules. defthm-lambda has the same signature as defthm.
Below is an example defthm-lambda event and what it translates to:
(defthm-lambda foo-redef (implies (p x) (equal (foo x) (let* ((a (f1 x)) (b (f2 x))) (f4 a a b))))) ;; The above event is translated into this: (encapsulate (((foo-redef_lambda-fnc_1 * *) => *) ((foo-redef_lambda-fnc_0 * *) => *)) (local (defun-nx foo-redef_lambda-fnc_1 (b a) (f4 a a b))) (local (defun-nx foo-redef_lambda-fnc_0 (a x) (foo-redef_lambda-fnc_1 (f2 x) a))) (def-rp-rule foo-redef_lambda-opener (and (equal (foo-redef_lambda-fnc_1 b a) (f4 a a b)) (equal (foo-redef_lambda-fnc_0 a x) (foo-redef_lambda-fnc_1 (f2 x) a)))) (def-rp-rule foo-redef (implies (p x) (equal (foo x) (foo-redef_lambda-fnc_0 (f1 x) x)))))