		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-proof

Execute a proof.

Signature
(defisar-proof commands name formula disable rule-classes ctx state) → (mv erp events state)
Arguments: commands — Guard (true-listp commands).; name — Guard (symbolp name).; disable — Guard (booleanp disable).
Returns: events — Type (pseudo-event-form-listp events).

Definitions and Theorems

Function: defisar-proof

(defun defisar-proof
       (commands name
                 formula disable rule-classes ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (true-listp commands)
                              (symbolp name)
                              (booleanp disable))))
  (let ((__function__ 'defisar-proof))
    (declare (ignorable __function__))
    (b* (((mv hyps &)
          (defisar-formula-to-hyps+concl formula))
         ((er events)
          (defisar-commands commands name formula hyps nil nil
                            nil disable rule-classes ctx state)))
      (value (rev events)))))

Theorem: pseudo-event-form-listp-of-defisar-proof.events

(defthm pseudo-event-form-listp-of-defisar-proof.events
  (b* (((mv ?erp ?events acl2::?state)
        (defisar-proof commands name formula
                       disable rule-classes ctx state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)