		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svex-lhsrewrite

Signature
(svex-lhsrewrite x width) → new-x
Arguments: x — Guard (svex-p x).; width — Guard (natp width).
Returns: new-x — Type (svex-p new-x).

Definitions and Theorems

Function: svex-lhsrewrite

(defun svex-lhsrewrite (x width)
  (declare (xargs :guard (and (svex-p x) (natp width))))
  (let ((__function__ 'svex-lhsrewrite))
    (declare (ignorable __function__))
    (b* ((preproc (svex-lhs-preproc x)))
      (svex-lhsrewrite-aux preproc 0 width))))

Theorem: svex-p-of-svex-lhsrewrite

(defthm svex-p-of-svex-lhsrewrite
  (b* ((new-x (svex-lhsrewrite x width)))
    (svex-p new-x))
  :rule-classes :rewrite)

Theorem: svex-lhsrewrite-correct-lemma

(defthm svex-lhsrewrite-correct-lemma
  (equal (4vec-concat (2vec (nfix w))
                      (svex-eval (svex-lhsrewrite x w) env)
                      (4vec-z))
         (4vec-concat (2vec (nfix w))
                      (svex-eval x env)
                      (4vec-z))))

Theorem: svex-lhsrewrite-vars

(defthm svex-lhsrewrite-vars
  (implies (not (member v (svex-vars x)))
           (not (member v (svex-vars (svex-lhsrewrite x w))))))

Theorem: svex-lhsrewrite-of-svex-fix-x

(defthm svex-lhsrewrite-of-svex-fix-x
  (equal (svex-lhsrewrite (svex-fix x) width)
         (svex-lhsrewrite x width)))

Theorem: svex-lhsrewrite-svex-equiv-congruence-on-x

(defthm svex-lhsrewrite-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-lhsrewrite x width)
                  (svex-lhsrewrite x-equiv width)))
  :rule-classes :congruence)

Theorem: svex-lhsrewrite-of-nfix-width

(defthm svex-lhsrewrite-of-nfix-width
  (equal (svex-lhsrewrite x (nfix width))
         (svex-lhsrewrite x width)))

Theorem: svex-lhsrewrite-nat-equiv-congruence-on-width

(defthm svex-lhsrewrite-nat-equiv-congruence-on-width
  (implies (nat-equiv width width-equiv)
           (equal (svex-lhsrewrite x width)
                  (svex-lhsrewrite x width-equiv)))
  :rule-classes :congruence)