		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-cast/mul-to-cast

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

Signature
(dimb-cast/mul-to-cast tyname inc/dec arg) → cast-expr
Arguments: tyname — Guard (tynamep tyname).; inc/dec — Guard (inc/dec-op-listp inc/dec).; arg — Guard (exprp arg).
Returns: cast-expr — Type (exprp cast-expr).

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

Definitions and Theorems

Function: dimb-cast/mul-to-cast

(defun dimb-cast/mul-to-cast (tyname inc/dec arg)
  (declare (xargs :guard (and (tynamep tyname)
                              (inc/dec-op-listp inc/dec)
                              (exprp arg))))
  (declare (xargs :guard (and (tyname-unambp tyname)
                              (expr-unambp arg))))
  (let ((__function__ 'dimb-cast/mul-to-cast))
    (declare (ignorable __function__))
    (dimb-make/adjust-expr-cast
         tyname inc/dec
         (dimb-make/adjust-expr-unary (unop-indir)
                                      arg))))

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

(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: expr-unambp-of-dimb-cast/mul-to-cast

(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: dimb-cast/mul-to-cast-of-tyname-fix-tyname

(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: dimb-cast/mul-to-cast-tyname-equiv-congruence-on-tyname

(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: dimb-cast/mul-to-cast-of-inc/dec-op-list-fix-inc/dec

(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: dimb-cast/mul-to-cast-inc/dec-op-list-equiv-congruence-on-inc/dec

(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: dimb-cast/mul-to-cast-of-expr-fix-arg

(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: dimb-cast/mul-to-cast-expr-equiv-congruence-on-arg

(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)