		Search-engine friendly clone of the ACL2 documentation.

Named-formulas

Prove-named-formulas

Try to prove a list of named formulas, one after the other.

Signature
(prove-named-formulas named-formulas named-hints verbose state) → (mv success msg state)
Arguments: named-formulas — Named formulas to prove (an alist from names to untranslated terms).
Guard (symbol-alistp named-formulas).; named-hints — Alist from names of formulas to proof hints to prove the corresponding formulas.
Guard (symbol-truelist-alistp named-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 of a named formula fails, the message is the error message generated by that proof attempt. When all the proofs of the named formulas succeed, currently the message is empty, but future versions of this function could return some non-empty message instead.

If the verbose argument is t, also print progress messages for the named formulas.

Definitions and Theorems

Function: prove-named-formulas

(defun prove-named-formulas
       (named-formulas named-hints verbose state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-alistp named-formulas)
                             (symbol-truelist-alistp named-hints)
                             (booleanp verbose))))
 (let ((__function__ 'prove-named-formulas))
  (declare (ignorable __function__))
  (cond
   ((endp named-formulas) (mv t "" state))
   (t (b* ((named-formula (car named-formulas))
           (name (car named-formula))
           (formula (cdr named-formula))
           (hints (cdr (assoc-eq name named-hints)))
           ((mv success msg state)
            (prove-named-formula name formula hints verbose state)))
        (if success (prove-named-formulas (cdr named-formulas)
                                          named-hints verbose state)
          (mv nil msg state)))))))