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]")whereGeneral Form: (defthm name term :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg :doc doc-string)

`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.