		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svex-norm-call

Signature
(svex-norm-call fn args) → call
Arguments: fn — Guard (fnsym-p fn).; args — Guard (svexlist-p args).
Returns: call — Type (svex-p call).

Definitions and Theorems

Function: svex-norm-call

(defun svex-norm-call (fn args)
  (declare (xargs :guard (and (fnsym-p fn) (svexlist-p args))))
  (let ((__function__ 'svex-norm-call))
    (declare (ignorable __function__))
    (if (svexlist-quotesp args)
        (svex-quote (svex-apply fn (svexlist-unquote args)))
      (svex-call fn args))))

Theorem: svex-p-of-svex-norm-call

(defthm svex-p-of-svex-norm-call
  (b* ((call (svex-norm-call fn args)))
    (svex-p call))
  :rule-classes :rewrite)

Theorem: svex-norm-call-correct

(defthm svex-norm-call-correct
  (equal (svex-eval (svex-norm-call fn args) env)
         (svex-apply fn (svexlist-eval args env))))

Theorem: vars-of-svex-norm-call

(defthm vars-of-svex-norm-call
  (implies (not (member v (svexlist-vars args)))
           (not (member v
                        (svex-vars (svex-norm-call fn args))))))

Theorem: svex-norm-call-of-fnsym-fix-fn

(defthm svex-norm-call-of-fnsym-fix-fn
  (equal (svex-norm-call (fnsym-fix fn) args)
         (svex-norm-call fn args)))

Theorem: svex-norm-call-fnsym-equiv-congruence-on-fn

(defthm svex-norm-call-fnsym-equiv-congruence-on-fn
  (implies (fnsym-equiv fn fn-equiv)
           (equal (svex-norm-call fn args)
                  (svex-norm-call fn-equiv args)))
  :rule-classes :congruence)

Theorem: svex-norm-call-of-svexlist-fix-args

(defthm svex-norm-call-of-svexlist-fix-args
  (equal (svex-norm-call fn (svexlist-fix args))
         (svex-norm-call fn args)))

Theorem: svex-norm-call-svexlist-equiv-congruence-on-args

(defthm svex-norm-call-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svex-norm-call fn args)
                  (svex-norm-call fn args-equiv)))
  :rule-classes :congruence)