Email Gateway (Aug 18 2022 at 10:02): Email Gateway (Aug 18 2022 at 10:02):From: Brian Huffman <brianh@csee.ogi.edu>
Hello all,
I have been working on a library of bitwise operations and modular arithmetic,
and I would welcome anyone to try it out and let me know what you think, or
give suggestions for what features to add. If it turns out to be useful, I
would be happy to contribute it to the Isabelle distribution.
The theory files for the Bits library are available at my homepage:
http://www.csee.ogi.edu/~brianh/isabelle/Bits.tar.gz
Note that you will need to use a recent developer snapshot of Isabelle,
although it might work with Isabelle 2005 with only minor changes.
The library defines type constructors for n-bit words and for integers mod n,
where the parameter n is given using a numeric syntax for types. For example,
"16 bits" is how to write the type of 16-bit integers. The bitwise operators
NOT, AND, OR and XOR are defined on n-bit words and type int. They are shown
to satisfy all the properties of a boolean algebra, and simplification of
bitwise operations on numeric literals is also supported.
Last updated: Nov 21 2024 at 12:39 UTC