		Search-engine friendly clone of the ACL2 documentation.

Bit-list

Bit-list-fix

(bit-list-fix x) is a usual fty list fixing function.

Signature
(bit-list-fix x) → fty::newx
Arguments: x — Guard (bit-listp x).
Returns: fty::newx — Type (bit-listp fty::newx).

In the logic, we apply bfix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.

Definitions and Theorems

Function: bit-list-fix$inline

(defun bit-list-fix$inline (x)
  (declare (xargs :guard (bit-listp x)))
  (let ((__function__ 'bit-list-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (cons (bfix (car x))
                 (bit-list-fix (cdr x))))
         :exec x)))

Theorem: bit-listp-of-bit-list-fix

(defthm bit-listp-of-bit-list-fix
  (b* ((fty::newx (bit-list-fix$inline x)))
    (bit-listp fty::newx))
  :rule-classes :rewrite)

Theorem: bit-list-fix-when-bit-listp

(defthm bit-list-fix-when-bit-listp
  (implies (bit-listp x)
           (equal (bit-list-fix x) x)))

Function: bit-list-equiv$inline

(defun bit-list-equiv$inline (x y)
  (declare (xargs :guard (and (bit-listp x) (bit-listp y))))
  (equal (bit-list-fix x)
         (bit-list-fix y)))

Theorem: bit-list-equiv-is-an-equivalence

(defthm bit-list-equiv-is-an-equivalence
  (and (booleanp (bit-list-equiv x y))
       (bit-list-equiv x x)
       (implies (bit-list-equiv x y)
                (bit-list-equiv y x))
       (implies (and (bit-list-equiv x y)
                     (bit-list-equiv y z))
                (bit-list-equiv x z)))
  :rule-classes (:equivalence))

Theorem: bit-list-equiv-implies-equal-bit-list-fix-1

(defthm bit-list-equiv-implies-equal-bit-list-fix-1
  (implies (bit-list-equiv x x-equiv)
           (equal (bit-list-fix x)
                  (bit-list-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: bit-list-fix-under-bit-list-equiv

(defthm bit-list-fix-under-bit-list-equiv
  (bit-list-equiv (bit-list-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-bit-list-fix-1-forward-to-bit-list-equiv

(defthm equal-of-bit-list-fix-1-forward-to-bit-list-equiv
  (implies (equal (bit-list-fix x) y)
           (bit-list-equiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-bit-list-fix-2-forward-to-bit-list-equiv

(defthm equal-of-bit-list-fix-2-forward-to-bit-list-equiv
  (implies (equal x (bit-list-fix y))
           (bit-list-equiv x y))
  :rule-classes :forward-chaining)

Theorem: bit-list-equiv-of-bit-list-fix-1-forward

(defthm bit-list-equiv-of-bit-list-fix-1-forward
  (implies (bit-list-equiv (bit-list-fix x) y)
           (bit-list-equiv x y))
  :rule-classes :forward-chaining)

Theorem: bit-list-equiv-of-bit-list-fix-2-forward

(defthm bit-list-equiv-of-bit-list-fix-2-forward
  (implies (bit-list-equiv x (bit-list-fix y))
           (bit-list-equiv x y))
  :rule-classes :forward-chaining)

Theorem: car-of-bit-list-fix-x-under-bit-equiv

(defthm car-of-bit-list-fix-x-under-bit-equiv
  (bit-equiv (car (bit-list-fix x))
             (car x)))

Theorem: car-bit-list-equiv-congruence-on-x-under-bit-equiv

(defthm car-bit-list-equiv-congruence-on-x-under-bit-equiv
  (implies (bit-list-equiv x x-equiv)
           (bit-equiv (car x) (car x-equiv)))
  :rule-classes :congruence)

Theorem: cdr-of-bit-list-fix-x-under-bit-list-equiv

(defthm cdr-of-bit-list-fix-x-under-bit-list-equiv
  (bit-list-equiv (cdr (bit-list-fix x))
                  (cdr x)))

Theorem: cdr-bit-list-equiv-congruence-on-x-under-bit-list-equiv

(defthm cdr-bit-list-equiv-congruence-on-x-under-bit-list-equiv
  (implies (bit-list-equiv x x-equiv)
           (bit-list-equiv (cdr x) (cdr x-equiv)))
  :rule-classes :congruence)

Theorem: cons-of-bfix-x-under-bit-list-equiv

(defthm cons-of-bfix-x-under-bit-list-equiv
  (bit-list-equiv (cons (bfix x) y)
                  (cons x y)))

Theorem: cons-bit-equiv-congruence-on-x-under-bit-list-equiv

(defthm cons-bit-equiv-congruence-on-x-under-bit-list-equiv
  (implies (bit-equiv x x-equiv)
           (bit-list-equiv (cons x y)
                           (cons x-equiv y)))
  :rule-classes :congruence)

Theorem: cons-of-bit-list-fix-y-under-bit-list-equiv

(defthm cons-of-bit-list-fix-y-under-bit-list-equiv
  (bit-list-equiv (cons x (bit-list-fix y))
                  (cons x y)))

Theorem: cons-bit-list-equiv-congruence-on-y-under-bit-list-equiv

(defthm cons-bit-list-equiv-congruence-on-y-under-bit-list-equiv
  (implies (bit-list-equiv y y-equiv)
           (bit-list-equiv (cons x y)
                           (cons x y-equiv)))
  :rule-classes :congruence)

Theorem: consp-of-bit-list-fix

(defthm consp-of-bit-list-fix
  (equal (consp (bit-list-fix x))
         (consp x)))

Theorem: bit-list-fix-under-iff

(defthm bit-list-fix-under-iff
  (iff (bit-list-fix x) (consp x)))

Theorem: bit-list-fix-of-cons

(defthm bit-list-fix-of-cons
  (equal (bit-list-fix (cons a x))
         (cons (bfix a) (bit-list-fix x))))

Theorem: len-of-bit-list-fix

(defthm len-of-bit-list-fix
  (equal (len (bit-list-fix x)) (len x)))

Theorem: bit-list-fix-of-append

(defthm bit-list-fix-of-append
  (equal (bit-list-fix (append std::a std::b))
         (append (bit-list-fix std::a)
                 (bit-list-fix std::b))))

Theorem: bit-list-fix-of-repeat

(defthm bit-list-fix-of-repeat
  (equal (bit-list-fix (repeat n x))
         (repeat n (bfix x))))

Theorem: list-equiv-refines-bit-list-equiv

(defthm list-equiv-refines-bit-list-equiv
  (implies (list-equiv x y)
           (bit-list-equiv x y))
  :rule-classes :refinement)

Theorem: nth-of-bit-list-fix

(defthm nth-of-bit-list-fix
  (equal (nth n (bit-list-fix x))
         (if (< (nfix n) (len x))
             (bfix (nth n x))
           nil)))

Theorem: bit-list-equiv-implies-bit-list-equiv-append-1

(defthm bit-list-equiv-implies-bit-list-equiv-append-1
  (implies (bit-list-equiv x fty::x-equiv)
           (bit-list-equiv (append x y)
                           (append fty::x-equiv y)))
  :rule-classes (:congruence))

Theorem: bit-list-equiv-implies-bit-list-equiv-append-2

(defthm bit-list-equiv-implies-bit-list-equiv-append-2
  (implies (bit-list-equiv y fty::y-equiv)
           (bit-list-equiv (append x y)
                           (append x fty::y-equiv)))
  :rule-classes (:congruence))

Theorem: bit-list-equiv-implies-bit-list-equiv-nthcdr-2

(defthm bit-list-equiv-implies-bit-list-equiv-nthcdr-2
  (implies (bit-list-equiv l l-equiv)
           (bit-list-equiv (nthcdr n l)
                           (nthcdr n l-equiv)))
  :rule-classes (:congruence))

Theorem: bit-list-equiv-implies-bit-list-equiv-take-2

(defthm bit-list-equiv-implies-bit-list-equiv-take-2
  (implies (bit-list-equiv l l-equiv)
           (bit-list-equiv (take n l)
                           (take n l-equiv)))
  :rule-classes (:congruence))