Disambiguate an ambiguous cast or addition/subtraction expression to be an addition or subtraction expression.
(dimb-cast/addsub-to-addsub arg1 inc/dec arg2 add/sub) → 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
Function:
(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 (or (binop-case add/sub :add) (binop-case add/sub :sub)))) (let ((__function__ 'dimb-cast/addsub-to-addsub)) (declare (ignorable __function__)) (make-expr-binary :op add/sub :arg1 (apply-post-inc/dec-ops arg1 inc/dec) :arg2 arg2)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)