Rules about write-static-var.
These are analogous to the ones for write-var. We introduce a predicate saying when write-static-var is equivalent to update-static-var, and rules to show that the predicate holds. The second-to-last rule states the equivalence.
The last rule is more about
Function:
(defun write-static-var-okp (var val compst) (declare (xargs :guard (and (identp var) (valuep val) (compustatep compst)))) (let ((__function__ 'write-static-var-okp)) (declare (ignorable __function__)) (b* ((static (compustate->static compst)) (pair (omap::assoc (ident-fix var) static))) (and (consp pair) (equal (type-of-value (cdr pair)) (type-of-value val))))))
Theorem:
(defthm booleanp-of-write-static-var-okp (b* ((yes/no (write-static-var-okp var val compst))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm write-static-var-okp-of-ident-fix-var (equal (write-static-var-okp (ident-fix var) val compst) (write-static-var-okp var val compst)))
Theorem:
(defthm write-static-var-okp-ident-equiv-congruence-on-var (implies (ident-equiv var var-equiv) (equal (write-static-var-okp var val compst) (write-static-var-okp var-equiv val compst))) :rule-classes :congruence)
Theorem:
(defthm write-static-var-okp-of-value-fix-val (equal (write-static-var-okp var (value-fix val) compst) (write-static-var-okp var val compst)))
Theorem:
(defthm write-static-var-okp-value-equiv-congruence-on-val (implies (value-equiv val val-equiv) (equal (write-static-var-okp var val compst) (write-static-var-okp var val-equiv compst))) :rule-classes :congruence)
Theorem:
(defthm write-static-var-okp-of-compustate-fix-compst (equal (write-static-var-okp var val (compustate-fix compst)) (write-static-var-okp var val compst)))
Theorem:
(defthm write-static-var-okp-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (write-static-var-okp var val compst) (write-static-var-okp var val compst-equiv))) :rule-classes :congruence)
Theorem:
(defthm write-static-var-okp-of-add-frame (equal (write-static-var-okp var val (add-frame fun compst)) (write-static-var-okp var val compst)))
Theorem:
(defthm write-static-var-okp-of-enter-scope (equal (write-static-var-okp var val (enter-scope compst)) (write-static-var-okp var val compst)))
Theorem:
(defthm write-static-var-okp-of-add-var (equal (write-static-var-okp var val (add-var var2 val2 compst)) (write-static-var-okp var val compst)))
Theorem:
(defthm write-static-var-okp-of-update-var (implies (not (equal (ident-fix var) (ident-fix var2))) (equal (write-static-var-okp var val (update-var var2 val2 compst)) (write-static-var-okp var val compst))))
Theorem:
(defthm write-static-var-okp-of-update-static-var (equal (write-static-var-okp var val (update-static-var var2 val2 compst)) (if (equal (ident-fix var) (ident-fix var2)) (equal (type-of-value val2) (type-of-value val)) (write-static-var-okp var val compst))))
Theorem:
(defthm write-static-var-okp-of-update-object (equal (write-static-var-okp var val (update-object objdes obj compst)) (write-static-var-okp var val compst)))
Theorem:
(defthm write-static-var-okp-when-valuep-of-read-static-var (implies (and (syntaxp (symbolp compst)) (equal old-val (read-static-var var compst)) (valuep old-val)) (equal (write-static-var-okp var val compst) (equal (type-of-value val) (type-of-value old-val)))))
Theorem:
(defthm write-static-var-to-update-static-var (implies (write-static-var-okp var val compst) (equal (write-static-var var val compst) (update-static-var var val compst))))
Theorem:
(defthm write-var-okp-of-add-frame (equal (write-var-okp var val (add-frame fun compst)) (write-static-var-okp var val (add-frame fun compst))))