[isabelle-dev] Word sessions and theories

[Klein, Gerwin (Data61, Kensington NSW)]

> On 18 Oct 2020, at 03:35, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> 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

-------------- 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/20201018/cf0b78bf/attachment.sig>