		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Atc-read-static-var-rules

Rules about read-static-var.

These are somewhat similar to the ones about read-var. We go through the frame, the scopes, and the added (automatic) variables. We also go through the updated variables, provided that the names are distinct; this will have to be refined soon. We also go through object updates, which currently are only for objects in the heap (see update-object).

Definitions and Theorems

Theorem: read-static-var-of-add-frame

(defthm read-static-var-of-add-frame
  (equal (read-static-var var (add-frame fun compst))
         (read-static-var var compst)))

Theorem: read-static-var-of-enter-scope

(defthm read-static-var-of-enter-scope
  (equal (read-static-var var (enter-scope compst))
         (read-static-var var compst)))

Theorem: read-static-var-of-add-var

(defthm read-static-var-of-add-var
  (equal (read-static-var var (add-var var2 val compst))
         (read-static-var var compst)))

Theorem: read-static-var-of-update-var

(defthm read-static-var-of-update-var
  (implies (not (equal (ident-fix var)
                       (ident-fix var2)))
           (equal (read-static-var var (update-var var2 val compst))
                  (read-static-var var compst))))

Theorem: read-static-var-of-update-static-var

(defthm read-static-var-of-update-static-var
  (equal (read-static-var var (update-static-var var2 val compst))
         (if (equal (ident-fix var) (ident-fix var2))
             (remove-flexible-array-member val)
           (read-static-var var compst))))

Theorem: read-static-var-of-update-object

(defthm read-static-var-of-update-object
  (equal (read-static-var var (update-object objdes val compst))
         (read-static-var var compst)))