• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Alist-map-keys
      • Std/alists/hons-assoc-equal
      • Fal-extract
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract-vals
      • Std/alists/abstract
      • Fal-all-boundp
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Alists-agree
      • Worth-hashing
      • Sub-alistp
      • Alist-fix
      • Std/alists/remove-assoc-equal
      • Std/alists/assoc-equal
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/alists
• Alists

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))))