		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Tidentifier

Fixtype of Java type identifiers.

The grammar rule for type-identifier in [JLS25:3.8] defines a type identifier as a regular identifier that is not permits, record, sealed, var, or yield.

Accordingly, we model Java type identifiers as regular identifiers that differ from the Unicode sequences for those keywords.

Definitions and Theorems

Function: tidentifierp

(defun tidentifierp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'tidentifierp))
    (declare (ignorable __function__))
    (and (identifierp x)
         (not (equal x (string=>unicode "permits")))
         (not (equal x (string=>unicode "record")))
         (not (equal x (string=>unicode "sealed")))
         (not (equal x (string=>unicode "var")))
         (not (equal x (string=>unicode "yield"))))))

Theorem: booleanp-of-tidentifierp

(defthm booleanp-of-tidentifierp
  (b* ((yes/no (tidentifierp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Function: tidentifier-fix

(defun tidentifier-fix (x)
  (declare (xargs :guard (tidentifierp x)))
  (mbe :logic
       (if (tidentifierp x)
           x
         (list (char-code #\$)))
       :exec x))

Theorem: tidentifierp-of-tidentifier-fix

(defthm tidentifierp-of-tidentifier-fix
  (b* ((fixed-x (tidentifier-fix x)))
    (tidentifierp fixed-x))
  :rule-classes :rewrite)

Theorem: tidentifier-fix-when-tidentifierp

(defthm tidentifier-fix-when-tidentifierp
  (implies (tidentifierp x)
           (equal (tidentifier-fix x) x)))

Function: tidentifier-equiv$inline

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

Theorem: tidentifier-equiv-is-an-equivalence

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

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

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

Theorem: tidentifier-fix-under-tidentifier-equiv

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

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

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

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

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

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

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

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

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