Add tag information to a tag environment.
(tag-env-add tag info env) → new-env
We return the updated environment if the tag is not already present, otherwise we return no tag environment.
Function:
(defun tag-env-add (tag info env) (declare (xargs :guard (and (identp tag) (tag-infop info) (tag-envp env)))) (let ((__function__ 'tag-env-add)) (declare (ignorable __function__)) (b* ((tag (ident-fix tag)) (info (tag-info-fix info)) (env (tag-env-fix env))) (if (omap::assoc tag env) (tag-env-option-none) (tag-env-option-some (omap::update tag info env))))))
Theorem:
(defthm tag-env-optionp-of-tag-env-add (b* ((new-env (tag-env-add tag info env))) (tag-env-optionp new-env)) :rule-classes :rewrite)
Theorem:
(defthm tag-env-add-of-ident-fix-tag (equal (tag-env-add (ident-fix tag) info env) (tag-env-add tag info env)))
Theorem:
(defthm tag-env-add-ident-equiv-congruence-on-tag (implies (ident-equiv tag tag-equiv) (equal (tag-env-add tag info env) (tag-env-add tag-equiv info env))) :rule-classes :congruence)
Theorem:
(defthm tag-env-add-of-tag-info-fix-info (equal (tag-env-add tag (tag-info-fix info) env) (tag-env-add tag info env)))
Theorem:
(defthm tag-env-add-tag-info-equiv-congruence-on-info (implies (tag-info-equiv info info-equiv) (equal (tag-env-add tag info env) (tag-env-add tag info-equiv env))) :rule-classes :congruence)
Theorem:
(defthm tag-env-add-of-tag-env-fix-env (equal (tag-env-add tag info (tag-env-fix env)) (tag-env-add tag info env)))
Theorem:
(defthm tag-env-add-tag-env-equiv-congruence-on-env (implies (tag-env-equiv env env-equiv) (equal (tag-env-add tag info env) (tag-env-add tag info env-equiv))) :rule-classes :congruence)