*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] bit vs. bool in HOL-Word*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Mon, 19 Aug 2013 11:13:21 +1000*In-reply-to*: <CAAMXsiY95eUkA5KuTNTdhNrNRu+TMwRN5JbSXbq9438jp6Udww@mail.gmail.com>*References*: <5210DBB8.1090603@informatik.tu-muenchen.de> <CAAMXsiY95eUkA5KuTNTdhNrNRu+TMwRN5JbSXbq9438jp6Udww@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

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)

Sincerely, Thomas. 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. - Brian On Sun, Aug 18, 2013 at 7:35 AM, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> 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: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**References**:**[isabelle] bit vs. bool in HOL-Word***From:*Florian Haftmann

**Re: [isabelle] bit vs. bool in HOL-Word***From:*Brian Huffman

- Previous by Date: Re: [isabelle] bit vs. bool in HOL-Word
- Next by Date: [isabelle] install question
- Previous by Thread: Re: [isabelle] bit vs. bool in HOL-Word
- Next by Thread: Re: [isabelle] bit vs. bool in HOL-Word
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list