		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-block-item-list-rules

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.

Definitions and Theorems

Theorem: exec-block-item-list-of-nil

(defthm exec-block-item-list-of-nil
  (implies (and (not (zp limit))
                (compustatep compst))
           (equal (exec-block-item-list nil compst fenv limit)
                  (mv (stmt-value-none) compst))))

Theorem: exec-block-item-list-when-consp

(defthm exec-block-item-list-when-consp
  (implies
       (and (syntaxp (quotep items))
            (consp items)
            (not (zp limit))
            (equal sval+compst1
                   (exec-block-item (car items)
                                    compst fenv (1- limit)))
            (equal sval (mv-nth 0 sval+compst1))
            (stmt-valuep sval)
            (equal compst1 (mv-nth 1 sval+compst1)))
       (equal (exec-block-item-list items compst fenv limit)
              (if (equal (stmt-value-kind sval) :return)
                  (mv sval compst1)
                (exec-block-item-list (cdr items)
                                      compst1 fenv (1- limit))))))

Theorem: exec-block-item-list-of-append

(defthm exec-block-item-list-of-append
 (equal
      (exec-block-item-list (append items1 items2)
                            compst fenv limit)
      (b* (((mv sval compst)
            (exec-block-item-list items1 compst fenv limit))
           ((when (errorp sval)) (mv sval compst))
           ((when (stmt-value-case sval :return))
            (mv sval compst)))
        (exec-block-item-list items2
                              compst fenv (- limit (len items1))))))

Theorem: append-of-take-and-nthcdr

(defthm append-of-take-and-nthcdr
  (implies (<= (nfix n) (len x))
           (equal (append (take n x) (nthcdr n x))
                  x)))

Theorem: len-of-take

(defthm len-of-take
  (equal (len (take n x)) (nfix n)))