Construct a syntaxp hypothesis for a symbolic execution rule for pure expressions.
(atc-syntaxp-hyp-for-expr-pure var) → hyp
We use these hypotheses to ensure that certain execution subterms are rewritten to their shallow embedding counterparts before their enclosing terms are rewritten. These hypotheses require that the (sub)term in question does not contain any of the execution functions that are expected to be rewritten to their shallow embedding counterparts.
Function:
(defun atc-syntaxp-hyp-for-expr-pure (var) (declare (xargs :guard (symbolp var))) (let ((__function__ 'atc-syntaxp-hyp-for-expr-pure)) (declare (ignorable __function__)) (cons 'syntaxp (cons (cons 'or (cons (cons 'atom (cons var 'nil)) (cons (cons 'not (cons (cons 'member-eq (cons (cons 'car (cons var 'nil)) '('(exec-const exec-ident exec-address exec-indir exec-unary exec-binary-strict-pure exec-cast exec-arrsub exec-member exec-memberp exec-arrsub-of-member exec-arrsub-of-memberp exec-expr-pure test-value)))) 'nil)) 'nil))) 'nil))))
Theorem:
(defthm pseudo-termp-of-atc-syntaxp-hyp-for-expr-pure (implies (symbolp var) (b* ((hyp (atc-syntaxp-hyp-for-expr-pure var))) (pseudo-termp hyp))) :rule-classes :rewrite)