		Search-engine friendly clone of the ACL2 documentation.

S4vecs

Svex-s4apply

Apply an svex function to some s4vec arguments.

Signature
(svex-s4apply fn args) → result
Arguments: fn — Name of the function to apply.
Guard (fnsym-p fn).; args — Arguments to apply it to.
Guard (s4veclist-p args).
Returns: result — Result of applying the function.
Type (s4vec-p result).

Like svex-apply, but applies to s4vecs instead of 4vecs.

Definitions and Theorems

Function: svex-s4apply

(defun svex-s4apply (fn args)
  (declare (xargs :guard (and (fnsym-p fn) (s4veclist-p args))))
  (let ((__function__ 'svex-s4apply))
    (declare (ignorable __function__))
    (let* ((fn (mbe :exec fn :logic (fnsym-fix fn)))
           (args (mbe :logic (s4veclist-fix args)
                      :exec args)))
      (svex-s4apply-cases fn args))))

Theorem: s4vec-p-of-svex-s4apply

(defthm s4vec-p-of-svex-s4apply
  (b* ((result (svex-s4apply fn args)))
    (s4vec-p result))
  :rule-classes :rewrite)

Theorem: svex-s4apply-correct

(defthm svex-s4apply-correct
  (b* ((?result (svex-s4apply fn args)))
    (equal (s4vec->4vec result)
           (svex-apply fn (s4veclist->4veclist args)))))

Theorem: svex-s4apply-of-fnsym-fix-fn

(defthm svex-s4apply-of-fnsym-fix-fn
  (equal (svex-s4apply (fnsym-fix fn) args)
         (svex-s4apply fn args)))

Theorem: svex-s4apply-fnsym-equiv-congruence-on-fn

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

Theorem: svex-s4apply-of-s4veclist-fix-args

(defthm svex-s4apply-of-s4veclist-fix-args
  (equal (svex-s4apply fn (s4veclist-fix args))
         (svex-s4apply fn args)))

Theorem: svex-s4apply-s4veclist-equiv-congruence-on-args

(defthm svex-s4apply-s4veclist-equiv-congruence-on-args
  (implies (s4veclist-equiv args args-equiv)
           (equal (svex-s4apply fn args)
                  (svex-s4apply fn args-equiv)))
  :rule-classes :congruence)