		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhs-concat

Signature
(lhs-concat w x y) → concat
Arguments: w — Guard (natp w).; x — Guard (lhs-p x).; y — Guard (lhs-p y).
Returns: concat — Type (lhs-p concat).

Definitions and Theorems

Function: lhs-concat

(defun lhs-concat (w x y)
  (declare (xargs :guard (and (natp w) (lhs-p x) (lhs-p y))))
  (let ((__function__ 'lhs-concat))
    (declare (ignorable __function__))
    (b* (((when (zp w)) (lhs-fix y))
         ((when (atom x))
          (lhs-cons (lhrange w (lhatom-z)) y))
         ((lhrange xf) (car x))
         ((when (<= xf.w w))
          (lhs-cons (car x)
                    (lhs-concat (- w xf.w) (cdr x) y))))
      (lhs-cons (lhrange w xf.atom) y))))

Theorem: lhs-p-of-lhs-concat

(defthm lhs-p-of-lhs-concat
  (b* ((concat (lhs-concat w x y)))
    (lhs-p concat))
  :rule-classes :rewrite)

Theorem: lhs-concat-of-nfix-w

(defthm lhs-concat-of-nfix-w
  (equal (lhs-concat (nfix w) x y)
         (lhs-concat w x y)))

Theorem: lhs-concat-nat-equiv-congruence-on-w

(defthm lhs-concat-nat-equiv-congruence-on-w
  (implies (nat-equiv w w-equiv)
           (equal (lhs-concat w x y)
                  (lhs-concat w-equiv x y)))
  :rule-classes :congruence)

Theorem: lhs-concat-of-lhs-fix-x

(defthm lhs-concat-of-lhs-fix-x
  (equal (lhs-concat w (lhs-fix x) y)
         (lhs-concat w x y)))

Theorem: lhs-concat-lhs-equiv-congruence-on-x

(defthm lhs-concat-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs-concat w x y)
                  (lhs-concat w x-equiv y)))
  :rule-classes :congruence)

Theorem: lhs-concat-of-lhs-fix-y

(defthm lhs-concat-of-lhs-fix-y
  (equal (lhs-concat w x (lhs-fix y))
         (lhs-concat w x y)))

Theorem: lhs-concat-lhs-equiv-congruence-on-y

(defthm lhs-concat-lhs-equiv-congruence-on-y
  (implies (lhs-equiv y y-equiv)
           (equal (lhs-concat w x y)
                  (lhs-concat w x y-equiv)))
  :rule-classes :congruence)

Theorem: lhs-concat-of-lhs-cons-under-norm-equiv

(defthm lhs-concat-of-lhs-cons-under-norm-equiv
  (equal (lhs-concat w (lhs-cons x y) z)
         (lhs-concat w (cons x y) z)))

Theorem: lhs-concat-of-lhs-norm-x

(defthm lhs-concat-of-lhs-norm-x
  (equal (lhs-concat w (lhs-norm x) y)
         (lhs-concat w x y)))

Theorem: lhs-concat-lhs-norm-equiv-congruence-on-x

(defthm lhs-concat-lhs-norm-equiv-congruence-on-x
  (implies (lhs-norm-equiv x x-equiv)
           (equal (lhs-concat w x y)
                  (lhs-concat w x-equiv y)))
  :rule-classes :congruence)

Theorem: lhs-concat-of-lhs-norm-y-under-lhs-norm-equiv

(defthm lhs-concat-of-lhs-norm-y-under-lhs-norm-equiv
  (lhs-norm-equiv (lhs-concat w x (lhs-norm y))
                  (lhs-concat w x y)))

Theorem: lhs-concat-lhs-norm-equiv-congruence-on-y-under-lhs-norm-equiv

(defthm
     lhs-concat-lhs-norm-equiv-congruence-on-y-under-lhs-norm-equiv
  (implies (lhs-norm-equiv y y-equiv)
           (lhs-norm-equiv (lhs-concat w x y)
                           (lhs-concat w x y-equiv)))
  :rule-classes :congruence)

Theorem: lhs-concat-correct

(defthm lhs-concat-correct
  (equal (lhs-eval (lhs-concat w x y) env)
         (4vec-concat (2vec (nfix w))
                      (lhs-eval x env)
                      (lhs-eval y env))))

Theorem: lhs-concat-correct-zero

(defthm lhs-concat-correct-zero
  (equal (lhs-eval-zx (lhs-concat w x y) env)
         (4vec-concat (2vec (nfix w))
                      (lhs-eval-zx x env)
                      (lhs-eval-zx y env))))

Theorem: lhs-width-of-lhs-concat

(defthm lhs-width-of-lhs-concat
  (<= (lhs-width (lhs-concat w x y))
      (+ (nfix w) (lhs-width y)))
  :rule-classes :linear)