add a new hypothesis
Major Section: PROOF-CHECKER-COMMANDS
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 (as described in its
documentation). 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.
