Major Section: EVENTS
Examples:
(defthm assoc-of-app
(equal (app (app a b) c)
(app a (app b c))))
The following nonsensical example illustrates all the optional
arguments but is illegal because not all combinations are permitted.
See hints for a complete list of hints.
(defthm main
(implies (hyps x y z) (concl x y z))
:rule-classes (:REWRITE :GENERALIZE)
:instructions (induct prove promote (dive 1) x
(dive 2) = top (drop 2) prove)
:hints (("Goal"
:do-not '(generalize fertilize)
:in-theory (set-difference-theories
(current-theory :here)
'(assoc))
:induct (and (nth n a) (nth n b))
:use ((:instance assoc-of-append
(x a) (y b) (z c))
(:functional-instance
(:instance p-f (x a) (y b))
(p consp)
(f assoc)))))
:otf-flg t
:doc "#0[one-liner/example/details]")
General Form:
(defthm name term
:rule-classes rule-classes
:instructions instructions
:hints hints
:otf-flg otf-flg
:doc doc-string)
where name is a new symbolic name (see name), term is a
term alleged to be a theorem, and rule-classes, instructions,
hints, otf-flg and doc-string are as described in their
respective documentation. The five keyword arguments above are
all optional, however you may not supply both :instructions
and :hints, since one drives the proof checker and the other
drives the theorem prover. If :rule-classes is not specified,
the list (:rewrite) is used; if you wish the theorem to generate
no rules, specify :rule-classes nil.When ACL2 processes a defthm event, it first tries to prove the
term using the indicated hints (see hints) or instructions
(see proof-checker). If it is successful, it stores the rules
described by the rule-classes (see rule-classes), proving the
necessary corollaries.
