Re: [isabelle] bit vs. bool in HOL-Word
I'll try to give you my understanding of the situation.
As users, we mostly use these n-bit machine word representations:
- as lists of booleans of length n (to_bl/of_bl)
- as functions from a domain of cardinality n to bool (test_bit)
- as naturals modulo 2^n (unat/of_nat)
- as nonnegative integers modulo 2 ^ n (uint/word_of_int)
- as a integers - 2 ^ (n - 1) <= x < 2 ^ (n - 1) (sint/word_of_int)
The word type could also have been defined as any of these
representations, and the strength of the library is that the user
doesn't need to care much what the underlying type definition is.
I think that HOL-Word has a lot of history in it. It was created around
the time of an earlier change in the numeral representation, which
annoyed its author somewhat and resulted in some compatibility layers.
As a user, seeing these layers, types and definitions is a strong
indication that you've dug too deep. The same goes for the "_ BIT _"
representation. I suspect that these representations only get used in
user proofs in evaluating concrete n-bit arithmetic (that is, the
simpset introduces them then removes them again).
So, in short, go ahead and reconcile. I don't think users will have too
much work to do if the key representations and theorems about them are
Final comment, the word_bitwise representation Sascha and I worked on in
2010 uses the boolean list representation (to_bl/of_bl) or, more
precisely, its reverse (rev o to_bl/of_bl o rev). In hindsight, the HOL4
group's approach based on the function-to-bool representation (test-bit
in Isabelle) is probably smarter, since it caches better, though it
involves lots of natural inequalities which require simprocs to resolve
in Isabelle and are a bit of a nuisance. I'm not sure if that is even
On 19/08/13 03:35, Brian Huffman wrote:
I created Library/Bit.thy in February 2009 as a theory of the field of
integers mod 2. One motivation was to be able to have polynomials with
integers mod 2 as coefficients, which have applications in
cryptography. (I had also been working on Library/Polynomial.thy
around the same time.) As a field, it is possible to use type "bit"
with polynomial operations like div, mod, and gcd.
The connections between Bit.thy and the ancient numeral representation
using _ BIT _ are accidental (see rev. 8e33b9d04a82); it is just a
coincidence that the new type is also named "bit". The other uses of
Bit.thy in HOL-Word are also likely due to my choice of the name of
the type "bit" more than anything else. Perhaps "Z2" or "z2" would
have been a better name for the new type; I just thought that an
English word would fit better with Isabelle's naming conventions.
In summary: I never meant for Library/Bit.thy to have any connection
whatsoever to HOL-Word; I'd be in favor of converting HOL-Word to use
type bool instead. Also, I'm open to renaming Library/Bit.thy to more
accurately describe its contents and intended use.
On Sun, Aug 18, 2013 at 7:35 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
I have been revisiting the HOL-Word theories, and a central question
which has come to my mind is how bits are to be represented. Some
theories are just using bool, but some use a dedicated but also
two-valued type bit. This mixture is awkward. Further, it seems to me
that the use of the bit type (in connection with the pseudo infix
constructor _ BIT _, which is the seed of almost all further usages of
type bit) goes back to the ancient numeral representation as signed bit
strings, which is now gone.
So, I would call for feedback from users of the HOL-Word theories:
* Is there a reason to prefer bit over bool or the other way round, and
if yes, in which situations? Or does that just appear as accident?
* If bool would be the preferred type, is it feasible (wrt. to existing
applications »outside there«) to replace bit by bool entirely? This
could also include input syntax 0 and 1 for False and True respectively,
a conversion of_bool :: bool => 'a::zero_neq_one etc.
This archive was generated by a fusion of
Pipermail (Mailman edition) and