Bits

_From [rage...@gmail.com](https://code.google.com/u/102895947197065323718/) on November 20, 2013 16:55:55_

We could use a nice, standard, definition, similar to the version of bits in the rtl library, that comes with a lot of nice lemmas (a linear rule to describe the maximum value returned by bits, what it means to logapp calls of bits, etc.). Furthermore, it should work well with GL/SAT.

Here's one possible definition:

(define gl-bits
((x integerp "Integer from which to select bits")
(i natp "Starting position for selection (inclusive and also the smaller number")
(j natp "Ending position for selection (exclusive and also the larger number"))
:parents (oracle-undocumented)
(logtail i (loghead j x)))

There's another in books/centaur/bitops/part-select, but it's written in terms or rdb and bsp. That might be an issue for those that aren't already using rdb and bsp, but if there was a nice theory around part-select, I'd guess it wouldn't matter what the implementation was.

_Original issue: http://code.google.com/p/acl2-books/issues/detail?id=122_