• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
          • 4v-shannon-expansion
          • Onehot-rewriting
          • 4v-sexpr-restrict-with-rw
          • 4v-sexpr-compose-with-rw
          • Sexpr-rewrite
          • Sexpr-rewrite-default
          • Sexpr-rewriting-internals
          • *sexpr-rewrites*
        • 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
  • Testing-utilities
  • Math

• Sexpr-rewriting
• 4v-sexprs

4v-sexpr-compose-with-rw

4v-sexpr-compose with inline rewriting.

This is different from sexpr-rewrite-of-compose because it doesn't apply rewriting to the alist lookups; it basically assumes they've already been rewritten. So while we can't prove that this is equal to sexpr-rewrite of 4v-sexpr-compose, we can prove that it's sexpr-equivalent to 4v-sexpr-compose, and contains a subset of its variables. Careful about memoization here; wouldn't want to use this when you're about to (or just have) done a 4v-sexpr-compose of a similar sexpression with the same alist, or done a sexpr-rewrite of an sexpression similar to your result. Memoization won't carry over.

Definitions and Theorems

Function: 4v-sexpr-compose-with-rw

(defun 4v-sexpr-compose-with-rw (x al)
       (declare (xargs :guard t))
       (if (atom x)
           (and x
                (let ((look (hons-get x al)))
                     (and look (cdr look))))
           (b* ((args (4v-sexpr-compose-with-rw-list (cdr x)
                                                     al)))
               (sexpr-rewrite-fncall 100 (car x)
                                     args *sexpr-rewrites*))))

Function: 4v-sexpr-compose-with-rw-list

(defun 4v-sexpr-compose-with-rw-list (x al)
       (declare (xargs :guard t))
       (if (atom x)
           x
           (hons (4v-sexpr-compose-with-rw (car x) al)
                 (4v-sexpr-compose-with-rw-list (cdr x)
                                                al))))

Function: 4v-sexpr-compose-with-rw-memoize-condition

(defun 4v-sexpr-compose-with-rw-memoize-condition
       (x al)
       (declare (ignorable x al)
                (xargs :guard 't))
       (consp x))

Theorem: 4v-sexpr-compose-with-rw-equiv-to-4v-sexpr-compose

(defthm 4v-sexpr-compose-with-rw-equiv-to-4v-sexpr-compose
        (4v-sexpr-equiv (4v-sexpr-compose-with-rw x al)
                        (4v-sexpr-compose x al)))

Theorem: 4v-sexpr-compose-with-rw-list-equiv-to-4v-sexpr-compose-list

(defthm 4v-sexpr-compose-with-rw-list-equiv-to-4v-sexpr-compose-list
        (4v-sexpr-list-equiv (4v-sexpr-compose-with-rw-list x al)
                             (4v-sexpr-compose-list x al)))

Theorem: 4v-sexpr-vars-4v-sexpr-compose-with-rw

(defthm
 4v-sexpr-vars-4v-sexpr-compose-with-rw
 (implies
  (not (member-equal k (4v-sexpr-vars-list (alist-vals al))))
  (not
   (member-equal k
                 (4v-sexpr-vars (4v-sexpr-compose-with-rw x al))))))

Theorem: 4v-sexpr-vars-list-4v-sexpr-compose-with-rw-list

(defthm
 4v-sexpr-vars-list-4v-sexpr-compose-with-rw-list
 (implies
  (not (member-equal k (4v-sexpr-vars-list (alist-vals al))))
  (not
   (member-equal
       k
       (4v-sexpr-vars-list (4v-sexpr-compose-with-rw-list x al))))))

Function: 4v-sexpr-compose-with-rw-alist

(defun 4v-sexpr-compose-with-rw-alist (x al)
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (if (atom (car x))
               (4v-sexpr-compose-with-rw-alist (cdr x)
                                               al)
               (cons (cons (caar x)
                           (4v-sexpr-compose-with-rw (cdar x) al))
                     (4v-sexpr-compose-with-rw-alist (cdr x)
                                                     al)))))

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

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

Theorem: 4v-sexpr-compose-with-rw-alist-equiv-to-4v-sexpr-compose-alist

(defthm
     4v-sexpr-compose-with-rw-alist-equiv-to-4v-sexpr-compose-alist
     (4v-sexpr-alist-equiv (4v-sexpr-compose-with-rw-alist x al)
                           (4v-sexpr-compose-alist x al)))

Theorem: sexpr-eval-alist-of-4v-sexpr-compose-with-rw-alist

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

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

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

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

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

Function: 4v-sexpr-compose-with-rw-alists

(defun 4v-sexpr-compose-with-rw-alists (x al)
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (cons (4v-sexpr-compose-with-rw-alist (car x)
                                                 al)
                 (4v-sexpr-compose-with-rw-alists (cdr x)
                                                  al))))

Function: 4v-sexpr-compose-with-rw-list-list

(defun 4v-sexpr-compose-with-rw-list-list
       (x al)
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (cons (4v-sexpr-compose-with-rw-list (car x)
                                                al)
                 (4v-sexpr-compose-with-rw-list-list (cdr x)
                                                     al))))