Constrained recognizer and fixer and mappings, and fixtype, for the source character set.
We constrain the recognizer to return a boolean.
Besides the recognizer, we also introduce a fixer, with the usual properties. This will let us define a fixtype for the source characters.
We constrain the mapping from the ASCII characters to fix its argument, to return source characters, and to be injective.
We constrain the function to the character numbers to fix its argument, to return natural numbers, and to be injective. We also constrain it to always return a number below an unspecified bound: this ensures that there is a finite number of source characters.
The bound itself is a constrained nullary function, constrained to return a positive integer.
Theorem:
(defthm booleanp-of-source-charp (booleanp (source-charp x)) :rule-classes :type-prescription)
Theorem:
(defthm source-charp-of-source-char-fix (source-charp (source-char-fix x)))
Theorem:
(defthm source-char-fix-when-source-charp (implies (source-charp x) (equal (source-char-fix x) x)))
Theorem:
(defthm ascii-to-source-char-of-ascii-basic-source-char-fix (equal (ascii-to-source-char (ascii-basic-source-char-fix x)) (ascii-to-source-char x)))
Theorem:
(defthm source-charp-of-ascii-to-source-char (source-charp (ascii-to-source-char x)))
Theorem:
(defthm ascii-to-source-char-injective (equal (equal (ascii-to-source-char x) (ascii-to-source-char y)) (ascii-basic-source-char-equiv x y)))
Theorem:
(defthm source-char-to-number-of-source-char-fix (equal (source-char-to-number (source-char-fix x)) (source-char-to-number x)))
Theorem:
(defthm natp-of-source-char-to-number (natp (source-char-to-number x)) :rule-classes :type-prescription)
Theorem:
(defthm source-char-to-number-injective-lemma (equal (equal (source-char-to-number x) (source-char-to-number y)) (equal (source-char-fix x) (source-char-fix y))))
Theorem:
(defthm posp-of-source-char-to-number-bound (posp (source-char-to-number-bound)) :rule-classes :type-prescription)
Theorem:
(defthm source-char-to-number-below-bound (< (source-char-to-number x) (source-char-to-number-bound)) :rule-classes :linear)
Function:
(defun source-char-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (source-charp acl2::x) (source-charp acl2::y)))) (equal (source-char-fix acl2::x) (source-char-fix acl2::y)))
Theorem:
(defthm source-char-equiv-is-an-equivalence (and (booleanp (source-char-equiv x y)) (source-char-equiv x x) (implies (source-char-equiv x y) (source-char-equiv y x)) (implies (and (source-char-equiv x y) (source-char-equiv y z)) (source-char-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm source-char-equiv-implies-equal-source-char-fix-1 (implies (source-char-equiv acl2::x x-equiv) (equal (source-char-fix acl2::x) (source-char-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm source-char-fix-under-source-char-equiv (source-char-equiv (source-char-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-source-char-fix-1-forward-to-source-char-equiv (implies (equal (source-char-fix acl2::x) acl2::y) (source-char-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-source-char-fix-2-forward-to-source-char-equiv (implies (equal acl2::x (source-char-fix acl2::y)) (source-char-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm source-char-equiv-of-source-char-fix-1-forward (implies (source-char-equiv (source-char-fix acl2::x) acl2::y) (source-char-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm source-char-equiv-of-source-char-fix-2-forward (implies (source-char-equiv acl2::x (source-char-fix acl2::y)) (source-char-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm source-char-to-number-injective (equal (equal (source-char-to-number x) (source-char-to-number y)) (source-char-equiv x y)))
Theorem:
(defthm ascii-to-source-char-of-ascii-basic-source-char-fix-x (equal (ascii-to-source-char (ascii-basic-source-char-fix x)) (ascii-to-source-char x)))
Theorem:
(defthm ascii-to-source-char-ascii-basic-source-char-equiv-congruence-on-x (implies (ascii-basic-source-char-equiv x x-equiv) (equal (ascii-to-source-char x) (ascii-to-source-char x-equiv))) :rule-classes :congruence)
Theorem:
(defthm source-char-to-number-of-source-char-fix-x (equal (source-char-to-number (source-char-fix x)) (source-char-to-number x)))
Theorem:
(defthm source-char-to-number-source-char-equiv-congruence-on-x (implies (source-char-equiv x x-equiv) (equal (source-char-to-number x) (source-char-to-number x-equiv))) :rule-classes :congruence)