		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Ident-formalp

Check if an identifier has formal dynamic semantics.

Signature
(ident-formalp ident) → yes/no
Arguments: ident — Guard (identp ident).
Returns: yes/no — Type (booleanp yes/no).

Identifiers are supported, via c::exec-ident, when they denote variables. Based on the identifier alone, we cannot determine whether it denotes a variable, so we must accept it here, delegating the test to whether it denotes a variable elsewhere.

However, we impose a restriction here, to ensure that the C subset defined by these predicates is a subset of the one defined by the syntactic language mapping, whose ldm-ident function requires the identifier to be an ACL2 string. So here we require the identifier to be an ACL2 string as well.

This may turn out to be too restrictive, e.g. if we want to support the verification of transformations that take advantage of the flexibility mentioned in ident. So we may revisit this in the future.

Definitions and Theorems

Function: ident-formalp

(defun ident-formalp (ident)
  (declare (xargs :guard (identp ident)))
  (let ((__function__ 'ident-formalp))
    (declare (ignorable __function__))
    (stringp (ident->unwrap ident))))

Theorem: booleanp-of-ident-formalp

(defthm booleanp-of-ident-formalp
  (b* ((yes/no (ident-formalp ident)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: ident-formalp-of-ident-fix-ident

(defthm ident-formalp-of-ident-fix-ident
  (equal (ident-formalp (ident-fix ident))
         (ident-formalp ident)))

Theorem: ident-formalp-ident-equiv-congruence-on-ident

(defthm ident-formalp-ident-equiv-congruence-on-ident
  (implies (ident-equiv ident ident-equiv)
           (equal (ident-formalp ident)
                  (ident-formalp ident-equiv)))
  :rule-classes :congruence)