ACL2-pc::claim
(atomic macro)
add a new hypothesis
Examples:
(claim (< x y)) -- attempt to prove (< x y) from the current
top-level hypotheses and if successful, then
add (< x y) as a new top-level hypothesis in
the current goal
(claim (< x y)
:otf-flg t
:hints (("Goal" :induct t)))
-- as above, but call the prover using the
indicated values for the otf-flg and hints
(claim (< x y) 0) -- as above, except instead of attempting to
prove (< x y), create a new subgoal with the
same top-level hypotheses as the current goal
that has (< x y) as its conclusion
(claim (< x y) :hints :none)
-- same as immediately above
General Form:
(claim expr &rest rest-args)
This command creates a new subgoal with the same top-level hypotheses as
the current goal but with a conclusion of expr. If rest-args is a
non-empty list headed by a non-keyword, then there will be no proof attempted
for the new subgoal. With that possible exception, rest-args should
consist of keyword arguments. The keyword argument :do-not-flatten
controls the ``flattening'' of new hypotheses, just as with the casesplit
command (see ACL2-pc::casesplit). The remaining rest-args are
used with a call the prove command on the new subgoal, except that if
:hints is a non-nil atom, then the prover is not called —
rather, this is the same as the situation described above, where
rest-args is a non-empty list headed by a non-keyword.
Remarks: (1) Unlike the casesplit command, the claim
command is completely insensitive to governors. (2) It is allowed to use
abbreviations in the hints. (3) The keyword :none has the special
role as a value of :hints that is shown clearly in an example
above.
