ACL2-PC::CLAIM

(atomic macro) 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.

Notes: (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.