		Search-engine friendly clone of the ACL2 documentation.

Pad-trim

Trim-bag

Remove particular characters from the front and end of a string.

(trim-bag x bag) removes the characters in bag from the front and end of the string x.

BOZO eventually make this efficient.

Definitions and Theorems

Function: trim-aux

(defun trim-aux (x bag)
  (declare (xargs :guard (and (character-listp x)
                              (character-listp bag))))
  (if (consp x)
      (if (member (car x) bag)
          (trim-aux (cdr x) bag)
        x)
    nil))

Theorem: character-listp-of-trim-aux

(defthm character-listp-of-trim-aux
  (implies (force (character-listp x))
           (character-listp (trim-aux x bag))))

Function: trim-bag

(defun trim-bag (x bag)
  (declare (xargs :guard (and (stringp x)
                              (character-listp bag))))
  (let* ((chars (explode x))
         (chars (trim-aux chars bag))
         (chars (reverse chars))
         (chars (trim-aux chars bag))
         (chars (reverse chars)))
    (implode chars)))

Theorem: stringp-of-trim-bag

(defthm stringp-of-trim-bag
  (stringp (trim-bag x bag))
  :rule-classes :type-prescription)