Disambiguate an ambiguous cast or multiplication expression to be a multiplication expression.
(dimb-cast/mul-to-mul arg1 inc/dec arg2) → mul-expr
This is analogous in purpose to dimb-cast/call-to-call,
but for a different kind of ambiguous expression.
Note that the
Function:
(defun dimb-cast/mul-to-mul (arg1 inc/dec arg2) (declare (xargs :guard (and (exprp arg1) (inc/dec-op-listp inc/dec) (exprp arg2)))) (let ((__function__ 'dimb-cast/mul-to-mul)) (declare (ignorable __function__)) (make-expr-binary :op (binop-mul) :arg1 (apply-post-inc/dec-ops arg1 inc/dec) :arg2 arg2)))
Theorem:
(defthm exprp-of-dimb-cast/mul-to-mul (b* ((mul-expr (dimb-cast/mul-to-mul arg1 inc/dec arg2))) (exprp mul-expr)) :rule-classes :rewrite)
Theorem:
(defthm expr-unambp-of-dimb-cast/mul-to-mul (implies (and (expr-unambp arg1) (expr-unambp arg2)) (b* ((?mul-expr (dimb-cast/mul-to-mul arg1 inc/dec arg2))) (expr-unambp mul-expr))))
Theorem:
(defthm dimb-cast/mul-to-mul-of-expr-fix-arg1 (equal (dimb-cast/mul-to-mul (expr-fix arg1) inc/dec arg2) (dimb-cast/mul-to-mul arg1 inc/dec arg2)))
Theorem:
(defthm dimb-cast/mul-to-mul-expr-equiv-congruence-on-arg1 (implies (expr-equiv arg1 arg1-equiv) (equal (dimb-cast/mul-to-mul arg1 inc/dec arg2) (dimb-cast/mul-to-mul arg1-equiv inc/dec arg2))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/mul-to-mul-of-inc/dec-op-list-fix-inc/dec (equal (dimb-cast/mul-to-mul arg1 (inc/dec-op-list-fix inc/dec) arg2) (dimb-cast/mul-to-mul arg1 inc/dec arg2)))
Theorem:
(defthm dimb-cast/mul-to-mul-inc/dec-op-list-equiv-congruence-on-inc/dec (implies (inc/dec-op-list-equiv inc/dec inc/dec-equiv) (equal (dimb-cast/mul-to-mul arg1 inc/dec arg2) (dimb-cast/mul-to-mul arg1 inc/dec-equiv arg2))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/mul-to-mul-of-expr-fix-arg2 (equal (dimb-cast/mul-to-mul arg1 inc/dec (expr-fix arg2)) (dimb-cast/mul-to-mul arg1 inc/dec arg2)))
Theorem:
(defthm dimb-cast/mul-to-mul-expr-equiv-congruence-on-arg2 (implies (expr-equiv arg2 arg2-equiv) (equal (dimb-cast/mul-to-mul arg1 inc/dec arg2) (dimb-cast/mul-to-mul arg1 inc/dec arg2-equiv))) :rule-classes :congruence)