		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-ident

Transform an identifier expression (i.e. a variable).

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

This undergoes no actual transformation, but we introduce it for uniformity, also because we may eventually evolve the simpadd0 implementation into a much more general transformation. Thus, the output identifier and validation information are always the same as the input ones.

If the variable has type int, which we check in the validation information, then we generate a theorem saying that the expression, when executed, yields a value of type int.

Under the assumption that the variable is in scope, which is included in the generated theorem, the execution of a variable never results in an error, so we pass nil as the falliblep flag to the theorem generation function, and we set to nil the falliblep component of simpadd0-gout.

The generated theorem is proved via a general supporting lemma, which is proved below.

Definitions and Theorems

Function: simpadd0-expr-ident

(defun simpadd0-expr-ident (ident info gin)
 (declare (xargs :guard (and (identp ident)
                             (c$::var-infop info)
                             (simpadd0-ginp gin))))
 (let ((__function__ 'simpadd0-expr-ident))
  (declare (ignorable __function__))
  (b*
   ((ident (ident-fix ident))
    (info (c$::var-info-fix info))
    ((simpadd0-gin gin) gin)
    ((c$::var-info info) info)
    ((unless (c$::type-case info.type :sint))
     (mv ident info
         (make-simpadd0-gout :events nil
                             :thm-name nil
                             :thm-index gin.thm-index
                             :names-to-avoid gin.names-to-avoid
                             :vars nil
                             :diffp nil
                             :falliblep nil)))
    (vars (insert ident nil))
    (expr (c$::expr-ident ident info))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c$::expr-ident)
            (:e c$::expr-pure-formalp)
            (:e ident))
         (cons
          ':use
          (cons
           (cons
            ':instance
            (cons
              'simpadd0-expr-ident-support-lemma
              (cons (cons 'ident
                          (cons (cons 'quote (cons ident 'nil))
                                'nil))
                    (cons (cons 'info
                                (cons (cons 'quote (cons info 'nil))
                                      'nil))
                          'nil))))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (simpadd0-gen-expr-pure-thm
          expr expr nil vars
          gin.const-new gin.thm-index hints)))
   (mv ident info
       (make-simpadd0-gout :events (list thm-event)
                           :thm-name thm-name
                           :thm-index thm-index
                           :names-to-avoid (list thm-name)
                           :vars vars
                           :diffp nil
                           :falliblep nil)))))

Theorem: identp-of-simpadd0-expr-ident.new-ident

(defthm identp-of-simpadd0-expr-ident.new-ident
  (b* (((mv ?new-ident ?new-info ?gout)
        (simpadd0-expr-ident ident info gin)))
    (identp new-ident))
  :rule-classes :rewrite)

Theorem: var-infop-of-simpadd0-expr-ident.new-info

(defthm var-infop-of-simpadd0-expr-ident.new-info
  (b* (((mv ?new-ident ?new-info ?gout)
        (simpadd0-expr-ident ident info gin)))
    (c$::var-infop new-info))
  :rule-classes :rewrite)

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

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

Theorem: simpadd0-expr-ident-support-lemma

(defthm simpadd0-expr-ident-support-lemma
 (b* ((expr (mv-nth 1
                    (c$::ldm-expr (c$::expr-ident ident info))))
      (expr-result (c::exec-expr-pure expr compst))
      (expr-value (c::expr-value->value expr-result)))
   (implies (and (c$::expr-pure-formalp (c$::expr-ident ident info))
                 (b* ((var (mv-nth 1 (c$::ldm-ident ident)))
                      (objdes (c::objdesign-of-var var compst))
                      (val (c::read-object objdes compst)))
                   (and objdes (c::valuep val)
                        (c::value-case val :sint))))
            (equal (c::value-kind expr-value)
                   :sint))))

Theorem: simpadd0-expr-ident-of-ident-fix-ident

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

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

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

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

(defthm simpadd0-expr-ident-of-var-info-fix-info
  (equal (simpadd0-expr-ident ident (c$::var-info-fix info)
                              gin)
         (simpadd0-expr-ident ident info gin)))

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

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

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

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

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

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