call the ACL2 theorem prover to prove the current goal
Major Section: PROOF-CHECKER-COMMANDS
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 setAttempt to prove the current goal, whereGeneral Form: (prove &rest rest-args)
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.)
Note: 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.