Simplify
Simplify the definition of a given function.
For any function symbol f defined using defun, defun-sk, or the the soft::soft tool, defun-sk2, simplify
defines a corresponding new function whose body results from simplifying the
body of the definition of f. Simplify may also be used to simplify
a given term.
Simplify operates in related but different ways depending on its
input: a function symbol introduced with defun (or a wrapper such as
defun-nx), a function symbol introduced with defun-sk (or a wrapper
such as the soft::soft tool defun-sk2), or a term other than a
symbol or a constant. In the first case, (simplify fn ...) expands
directly to (simplify-defun fn ...); see simplify-defun. In the
second case, (simplify fn ...) expands directly to (simplify-defun-sk
fn ...); see simplify-defun-sk. Otherwise, the call, which is of the
form (simplify term ...), expands to (simplify-term term ...); see
simplify-term. In all three cases, the corresponding documentation
topic carefully describes keyword arguments and links to a corresponding topic
that contains examples.
Here are three very simple examples you may wish to read before you visit
those documentation topics. They give a sense of simplify-defun,
simplify-defun-sk, and simplify-term, respectively.
ACL2 !>(defun f1 (x) (car (cons x x)))
[[.. output omitted here ..]]
F1
ACL2 !>(simplify f1 :new-name f2 :theorem-name f1-is-f2)
(DEFUN F2 (X)
(DECLARE (XARGS :GUARD T
:VERIFY-GUARDS NIL))
X)
(DEFTHM F1-IS-F2 (EQUAL (F1 X) (F2 X)))
ACL2 !>
ACL2 !>(defun-sk g1 (x y) (exists z (equal (* z 2) (* x y))))
[[.. output omitted here ..]]
T
ACL2 !>(simplify g1 :theorem-disabled t)
(DEFUN-SK G1$1 (X Y) (EXISTS (Z) (EQUAL (* 2 Z) (* X Y))) :QUANT-OK T)
(DEFTHMD G1-BECOMES-G1$1 (IFF (G1 X Y) (G1$1 X Y)))
ACL2 !>
ACL2 !>(simplify (+ x (- x) 17) :thm-name foo)
(DEFTHM FOO (EQUAL (+ X (- X) 17) 17))
ACL2 !>
See simplify-failure for tips on how to deal with failures and other
undesirable results from evaluating calls of simplify.
Subtopics
- Simplify-failure
- Ways to address failed invocations of the simplify transformation.
- ACL2::return-last-blockers
- Functions and rules for prog2$ and other macros implemented with return-last.
