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