Theorems about init-local for the static soundness proof.
Some of these are actually more general and could be moved. These more general theorems are about adding variables, which is what init-local does for the local state of course.
First, we show that add-var-value fails iff add-var does (the value put into the variable entails no constraints), and the same holds for add-vars-values and add-vars provided that the number of values matches the number of variables.
We prove a theorem that characterizes the effect of init-local on the variable table of the computation state. This should belong to the theorems in theorems-about-cstate-to-vars-and-execution, and it can probably put there, but currently it needs some other theorems, but it may be possible to streamline and simplify its proof.
We finally show that init-local fails iff the addition of the variables to the variable table fails, or the number of values does not match the number of variables.
(defthm error-add-var-value-iff-error-add-var (equal (reserrp (add-var-value var val cstate)) (reserrp (add-var var (cstate-to-vars cstate)))))
(defthm error-add-vars-values-iff-error-add-vars (implies (equal (len vals) (len vars)) (equal (reserrp (add-vars-values vars vals cstate)) (reserrp (add-vars vars (cstate-to-vars cstate))))))
(defthm cstate-to-vars-of-init-local (implies (and (equal (len in-vals) (len in-vars)) (not (reserrp (init-local in-vars in-vals out-vars cstate)))) (equal (cstate-to-vars (init-local in-vars in-vals out-vars cstate)) (add-vars out-vars (add-vars in-vars nil)))))
(defthm check-var-list-when-add-vars-not-error (implies (and (identifier-listp vars) (identifier-setp varset) (not (reserrp (add-vars vars varset)))) (check-var-list vars (add-vars vars varset))))