[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: 

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.