		Search-engine friendly clone of the ACL2 documentation.

Sexpr-rewriting-internals

Sexpr-rewrite-ground

Checks whether the given s-expression's arguments are all constants, and if so, rewrites it to a constant by evaluating it under the empty environment.

Definitions and Theorems

Function: sexpr-ground-args-p

(defun sexpr-ground-args-p (args)
  (declare (xargs :guard t))
  (or (atom args)
      (and (let ((arg (car args)))
             (if (atom arg)
                 (eq arg nil)
               (atom (cdr arg))))
           (sexpr-ground-args-p (cdr args)))))

Function: sexpr-rewrite-ground

(defun sexpr-rewrite-ground (x)
  (declare (xargs :guard t))
  (if (and (consp x)
           (sexpr-ground-args-p (cdr x)))
      (hist (4v-sexpr-eval x nil))
    x))

Theorem: sexpr-eval-of-list-4vp

(defthm sexpr-eval-of-list-4vp
  (implies (4vp x)
           (equal (4v-sexpr-eval (list x) env) x)))

Theorem: sexpr-eval-list-norm-env-when-ground-args-p

(defthm sexpr-eval-list-norm-env-when-ground-args-p
  (implies (and (syntaxp (not (equal env ''nil)))
                (sexpr-ground-args-p x))
           (equal (4v-sexpr-eval-list x env)
                  (4v-sexpr-eval-list x nil))))

Theorem: sexpr-eval-norm-env-when-ground-args-p

(defthm sexpr-eval-norm-env-when-ground-args-p
  (implies (and (syntaxp (not (equal env ''nil)))
                (consp x)
                (sexpr-ground-args-p (cdr x)))
           (equal (4v-sexpr-eval x env)
                  (4v-sexpr-eval x nil))))

Theorem: 4vp-4v-sexpr-eval

(defthm 4vp-4v-sexpr-eval
  (4vp (4v-sexpr-eval x env)))

Theorem: sexpr-rewrite-ground-correct

(defthm sexpr-rewrite-ground-correct
  (4v-sexpr-equiv (sexpr-rewrite-ground x)
                  x))

Theorem: 4v-sexpr-vars-sexpr-rewrite-ground

(defthm 4v-sexpr-vars-sexpr-rewrite-ground
 (implies
     (not (member-equal k (4v-sexpr-vars x)))
     (not (member-equal k
                        (4v-sexpr-vars (sexpr-rewrite-ground x))))))