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

• Std/alists

Hons-remove-assoc

Remove a particular key from a "modern" alist.

The hons- here just refers to our observation of the "modern" atom-skipping convention as in hons-assoc-equal, etc. There is nothing fast or hons-specific here.

Definitions and Theorems

Theorem: hons-remove-assoc-of-cons

(defthm hons-remove-assoc-of-cons
  (equal (hons-remove-assoc k (cons x y))
         (if (and (consp x) (not (equal (car x) k)))
             (cons x (hons-remove-assoc k y))
           (hons-remove-assoc k y))))

Theorem: hons-remove-assoc-of-atom

(defthm hons-remove-assoc-of-atom
  (implies (not (consp x))
           (equal (hons-remove-assoc k x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: hons-remove-assoc-commutes

(defthm hons-remove-assoc-commutes
  (equal (hons-remove-assoc k (hons-remove-assoc j x))
         (hons-remove-assoc j (hons-remove-assoc k x)))
  :rule-classes ((:rewrite :loop-stopper ((j k)))))

Theorem: hons-assoc-equal-remove-assoc

(defthm hons-assoc-equal-remove-assoc
  (equal (hons-assoc-equal k (hons-remove-assoc j x))
         (and (not (equal k j))
              (hons-assoc-equal k x))))

Theorem: hons-remove-assoc-of-fast-alist-fork

(defthm hons-remove-assoc-of-fast-alist-fork
  (equal (hons-remove-assoc k (fast-alist-fork x y))
         (fast-alist-fork (hons-remove-assoc k x)
                          (hons-remove-assoc k y))))

Theorem: hons-remove-assoc-of-append

(defthm hons-remove-assoc-of-append
  (equal (hons-remove-assoc k (append x y))
         (append (hons-remove-assoc k x)
                 (hons-remove-assoc k y))))

Theorem: hons-remove-assoc-when-not-hons-assoc-equal

(defthm hons-remove-assoc-when-not-hons-assoc-equal
  (implies (not (hons-assoc-equal k x))
           (equal (hons-remove-assoc k x)
                  (alist-fix x))))

Theorem: alistp-of-hons-remove-assoc

(defthm alistp-of-hons-remove-assoc
  (alistp (hons-remove-assoc k x)))

Theorem: hons-remove-assoc-of-alist-fix

(defthm hons-remove-assoc-of-alist-fix
  (equal (hons-remove-assoc k (alist-fix x))
         (hons-remove-assoc k x)))