Create a defthm equating a call with its simplification.

For a related tool, see defopen.

Example:

(include-book "misc/defopener" :dir :system) (defopener append-open (append x y) :hyp (and (true-listp x) (true-listp (cdr x))) :hints (("Goal" :expand ((append x y)))))

The above example creates the following theorem.

(DEFTHM APPEND-OPEN (IMPLIES (AND (TRUE-LISTP X) (TRUE-LISTP (CDR X))) (EQUAL (APPEND X Y) (IF (NOT X) Y (CONS (CAR X) (APPEND (CDR X) Y))))))

In general, the form

(defopener name term :hyp hyp ...)

attempts to create a theorem of the form

(DEFTHM NAME (IMPLIES HYP (EQUAL TERM rhs)))

where

(DEFTHM NAME (EQUAL TERM rhs)).

If an equivalence relation symbol is supplied for

The output can be rather verbose. Once

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ >>> STARTING PROOF OF: (DEFTHM NAME ...) @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

To abbreviate the above message, you can specify an `evisc-tuple` using the

The simplification that takes place uses a prover interface that is also
used in the distributed book

:do-not (generalize eliminate-destructors fertilize eliminate-irrelevance)

A suitable

If you only want to see the generated theorem, and not the attempted proof
of it, use

The

None of the arguments of this macro is evaluated.

This tool is heuristic in nature, and failures are possible. The error message might provide debugging clues. Let us consider an example that actually occurred that generated an error message of the following form.

ACL2 Error in (DEFOPENER MY-DEFOPENER-RULE ...): The last literal of each clause generated is expected to be of the form (equiv lhs rhs) for the same equiv and lhs. The equiv for the last literal of the first clause is EQUAL and its lhs is (HIDE (FOO X Y)) but the last literal of one clause generated is: (MY-PREDICATE (HIDE (FOO X Y)))

The message suggests that each goal (i.e., clause) after the first should be
of the form

(equal (equal (f1 a) b) (and (my-predicate b) ...))

ACL2 was able to match the term