• 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-characters

Built-in theorems about characters.

Definition: booleanp-characterp

(defaxiom booleanp-characterp
          (booleanp (characterp x))
          :rule-classes nil)

Definition: characterp-page

(defaxiom characterp-page (characterp #\Page)
          :rule-classes nil)

Definition: characterp-tab

(defaxiom characterp-tab (characterp #\Tab)
          :rule-classes nil)

Definition: characterp-rubout

(defaxiom characterp-rubout (characterp #\Rubout)
          :rule-classes nil)

Definition: characterp-return

(defaxiom characterp-return (characterp #\Return)
          :rule-classes nil)

Definition: char-code-linear

(defaxiom char-code-linear (< (char-code x) 256)
          :rule-classes :linear)

Definition: code-char-type

(defaxiom code-char-type
          (characterp (code-char n))
          :rule-classes :type-prescription)

Definition: code-char-char-code-is-identity

(defaxiom code-char-char-code-is-identity
          (implies (force (characterp c))
                   (equal (code-char (char-code c)) c)))

Definition: char-code-code-char-is-identity

(defaxiom char-code-code-char-is-identity
          (implies (and (force (integerp n))
                        (force (<= 0 n))
                        (force (< n 256)))
                   (equal (char-code (code-char n)) n)))

Definition: completion-of-char-code

(defaxiom completion-of-char-code
          (equal (char-code x)
                 (if (characterp x) (char-code x) 0))
          :rule-classes nil)

Definition: completion-of-code-char

(defaxiom completion-of-code-char
          (equal (code-char x)
                 (if (and (integerp x) (>= x 0) (< x 256))
                     (code-char x)
                     (code-char 0)))
          :rule-classes nil)

Theorem: lower-case-p-char-downcase

(defthm lower-case-p-char-downcase
        (implies (upper-case-p x)
                 (lower-case-p (char-downcase x))))

Theorem: upper-case-p-char-upcase

(defthm upper-case-p-char-upcase
        (implies (lower-case-p x)
                 (upper-case-p (char-upcase x))))

Theorem: lower-case-p-forward-to-alpha-char-p

(defthm lower-case-p-forward-to-alpha-char-p
        (implies (lower-case-p x)
                 (alpha-char-p x))
        :rule-classes :forward-chaining)

Theorem: upper-case-p-forward-to-alpha-char-p

(defthm upper-case-p-forward-to-alpha-char-p
        (implies (upper-case-p x)
                 (alpha-char-p x))
        :rule-classes :forward-chaining)

Theorem: alpha-char-p-forward-to-standard-char-p

(defthm alpha-char-p-forward-to-standard-char-p
        (implies (alpha-char-p x)
                 (standard-char-p x))
        :rule-classes :forward-chaining)

Theorem: standard-char-p-forward-to-characterp

(defthm standard-char-p-forward-to-characterp
        (implies (standard-char-p x)
                 (characterp x))
        :rule-classes :forward-chaining)

Theorem: characterp-char-downcase

(defthm characterp-char-downcase
        (characterp (char-downcase x))
        :rule-classes :type-prescription)

Theorem: characterp-char-upcase

(defthm characterp-char-upcase
        (characterp (char-upcase x))
        :rule-classes :type-prescription)

Theorem: characterp-nth

(defthm characterp-nth
        (implies (and (character-listp x)
                      (<= 0 i)
                      (< i (len x)))
                 (characterp (nth i x))))

Theorem: standard-char-listp-append

(defthm standard-char-listp-append
        (implies (true-listp x)
                 (equal (standard-char-listp (append x y))
                        (and (standard-char-listp x)
                             (standard-char-listp y)))))

Theorem: character-listp-append

(defthm character-listp-append
        (implies (true-listp x)
                 (equal (character-listp (append x y))
                        (and (character-listp x)
                             (character-listp y)))))

Theorem: character-listp-remove-duplicates

(defthm character-listp-remove-duplicates
        (implies (character-listp x)
                 (character-listp (remove-duplicates x))))

Theorem: character-listp-revappend

(defthm character-listp-revappend
        (implies (true-listp x)
                 (equal (character-listp (revappend x y))
                        (and (character-listp x)
                             (character-listp y)))))

Theorem: standard-char-p-nth

(defthm standard-char-p-nth
        (implies (and (standard-char-listp chars)
                      (<= 0 i)
                      (< i (len chars)))
                 (standard-char-p (nth i chars))))

Theorem: equal-char-code

(defthm equal-char-code
        (implies (and (characterp x) (characterp y))
                 (implies (equal (char-code x) (char-code y))
                          (equal x y)))
        :rule-classes nil)

Theorem: default-char-code

(defthm default-char-code
        (implies (not (characterp x))
                 (equal (char-code x) 0)))

Theorem: default-code-char

(defthm default-code-char
        (implies (and (syntaxp (not (equal x ''0)))
                      (not (and (integerp x) (>= x 0) (< x 256))))
                 (equal (code-char x) (code-char 0))))

Theorem: make-character-list-make-character-list

(defthm make-character-list-make-character-list
        (equal (make-character-list (make-character-list x))
               (make-character-list x)))

Theorem: true-listp-explode-atom

(defthm true-listp-explode-atom
        (true-listp (explode-atom n print-base))
        :rule-classes :type-prescription)