		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-formula-to-hyps+concl

Decompose the input formula into hypotheses and conclusion.

Signature
(defisar-formula-to-hyps+concl formula) → (mv hyps concl)
Returns: hyps — Type (true-listp hyps).

Definitions and Theorems

Function: defisar-formula-to-hyps+concl

(defun defisar-formula-to-hyps+concl (formula)
 (declare (xargs :guard t))
 (let ((__function__ 'defisar-formula-to-hyps+concl))
  (declare (ignorable __function__))
  (case-match formula
   (('implies hyp/hyps concl)
    (case-match hyp/hyps
     (('and . hyp/hyps)
      (if (true-listp hyp/hyps)
          (mv hyp/hyps concl)
       (prog2$
           (raise "Internal error: malformed hypotheses ~x0 in ~x1."
                  hyp/hyps formula)
           (mv nil nil))))
     (& (mv (list hyp/hyps) concl))))
   (& (mv nil formula)))))

Theorem: true-listp-of-defisar-formula-to-hyps+concl.hyps

(defthm true-listp-of-defisar-formula-to-hyps+concl.hyps
  (b* (((mv ?hyps ?concl)
        (defisar-formula-to-hyps+concl formula)))
    (true-listp hyps))
  :rule-classes :rewrite)