Check if a symbol names a theorem,
i.e. it has a
(theorem-symbolp sym wrld) → yes/no
This function is named in analogy to the function-symbolp built-in system utility.
(defun theorem-symbolp (sym wrld) (declare (xargs :guard (and (symbolp sym) (plist-worldp wrld)))) (let ((__function__ 'theorem-symbolp)) (declare (ignorable __function__)) (not (eq (getpropc sym 'theorem t wrld) t))))
(defthm booleanp-of-theorem-symbolp (b* ((yes/no (theorem-symbolp sym wrld))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm theorem-symbolp-forward-to-symbolp (implies (and (theorem-symbolp fn wrld) (plist-worldp wrld)) (symbolp fn)) :rule-classes :forward-chaining)