ACL2-pc::prove
(primitive)
call the ACL2 theorem prover to prove the current goal
Examples:
prove -- attempt to prove the current goal
(prove :otf-flg t
:hints (("Subgoal 2" :by foo) ("Subgoal 1" :use bar)))
-- attempt to prove the current goal, with the indicated hints
and with OTF-FLG set
General Form:
(prove &rest rest-args)
Attempt to prove the current goal, where rest-args is as in the
keyword arguments to defthm except that only :hints and
:otf-flg are allowed. The command succeeds exactly when the
corresponding defthm would succeed, except that it is all right for some
goals to be given ``bye''s. Each goal given a ``bye'' will be turned into a
new subgoal. (See hints for an explanation of :by hints.)
Remark: Use (= t) instead if you are not at the top of the
conclusion. Also note that if there are any hypotheses in the current goal,
then what is actually attempted is a proof of (implies hyps conc), where
hyps is the conjunction of the top-level hypotheses and conc is the
goal's conclusion.
Remark: It is allowed to use abbreviations in the hints.
