		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-commands

Execute a sequence of commands.

Signature
(defisar-commands commands name formula hyps events facts bindings disable rule-classes ctx state) → (mv erp events state)
Arguments: commands — Guard (true-listp commands).; name — Guard (symbolp name).; hyps — Guard (true-listp hyps).; events — Guard (pseudo-event-form-listp events).; facts — Guard (keyword-fact-info-alistp facts).; bindings — Guard (symbol-alistp bindings).; disable — Guard (booleanp disable).
Returns: events — Type (pseudo-event-form-listp events), given (and (pseudo-event-form-listp events) (keyword-fact-info-alistp facts)) .

Definitions and Theorems

Function: defisar-commands

(defun defisar-commands
       (commands name formula hyps events facts
                 bindings disable rule-classes ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp commands)
                             (symbolp name)
                             (true-listp hyps)
                             (pseudo-event-form-listp events)
                             (keyword-fact-info-alistp facts)
                             (symbol-alistp bindings)
                             (booleanp disable))))
 (let ((__function__ 'defisar-commands))
  (declare (ignorable __function__))
  (b* (((when (endp commands))
        (value (cons '(cw-event "~%~%~%~s0~s1~s0~%"
                                "!!!!!!!!!!!!!!!!!!!!"
                                " The proof is partial (no :QED). ")
                     events)))
       (command (car commands))
       ((unless (and (true-listp command)
                     (consp command)))
        (er-soft+ ctx t nil
                  "Malformed proof command ~x0." command))
       (command-name (car command))
       ((unless (keywordp command-name))
        (er-soft+ ctx t nil
                  "Non-keyword proof command name ~x0."
                  command-name)))
   (case command-name
    (:assume
        (b* (((mv erp (list events facts) state)
              (defisar-assume (cdr command)
                              name
                              hyps events facts bindings ctx state))
             ((when erp) (mv erp nil state)))
          (defisar-commands (cdr commands)
                            name formula hyps events facts bindings
                            disable rule-classes ctx state)))
    (:let
         (b* (((mv erp bindings state)
               (defisar-let (cdr command)
                            bindings ctx state))
              ((when erp) (mv erp nil state)))
           (defisar-commands (cdr commands)
                             name formula hyps events facts bindings
                             disable rule-classes ctx state)))
    (:derive
        (b* (((mv erp (list events facts) state)
              (defisar-derive (cdr command)
                              name events facts bindings ctx state))
             ((when erp) (mv erp nil state)))
          (defisar-commands (cdr commands)
                            name formula hyps events facts bindings
                            disable rule-classes ctx state)))
    (:qed
         (b* (((run-unless (endp (cdr commands)))
               (cw "Commands ~x0 found after :QED."
                   (cdr commands))))
           (value (defisar-qed name formula
                               events facts disable rule-classes))))
    (t (er-soft+ ctx t nil "Unrecognized command ~x0."
                 command-name))))))

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

(defthm pseudo-event-form-listp-of-defisar-commands.events
 (implies
     (and (pseudo-event-form-listp events)
          (keyword-fact-info-alistp facts))
     (b* (((mv ?erp ?events acl2::?state)
           (defisar-commands commands
                             name formula hyps events facts bindings
                             disable rule-classes ctx state)))
       (pseudo-event-form-listp events)))
 :rule-classes :rewrite)