• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
          • Name-database
          • Vl-gc
          • Make-lookup-alist
          • Symbol-list-names
            • Html-encoding
            • Nats-from
            • Redundant-mergesort
            • Longest-common-prefix
            • Vl-edition-p
            • Nat-listp
            • Vl-plural-p
            • Vl-remove-keys
            • Sum-nats
            • Vl-maybe-nat-listp
            • Url-encoding
            • Fast-memberp
            • Vl-string-keys-p
            • Max-nats
            • Longest-common-prefix-list
            • Character-list-listp
            • Vl-string-list-values-p
            • Vl-character-list-list-values-p
            • Remove-from-alist
            • Prefix-of-eachp
            • Vl-maybe-string-listp
            • Pos-listp
            • Vl-string-values-p
            • String-list-listp
            • True-list-listp
            • Symbol-list-listp
            • Explode-list
            • All-have-len
            • Min-nats
            • Debuggable-and
            • Vl-starname
            • Remove-equal-without-guard
            • String-fix
            • Longer-than-p
            • Clean-alist
            • Anyp
            • Or*
            • Fast-alist-free-each-alist-val
            • And*
            • Not*
            • Free-list-of-fast-alists
            • *nls*
          • Loader
          • Transforms
          • Lint
          • Mlib
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Utilities

    Symbol-list-names

    (symbol-list-names x) maps symbol-name across a list.

    Signature
    (symbol-list-names x) → *

    This is an ordinary defprojection.

    Definitions and Theorems

    Function: symbol-list-names-exec

    (defun symbol-list-names-exec (x acc)
      (declare (xargs :guard (symbol-listp x)))
      (let ((__function__ 'symbol-list-names-exec))
        (declare (ignorable __function__))
        (if (consp x)
            (symbol-list-names-exec (cdr x)
                                    (cons (symbol-name (car x)) acc))
          acc)))

    Function: symbol-list-names-nrev

    (defun symbol-list-names-nrev (x nrev)
      (declare (xargs :stobjs (nrev)))
      (declare (xargs :guard (symbol-listp x)))
      (let ((__function__ 'symbol-list-names-nrev))
        (declare (ignorable __function__))
        (if (atom x)
            (nrev-fix nrev)
          (let ((nrev (nrev-push (symbol-name (car x)) nrev)))
            (symbol-list-names-nrev (cdr x)
                                    nrev)))))

    Function: symbol-list-names

    (defun symbol-list-names (x)
      (declare (xargs :guard (symbol-listp x)))
      (let ((__function__ 'symbol-list-names))
        (declare (ignorable __function__))
        (mbe :logic
             (if (consp x)
                 (cons (symbol-name (car x))
                       (symbol-list-names (cdr x)))
               nil)
             :exec
             (if (atom x)
                 nil
               (with-local-nrev (symbol-list-names-nrev x nrev))))))

    Theorem: symbol-list-names-nrev-removal

    (defthm symbol-list-names-nrev-removal
      (equal (symbol-list-names-nrev acl2::x nrev)
             (append nrev (symbol-list-names acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: symbol-list-names-exec-removal

    (defthm symbol-list-names-exec-removal
      (equal (symbol-list-names-exec acl2::x acl2::acc)
             (revappend (symbol-list-names acl2::x)
                        acl2::acc))
      :rule-classes ((:rewrite)))

    Theorem: symbol-list-names-of-take

    (defthm symbol-list-names-of-take
      (implies (<= (nfix acl2::n) (len acl2::x))
               (equal (symbol-list-names (take acl2::n acl2::x))
                      (take acl2::n (symbol-list-names acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: set-equiv-congruence-over-symbol-list-names

    (defthm set-equiv-congruence-over-symbol-list-names
      (implies (set-equiv acl2::x acl2::y)
               (set-equiv (symbol-list-names acl2::x)
                          (symbol-list-names acl2::y)))
      :rule-classes ((:congruence)))

    Theorem: subsetp-of-symbol-list-names-when-subsetp

    (defthm subsetp-of-symbol-list-names-when-subsetp
      (implies (subsetp acl2::x acl2::y)
               (subsetp (symbol-list-names acl2::x)
                        (symbol-list-names acl2::y)))
      :rule-classes ((:rewrite)))

    Theorem: member-of-symbol-name-in-symbol-list-names

    (defthm member-of-symbol-name-in-symbol-list-names
      (implies (member acl2::k acl2::x)
               (member (symbol-name acl2::k)
                       (symbol-list-names acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: symbol-list-names-of-rev

    (defthm symbol-list-names-of-rev
      (equal (symbol-list-names (rev acl2::x))
             (rev (symbol-list-names acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: symbol-list-names-of-list-fix

    (defthm symbol-list-names-of-list-fix
      (equal (symbol-list-names (list-fix acl2::x))
             (symbol-list-names acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: symbol-list-names-of-append

    (defthm symbol-list-names-of-append
      (equal (symbol-list-names (append acl2::a acl2::b))
             (append (symbol-list-names acl2::a)
                     (symbol-list-names acl2::b)))
      :rule-classes ((:rewrite)))

    Theorem: cdr-of-symbol-list-names

    (defthm cdr-of-symbol-list-names
      (equal (cdr (symbol-list-names acl2::x))
             (symbol-list-names (cdr acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: car-of-symbol-list-names

    (defthm car-of-symbol-list-names
      (equal (car (symbol-list-names acl2::x))
             (and (consp acl2::x)
                  (symbol-name (car acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: symbol-list-names-under-iff

    (defthm symbol-list-names-under-iff
      (iff (symbol-list-names acl2::x)
           (consp acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: consp-of-symbol-list-names

    (defthm consp-of-symbol-list-names
      (equal (consp (symbol-list-names acl2::x))
             (consp acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: len-of-symbol-list-names

    (defthm len-of-symbol-list-names
      (equal (len (symbol-list-names acl2::x))
             (len acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: true-listp-of-symbol-list-names

    (defthm true-listp-of-symbol-list-names
      (true-listp (symbol-list-names acl2::x))
      :rule-classes :type-prescription)

    Theorem: symbol-list-names-when-not-consp

    (defthm symbol-list-names-when-not-consp
      (implies (not (consp acl2::x))
               (equal (symbol-list-names acl2::x) nil))
      :rule-classes ((:rewrite)))

    Theorem: symbol-list-names-of-cons

    (defthm symbol-list-names-of-cons
      (equal (symbol-list-names (cons acl2::a acl2::b))
             (cons (symbol-name acl2::a)
                   (symbol-list-names acl2::b)))
      :rule-classes ((:rewrite)))

    Theorem: string-listp-of-symbol-list-names

    (defthm string-listp-of-symbol-list-names
      (implies (force (symbol-listp x))
               (string-listp (symbol-list-names x))))