Rule names that are defined in a list of rules but not used anywhere in those rules.
(rulelist-unused-rules rules) → rulenames
It is not uncommon for this set to be non-empty. First, top-level rule names are often not used in other rules. Second, sometimes grammars define certain rules to establish nomenclatures, even if those rules may not be used explicitly in other rules.
Function:
(defun rulelist-unused-rules (rules) (declare (xargs :guard (rulelistp rules))) (difference (rulelist-defined-rules rules) (rulelist-called-rules rules)))
Theorem:
(defthm rulename-setp-of-rulelist-unused-rules (b* ((rulenames (rulelist-unused-rules rules))) (rulename-setp rulenames)) :rule-classes :rewrite)