• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
      • Simplify-defun
      • Isodata
      • Tailrec
      • Schemalg
      • Restrict
      • Expdata
      • Casesplit
      • Simplify-term
        • Simplify-term-examples
      • Simplify-defun-sk
      • Parteval
      • Solve
      • Wrap-output
      • Propagate-iso
      • Simplify
      • Finite-difference
      • Drop-irrelevant-params
      • Copy-function
      • Lift-iso
      • Rename-params
      • Utilities
      • Simplify-term-programmatic
      • Simplify-defun-sk-programmatic
      • Simplify-defun-programmatic
      • Simplify-defun+
      • Common-options
      • Common-concepts
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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 !>