Re: [isabelle] bit vs. bool in HOL-Word

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.

- Brian

On Sun, Aug 18, 2013 at 7:35 AM, Florian Haftmann
<florian.haftmann at> wrote:
> Hello all,
> 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.
> Suggestions welcome,
>         Florian
> --
> PGP available:

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