		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-cast/addsub-to-addsub

Disambiguate an ambiguous cast or addition/subtraction expression to be an addition or subtraction expression.

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

This is analogous in purpose to dimb-cast/call-to-call, but for a different kind of ambiguous expression, actually two kinds, which are very similar and thus handled together; the two kinds are selected by the binary operator passed as input. Note that the + or -, which is binary in this disambiguation, is implicit in the abstract syntax of the ambiguous expression.

Definitions and Theorems

Function: dimb-cast/addsub-to-addsub

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: dimb-cast/addsub-to-addsub-of-binop-fix-add/sub

(defthm dimb-cast/addsub-to-addsub-of-binop-fix-add/sub
 (equal
  (dimb-cast/addsub-to-addsub arg1 inc/dec arg2 (binop-fix add/sub))
  (dimb-cast/addsub-to-addsub arg1 inc/dec arg2 add/sub)))

Theorem: dimb-cast/addsub-to-addsub-binop-equiv-congruence-on-add/sub

(defthm dimb-cast/addsub-to-addsub-binop-equiv-congruence-on-add/sub
 (implies
  (binop-equiv add/sub add/sub-equiv)
  (equal
      (dimb-cast/addsub-to-addsub arg1 inc/dec arg2 add/sub)
      (dimb-cast/addsub-to-addsub arg1 inc/dec arg2 add/sub-equiv)))
 :rule-classes :congruence)