• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
          • 4v-sexpr-compose-alist
          • 4v-nsexpr-p-4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-compose

4v-sexpr-compose-alist

Extension of 4v-sexpr-compose to alists.

(4v-sexpr-compose-alist x al) is given an alist x that typically binds names to sexprs. It composes each of these sexprs with al, and returns a new alist that binds the same names to the resulting sexprs. The resulting alist is an ordinary, non-fast alist.

It is beneficial for env to be a fast alist; if it is not fast, we we temporarily make it fast.

Definitions and Theorems

Function: 4v-sexpr-compose-alist1

(defun 4v-sexpr-compose-alist1 (x al)
  "Assumes AL is fast"
  (declare (xargs :guard t))
  (cond ((atom x) nil)
        ((atom (car x))
         (4v-sexpr-compose-alist1 (cdr x) al))
        (t (cons (cons (caar x)
                       (4v-sexpr-compose (cdar x) al))
                 (4v-sexpr-compose-alist1 (cdr x) al)))))

Function: 4v-sexpr-compose-alist

(defun 4v-sexpr-compose-alist (x al)
  "Makes AL fast if necessary"
  (declare (xargs :guard t))
  (mbe :logic (cond ((atom x) nil)
                    ((atom (car x))
                     (4v-sexpr-compose-alist (cdr x) al))
                    (t (cons (cons (caar x)
                                   (4v-sexpr-compose (cdar x) al))
                             (4v-sexpr-compose-alist (cdr x) al))))
       :exec (with-fast-alist al (4v-sexpr-compose-alist1 x al))))

Theorem: 4v-sexpr-compose-alist1-removal

(defthm 4v-sexpr-compose-alist1-removal
  (equal (4v-sexpr-compose-alist1 x al)
         (4v-sexpr-compose-alist x al)))

Theorem: hons-assoc-equal-4v-sexpr-compose-alist

(defthm hons-assoc-equal-4v-sexpr-compose-alist
  (equal (hons-assoc-equal k (4v-sexpr-compose-alist x al))
         (and (hons-assoc-equal k x)
              (cons k
                    (4v-sexpr-compose (cdr (hons-assoc-equal k x))
                                      al)))))

Theorem: 4v-sexpr-eval-alist-4v-sexpr-compose-alist

(defthm 4v-sexpr-eval-alist-4v-sexpr-compose-alist
  (equal (4v-sexpr-eval-alist (4v-sexpr-compose-alist x al)
                              env)
         (4v-sexpr-eval-alist x (4v-sexpr-eval-alist al env))))

Theorem: alist-keys-4v-sexpr-compose-alist

(defthm alist-keys-4v-sexpr-compose-alist
  (equal (alist-keys (4v-sexpr-compose-alist al env))
         (alist-keys al)))

Theorem: 4v-sexpr-compose-alist-append

(defthm 4v-sexpr-compose-alist-append
  (equal (4v-sexpr-compose-alist (append al1 al2)
                                 env)
         (append (4v-sexpr-compose-alist al1 env)
                 (4v-sexpr-compose-alist al2 env))))