		Search-engine friendly clone of the ACL2 documentation.

Onehot-rewriting

4v-onehot-rw-sexpr-alist

Apply onehot-rewriting to a sexpr alist.

(4v-onehot-rw-sexpr-alist vars sexpr-alist) is given:

vars, which must be a nil-free list of atoms, and
sexpr-alist, an alist binding names to sexprs.

We return a new, ordinary (slow) sexpr-alist which is a (possibly simpler) conservative approximation of the original. The basic idea is to apply 4v-onehot-rw-sexpr to any sexprs that mention any of the vars, and leave any other sexprs unchanged.

Definitions and Theorems

Function: 4v-onehot-rw-sexpr-alist

(defun 4v-onehot-rw-sexpr-alist (vars sexpr-alist)
 (declare (xargs :guard (and (atom-listp vars)
                             (not (member-equal nil vars)))))
 (b*
  ((-
    (or
     (uniquep vars)
     (er
      hard? '4v-onehot-rw-sexpr-alist
      "You really want to use unique variables for onehot ~
                   rewriting. Duplicated variables are: ~&0.~%"
      (duplicated-members vars))))
   (sexpr-alist
        (fast-alist-free (hons-shrink-alist sexpr-alist nil)))
   (vars-fal (make-fast-alist (pairlis$ vars nil)))
   ((mv relevant-part irrelevant-part)
    (4v-onehot-filter sexpr-alist vars-fal nil nil))
   (- (fast-alist-free vars-fal))
   (- (clear-memoize-table '4v-sexpr-mentions))
   ((unless relevant-part) sexpr-alist))
  (append (4v-onehot-rw-sexpr-alist-aux vars relevant-part)
          irrelevant-part)))

Theorem: 4v-sexpr-alist-<=-of-4v-onehot-rw-sexpr-alist

(defthm 4v-sexpr-alist-<=-of-4v-onehot-rw-sexpr-alist
 (implies
      (and (atom-listp vars)
           (not (member-equal nil vars)))
      (4v-sexpr-alist-<= (4v-onehot-rw-sexpr-alist vars sexpr-alist)
                         sexpr-alist)))

Theorem: alist-keys-of-4v-onehot-rw-sexpr-alist

(defthm alist-keys-of-4v-onehot-rw-sexpr-alist
 (set-equiv (alist-keys (4v-onehot-rw-sexpr-alist vars sexpr-alist))
            (alist-keys sexpr-alist)))

Theorem: 4v-sexpr-vars-of-4v-onehot-rw-sexpr-alist

(defthm 4v-sexpr-vars-of-4v-onehot-rw-sexpr-alist
 (let ((new-alist (4v-onehot-rw-sexpr-alist vars sexpr-alist)))
  (implies
     (atom-listp vars)
     (subsetp-equal
          (4v-sexpr-vars-list (alist-vals new-alist))
          (append vars
                  (4v-sexpr-vars-list (alist-vals sexpr-alist)))))))