		Search-engine friendly clone of the ACL2 documentation.

Bitwise-operations

Op-not

Leo logical or bitwise negation operation.

Signature
(op-not arg) → result
Arguments: arg — Guard (valuep arg).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-not

(defun op-not (arg)
 (declare (xargs :guard (valuep arg)))
 (let ((__function__ 'op-not))
  (declare (ignorable __function__))
  (b* ((err (list :op-not (value-fix arg))))
   (cond ((value-case arg :bool)
          (value-bool (not (value-bool->get arg))))
         ((value-case arg :u8)
          (value-u8 (loghead 8 (lognot (value-u8->get arg)))))
         ((value-case arg :u16)
          (value-u16 (loghead 16 (lognot (value-u16->get arg)))))
         ((value-case arg :u32)
          (value-u32 (loghead 32 (lognot (value-u32->get arg)))))
         ((value-case arg :u64)
          (value-u64 (loghead 64 (lognot (value-u64->get arg)))))
         ((value-case arg :u128)
          (value-u128 (loghead 128 (lognot (value-u128->get arg)))))
         ((value-case arg :i8)
          (value-i8 (lognot (value-i8->get arg))))
         ((value-case arg :i16)
          (value-i16 (lognot (value-i16->get arg))))
         ((value-case arg :i32)
          (value-i32 (lognot (value-i32->get arg))))
         ((value-case arg :i64)
          (value-i64 (lognot (value-i64->get arg))))
         ((value-case arg :i128)
          (value-i128 (lognot (value-i128->get arg))))
         (t (reserrf err))))))

Theorem: value-resultp-of-op-not

(defthm value-resultp-of-op-not
  (b* ((result (op-not arg)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-not-of-value-fix-arg

(defthm op-not-of-value-fix-arg
  (equal (op-not (value-fix arg))
         (op-not arg)))

Theorem: op-not-value-equiv-congruence-on-arg

(defthm op-not-value-equiv-congruence-on-arg
  (implies (value-equiv arg arg-equiv)
           (equal (op-not arg) (op-not arg-equiv)))
  :rule-classes :congruence)