		Search-engine friendly clone of the ACL2 documentation.

Bit-list

Bit-list-fix

(bit-list-fix x) is a usual ACL2::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 acl2::y)
  (declare (xargs :guard (and (bit-listp x)
                              (bit-listp acl2::y))))
  (equal (bit-list-fix x)
         (bit-list-fix acl2::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) acl2::y)
           (bit-list-equiv x acl2::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 acl2::y))
           (bit-list-equiv x acl2::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)
                           acl2::y)
           (bit-list-equiv x acl2::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 acl2::y))
           (bit-list-equiv x acl2::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) acl2::y)
                  (cons x acl2::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 acl2::y)
                           (cons x-equiv acl2::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 acl2::y))
                  (cons x acl2::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 acl2::y y-equiv)
           (bit-list-equiv (cons x acl2::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 (acl2::repeat acl2::n x))
         (acl2::repeat acl2::n (bfix x))))

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

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

Theorem: nth-of-bit-list-fix

(defthm nth-of-bit-list-fix
  (equal (nth acl2::n (bit-list-fix x))
         (if (< (nfix acl2::n) (len x))
             (bfix (nth acl2::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 acl2::y)
                           (append fty::x-equiv acl2::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 acl2::y fty::y-equiv)
           (bit-list-equiv (append x acl2::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 acl2::l l-equiv)
           (bit-list-equiv (nthcdr acl2::n acl2::l)
                           (nthcdr acl2::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 acl2::l l-equiv)
           (bit-list-equiv (take acl2::n acl2::l)
                           (take acl2::n l-equiv)))
  :rule-classes (:congruence))