		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-derive

Execute a :derive command.

Signature
(defisar-derive derive-args name events facts bindings ctx state) → (mv erp result state)
Arguments: name — Guard (symbolp name).; 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)) .

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

Definitions and Theorems

Function: defisar-derive

(defun defisar-derive
       (derive-args name events facts bindings ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp name)
                             (pseudo-event-form-listp events)
                             (keyword-fact-info-alistp facts)
                             (symbol-alistp bindings))))
 (let ((__function__ 'defisar-derive))
  (declare (ignorable __function__))
  (b*
   (((mv okp derive-id derive-fact
         derive-from derive-hints-etc)
     (case-match derive-args
       (((id fact)) (mv t id fact nil nil))
       (((id fact) :from from . hints-etc)
        (mv t id fact from hints-etc))
       (((id fact) . hints-etc)
        (mv t id fact nil hints-etc))
       (& (mv nil nil nil nil nil))))
    ((when (not okp))
     (er-soft+ ctx t (list nil nil)
               "Malformed :DERIVE arguments ~x0."
               derive-args))
    ((unless (keywordp derive-id))
     (er-soft+ ctx t (list nil nil)
               "The fact name ~x0 must be a keyword."
               derive-id))
    ((when (consp (assoc-eq derive-id facts)))
     (er-soft+ ctx t (list nil nil)
               "Duplicate fact name ~x0." derive-id))
    (thm-name (packn-pos (list name "<" derive-id ">")
                         name))
    ((unless (keyword-listp derive-from))
     (er-soft+ ctx t (list nil nil)
               "The :FROM fact names ~x0 must be keywords."
               derive-from))
    ((mv erp thm-hyps state)
     (defisar-derive-thm-hyps derive-from facts ctx state))
    ((when erp)
     (mv erp (list nil nil) state))
    (thm-formula (if (consp thm-hyps)
                     (cons 'implies
                           (cons (cons 'and thm-hyps)
                                 (cons derive-fact 'nil)))
                   derive-fact))
    (thm-formula
         (if bindings (cons 'let*
                            (cons (rev (alist-to-doublets bindings))
                                  (cons thm-formula 'nil)))
           thm-formula))
    (thm-hints-etc derive-hints-etc)
    (thm-event
     (cons
         'local
         (cons (cons 'defrule
                     (cons thm-name
                           (cons thm-formula
                                 (cons ':rule-classes
                                       (cons 'nil thm-hints-etc)))))
               'nil)))
    (thm-event (restore-output thm-event))
    (print-event
     (cons
      'cw-event
      (cons
          '"~%~%~%~s0~%~x1~%~%"
          (cons '"****************************************"
                (cons (cons 'quote
                            (cons (cons ':derive derive-args) 'nil))
                      'nil)))))
    (events (list* thm-event print-event events))
    (fact-info (make-fact-info :thm-name thm-name
                               :formula derive-fact))
    (facts (acons derive-id fact-info facts)))
   (value (list events facts)))))

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

(defthm return-type-of-defisar-derive.result
  (implies
       (and (pseudo-event-form-listp events)
            (keyword-fact-info-alistp facts))
       (b* (((mv ?erp ?result acl2::?state)
             (defisar-derive derive-args
                             name 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-derive.result

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