		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Disjoin-expressions

Disjoin a list of expressions.

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

Currently Syntheto's boolean disjunction operator is binary. Thus, to disjoin 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: disjoin-expressions

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

Theorem: expressionp-of-disjoin-expressions

(defthm expressionp-of-disjoin-expressions
  (b* ((disjoined-expression (disjoin-expressions exprs)))
    (expressionp disjoined-expression))
  :rule-classes :rewrite)

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

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

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

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