Rules about update-static-var.
These are similar to the ones for update-var and update-object.
Theorem:
(defthm update-static-var-of-add-frame (equal (update-static-var var val (add-frame fun compst)) (add-frame fun (update-static-var var val compst))))
Theorem:
(defthm update-static-var-of-enter-scope (equal (update-static-var var val (enter-scope compst)) (enter-scope (update-static-var var val compst))))
Theorem:
(defthm update-static-var-of-add-var (equal (update-static-var var val (add-var var2 val2 compst)) (add-var var2 val2 (update-static-var var val compst))))
Theorem:
(defthm update-static-var-of-update-var (implies (not (equal (ident-fix var) (ident-fix var2))) (equal (update-static-var var val (update-var var2 val2 compst)) (update-var var2 val2 (update-static-var var val compst)))))
Theorem:
(defthm update-static-var-of-update-static-var-same (equal (update-static-var var val (update-static-var var val2 compst)) (update-static-var var val compst)))
Theorem:
(defthm update-static-var-of-update-static-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))) (equal (update-static-var var val (update-static-var var2 val2 compst)) (update-static-var var2 val2 (update-static-var var val compst)))) :rule-classes ((:rewrite :loop-stopper nil)))
Theorem:
(defthm update-static-var-of-read-static-var-same (implies (and (syntaxp (symbolp compst)) (compustatep compst1) (valuep (read-static-var var compst)) (not (flexible-array-member-p (read-static-var var compst))) (equal (read-static-var var compst) (read-static-var var compst1))) (equal (update-static-var var (read-static-var var compst) compst1) compst1)))
Theorem:
(defthm update-static-var-of-if*-val (equal (update-static-var var (if* a b c) compst) (if* a (update-static-var var b compst) (update-static-var var c compst))))