		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-expr-cast

Equality lifting transformation of a cast expression.

Signature
(xeq-expr-cast type type-new type-thm-name arg arg-new arg-thm-name info gin) → (mv expr gout)
Arguments: type — Guard (tynamep type).; type-new — Guard (tynamep type-new).; type-thm-name — Guard (symbolp type-thm-name).; arg — Guard (exprp arg).; arg-new — Guard (exprp arg-new).; arg-thm-name — Guard (symbolp arg-thm-name).; info — Guard (tyname-infop info).; gin — Guard (ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (goutp gout).

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

For now, we generate no theorem for the transformation of the type name, but we double-check that here. The argument expression may be pure or not, since the type name does not undergo execution.

Definitions and Theorems

Function: xeq-expr-cast

(defun xeq-expr-cast (type type-new type-thm-name
                           arg arg-new arg-thm-name info gin)
 (declare (xargs :guard (and (tynamep type)
                             (tynamep type-new)
                             (symbolp type-thm-name)
                             (exprp arg)
                             (exprp arg-new)
                             (symbolp arg-thm-name)
                             (tyname-infop info)
                             (ginp gin))))
 (declare (xargs :guard (and (tyname-unambp type)
                             (tyname-annop type)
                             (tyname-unambp type-new)
                             (tyname-annop type-new)
                             (expr-unambp arg)
                             (expr-annop arg)
                             (expr-unambp arg-new)
                             (expr-annop arg-new))))
 (let ((__function__ 'xeq-expr-cast))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (expr (make-expr-cast :type type :arg arg))
    (expr-new (make-expr-cast :type type-new
                              :arg arg-new))
    ((when type-thm-name)
     (raise
      "Internal error: ~
                unexpected type name transformation theorem ~x0."
      type-thm-name)
     (mv expr-new (irr-gout)))
    ((tyname-info info) info)
    ((unless (and arg-thm-name (type-formalp info.type)
                  (not (type-case info.type :void))
                  (not (type-case info.type :char))))
     (mv expr-new (gout-no-thm gin)))
    ((unless (equal type type-new))
     (raise
      "Internal error: ~
                type names ~x0 and ~x1 differ."
      type type-new)
     (mv expr-new (irr-gout)))
    ((mv & ctyname) (ldm-tyname type))
    ((mv & old-arg) (ldm-expr arg))
    ((mv & new-arg) (ldm-expr arg-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::expr-cast)
            (:e c::tyname-to-type)
            (:e c::type-nonchar-integerp)
            expr-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons arg-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'expr-cast-congruence
               (cons
                (cons 'tyname
                      (cons (cons 'quote (cons ctyname 'nil))
                            'nil))
                (cons
                 (cons 'old-arg
                       (cons (cons 'quote (cons old-arg 'nil))
                             'nil))
                 (cons (cons 'new-arg
                             (cons (cons 'quote (cons new-arg 'nil))
                                   'nil))
                       'nil)))))
             (cons
              (cons
               ':instance
               (cons
                'expr-cast-errors
                (cons
                 (cons 'tyname
                       (cons (cons 'quote (cons ctyname 'nil))
                             'nil))
                 (cons (cons 'arg
                             (cons (cons 'quote (cons old-arg 'nil))
                                   'nil))
                       '((fenv old-fenv))))))
              'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-expr-thm expr expr-new gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv expr-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

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

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

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

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

Theorem: expr-unambp-of-xeq-expr-cast

(defthm expr-unambp-of-xeq-expr-cast
  (implies (and (tyname-unambp type-new)
                (expr-unambp arg-new))
           (b* (((mv ?expr ?gout)
                 (xeq-expr-cast type type-new type-thm-name
                                arg arg-new arg-thm-name info gin)))
             (expr-unambp expr))))

Theorem: expr-annop-of-xeq-expr-cast

(defthm expr-annop-of-xeq-expr-cast
  (implies (and (tyname-annop type-new)
                (expr-annop arg-new))
           (b* (((mv ?expr ?gout)
                 (xeq-expr-cast type type-new type-thm-name
                                arg arg-new arg-thm-name info gin)))
             (expr-annop expr))))

Theorem: expr-aidentp-of-xeq-expr-cast

(defthm expr-aidentp-of-xeq-expr-cast
  (implies (and (tyname-aidentp type-new gcc)
                (expr-aidentp arg-new gcc))
           (b* (((mv ?expr ?gout)
                 (xeq-expr-cast type type-new type-thm-name
                                arg arg-new arg-thm-name info gin)))
             (expr-aidentp expr gcc))))