Recognize repetitions, elements, rule names, and character strings.
(repetition/element/rulename/charstring-p x) → yes/no
Note that these are pairwise disjoint.
Function:
(defun repetition/element/rulename/charstring-p (x) (declare (xargs :guard t)) (or (repetitionp x) (elementp x) (rulenamep x) (common-lisp::stringp x)))
Theorem:
(defthm booleanp-of-repetition/element/rulename/charstring-p (b* ((yes/no (repetition/element/rulename/charstring-p x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm disjoint-repetition/element (not (and (repetitionp x) (elementp x))))
Theorem:
(defthm disjoint-repetition/rulename (not (and (repetitionp x) (rulenamep x))))
Theorem:
(defthm disjoint-repetition/charstring (not (and (repetitionp x) (common-lisp::stringp x))))
Theorem:
(defthm disjoint-element/charstring (not (and (elementp x) (common-lisp::stringp x))))
Theorem:
(defthm disjoint-rulename/charstring (not (and (rulenamep x) (common-lisp::stringp x))))