Rules for exec-block-item-list.
The first two rules should be obvious in purpose.
The remaining rules are for the modular proofs. In the modular proofs, there is a need to compose the execution of some block items with the execution of some subsequent block items. That is, given a modular theorem for the first chunk of blocks, and a modular theorem for the second chunk of blocks, we need to generate a modular theorem for the concatenated chunks.
Thus, unsurprisingly, we need a theorem about exec-block-item-list applied to an append of block items, which is proved using a custom induction scheme.
However, this theorem is not directly applicable in modular proofs. This is because the concatenate block items come as a quoted constant, not as an append of the two chunks. Thus, in the modular proofs, we generate rules of a different form, as needed for each case (we always know the sizes of the two chunks). To support the generation of proofs for these custom rules, here we put two rules about lists that we need in those proofs.
Theorem:
(defthm exec-block-item-list-of-nil (implies (and (not (zp limit)) (compustatep compst)) (equal (exec-block-item-list nil compst fenv limit) (mv nil compst))))
Theorem:
(defthm exec-block-item-list-when-consp (implies (and (syntaxp (quotep items)) (consp items) (not (zp limit)) (equal val?+compst1 (exec-block-item (car items) compst fenv (1- limit))) (equal val? (mv-nth 0 val?+compst1)) (value-optionp val?) (equal compst1 (mv-nth 1 val?+compst1))) (equal (exec-block-item-list items compst fenv limit) (if (valuep val?) (mv val? compst1) (exec-block-item-list (cdr items) compst1 fenv (1- limit))))))
Theorem:
(defthm exec-block-item-list-of-append (equal (exec-block-item-list (append items1 items2) compst fenv limit) (b* (((mv val? compst) (exec-block-item-list items1 compst fenv limit)) ((when (errorp val?)) (mv val? compst)) ((when (valuep val?)) (mv val? compst))) (exec-block-item-list items2 compst fenv (- limit (len items1))))))
Theorem:
(defthm append-of-take-and-nthcdr (implies (<= (nfix n) (len x)) (equal (append (take n x) (nthcdr n x)) x)))
Theorem:
(defthm len-of-take (equal (len (take n x)) (nfix n)))