• 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-restrict-alist
          • 4v-nsexpr-p-4v-sexpr-restrict
          • 4v-sexpr-restrict-list
        • 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-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4v-sexpr-restrict

4v-sexpr-restrict-alist

Extension of 4v-sexpr-restrict to alists.

(4v-sexpr-restrict-alist x al) is given an alist x that typically binds names to sexprs. It restricts each of these sexprs using 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-restrict-alist1

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

Function: 4v-sexpr-restrict-alist

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

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

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

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

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

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

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

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

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

Theorem: alist-equiv-implies-alist-equiv-4v-sexpr-restrict-alist-1

(defthm alist-equiv-implies-alist-equiv-4v-sexpr-restrict-alist-1
  (implies (alist-equiv a a-equiv)
           (alist-equiv (4v-sexpr-restrict-alist a b)
                        (4v-sexpr-restrict-alist a-equiv b)))
  :rule-classes (:congruence))