Simp
Simp returns a list of simplified versions of its input
term, each paired with a hypothesis list under which the input and output
terms are provably equal.
This tool is implemented on top of another tool, bash-term-to-dnf.
However, bash-term-to-dnf treats its input term as a propositional
assertion, so it is unsuitable if you want to simpify a non-Boolean term to
produce a provably equal output term. The simp tool is well-suited to
that task.
However, a case split may occur under simplification. Moroever, simp
takes a second argument, which is a list of hypotheses, which are simplified
too and hence might also generate case splits. Thus, simp actually
returns a list of term/hypothesises pairs each of the form
(<simplified-term> <simplified-hypothesis-1>
... <simplified-hypothesis-k>), where for each such pair the following may
be expected to be a theorem:
(implies (and <simplified-hypothesis-1>
...
<simplified-hypothesis-k>)
<simplified-term>)
Example:
Suppose we have submitted the following two definitions.
(defun p (x) (or (stringp x) (acl2-numberp x)))
(defun f (x) (if (p x) (cons x x) 17))
Then:
ACL2 !>(simp (f x) nil)
(((CONS X X) (ACL2-NUMBERP X))
(17 (NOT (STRINGP X))
(NOT (ACL2-NUMBERP X)))
((CONS X X) (STRINGP X)))
ACL2 !>(simp (f x) nil :hints (("Goal" :in-theory (disable p))))
((17 (NOT (P X))) ((CONS X X) (P X)))
ACL2 !>
Notice the space in front of the results. This indicates that what is
actually returned is an error
triple, for example as follows in the final case above.
(mv ((17 (NOT (P X))) ((CONS X X) (P X))) <state>)
General Form:
(simp term hypothesis-list :hints hints :verbose verbose)
where term and each member of the list hypothesis-list are terms
in user-level syntax, hints (which is optional) is a list of hints
such as might be given to defthm, and a verbose (which is
optional, nil by default) allows output from the prover if non-nil.
The result is an error triple,
(mv nil val state), where val is a list, each member of
which is of the form (<simplified-term> <simplified-hypothesis-1>
... <simplified-hypothesis-k>), where <simplified-term> and each
<simplified-hypothesis-i> are untranslated (user-level) forms, as
described earlier in this topic.
