		Search-engine friendly clone of the ACL2 documentation.

Unicode-characters

Unicode

Fixtype of Java Unicode characters.

This type models Java characters in the context of modeling Java's syntax. This is isomorphic, but distinct from, the type char-value that models Java characters in the context of modeling Java's semantics. The reason for having these two different types is that we want character values to be tagged when modeling semantics, while we want characters to be simple numbers when modeling syntax.

Definitions and Theorems

Function: unicode-equiv$inline

(defun unicode-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (unicodep acl2::x)
                              (unicodep acl2::y))))
  (equal (unicode-fix acl2::x)
         (unicode-fix acl2::y)))

Theorem: unicode-equiv-is-an-equivalence

(defthm unicode-equiv-is-an-equivalence
  (and (booleanp (unicode-equiv x y))
       (unicode-equiv x x)
       (implies (unicode-equiv x y)
                (unicode-equiv y x))
       (implies (and (unicode-equiv x y)
                     (unicode-equiv y z))
                (unicode-equiv x z)))
  :rule-classes (:equivalence))

Theorem: unicode-equiv-implies-equal-unicode-fix-1

(defthm unicode-equiv-implies-equal-unicode-fix-1
  (implies (unicode-equiv acl2::x x-equiv)
           (equal (unicode-fix acl2::x)
                  (unicode-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: unicode-fix-under-unicode-equiv

(defthm unicode-fix-under-unicode-equiv
  (unicode-equiv (unicode-fix acl2::x)
                 acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-unicode-fix-1-forward-to-unicode-equiv

(defthm equal-of-unicode-fix-1-forward-to-unicode-equiv
  (implies (equal (unicode-fix acl2::x) acl2::y)
           (unicode-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-unicode-fix-2-forward-to-unicode-equiv

(defthm equal-of-unicode-fix-2-forward-to-unicode-equiv
  (implies (equal acl2::x (unicode-fix acl2::y))
           (unicode-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: unicode-equiv-of-unicode-fix-1-forward

(defthm unicode-equiv-of-unicode-fix-1-forward
  (implies (unicode-equiv (unicode-fix acl2::x)
                          acl2::y)
           (unicode-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: unicode-equiv-of-unicode-fix-2-forward

(defthm unicode-equiv-of-unicode-fix-2-forward
  (implies (unicode-equiv acl2::x (unicode-fix acl2::y))
           (unicode-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Subtopics

Unicodep: Recognizer for unicode.
Unicode-fix: Fixer for unicode.