		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-derive-thm-hyps

Generate the hypotheses for the theorem generated for a :derive command.

Signature
(defisar-derive-thm-hyps derive-from facts ctx state) → (mv erp thm-hyps state)
Arguments: derive-from — Guard (keyword-listp derive-from).; facts — Guard (keyword-fact-info-alistp facts).
Returns: thm-hyps — Type (true-listp thm-hyps).

Definitions and Theorems

Function: defisar-derive-thm-hyps

(defun defisar-derive-thm-hyps (derive-from facts ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (keyword-listp derive-from)
                              (keyword-fact-info-alistp facts))))
  (let ((__function__ 'defisar-derive-thm-hyps))
    (declare (ignorable __function__))
    (b* (((when (endp derive-from)) (value nil))
         (id (car derive-from))
         (lookup (assoc-eq id facts))
         ((unless (consp lookup))
          (er-soft+ ctx t nil "Fact ~x0 not found." id))
         (info (cdr lookup))
         (thm-hyp (fact-info->formula info))
         ((er thm-hyps)
          (defisar-derive-thm-hyps (cdr derive-from)
                                   facts ctx state)))
      (value (cons thm-hyp thm-hyps)))))

Theorem: true-listp-of-defisar-derive-thm-hyps.thm-hyps

(defthm true-listp-of-defisar-derive-thm-hyps.thm-hyps
  (b* (((mv ?erp ?thm-hyps acl2::?state)
        (defisar-derive-thm-hyps derive-from facts ctx state)))
    (true-listp thm-hyps))
  :rule-classes :rewrite)