		Search-engine friendly clone of the ACL2 documentation.

In-terminal-set

Symbol-in-termset-p

Check if a symbol is either a rule name or a natural number in a set.

Signature
(symbol-in-termset-p symbol termset) → yes/no
Arguments: symbol — Guard (symbolp symbol).; termset — Guard (nat-setp termset).
Returns: yes/no — Type (booleanp yes/no).

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.

Definitions and Theorems

Function: symbol-in-termset-p

(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: booleanp-of-symbol-in-termset-p

(defthm booleanp-of-symbol-in-termset-p
  (b* ((yes/no (symbol-in-termset-p symbol termset)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbol-in-termset-p-when-natp

(defthm symbol-in-termset-p-when-natp
  (implies (natp nat)
           (equal (symbol-in-termset-p nat termset)
                  (in nat termset))))

Theorem: symbol-in-termset-p-when-rulenamep

(defthm symbol-in-termset-p-when-rulenamep
  (implies (rulenamep rulename)
           (symbol-in-termset-p rulename termset)))