Disambiguate an ambiguous cast or multiplication expression to be a cast expression.
(dimb-cast/mul-to-cast tyname inc/dec arg) → cast-expr
This is analogous in purpose to dimb-cast/call-to-cast,
but for a different kind of ambiguous expression.
Note that the
Function:
(defun dimb-cast/mul-to-cast (tyname inc/dec arg) (declare (xargs :guard (and (tynamep tyname) (inc/dec-op-listp inc/dec) (exprp arg)))) (let ((__function__ 'dimb-cast/mul-to-cast)) (declare (ignorable __function__)) (make-expr-cast :type tyname :arg (make-expr-unary :op (unop-indir) :arg (apply-pre-inc/dec-ops inc/dec arg)))))
Theorem:
(defthm exprp-of-dimb-cast/mul-to-cast (b* ((cast-expr (dimb-cast/mul-to-cast tyname inc/dec arg))) (exprp cast-expr)) :rule-classes :rewrite)
Theorem:
(defthm expr-unambp-of-dimb-cast/mul-to-cast (implies (and (tyname-unambp tyname) (expr-unambp arg)) (b* ((?cast-expr (dimb-cast/mul-to-cast tyname inc/dec arg))) (expr-unambp cast-expr))))
Theorem:
(defthm dimb-cast/mul-to-cast-of-tyname-fix-tyname (equal (dimb-cast/mul-to-cast (tyname-fix tyname) inc/dec arg) (dimb-cast/mul-to-cast tyname inc/dec arg)))
Theorem:
(defthm dimb-cast/mul-to-cast-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (dimb-cast/mul-to-cast tyname inc/dec arg) (dimb-cast/mul-to-cast tyname-equiv inc/dec arg))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/mul-to-cast-of-inc/dec-op-list-fix-inc/dec (equal (dimb-cast/mul-to-cast tyname (inc/dec-op-list-fix inc/dec) arg) (dimb-cast/mul-to-cast tyname inc/dec arg)))
Theorem:
(defthm dimb-cast/mul-to-cast-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-cast tyname inc/dec arg) (dimb-cast/mul-to-cast tyname inc/dec-equiv arg))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/mul-to-cast-of-expr-fix-arg (equal (dimb-cast/mul-to-cast tyname inc/dec (expr-fix arg)) (dimb-cast/mul-to-cast tyname inc/dec arg)))
Theorem:
(defthm dimb-cast/mul-to-cast-expr-equiv-congruence-on-arg (implies (expr-equiv arg arg-equiv) (equal (dimb-cast/mul-to-cast tyname inc/dec arg) (dimb-cast/mul-to-cast tyname inc/dec arg-equiv))) :rule-classes :congruence)