		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-assume

Execute an :assume command.

Signature
(defisar-assume assume-args name hyps events facts bindings ctx state) → (mv erp result state)
Arguments: 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).
Returns: result — Type (tuple (new-events pseudo-event-form-listp) (new-facts keyword-fact-info-alistp) result) , given (and (pseudo-event-form-listp events) (keyword-fact-info-alistp facts)) .

An :assume command takes exactly one argument, which must be a list of a keyword and a formula. The keyword must not be already the name of a fact. We do not check the formula here; we implicitly check it when the generated theorem is submitted.

The bindings are reversed before being put into the formula, because they are consed as go through the :lets.

Definitions and Theorems

Function: defisar-assume

(defun defisar-assume
       (assume-args name
                    hyps events facts bindings ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp name)
                             (true-listp hyps)
                             (pseudo-event-form-listp events)
                             (keyword-fact-info-alistp facts)
                             (symbol-alistp bindings))))
 (let ((__function__ 'defisar-assume))
  (declare (ignorable __function__))
  (b*
   (((unless (tuplep 1 assume-args))
     (er-soft+ ctx t (list nil nil)
               "Malformed :ASSUME arguments ~x0."
               assume-args))
    (assume-id+fact (car assume-args))
    ((unless (tuplep 2 assume-id+fact))
     (er-soft+ ctx t (list nil nil)
               "Malformed :ASSUME argument ~x0."
               assume-id+fact))
    (assume-id (first assume-id+fact))
    (assume-fact (second assume-id+fact))
    ((unless (keywordp assume-id))
     (er-soft+ ctx t (list nil nil)
               "The fact name ~x0 must be a keyword."
               assume-id))
    ((when (consp (assoc-eq assume-id facts)))
     (er-soft+ ctx t (list nil nil)
               "Duplicate fact name ~x0." assume-id))
    (thm-name (packn-pos (list name "<" assume-id ">")
                         name))
    (thm-formula (if (consp hyps)
                     (cons 'implies
                           (cons (cons 'and hyps)
                                 (cons assume-fact 'nil)))
                   assume-fact))
    (thm-formula
         (if bindings (cons 'let*
                            (cons (rev (alist-to-doublets bindings))
                                  (cons thm-formula 'nil)))
           thm-formula))
    (thm-hints '(("Goal" :in-theory nil)))
    (thm-event
     (cons
      'local
      (cons
       (cons
         'defthm
         (cons thm-name
               (cons thm-formula
                     (cons ':hints
                           (cons thm-hints '(:rule-classes nil))))))
       'nil)))
    (thm-event (restore-output thm-event))
    (print-event
     (cons
      'cw-event
      (cons
          '"~%~%~%~s0~%~x1~%~%"
          (cons '"****************************************"
                (cons (cons 'quote
                            (cons (cons ':assume assume-args) 'nil))
                      'nil)))))
    (events (list* thm-event print-event events))
    (fact-info (make-fact-info :thm-name thm-name
                               :formula assume-fact))
    (facts (acons assume-id fact-info facts)))
   (value (list events facts)))))

Theorem: return-type-of-defisar-assume.result

(defthm return-type-of-defisar-assume.result
  (implies
       (and (pseudo-event-form-listp events)
            (keyword-fact-info-alistp facts))
       (b* (((mv ?erp ?result acl2::?state)
             (defisar-assume assume-args name
                             hyps events facts bindings ctx state)))
         (tuple (new-events pseudo-event-form-listp)
                (new-facts keyword-fact-info-alistp)
                result)))
  :rule-classes :rewrite)

Theorem: true-listp-of-defisar-assume.result

(defthm true-listp-of-defisar-assume.result
  (b* (((mv ?erp ?result acl2::?state)
        (defisar-assume assume-args name
                        hyps events facts bindings ctx state)))
    (true-listp result))
  :rule-classes :type-prescription)