		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Identifier

Fixtype of Java identifiers, for most contexts.

These are Java identifiers that exclude just the reserved keywords, as discussed in the topic on identifiers. Since these are used in most contexts (except for some module-related contexts), we use the general name identifierp for this recognizer.

We model these Java identifiers as lists of Java Unicode characters that are not empty, that start with a character satisfying identifier-start-p, that continue with characters satisfying identifier-part-p, that differ from all the non-restricted keywords, and that differ from the boolean and null literals. See [JLS25:3.8].

Definitions and Theorems

Function: identifierp

(defun identifierp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'identifierp))
    (declare (ignorable __function__))
    (and (unicode-listp x)
         (consp x)
         (identifier-start-p (car x))
         (identifier-part-listp (cdr x))
         (not (reserved-keywordp x))
         (not (boolean-literalp x))
         (not (null-literalp x)))))

Theorem: booleanp-of-identifierp

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

Function: identifier-fix

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

Theorem: identifierp-of-identifier-fix

(defthm identifierp-of-identifier-fix
  (b* ((fixed-x (identifier-fix x)))
    (identifierp fixed-x))
  :rule-classes :rewrite)

Theorem: identifier-fix-when-identifierp

(defthm identifier-fix-when-identifierp
  (implies (identifierp x)
           (equal (identifier-fix x) x)))

Function: identifier-equiv$inline

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

Theorem: identifier-equiv-is-an-equivalence

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

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

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

Theorem: identifier-fix-under-identifier-equiv

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

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

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

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

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

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

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

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

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