		Search-engine friendly clone of the ACL2 documentation.

Named-formulas

Prove-named-formula

Try to prove a named formula.

Signature
(prove-named-formula name formula hints verbose state) → (mv success msg state)
Arguments: name — Name of the formula to prove.
Guard (symbolp name).; formula — Formula to prove (an untranslated term).; hints — Hints to prove the formula.
Guard (true-listp hints).; verbose — Print progress messages or not.
Guard (booleanp verbose).
Returns: success — A booleanp.; msg — A msgp.

Besides returning an indication of success or failure, return a structured message (printable with ~@). When the proof fails, the message is an error message. When the proof succeeds, currently the message is empty, but future versions of this function could return some non-empty message instead.

Note that prove$ always returns a nil error flag, so the code below ignores that result.

If the verbose argument is t, also print a progress message to indicate that the proof of the named formula is being attempted, and then to indicate the outcome of the attempt.

Parentheses are printed around the progress message to ease navigation in an Emacs buffer.

Definitions and Theorems

Function: prove-named-formula

(defun prove-named-formula (name formula hints verbose state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbolp name)
                              (true-listp hints)
                              (booleanp verbose))))
  (let ((__function__ 'prove-named-formula))
    (declare (ignorable __function__))
    (b* (((run-when verbose)
          (cw "~%(Proving ~x0:~%~x1~|" name formula))
         ((mv & yes/no state)
          (prove$ formula :hints hints)))
      (if yes/no (b* (((run-when verbose) (cw "Done.)~%")))
                   (mv t "" state))
        (b* (((run-when verbose) (cw "Failed.)~%")))
          (mv nil
              (msg "Unable to prove ~x0:~%~x1~|"
                   name formula)
              state))))))