		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-syntaxp-hyp-for-expr-pure

Construct a syntaxp hypothesis for a symbolic execution rule for pure expressions.

Signature
(atc-syntaxp-hyp-for-expr-pure var) → hyp
Arguments: var — Guard (symbolp var).
Returns: hyp — Type (pseudo-termp hyp), given (symbolp var).

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.

Definitions and Theorems

Function: atc-syntaxp-hyp-for-expr-pure

(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: pseudo-termp-of-atc-syntaxp-hyp-for-expr-pure

(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)