Check if a symbol is either a rule name or a natural number in a set.
To prove that the terminal strings generated by a rule list consist of only terminals in a set, it is convenient to work with trees whose rule names may not all be expanded, to avoid dealing with this additional constraint. For these trees, we need to weaken the notion that tree->string only consists of terminals in the set, by allowing non-terminal symbols as well.
Function:
(defun symbol-in-termset-p (symbol termset) (declare (xargs :guard (and (symbolp symbol) (nat-setp termset)))) (symbol-case symbol :terminal (in symbol.get termset) :nonterminal t))
Theorem:
(defthm booleanp-of-symbol-in-termset-p (b* ((yes/no (symbol-in-termset-p symbol termset))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm symbol-in-termset-p-when-natp (implies (natp nat) (equal (symbol-in-termset-p nat termset) (in nat termset))))
Theorem:
(defthm symbol-in-termset-p-when-rulenamep (implies (rulenamep rulename) (symbol-in-termset-p rulename termset)))