• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
        • Alist-map-vals-functions-and-macros
        • Alist-map-vals-theorems
      • 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

• Alist-map-vals

Alist-map-vals-functions-and-macros

Definitions of the alist-map-vals functions and macros, and basic theorems about them.

Definitions and Theorems

Function: alist-map-vals-equal

(defun
 alist-map-vals-equal (alist)
 (declare (xargs :guard (alistp alist)))
 (cond
      ((endp alist) nil)
      (t (let* ((pair (car alist))
                (key (car pair))
                (val (cdr pair)))
               (cons val
                     (alist-map-vals-equal
                          (remove-assoc-equal key (cdr alist))))))))

Function: alist-map-vals-eq-exec$guard-check

(defun alist-map-vals-eq-exec$guard-check
       (alist)
       (declare (xargs :guard (symbol-alistp alist)))
       (declare (ignore alist))
       t)

Function: alist-map-vals-eq-exec

(defun
 alist-map-vals-eq-exec (alist)
 (declare (xargs :guard (symbol-alistp alist)))
 (cond
  ((endp alist) nil)
  (t
   (let*
    ((pair (car alist))
     (key (car pair))
     (val (cdr pair)))
    (cons
     val
     (alist-map-vals-eq-exec (remove-assoc-eq key (cdr alist))))))))

Function: alist-map-vals-eql-exec$guard-check

(defun alist-map-vals-eql-exec$guard-check
       (alist)
       (declare (xargs :guard (eqlable-alistp alist)))
       (declare (ignore alist))
       t)

Function: alist-map-vals-eql-exec

(defun
 alist-map-vals-eql-exec (alist)
 (declare (xargs :guard (eqlable-alistp alist)))
 (cond
   ((endp alist) nil)
   (t (let* ((pair (car alist))
             (key (car pair))
             (val (cdr pair)))
            (cons val
                  (alist-map-vals-eql-exec
                       (remove-assoc-eql-exec key (cdr alist))))))))

Theorem: alist-map-vals-eq-exec-is-alist-map-vals-equal

(defthm alist-map-vals-eq-exec-is-alist-map-vals-equal
        (equal (alist-map-vals-eq-exec alist)
               (alist-map-vals-equal alist)))

Theorem: alist-map-vals-eql-exec-is-alist-map-vals-equal

(defthm alist-map-vals-eql-exec-is-alist-map-vals-equal
        (equal (alist-map-vals-eql-exec alist)
               (alist-map-vals-equal alist)))