• 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

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