		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-cast

Transform a cast expression.

Signature
(simpadd0-expr-cast type type-new type-events type-thm-name type-vartys type-diffp arg arg-new arg-events arg-thm-name arg-vartys arg-diffp gin) → (mv expr gout)
Arguments: type — Guard (tynamep type).; type-new — Guard (tynamep type-new).; type-events — Guard (pseudo-event-form-listp type-events).; type-thm-name — Guard (symbolp type-thm-name).; type-vartys — Guard (ident-type-mapp type-vartys).; type-diffp — Guard (booleanp type-diffp).; arg — Guard (exprp arg).; arg-new — Guard (exprp arg-new).; arg-events — Guard (pseudo-event-form-listp arg-events).; arg-thm-name — Guard (symbolp arg-thm-name).; arg-vartys — Guard (ident-type-mapp arg-vartys).; arg-diffp — Guard (booleanp arg-diffp).; gin — Guard (simpadd0-ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (simpadd0-goutp gout).

The resulting expression is obtained by combining the possibly transformed type name with the possibly transformed argument expression.

Definitions and Theorems

Function: simpadd0-expr-cast

(defun simpadd0-expr-cast
       (type type-new
             type-events type-thm-name type-vartys
             type-diffp arg arg-new arg-events
             arg-thm-name arg-vartys arg-diffp gin)
 (declare (xargs :guard (and (tynamep type)
                             (tynamep type-new)
                             (pseudo-event-form-listp type-events)
                             (symbolp type-thm-name)
                             (ident-type-mapp type-vartys)
                             (booleanp type-diffp)
                             (exprp arg)
                             (exprp arg-new)
                             (pseudo-event-form-listp arg-events)
                             (symbolp arg-thm-name)
                             (ident-type-mapp arg-vartys)
                             (booleanp arg-diffp)
                             (simpadd0-ginp gin))))
 (declare (ignore type type-thm-name arg arg-thm-name))
 (declare (xargs :guard (and (tyname-unambp type)
                             (expr-unambp arg))))
 (let ((__function__ 'simpadd0-expr-cast))
  (declare (ignorable __function__))
  (b*
   (((simpadd0-gin gin) gin)
    (expr-new (make-expr-cast :type type-new
                              :arg arg-new))
    (type-vartys (ident-type-map-fix type-vartys))
    (arg-vartys (ident-type-map-fix arg-vartys))
    ((unless (omap::compatiblep type-vartys arg-vartys))
     (raise
      "Internal error: ~
                incompatible variable-type maps ~x0 and ~x1."
      type-vartys arg-vartys)
     (mv (irr-expr) (irr-simpadd0-gout)))
    (vartys (omap::update* type-vartys arg-vartys))
    (diffp (or type-diffp arg-diffp)))
   (mv expr-new
       (make-simpadd0-gout :events (append type-events arg-events)
                           :thm-name nil
                           :thm-index gin.thm-index
                           :names-to-avoid gin.names-to-avoid
                           :vartys vartys
                           :diffp diffp)))))

Theorem: exprp-of-simpadd0-expr-cast.expr

(defthm exprp-of-simpadd0-expr-cast.expr
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-cast type type-new
                            type-events type-thm-name type-vartys
                            type-diffp arg arg-new arg-events
                            arg-thm-name arg-vartys arg-diffp gin)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-expr-cast.gout

(defthm simpadd0-goutp-of-simpadd0-expr-cast.gout
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-cast type type-new
                            type-events type-thm-name type-vartys
                            type-diffp arg arg-new arg-events
                            arg-thm-name arg-vartys arg-diffp gin)))
    (simpadd0-goutp gout))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-simpadd0-expr-cast

(defthm expr-unambp-of-simpadd0-expr-cast
 (implies
  (and (tyname-unambp type-new)
       (expr-unambp arg-new))
  (b* (((mv ?expr ?gout)
        (simpadd0-expr-cast type type-new
                            type-events type-thm-name type-vartys
                            type-diffp arg arg-new arg-events
                            arg-thm-name arg-vartys arg-diffp gin)))
    (expr-unambp expr))))