		Search-engine friendly clone of the ACL2 documentation.

Bitops/extra-defs

Copybit

Set To[n] := From[n]

Signature
(copybit n from to) → ans
Arguments: n — Bit position to copy.
Guard (natp n).; from — Guard (integerp from).; to — Guard (integerp to).
Returns: ans — Type (integerp ans).

Definitions and Theorems

Function: copybit

(defun copybit (n from to)
  (declare (xargs :guard (and (natp n)
                              (integerp from)
                              (integerp to))))
  (let ((__function__ 'copybit))
    (declare (ignorable __function__))
    (if (logbitp n from)
        (setbit n to)
      (clearbit n to))))

Theorem: integerp-of-copybit

(defthm acl2::integerp-of-copybit
  (b* ((ans (copybit n from to)))
    (integerp ans))
  :rule-classes :type-prescription)

Theorem: nat-equiv-implies-equal-copybit-1

(defthm nat-equiv-implies-equal-copybit-1
  (implies (nat-equiv n n-equiv)
           (equal (copybit n x y)
                  (copybit n-equiv x y)))
  :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-copybit-2

(defthm int-equiv-implies-equal-copybit-2
  (implies (int-equiv x x-equiv)
           (equal (copybit n x y)
                  (copybit n x-equiv y)))
  :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-copybit-3

(defthm int-equiv-implies-equal-copybit-3
  (implies (int-equiv y y-equiv)
           (equal (copybit n x y)
                  (copybit n x y-equiv)))
  :rule-classes (:congruence))