# Defthm

Prove and name a theorem

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)
General Form:
(defthm name term
:rule-classes rule-classes
:instructions instructions
:hints hints
:otf-flg otf-flg)

where name is a new symbolic name (see name), term is a
term alleged to be a theorem, and `rule-classes`, `instructions`,
`hints`, and `otf-flg` are as described in their respective documentation. The keyword arguments above are all optional, however you may
not supply both :`instructions` and :`hints`, since one
drives the interactive proof-builder 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-builder). If it is successful, it stores the rules described by
the rule-classes (see rule-classes), proving the necessary
corollaries.

### Subtopics

- Otf-flg
- Allow more than one initial subgoal to be pushed for induction
- Defthm<w
- Attempt to prove a theorem directly from previously-proved theorems.
- Defthmr
- Submit a theorem, as a rewrite rule only if possible.
- Defthmd
- Prove and name a theorem and then disable it
- Previous-subsumer-hints
- Hints to prove a theorem directly from previously-proved theorems.
- Dft
- Provide an explicit proof, for example chaining equalities
- Thm<w
- Attempt to prove a theorem directly from previously-proved theorems.
- Defthmd<w
- Attempt to prove a theorem directly from previously-proved theorems.