		Search-engine friendly clone of the ACL2 documentation.

Simplify-term

Simplify-term-examples

Examples illustrating simplify-term.

The examples below are deliberately quite trivial, in order to show how simplify-term behaves with some keyword arguments. For all those examples, we assume that the following event has already been evaluated.

(defun f (x) (+ 3 -3 (car x)))

The results in the log below are intended to follow clearly from the keyword arguments supplied in the respective invocations of simplify-term, which we invoke here with simplify.

ACL2 !>(simplify (f (cons y z))
                 :disable (car-cons)
                 :thm-enable nil)
(DEFTHMD SIMPLIFY-TERM-THM
         (EQUAL (F (CONS Y Z))
                (IF (ACL2-NUMBERP (CAR (CONS Y Z)))
                    (CAR (CONS Y Z))
                    0)))
ACL2 !>(simplify (f (cons y z))
                 :thm-name f1
                 :assumptions ((natp y)))
(DEFTHM F1 (IMPLIES (NATP Y) (EQUAL (F (CONS Y Z)) Y)))
ACL2 !>(simplify (f (cons (+ 7 y) z))
                 :thm-name f2
                 :untranslate nil)
(DEFTHM F2 (EQUAL (F (CONS (+ 7 Y) Z)) (BINARY-+ '7 Y)))
ACL2 !>