		Search-engine friendly clone of the ACL2 documentation.

Substrings

Collect-syms-with-isubstr

Gather symbols whose names have some (case-insensitive) substring.

(collect-syms-with-isubstr a x) returns a list of all the symbols in the list x that have a as a case-insensitve substring of their symbol-name. The substring tests are carried out with isubstrp.

See also collect-strs-with-isubstr, which is similar but for string lists instead of symbol lists.

Definitions and Theorems

Function: collect-syms-with-isubstr

(defun collect-syms-with-isubstr (a x)
  (declare (xargs :guard (and (stringp a) (symbol-listp x))))
  (cond ((atom x) nil)
        ((isubstrp a (symbol-name (car x)))
         (cons (car x)
               (collect-syms-with-isubstr a (cdr x))))
        (t (collect-syms-with-isubstr a (cdr x)))))

Theorem: istreqv-implies-equal-collect-syms-with-isubstr-1

(defthm istreqv-implies-equal-collect-syms-with-isubstr-1
  (implies (istreqv a a-equiv)
           (equal (collect-syms-with-isubstr a x)
                  (collect-syms-with-isubstr a-equiv x)))
  :rule-classes (:congruence))

Theorem: collect-syms-with-isubstr-when-atom

(defthm collect-syms-with-isubstr-when-atom
  (implies (atom x)
           (equal (collect-syms-with-isubstr a x)
                  nil)))

Theorem: collect-syms-with-isubstr-of-cons

(defthm collect-syms-with-isubstr-of-cons
  (equal (collect-syms-with-isubstr a (cons b x))
         (if (isubstrp a (symbol-name b))
             (cons b (collect-syms-with-isubstr a x))
           (collect-syms-with-isubstr a x))))

Theorem: member-equal-collect-syms-with-isubstr

(defthm member-equal-collect-syms-with-isubstr
  (iff (member-equal b (collect-syms-with-isubstr a x))
       (and (member-equal b x)
            (isubstrp a (symbol-name b)))))

Theorem: subsetp-equal-of-collect-syms-with-isubstr

(defthm subsetp-equal-of-collect-syms-with-isubstr
  (implies (subsetp-equal x y)
           (subsetp-equal (collect-syms-with-isubstr a x)
                          y)))

Theorem: subsetp-equal-collect-syms-with-isubstr-self

(defthm subsetp-equal-collect-syms-with-isubstr-self
  (subsetp-equal (collect-syms-with-isubstr a x)
                 x))