		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-cast/and-to-and

Disambiguate an ambiguous cast or conjunction expression to be a conjunction expression.

Signature
(dimb-cast/and-to-and arg1 inc/dec arg2) → expr
Arguments: arg1 — Guard (exprp arg1).; inc/dec — Guard (inc/dec-op-listp inc/dec).; arg2 — Guard (exprp arg2).
Returns: expr — Type (exprp expr).

This is analogous in purpose to dimb-cast/call-to-call, but for a different kind of ambiguous expression. Note that the &, which is binary in this disambiguation, is implicit in the abstract syntax of the ambiguous expression.

Definitions and Theorems

Function: dimb-cast/and-to-and

(defun dimb-cast/and-to-and (arg1 inc/dec arg2)
  (declare (xargs :guard (and (exprp arg1)
                              (inc/dec-op-listp inc/dec)
                              (exprp arg2))))
  (declare (xargs :guard (and (expr-unambp arg1)
                              (expr-unambp arg2))))
  (let ((__function__ 'dimb-cast/and-to-and))
    (declare (ignorable __function__))
    (dimb-make/adjust-expr-binary
         (binop-bitand)
         (apply-post-inc/dec-ops arg1 inc/dec)
         arg2)))

Theorem: exprp-of-dimb-cast/and-to-and

(defthm exprp-of-dimb-cast/and-to-and
  (b* ((expr (dimb-cast/and-to-and arg1 inc/dec arg2)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-dimb-cast/and-to-and

(defthm expr-unambp-of-dimb-cast/and-to-and
  (implies (and (expr-unambp arg1)
                (expr-unambp arg2))
           (b* ((?expr (dimb-cast/and-to-and arg1 inc/dec arg2)))
             (expr-unambp expr))))

Theorem: dimb-cast/and-to-and-of-expr-fix-arg1

(defthm dimb-cast/and-to-and-of-expr-fix-arg1
  (equal (dimb-cast/and-to-and (expr-fix arg1)
                               inc/dec arg2)
         (dimb-cast/and-to-and arg1 inc/dec arg2)))

Theorem: dimb-cast/and-to-and-expr-equiv-congruence-on-arg1

(defthm dimb-cast/and-to-and-expr-equiv-congruence-on-arg1
  (implies (expr-equiv arg1 arg1-equiv)
           (equal (dimb-cast/and-to-and arg1 inc/dec arg2)
                  (dimb-cast/and-to-and arg1-equiv inc/dec arg2)))
  :rule-classes :congruence)

Theorem: dimb-cast/and-to-and-of-inc/dec-op-list-fix-inc/dec

(defthm dimb-cast/and-to-and-of-inc/dec-op-list-fix-inc/dec
  (equal (dimb-cast/and-to-and arg1 (inc/dec-op-list-fix inc/dec)
                               arg2)
         (dimb-cast/and-to-and arg1 inc/dec arg2)))

Theorem: dimb-cast/and-to-and-inc/dec-op-list-equiv-congruence-on-inc/dec

(defthm
   dimb-cast/and-to-and-inc/dec-op-list-equiv-congruence-on-inc/dec
  (implies (inc/dec-op-list-equiv inc/dec inc/dec-equiv)
           (equal (dimb-cast/and-to-and arg1 inc/dec arg2)
                  (dimb-cast/and-to-and arg1 inc/dec-equiv arg2)))
  :rule-classes :congruence)

Theorem: dimb-cast/and-to-and-of-expr-fix-arg2

(defthm dimb-cast/and-to-and-of-expr-fix-arg2
  (equal (dimb-cast/and-to-and arg1 inc/dec (expr-fix arg2))
         (dimb-cast/and-to-and arg1 inc/dec arg2)))

Theorem: dimb-cast/and-to-and-expr-equiv-congruence-on-arg2

(defthm dimb-cast/and-to-and-expr-equiv-congruence-on-arg2
  (implies (expr-equiv arg2 arg2-equiv)
           (equal (dimb-cast/and-to-and arg1 inc/dec arg2)
                  (dimb-cast/and-to-and arg1 inc/dec arg2-equiv)))
  :rule-classes :congruence)