Rules about create-var.
The theorem about create-var turns that into add-var,
provided that the variable can be created,
which we check via the function
Function:
(defun create-var-okp (var compst) (declare (xargs :guard (and (identp var) (compustatep compst)))) (declare (xargs :guard (> (compustate-frames-number compst) 0))) (let ((__function__ 'create-var-okp)) (declare (ignorable __function__)) (b* ((frame (top-frame compst)) (scopes (frame->scopes frame)) (scope (car scopes))) (not (consp (omap::assoc (ident-fix var) scope))))))
Theorem:
(defthm booleanp-of-create-var-okp (b* ((yes/no (create-var-okp var compst))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm create-var-okp-of-ident-fix-var (equal (create-var-okp (ident-fix var) compst) (create-var-okp var compst)))
Theorem:
(defthm create-var-okp-ident-equiv-congruence-on-var (implies (ident-equiv var var-equiv) (equal (create-var-okp var compst) (create-var-okp var-equiv compst))) :rule-classes :congruence)
Theorem:
(defthm create-var-okp-of-compustate-fix-compst (equal (create-var-okp var (compustate-fix compst)) (create-var-okp var compst)))
Theorem:
(defthm create-var-okp-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (create-var-okp var compst) (create-var-okp var compst-equiv))) :rule-classes :congruence)
Theorem:
(defthm create-var-okp-of-add-frame (create-var-okp var (add-frame fun compst)))
Theorem:
(defthm create-var-okp-of-enter-scope (create-var-okp var (enter-scope compst)))
Theorem:
(defthm create-var-okp-of-add-var (equal (create-var-okp var (add-var var2 val compst)) (and (not (equal (ident-fix var) (ident-fix var2))) (create-var-okp var compst))))
Theorem:
(defthm create-var-okp-of-update-var (equal (create-var-okp var (update-var var2 val compst)) (create-var-okp var compst)))
Theorem:
(defthm create-var-okp-of-update-object (equal (create-var-okp var (update-object objdes val compst)) (create-var-okp var compst)))
Theorem:
(defthm create-var-to-add-var (implies (and (create-var-okp var compst) (> (compustate-frames-number compst) 0)) (equal (create-var var val compst) (add-var var val compst))))