> On 18 Oct 2020, at 03:35, Florian Haftmann > <[email protected]> wrote: > >> 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? > > I forgot to answer: Guide.thy resides just in the regular AFP > development repository, session Word_Lib.
Thanks, I should have another look at it this week. (Sorry for the slowness, my employer has found it opportune to majorly distract me from proof work these past months) >> 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. > > I updated the guide with recent feedback. Cool, thanks. > What seems worth further discussion is the lsb / msb issue. Since there > are strong arguments / desires to keep them in the long run, currently > my proposal would be: > > * Restrict lsb and msb to word type. > > * lsb as regular abbreviation for odd. > > * msb as dedicated operation. I’d be happy with that, yes. Cheers, Gerwin
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
