		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-expr-ident

Equality transformation of an identifier expression (i.e. variable).

Signature
(xeq-expr-ident ident info gin) → (mv expr gout)
Arguments: ident — Guard (identp ident).; info — Guard (var-infop info).; gin — Guard (ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (goutp gout).

Since an identifier expression has no sub-constructs, this is a special case of lifting equalities (see discussion in proof-generation), where there is no equality of sub-constructs to lift, but we just generate a new expression that is identical to the old one, with an equality theorem about them; but, importantly, the theorem includes assertions about the type of the variable and the preservation of variables (see gen-expr-thm).

We generate a theorem if the variable has a type supported in our C formalization, and if the variable is known in scope.

Definitions and Theorems

Function: xeq-expr-ident

(defun xeq-expr-ident (ident info gin)
 (declare (xargs :guard (and (identp ident)
                             (var-infop info)
                             (ginp gin))))
 (let ((__function__ 'xeq-expr-ident))
  (declare (ignorable __function__))
  (b*
   ((ident (ident-fix ident))
    ((var-info info) (var-info-fix info))
    ((gin gin) gin)
    (expr (make-expr-ident :ident ident
                           :info info))
    (gout-no-thm (gout-no-thm gin))
    ((unless (and (ident-formalp ident)
                  (type-formalp info.type)
                  (not (type-case info.type :void))
                  (not (type-case info.type :char))))
     (mv expr gout-no-thm))
    ((mv & cvar) (ldm-ident ident))
    ((mv & ctype) (ldm-type info.type))
    ((unless (omap::assoc cvar gin.vartys))
     (mv expr gout-no-thm))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::expr-ident)
            (:e c::type-fix)
            expr-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons
             ':instance
             (cons
              'expr-ident-compustate-vars
              (cons
                   (cons 'var
                         (cons (cons 'quote (cons cvar 'nil))
                               'nil))
                   (cons (cons 'type
                               (cons (cons 'quote (cons ctype 'nil))
                                     'nil))
                         'nil))))
            (cons
             (cons
              ':instance
              (cons
               'expr-ident-congruence
               (cons
                   (cons 'var
                         (cons (cons 'quote (cons cvar 'nil))
                               'nil))
                   (cons (cons 'type
                               (cons (cons 'quote (cons ctype 'nil))
                                     'nil))
                         'nil))))
             'nil))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-expr-thm expr expr gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv expr
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

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

(defthm exprp-of-xeq-expr-ident.expr
  (b* (((mv ?expr ?gout)
        (xeq-expr-ident ident info gin)))
    (exprp expr))
  :rule-classes :rewrite)

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

(defthm goutp-of-xeq-expr-ident.gout
  (b* (((mv ?expr ?gout)
        (xeq-expr-ident ident info gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-expr-ident

(defthm expr-unambp-of-expr-ident
  (b* (((mv ?expr ?gout)
        (xeq-expr-ident ident info gin)))
    (expr-unambp expr)))

Theorem: expr-annop-of-expr-ident

(defthm expr-annop-of-expr-ident
  (b* (((mv ?expr ?gout)
        (xeq-expr-ident ident info gin)))
    (expr-annop expr)))

Theorem: expr-aidentp-of-expr-ident

(defthm expr-aidentp-of-expr-ident
  (implies (ident-aidentp ident gcc)
           (b* (((mv ?expr ?gout)
                 (xeq-expr-ident ident info gin)))
             (expr-aidentp expr gcc))))

Theorem: xeq-expr-ident-of-ident-fix-ident

(defthm xeq-expr-ident-of-ident-fix-ident
  (equal (xeq-expr-ident (ident-fix ident)
                         info gin)
         (xeq-expr-ident ident info gin)))

Theorem: xeq-expr-ident-ident-equiv-congruence-on-ident

(defthm xeq-expr-ident-ident-equiv-congruence-on-ident
  (implies (c$::ident-equiv ident ident-equiv)
           (equal (xeq-expr-ident ident info gin)
                  (xeq-expr-ident ident-equiv info gin)))
  :rule-classes :congruence)

Theorem: xeq-expr-ident-of-var-info-fix-info

(defthm xeq-expr-ident-of-var-info-fix-info
  (equal (xeq-expr-ident ident (var-info-fix info)
                         gin)
         (xeq-expr-ident ident info gin)))

Theorem: xeq-expr-ident-var-info-equiv-congruence-on-info

(defthm xeq-expr-ident-var-info-equiv-congruence-on-info
  (implies (c$::var-info-equiv info info-equiv)
           (equal (xeq-expr-ident ident info gin)
                  (xeq-expr-ident ident info-equiv gin)))
  :rule-classes :congruence)

Theorem: xeq-expr-ident-of-gin-fix-gin

(defthm xeq-expr-ident-of-gin-fix-gin
  (equal (xeq-expr-ident ident info (gin-fix gin))
         (xeq-expr-ident ident info gin)))

Theorem: xeq-expr-ident-gin-equiv-congruence-on-gin

(defthm xeq-expr-ident-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (xeq-expr-ident ident info gin)
                  (xeq-expr-ident ident info gin-equiv)))
  :rule-classes :congruence)