[isabelle-dev] Word sessions and theories

[Klein, Gerwin (Data61, Kensington NSW)]

Hi Florian,

Thanks for making a start with this, an overview for the Word libraries is long overdue.

I’m happy to add a bit of material and design rationale to the document for parts of Word_Lib that seem unclear. Is there a repo I should contribute to?

There are a few bits I disagree with, though, in particular the desire to replace operations like lsb, msb, etc with existing operations. That would be counter productive. If they can be made abbreviations on the word type, that is fine, and should probably be done, but the names are important. Programmers know what “lsb" ist, but will have to really think about this being equivalent to “odd”. If you’re writing theorem statements or specifications that other people need to be able to understand, familiarity is important.

Minor points: the tagging for word types with signedness (or not) is useful in program verification where you sometimes want to track what the compiler understands the type to be, so that you can later pick corresponding transformations based on that understanding. It doesn’t have any relevance to theorems you’d prove manually.

Misc_Typedef: not sure it deserves the attribute “invasive”. I haven’t checked how it has developed, but it used to be a simple constant definition. I remember Jeremy introducing it to get simpler isomorphism results or something along that line. If it is not necessary any more, it’d be perfectly fine to eliminate.

Reversed_Bit_Lists: they are rarely used for algebraic properties, but they are useful for more complex append and slicing operations as you sometimes find in hardware specs. In general, I wouldn’t make too many comments on use in the overview. Takes too long to explain and is very dependent on application.

As for location: I’d be fine with the overview living in Word_Lib. From there it can reference everything in Word_Lib and HOL-Word, and it can provide a few comments on + a pointer to the Native_Word entry, which could contain its own overview.

Cheers,
Gerwin

> On 8 Oct 2020, at 23:21, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> Hi all,
> 
> in the course of iterating through the accumulated theories on words, I
> came to the conclusion that it is high time to write up a guide to the
> existing material.
> 
> Currently, this resides in theory Guide in session Word_Lib; find a
> document excerpt here:
> http://isabelle.in.tum.de/~haftmann/bits_and_word/primer.pdf
> 
> I want to excite feedback:
> 
> * To my understanding, the base theories (Bit_Operations in HOL-Library
> and Word in HOL-Word) now contain all the substantial ideas brought up
> in informal sessions on HOL-Word, particularly: algebraic
> characterization of operations, uniform notation for different types
> using type classes, proper setup of the Isabelle tools ab initio (),
> generic conversions, avoiding unnecessary indirections in definitions
> etc.  Of course there is no claim that the corresponding lemmas are
> »complete« in any sense, but such can easily be added incrementally.
> Please tell me if you thing something substantially is missing wrt.
> operations.
> 
> * The guide is very terse on theories whose relevance I do not
> comprehend at the moment.  So I am open to feedback or extensions to the
> guide.
> 
> * A question of organization remains that goes to the AFP editors.  The
> following final structure is envisaged:
> 
>    a) Isabelle distribution: theories Bit_Operations and Word.
> 
>    b) AFP session Word_Lib: further generic word theories.
> 
>    c) AFP session Native_Word: a self-contained entry.
> 
> Currently, the guide resides in theory Word_Lib.  Nevertheless IMHO it
> should cover the important library in session Native_Word also.  But to
> move it to Native_Word seems to be the wrong choice.
> 
> A possible solution would be a dedicated overview session in the AFP.
> But this would be a precedence case.
> 
> Cheers,
> 	Florian
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201008/dc7e5452/attachment-0001.sig>