Built-in axioms and theorems about characters.
Definition:
(defaxiom booleanp-characterp (booleanp (characterp x)) :rule-classes nil)
Definition:
(defaxiom characterp-page (characterp #\Page) :rule-classes nil)
Definition:
(defaxiom characterp-tab (characterp #\Tab) :rule-classes nil)
Definition:
(defaxiom characterp-rubout (characterp #\Rubout) :rule-classes nil)
Definition:
(defaxiom characterp-return (characterp #\Return) :rule-classes nil)
Definition:
(defaxiom char-code-linear (< (char-code x) 256) :rule-classes :linear)
Definition:
(defaxiom code-char-type (characterp (code-char n)) :rule-classes :type-prescription)
Definition:
(defaxiom code-char-char-code-is-identity (implies (characterp c) (equal (code-char (char-code c)) c)))
Definition:
(defaxiom char-code-code-char-is-identity (implies (and (integerp n) (<= 0 n) (< n 256)) (equal (char-code (code-char n)) n)))
Definition:
(defaxiom completion-of-char-code (equal (char-code x) (if (characterp x) (char-code x) 0)) :rule-classes nil)
Definition:
(defaxiom completion-of-code-char (equal (code-char x) (if (and (integerp x) (>= x 0) (< x 256)) (code-char x) *null-char*)) :rule-classes nil)
Theorem:
(defthm lower-case-p-char-downcase (implies (upper-case-p x) (lower-case-p (char-downcase x))))
Theorem:
(defthm upper-case-p-char-upcase (implies (lower-case-p x) (upper-case-p (char-upcase x))))
Theorem:
(defthm lower-case-p-forward-to-alpha-char-p (implies (lower-case-p x) (alpha-char-p x)) :rule-classes :forward-chaining)
Theorem:
(defthm upper-case-p-forward-to-alpha-char-p (implies (upper-case-p x) (alpha-char-p x)) :rule-classes :forward-chaining)
Theorem:
(defthm char-upcase/downcase-non-standard-inverses (implies (characterp x) (and (implies (upper-case-p-non-standard x) (equal (char-upcase-non-standard (char-downcase-non-standard x)) x)) (implies (lower-case-p-non-standard x) (equal (char-downcase-non-standard (char-upcase-non-standard x)) x)))))
Theorem:
(defthm char-upcase-maps-non-standard-to-non-standard (implies (characterp x) (equal (standard-char-p (char-upcase-non-standard x)) (standard-char-p x))))
Theorem:
(defthm char-downcase-maps-non-standard-to-non-standard (implies (characterp x) (equal (standard-char-p (char-downcase-non-standard x)) (standard-char-p x))))
Theorem:
(defthm characterp-char-downcase-non-standard (characterp (char-downcase-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm characterp-char-upcase-non-standard (characterp (char-upcase-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm standard-char-p-forward-to-characterp (implies (standard-char-p x) (characterp x)) :rule-classes :forward-chaining)
Theorem:
(defthm characterp-char-downcase (characterp (char-downcase x)) :rule-classes :type-prescription)
Theorem:
(defthm characterp-char-upcase (characterp (char-upcase x)) :rule-classes :type-prescription)
Theorem:
(defthm lower/upper-case-p-non-standard-disjointness (not (and (lower-case-p-non-standard x) (upper-case-p-non-standard x))) :rule-classes nil)
Theorem:
(defthm upper-case-p-non-standard-char-upcase-non-standard (implies (lower-case-p-non-standard x) (upper-case-p-non-standard (char-upcase-non-standard x))))
Theorem:
(defthm lower-case-p-non-standard-char-downcase-non-standard (implies (upper-case-p-non-standard x) (lower-case-p-non-standard (char-downcase-non-standard x))))
Theorem:
(defthm alpha-char-p-non-standard-implies-characterp (implies (alpha-char-p-non-standard x) (characterp x)) :rule-classes :forward-chaining)
Theorem:
(defthm lower-case-p-non-standard-implies-alpha-char-p-non-standard (implies (lower-case-p-non-standard x) (alpha-char-p-non-standard x)) :rule-classes :forward-chaining)
Theorem:
(defthm upper-case-p-non-standard-implies-alpha-char-p-non-standard (implies (upper-case-p-non-standard x) (alpha-char-p-non-standard x)) :rule-classes :forward-chaining)
Theorem:
(defthm booleanp-lower-case-p-non-standard (booleanp (lower-case-p-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-upper-case-p-non-standard (booleanp (upper-case-p-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-alpha-char-p-non-standard (booleanp (alpha-char-p-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm characterp-nth (implies (and (character-listp x) (<= 0 i) (< i (len x))) (characterp (nth i x))))
Theorem:
(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:
(defthm character-listp-append (implies (true-listp x) (equal (character-listp (append x y)) (and (character-listp x) (character-listp y)))))
Theorem:
(defthm character-listp-remove-duplicates (implies (character-listp x) (character-listp (remove-duplicates x))))
Theorem:
(defthm character-listp-revappend (implies (true-listp x) (equal (character-listp (revappend x y)) (and (character-listp x) (character-listp y)))))
Theorem:
(defthm standard-char-p-nth (implies (and (standard-char-listp chars) (<= 0 i) (< i (len chars))) (standard-char-p (nth i chars))))
Theorem:
(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:
(defthm default-char-code (implies (not (characterp x)) (equal (char-code x) 0)))
Theorem:
(defthm default-code-char (implies (and (syntaxp (not (equal x ''0))) (not (and (integerp x) (>= x 0) (< x 256)))) (equal (code-char x) *null-char*)))
Theorem:
(defthm make-character-list-make-character-list (equal (make-character-list (make-character-list x)) (make-character-list x)))
Theorem:
(defthm true-listp-explode-atom (true-listp (explode-atom n print-base)) :rule-classes :type-prescription)