		Search-engine friendly clone of the ACL2 documentation.

Bitops/equal-by-logbitp

Equal-by-logbitp-hint

The equal-by-logbitp-hint computed hint looks for goals of the form:

(implies (and hyp1 hyp2 ...)
         (equal lhs rhs))

And automatically generates an appropriate :functional-instance of the equal-by-logbitp theorem. A typical use of this hint might be:

:hints(("Goal"
        :in-theory (enable foo bar))
       (and stable-under-simplificationp
            (equal-by-logbitp-hint)))

Note that this hint is very aggressive. For instance, it doesn't try to determine whether lhs and rhs are numbers; it will try to use equal-by-logbitp anyway. Because of this, you would never want to add this to the default-hints.

Definitions and Theorems

Function: equal-by-logbitp-hint-fn

(defun equal-by-logbitp-hint-fn (clause)
 (b* ((concl (car (last clause)))
      ((unless (and (consp concl)
                    (eq (car concl) 'equal)))
       nil)
      (lhs (cadr concl))
      (rhs (caddr concl))
      (hyp (cons 'and
                 (acl2::dumb-negate-lit-lst (butlast clause 1)))))
  (cons
   ':use
   (cons
    (cons
     (cons
      ':functional-instance
      (cons
       'equal-by-logbitp
       (cons
          (cons 'logbitp-hyp
                (cons (cons 'lambda
                            (cons 'nil (cons hyp 'nil)))
                      'nil))
          (cons (cons 'logbitp-lhs
                      (cons (cons 'lambda
                                  (cons 'nil (cons lhs 'nil)))
                            'nil))
                (cons (cons 'logbitp-rhs
                            (cons (cons 'lambda
                                        (cons 'nil (cons rhs 'nil)))
                                  'nil))
                      'nil)))))
     'nil)
    'nil))))