Built-in axioms and theorems about strings.
Definition:
(defaxiom coerce-inverse-1 (implies (character-listp x) (equal (coerce (coerce x 'string) 'list) x)))
Definition:
(defaxiom coerce-inverse-2 (implies (stringp x) (equal (coerce (coerce x 'list) 'string) x)))
Definition:
(defaxiom character-listp-coerce (character-listp (coerce str 'list)) :rule-classes (:rewrite (:forward-chaining :trigger-terms ((coerce str 'list)))))
Definition:
(defaxiom completion-of-coerce (equal (coerce x y) (cond ((equal y 'list) (if (stringp x) (coerce x 'list) nil)) (t (coerce (make-character-list x) 'string)))) :rule-classes nil)
Theorem:
(defthm string<-irreflexive (not (string< s s)))
Theorem:
(defthm stringp-substitute-type-prescription (implies (stringp seq) (stringp (substitute new old seq))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-substitute-type-prescription (implies (not (stringp seq)) (true-listp (substitute new old seq))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-explode-nonnegative-integer (implies (true-listp ans) (true-listp (explode-nonnegative-integer n print-base ans))) :rule-classes :type-prescription)
Theorem:
(defthm stringp-subseq-type-prescription (implies (stringp seq) (stringp (subseq seq start end))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-subseq-type-prescription (implies (not (stringp seq)) (true-listp (subseq seq start end))) :rule-classes :type-prescription)
Theorem:
(defthm default-coerce-1 (implies (not (stringp x)) (equal (coerce x 'list) nil)))
Theorem:
(defthm default-coerce-2 (implies (and (syntaxp (not (equal y ''string))) (not (equal y 'list))) (equal (coerce x y) (coerce x 'string))))
Theorem:
(defthm default-coerce-3 (implies (not (consp x)) (equal (coerce x 'string) "")))
Theorem:
(defthm character-listp-string-downcase-1 (character-listp (string-downcase1 x)))
Theorem:
(defthm character-listp-string-upcase1-1 (character-listp (string-upcase1 x)))
Theorem:
(defthm string<-l-irreflexive (not (string<-l x x i)))
Theorem:
(defthm string<-l-asymmetric (implies (and (eqlable-listp x1) (eqlable-listp x2) (integerp i) (string<-l x1 x2 i)) (not (string<-l x2 x1 i))))
Theorem:
(defthm string<-l-transitive (implies (and (string<-l x y i) (string<-l y z j) (integerp i) (integerp j) (integerp k) (character-listp x) (character-listp y) (character-listp z)) (string<-l x z k)) :rule-classes ((:rewrite :match-free :all)))
Theorem:
(defthm string<-l-trichotomy (implies (and (not (string<-l x y i)) (integerp i) (integerp j) (character-listp x) (character-listp y)) (iff (string<-l y x j) (not (equal x y)))) :rule-classes ((:rewrite :match-free :all)))