		Search-engine friendly clone of the ACL2 documentation.

Rewriting-concatenations

Svex-normalize-concatenation

Signature
(svex-normalize-concatenation width first rest ctxalist) → new-concat
Arguments: width — Guard (natp width).; first — Guard (svex-p first).; rest — Guard (svex-p rest).; ctxalist — Guard (svex-context-alist-p ctxalist).
Returns: new-concat — Type (svex-p new-concat).

Definitions and Theorems

Function: svex-normalize-concatenation

(defun svex-normalize-concatenation (width first rest ctxalist)
 (declare (xargs :guard (and (natp width)
                             (svex-p first)
                             (svex-p rest)
                             (svex-context-alist-p ctxalist))))
 (let ((__function__ 'svex-normalize-concatenation))
  (declare (ignorable __function__))
  (b*
   ((width (lnfix width))
    (const-width-concat-p
       (svex-case first
                  :call (and (eq first.fn 'concat)
                             (eql (len first.args) 3)
                             (svex-quoted-index-p (car first.args)))
                  :otherwise nil))
    ((unless
      (and
       const-width-concat-p
       (eql (len (cdr (hons-get (svex-fix first)
                                (svex-context-alist-fix ctxalist))))
            1)))
     (svex-call 'concat
                (list (svex-quote (2vec (lnfix width)))
                      first rest)))
    ((list width1 first1 rest1)
     (svex-call->args first))
    (width1 (2vec->val (svex-quote->val width1)))
    ((when (>= width1 width))
     (svex-normalize-concatenation width first1 rest ctxalist)))
   (svex-normalize-concatenation
        width1 first1
        (svex-normalize-concatenation (- width width1)
                                      rest1 rest ctxalist)
        ctxalist))))

Theorem: svex-p-of-svex-normalize-concatenation

(defthm svex-p-of-svex-normalize-concatenation
  (b*
    ((new-concat
          (svex-normalize-concatenation width first rest ctxalist)))
    (svex-p new-concat))
  :rule-classes :rewrite)

Theorem: svex-normalize-concatenation-correct

(defthm svex-normalize-concatenation-correct
  (b*
    ((?new-concat
          (svex-normalize-concatenation width first rest ctxalist)))
    (equal (svex-eval new-concat env)
           (4vec-concat (2vec (nfix width))
                        (svex-eval first env)
                        (svex-eval rest env)))))

Theorem: svex-count-of-svex-normalize-concatenation

(defthm svex-count-of-svex-normalize-concatenation
 (b* nil
  (<= (svex-count
           (svex-normalize-concatenation width first rest ctxalist))
      (svex-count (svex-call 'concat
                             (list (svex-quote (2vec (nfix width)))
                                   first rest)))))
 :rule-classes nil)

Theorem: svex-count-of-svex-normalize-concatenation-special

(defthm svex-count-of-svex-normalize-concatenation-special
 (implies
  (svex-case x
             :call (and (equal x.fn 'concat)
                        (equal (len x.args) 3)
                        (svex-quoted-index-p (car x.args)))
             :otherwise nil)
  (b* (((svex-call x)))
   (<= (svex-count (svex-normalize-concatenation
                        (4vec->lower (svex-quote->val (car x.args)))
                        (cadr x.args)
                        (caddr x.args)
                        ctxalist))
       (svex-count x))))
 :rule-classes :linear)

Theorem: vars-of-svex-normalize-concatenation

(defthm vars-of-svex-normalize-concatenation
  (b*
    ((?new-concat
          (svex-normalize-concatenation width first rest ctxalist)))
    (implies (and (not (member v (svex-vars first)))
                  (not (member v (svex-vars rest))))
             (not (member v (svex-vars new-concat))))))

Theorem: svex-normalize-concatenation-of-nfix-width

(defthm svex-normalize-concatenation-of-nfix-width
  (equal (svex-normalize-concatenation (nfix width)
                                       first rest ctxalist)
         (svex-normalize-concatenation width first rest ctxalist)))

Theorem: svex-normalize-concatenation-nat-equiv-congruence-on-width

(defthm svex-normalize-concatenation-nat-equiv-congruence-on-width
 (implies
  (nat-equiv width width-equiv)
  (equal
    (svex-normalize-concatenation width first rest ctxalist)
    (svex-normalize-concatenation width-equiv first rest ctxalist)))
 :rule-classes :congruence)

Theorem: svex-normalize-concatenation-of-svex-fix-first

(defthm svex-normalize-concatenation-of-svex-fix-first
  (equal (svex-normalize-concatenation width (svex-fix first)
                                       rest ctxalist)
         (svex-normalize-concatenation width first rest ctxalist)))

Theorem: svex-normalize-concatenation-svex-equiv-congruence-on-first

(defthm svex-normalize-concatenation-svex-equiv-congruence-on-first
 (implies
  (svex-equiv first first-equiv)
  (equal
    (svex-normalize-concatenation width first rest ctxalist)
    (svex-normalize-concatenation width first-equiv rest ctxalist)))
 :rule-classes :congruence)

Theorem: svex-normalize-concatenation-of-svex-fix-rest

(defthm svex-normalize-concatenation-of-svex-fix-rest
  (equal (svex-normalize-concatenation width first (svex-fix rest)
                                       ctxalist)
         (svex-normalize-concatenation width first rest ctxalist)))

Theorem: svex-normalize-concatenation-svex-equiv-congruence-on-rest

(defthm svex-normalize-concatenation-svex-equiv-congruence-on-rest
 (implies
  (svex-equiv rest rest-equiv)
  (equal
    (svex-normalize-concatenation width first rest ctxalist)
    (svex-normalize-concatenation width first rest-equiv ctxalist)))
 :rule-classes :congruence)

Theorem: svex-normalize-concatenation-of-svex-context-alist-fix-ctxalist

(defthm
    svex-normalize-concatenation-of-svex-context-alist-fix-ctxalist
  (equal (svex-normalize-concatenation
              width first
              rest (svex-context-alist-fix ctxalist))
         (svex-normalize-concatenation width first rest ctxalist)))

Theorem: svex-normalize-concatenation-svex-context-alist-equiv-congruence-on-ctxalist

(defthm
 svex-normalize-concatenation-svex-context-alist-equiv-congruence-on-ctxalist
 (implies
  (svex-context-alist-equiv ctxalist ctxalist-equiv)
  (equal
    (svex-normalize-concatenation width first rest ctxalist)
    (svex-normalize-concatenation width first rest ctxalist-equiv)))
 :rule-classes :congruence)