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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
