Rules about update-var.
The theorems about update-var push them into the states, sometimes combining them into add-vars.
The first theorem turns update-var into update-static-var when reaching add-frame: at that point, there are no more accessible variables (by name) in automatic storage.
The second theorem pushes update-var into enter-scope.
The third theorem combines update-var with add-var if the variable is the same, otherwise it pushes update-var in.
The fourth theorem overwrites an update-var with an update-var for the same variable.
The fifth theorem is used to arrange a nest of update-vars in alphabetical order of the variable names: it swaps two update-vars when the outer one has an larger variable than the inner one. Note that we need to disable loop stoppers for this rule, otherwise ACL2 may not apply it based on the written value terms, which are irrelevant to this normalization based on alphabetical order. Note the syntaxp hypotheses that require the identifiers (i.e. variable names) to have the form described in atc-identifier-rules.
Finally, the sixth theorem serves to simplify the case in which
a variable is written with its current value;
this case may occur when proving the base case of a loop.
This theorem is phrased perhaps more generally than expected,
with two different computation state variables,
instead of the simpler form in
Theorem:
(defthm update-var-of-add-frame (equal (update-var var val (add-frame fun compst)) (add-frame fun (update-static-var var val compst))))
Theorem:
(defthm update-var-of-enter-scope (equal (update-var var val (enter-scope compst)) (enter-scope (update-var var val compst))))
Theorem:
(defthm update-var-of-add-var (equal (update-var var val (add-var var2 val2 compst)) (if (equal (ident-fix var) (ident-fix var2)) (add-var var2 val compst) (add-var var2 val2 (update-var var val compst)))))
Theorem:
(defthm update-var-of-update-var-same (equal (update-var var val (update-var var val2 compst)) (update-var var val compst)))
Theorem:
(defthm update-var-of-update-var-less (implies (and (syntaxp (and (consp var2) (eq (car var2) 'ident) (quotep (cadr var2)))) (syntaxp (and (consp var) (eq (car var) 'ident) (quotep (cadr var)))) (<< (ident-fix var2) (ident-fix var)) (> (compustate-frames-number compst) 0)) (equal (update-var var val (update-var var2 val2 compst)) (update-var var2 val2 (update-var var val compst)))) :rule-classes ((:rewrite :loop-stopper nil)))
Theorem:
(defthm update-var-of-read-var-same (implies (and (syntaxp (symbolp compst)) (compustatep compst1) (> (compustate-frames-number compst1) 0) (valuep (read-var var compst)) (not (flexible-array-member-p (read-var var compst))) (equal (read-var var compst) (read-var var compst1))) (equal (update-var var (read-var var compst) compst1) compst1)))