[isabelle-dev] Word sessions and theories

[Florian Haftmann]

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: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201008/baaeadd8/attachment.sig>