		Search-engine friendly clone of the ACL2 documentation.

Remove-assocs

Remove all pairs with given keys from an alist.

General Forms:
(remove-assocs keys alist)
(remove-assocs keys alist :test 'eql)   ; same as above (eql as equality test)
(remove-assocs keys alist :test 'eq)    ; same, but eq is equality test
(remove-assocs keys alist :test 'equal) ; same, but equal is equality test

This generalizes remove-assoc to multiple keys.

The optional keyword, :test, has no effect logically, but provides the test (default eql) used for comparing the keys of the alist with the ones to remove.

The guard for a call of remove-assocs depends on the test. In all cases, the first argument must satisfy true-listp and the second argument must satisfy alistp. If the test is eql, the first argument must satisfy eqlable-listp or the second argument must satisfy eqlable-alistp (or both). If the test is eq, the first argument must satisfy symbol-listp or the second argument must satisfy symbol-alistp (or both).

See equality-variants for a discussion of the relation between remove-assocs and its variants:

(remove-assocs-eq keys alist) is equivalent to (remove-assocs keys alist :test 'eq);
(remove-assocs-equal keys alist) is equivalent to (remove-assocs keys alist :test 'equal).

In particular, reasoning about any of these primitives reduces to reasoning about the function remove-assocs-equal.

Definitions and Theorems

Function: remove-assocs-equal

(defun remove-assocs-equal (keys alist)
  (declare (xargs :guard (and (true-listp keys) (alistp alist))))
  (cond ((endp alist) nil)
        ((member-equal (car (car alist)) keys)
         (remove-assocs-equal keys (cdr alist)))
        (t (cons (car alist)
                 (remove-assocs-equal keys (cdr alist))))))

Function: remove-assocs-eq-exec$guard-check

(defun remove-assocs-eq-exec$guard-check (keys alist)
  (declare (xargs :guard
                  (if (symbol-listp keys)
                      (alistp alist)
                    (and (true-listp keys)
                         (symbol-alistp alist)))))
  (declare (ignore keys alist))
  t)

Function: remove-assocs-eq-exec

(defun remove-assocs-eq-exec (keys alist)
  (declare (xargs :guard
                  (if (symbol-listp keys)
                      (alistp alist)
                    (and (true-listp keys)
                         (symbol-alistp alist)))))
  (cond ((endp alist) nil)
        ((member-eq (car (car alist)) keys)
         (remove-assocs-eq-exec keys (cdr alist)))
        (t (cons (car alist)
                 (remove-assocs-eq-exec keys (cdr alist))))))

Function: remove-assocs-eql-exec$guard-check

(defun remove-assocs-eql-exec$guard-check (keys alist)
  (declare (xargs :guard
                  (if (eqlable-listp keys)
                      (alistp alist)
                    (and (true-listp keys)
                         (eqlable-alistp alist)))))
  (declare (ignore keys alist))
  t)

Function: remove-assocs-eql-exec

(defun remove-assocs-eql-exec (keys alist)
  (declare (xargs :guard
                  (if (eqlable-listp keys)
                      (alistp alist)
                    (and (true-listp keys)
                         (eqlable-alistp alist)))))
  (cond ((endp alist) nil)
        ((member (car (car alist)) keys)
         (remove-assocs-eql-exec keys (cdr alist)))
        (t (cons (car alist)
                 (remove-assocs-eql-exec keys (cdr alist))))))

Theorem: remove-assocs-eq-exec-is-remove-assocs-equal

(defthm remove-assocs-eq-exec-is-remove-assocs-equal
  (equal (remove-assocs-eq-exec keys alist)
         (remove-assocs-equal keys alist)))

Theorem: remove-assocs-eql-exec-is-remove-assocs-equal

(defthm remove-assocs-eql-exec-is-remove-assocs-equal
  (equal (remove-assocs-eql-exec keys alist)
         (remove-assocs-equal keys alist)))

Theorem: alistp-of-remove-assocs-equal

(defthm alistp-of-remove-assocs-equal
  (implies (alistp alist)
           (alistp (remove-assocs-equal keys alist))))

Theorem: symbol-alistp-of-remove-assocs-equal

(defthm symbol-alistp-of-remove-assocs-equal
  (implies (symbol-alistp alist)
           (symbol-alistp (remove-assocs-equal keys alist))))