map-symbol-name

(in-package "ACL2")

(defund map-symbol-name
  (syms)
  (declare (xargs :guard (symbol-listp syms)))
  (if (endp syms)
    nil
    (cons (symbol-name (first syms))
      (map-symbol-name (rest syms)))))

(defthm string-listp-of-map-symbol-name
  (string-listp (map-symbol-name syms))
  :hints (("Goal" :in-theory (enable map-symbol-name))))

(defthm map-symbol-name-of-cons
  (equal (map-symbol-name (cons sym syms))
    (cons (symbol-name sym) (map-symbol-name syms)))
  :hints (("Goal" :in-theory (enable map-symbol-name))))