[isabelle] new bits library for isabelle



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.

- Brian






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.