		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Conjoin-expressions

Conjoin a list of expressions.

Signature
(conjoin-expressions exprs) → conjoined-expression
Arguments: exprs — Guard (expression-listp exprs).
Returns: conjoined-expression — Type (expressionp conjoined-expression).

Currently Syntheto's boolean conjunction operator is binary. Thus, to conjoin a list of expressions, we need to build a nest. If there are no expressions, we return the boolean literal for false. If there is one expression, we return it. If there are two or more expressions, we return a nest.

Definitions and Theorems

Function: conjoin-expressions

(defun conjoin-expressions (exprs)
 (declare (xargs :guard (expression-listp exprs)))
 (let ((__function__ 'conjoin-expressions))
  (declare (ignorable __function__))
  (cond
       ((endp exprs)
        (expression-literal (literal-boolean t)))
       ((endp (cdr exprs))
        (expression-fix (car exprs)))
       (t (make-expression-binary
               :operator (binary-op-and)
               :left-operand (car exprs)
               :right-operand (conjoin-expressions (cdr exprs)))))))

Theorem: expressionp-of-conjoin-expressions

(defthm expressionp-of-conjoin-expressions
  (b* ((conjoined-expression (conjoin-expressions exprs)))
    (expressionp conjoined-expression))
  :rule-classes :rewrite)

Theorem: conjoin-expressions-of-expression-list-fix-exprs

(defthm conjoin-expressions-of-expression-list-fix-exprs
  (equal (conjoin-expressions (expression-list-fix exprs))
         (conjoin-expressions exprs)))

Theorem: conjoin-expressions-expression-list-equiv-congruence-on-exprs

(defthm
      conjoin-expressions-expression-list-equiv-congruence-on-exprs
  (implies (expression-list-equiv exprs exprs-equiv)
           (equal (conjoin-expressions exprs)
                  (conjoin-expressions exprs-equiv)))
  :rule-classes :congruence)