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

Hi all,

thanks for the replies.  I will give a short summary and give some clues
what I am actually aiming for.  Note that this is just a roadmap for
future work, not anything I see for the near future (~ 3 months).

* Concerning Bit.thy – this is something separate, a formalisation of
the Z2 field actually.  It stand aparat, and references of the Word
theories to bit should be replaced by bool.

* Concerning bit operations – these should use bool uniformly.  Both
explicit list conversions and implicit structural operation like
test_bit and set_bit are relevant for user space. _ BIT _ is a historic
accident.  The idea is to clearly separate the bit operations into
separate HOL-Library theories, to make them properly available for
applications which do not need words but bits.

This suggests a few refinements, which then lead to naming questions,
e.g. for bin_nth :: int => nat => bool the name does not really make
sense ;-).  Maybe its best to have the bit operations in a theory named
Bit, to have qualified names like Bit.test :: 'a => nat => bool or :: nat => (bool => bool) => ('a => 'a) and such.  Then the
existing Z2 theory should maybe really be named Z2.  (Just rough
thoughts at the moment, not clear suggestions).

It is uncertain when I will come back to that issue, but the basic
landmarks are now far clearer than before.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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