Thm
Prove a theorem
Example:
(thm (equal (app (app a b) c)
(app a (app b c))))
Also see defthm. Unlike defthm, thm does not store an
event; it merely causes the theorem prover to attempt a proof. But like
defthm, calls of thm are legal in event contexts (see embedded-event-form).
General Form:
(thm term
:hints hints
:otf-flg otf-flg)
where term is a term alleged to be a theorem, and hints and
otf-flg are as described in the corresponding documentation
topics. The keyword arguments above are both optional. Unlike defthm,
the :instructions keyword is not legal for thm; use an
:instructions hint instead, i.e., :hints (("Goal" :instructions
...)).
For information on how thm is implemented using make-event,
see make-event-example-3.
Subtopics
- Otf-flg
- Allow more than one initial subgoal to be pushed for induction
- Rule
- A thm-like version of defrule.
