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.
The theorem
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.
Theorem:
(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)))))
Theorem:
(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))))))
Theorem:
(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)))))
Theorem:
(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))))
Theorem:
(defthm reserrp-of-init-local (equal (reserrp (init-local in-vars in-vals out-vars cstate)) (or (reserrp (add-vars in-vars nil)) (reserrp (add-vars out-vars (add-vars in-vars nil))) (not (equal (len in-vals) (len in-vars))))))