		Search-engine friendly clone of the ACL2 documentation.

Variable-resolution-preservation

Var-resolve-preservep-of-exec

Preservation of variable resolution under execution, for any number of peeled frames and scopes.

We prove by induction that var-resolve-preservep holds between each computation state before execution and the computation state after execution. As explained in variable-resolution-preservation, the theorems are weakened for object declarations, block items, and lists of block items, by going back to the previous scope or frame.

Definitions and Theorems

Theorem: var-resolve-preservep-of-exec-fun

(defthm var-resolve-preservep-of-exec-fun
  (b* (((mv result compst1)
        (exec-fun fun args compst fenv limit)))
    (implies (not (errorp result))
             (var-resolve-preservep compst compst1))))

Theorem: var-resolve-preservep-of-exec-expr

(defthm var-resolve-preservep-of-exec-expr
  (b* (((mv result compst1)
        (exec-expr e compst fenv limit)))
    (implies (not (errorp result))
             (var-resolve-preservep compst compst1))))

Theorem: var-resolve-preservep-of-exec-expr-list

(defthm var-resolve-preservep-of-exec-expr-list
  (b* (((mv result compst1)
        (exec-expr-list es compst fenv limit)))
    (implies (not (errorp result))
             (var-resolve-preservep compst compst1))))

Theorem: var-resolve-preservep-of-exec-stmt

(defthm var-resolve-preservep-of-exec-stmt
  (b* (((mv result compst1)
        (exec-stmt s compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-resolve-preservep compst compst1))))

Theorem: var-resolve-preservep-of-exec-stmt-while

(defthm var-resolve-preservep-of-exec-stmt-while
  (b* (((mv result compst1)
        (exec-stmt-while test body compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-resolve-preservep compst compst1))))

Theorem: var-resolve-preservep-of-exec-stmt-dowhile

(defthm var-resolve-preservep-of-exec-stmt-dowhile
  (b* (((mv result compst1)
        (exec-stmt-dowhile body test compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-resolve-preservep compst compst1))))

Theorem: var-resolve-preservep-of-exec-initer

(defthm var-resolve-preservep-of-exec-initer
  (b* (((mv result compst1)
        (exec-initer initer compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-resolve-preservep compst compst1))))

Theorem: var-resolve-preservep-of-exec-obj-declon

(defthm var-resolve-preservep-of-exec-obj-declon
  (b* ((compst1 (exec-obj-declon declon compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp compst1)))
             (var-resolve-preservep (prev-scope/frame compst)
                                    (prev-scope/frame compst1)))))

Theorem: var-resolve-preservep-of-exec-block-item

(defthm var-resolve-preservep-of-exec-block-item
  (b* (((mv result compst1)
        (exec-block-item item compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-resolve-preservep (prev-scope/frame compst)
                                    (prev-scope/frame compst1)))))

Theorem: var-resolve-preservep-of-exec-block-item-list

(defthm var-resolve-preservep-of-exec-block-item-list
  (b* (((mv result compst1)
        (exec-block-item-list items compst fenv limit)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp result)))
             (var-resolve-preservep (prev-scope/frame compst)
                                    (prev-scope/frame compst1)))))