		Search-engine friendly clone of the ACL2 documentation.

Open-logbitp-of-const-meta

Rewrite terms like (logbitp foo 7) to (or (not (natp foo)) (member-equal foo '(0 1 2))).

This meta rule targets terms of the form

(logbitp term const)

where const is a quoted constant, typically a number. We know that such a term can only be true when term happens to be one of the bit positions that has a 1 bit set in const, so we can split into cases based on which bits of const are set.

Note that this rule basically is going to split into n cases, where n is the number of 1 bits in const! Because of this we keep it disabled. But if you see a logbitp term applied to a constant, you might want to consider enabling this rule.

Definitions and Theorems

Theorem: lbpc-ev-constraint-0

(defthm lbpc-ev-constraint-0
 (implies (and (consp x)
               (syntaxp (not (equal a ''nil)))
               (not (equal (car x) 'quote)))
          (equal (lbpc-ev x a)
                 (lbpc-ev (cons (car x)
                                (kwote-lst (lbpc-ev-lst (cdr x) a)))
                          nil))))

Theorem: lbpc-ev-constraint-1

(defthm lbpc-ev-constraint-1
  (implies (symbolp x)
           (equal (lbpc-ev x a)
                  (and x (cdr (assoc-equal x a))))))

Theorem: lbpc-ev-constraint-2

(defthm lbpc-ev-constraint-2
  (implies (and (consp x) (equal (car x) 'quote))
           (equal (lbpc-ev x a) (cadr x))))

Theorem: lbpc-ev-constraint-3

(defthm lbpc-ev-constraint-3
  (implies (and (consp x) (consp (car x)))
           (equal (lbpc-ev x a)
                  (lbpc-ev (caddr (car x))
                           (pairlis$ (cadr (car x))
                                     (lbpc-ev-lst (cdr x) a))))))

Theorem: lbpc-ev-constraint-4

(defthm lbpc-ev-constraint-4
  (implies (not (consp acl2::x-lst))
           (equal (lbpc-ev-lst acl2::x-lst a)
                  nil)))

Theorem: lbpc-ev-constraint-5

(defthm lbpc-ev-constraint-5
  (implies (consp acl2::x-lst)
           (equal (lbpc-ev-lst acl2::x-lst a)
                  (cons (lbpc-ev (car acl2::x-lst) a)
                        (lbpc-ev-lst (cdr acl2::x-lst) a)))))

Theorem: lbpc-ev-constraint-6

(defthm lbpc-ev-constraint-6
  (implies (and (not (consp x)) (not (symbolp x)))
           (equal (lbpc-ev x a) nil)))

Theorem: lbpc-ev-constraint-7

(defthm lbpc-ev-constraint-7
  (implies (and (consp x)
                (not (consp (car x)))
                (not (symbolp (car x))))
           (equal (lbpc-ev x a) nil)))

Theorem: lbpc-ev-constraint-8

(defthm lbpc-ev-constraint-8
  (implies (and (consp x) (equal (car x) 'logbitp))
           (equal (lbpc-ev x a)
                  (logbitp (lbpc-ev (cadr x) a)
                           (lbpc-ev (caddr x) a)))))

Theorem: lbpc-ev-constraint-9

(defthm lbpc-ev-constraint-9
  (implies (and (consp x) (equal (car x) 'not))
           (equal (lbpc-ev x a)
                  (not (lbpc-ev (cadr x) a)))))

Theorem: lbpc-ev-constraint-10

(defthm lbpc-ev-constraint-10
  (implies (and (consp x) (equal (car x) 'if))
           (equal (lbpc-ev x a)
                  (if (lbpc-ev (cadr x) a)
                      (lbpc-ev (caddr x) a)
                    (lbpc-ev (cadddr x) a)))))

Theorem: lbpc-ev-constraint-11

(defthm lbpc-ev-constraint-11
  (implies (and (consp x) (equal (car x) 'equal))
           (equal (lbpc-ev x a)
                  (equal (lbpc-ev (cadr x) a)
                         (lbpc-ev (caddr x) a)))))

Theorem: lbpc-ev-constraint-12

(defthm lbpc-ev-constraint-12
  (implies (and (consp x) (equal (car x) 'natp))
           (equal (lbpc-ev x a)
                  (natp (lbpc-ev (cadr x) a)))))

Theorem: lbpc-ev-constraint-13

(defthm lbpc-ev-constraint-13
  (implies (and (consp x) (equal (car x) 'zp))
           (equal (lbpc-ev x a)
                  (zp (lbpc-ev (cadr x) a)))))

Theorem: lbpc-ev-constraint-14

(defthm lbpc-ev-constraint-14
  (implies (and (consp x)
                (equal (car x) 'member-equal))
           (equal (lbpc-ev x a)
                  (member-equal (lbpc-ev (cadr x) a)
                                (lbpc-ev (caddr x) a)))))

Function: bits-between

(defun bits-between (n m x)
  (declare (xargs :guard (and (natp n)
                              (natp m)
                              (<= n m)
                              (integerp x))))
  (let* ((n (lnfix n)) (m (lnfix m)))
    (cond ((mbe :logic (zp (- m n)) :exec (= m n))
           nil)
          ((logbitp n x)
           (cons n (bits-between (+ n 1) m x)))
          (t (bits-between (+ n 1) m x)))))

Function: enumerate-logbitps

(defun enumerate-logbitps (x)
  (declare (xargs :guard (integerp x)))
  (bits-between 0 (integer-length x) x))

Function: open-logbitp-of-const

(defun open-logbitp-of-const (term)
 (declare (xargs :guard (pseudo-termp term)))
 (case-match term
  (('logbitp x ('quote const . &) . &)
   (cond
    ((or (not (integerp const)) (= const 0))
     ''nil)
    ((= const -1) ''t)
    ((natp const)
     (cons
      'if
      (cons
       (cons 'natp (cons x 'nil))
       (cons
        (cons
         'if
         (cons
          (cons
           'member-equal
           (cons x
                 (cons (cons 'quote
                             (cons (enumerate-logbitps const) 'nil))
                       'nil)))
          '('t 'nil)))
        (cons (cons 'quote
                    (cons (logbitp 0 const) 'nil))
              'nil)))))
    (t
     (cons
      'if
      (cons
       (cons 'natp (cons x 'nil))
       (cons
        (cons
         'not
         (cons
          (cons
           'member-equal
           (cons
               x
               (cons (cons 'quote
                           (cons (enumerate-logbitps (lognot const))
                                 'nil))
                     'nil)))
          'nil))
        (cons (cons 'quote
                    (cons (logbitp 0 const) 'nil))
              'nil)))))))
  (& term)))

Theorem: open-logbitp-of-const-meta

(defthm open-logbitp-of-const-meta
  (equal (lbpc-ev x a)
         (lbpc-ev (open-logbitp-of-const x) a))
  :rule-classes ((:meta :trigger-fns (logbitp))))

Function: open-logbitp-of-const-lite

(defun open-logbitp-of-const-lite (term)
 (declare (xargs :guard (pseudo-termp term)))
 (case-match term
  (('logbitp x ('quote const . &) . &)
   (cond
    ((or (not (integerp const)) (= const 0))
     ''nil)
    ((= const -1) ''t)
    ((natp const)
     (let ((len (1- (integer-length const))))
       (if (equal const (ash 1 len))
           (if (= len 0)
               (cons 'zp (cons x 'nil))
             (cons 'equal
                   (cons x
                         (cons (cons 'quote (cons len 'nil))
                               'nil))))
         term)))
    (t
     (let* ((const (lognot const))
            (len (1- (integer-length const))))
      (if
       (equal const (ash 1 len))
       (if (= len 0)
           (cons 'not
                 (cons (cons 'zp (cons x 'nil)) 'nil))
         (cons 'not
               (cons (cons 'equal
                           (cons x
                                 (cons (cons 'quote (cons len 'nil))
                                       'nil)))
                     'nil)))
       term)))))
  (& term)))

Theorem: open-logbitp-of-const-lite-meta

(defthm open-logbitp-of-const-lite-meta
  (equal (lbpc-ev x a)
         (lbpc-ev (open-logbitp-of-const-lite x)
                  a))
  :rule-classes ((:meta :trigger-fns (logbitp))))