• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
      • Built-in-theorems-about-arithmetic
      • Built-in-theorems-about-symbols
      • Built-in-theorems-about-characters
      • Built-in-theorems-about-lists
      • Built-in-theorems-about-arrays
      • Built-in-theorems-about-strings
      • Built-in-theorems-about-alists
      • Built-in-theorems-about-total-order
      • Built-in-theorems-about-system-utilities
      • Built-in-theorems-about-cons-pairs
      • Built-in-theorems-for-tau
      • Built-in-theorems-about-bad-atoms
      • Built-in-theorems-about-logical-connectives
      • Built-in-theorems-about-booleans
      • Built-in-theorems-about-random$
      • Built-in-theorems-about-eqlables
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Built-in-theorems

Built-in-theorems-about-strings

Built-in theorems about strings.

Definition: coerce-inverse-1

(defaxiom coerce-inverse-1
          (implies (character-listp x)
                   (equal (coerce (coerce x 'string) 'list)
                          x)))

Definition: coerce-inverse-2

(defaxiom coerce-inverse-2
          (implies (stringp x)
                   (equal (coerce (coerce x 'list) 'string)
                          x)))

Definition: character-listp-coerce

(defaxiom
 character-listp-coerce
 (character-listp (coerce str 'list))
 :rule-classes
 (:rewrite (:forward-chaining :trigger-terms ((coerce str 'list)))))

Definition: completion-of-coerce

(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: string<-irreflexive

(defthm string<-irreflexive (not (string< s s)))

Theorem: stringp-substitute-type-prescription

(defthm stringp-substitute-type-prescription
        (implies (stringp seq)
                 (stringp (substitute new old seq)))
        :rule-classes :type-prescription)

Theorem: true-listp-substitute-type-prescription

(defthm true-listp-substitute-type-prescription
        (implies (not (stringp seq))
                 (true-listp (substitute new old seq)))
        :rule-classes :type-prescription)

Theorem: true-listp-explode-nonnegative-integer

(defthm
   true-listp-explode-nonnegative-integer
   (implies
        (true-listp ans)
        (true-listp (explode-nonnegative-integer n print-base ans)))
   :rule-classes :type-prescription)

Theorem: stringp-subseq-type-prescription

(defthm stringp-subseq-type-prescription
        (implies (stringp seq)
                 (stringp (subseq seq start end)))
        :rule-classes :type-prescription)

Theorem: true-listp-subseq-type-prescription

(defthm true-listp-subseq-type-prescription
        (implies (not (stringp seq))
                 (true-listp (subseq seq start end)))
        :rule-classes :type-prescription)

Theorem: default-coerce-1

(defthm default-coerce-1
        (implies (not (stringp x))
                 (equal (coerce x 'list) nil)))

Theorem: default-coerce-2

(defthm default-coerce-2
        (implies (and (syntaxp (not (equal y ''string)))
                      (not (equal y 'list)))
                 (equal (coerce x y)
                        (coerce x 'string))))

Theorem: default-coerce-3

(defthm default-coerce-3
        (implies (not (consp x))
                 (equal (coerce x 'string) "")))