[isabelle-dev] Word sessions and theories

[Florian Haftmann]

Hi Gerwin,

> 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.

I am happy to converge into that direction.  The critical question
remains whether they should be full or only input abbreviations.  In the
former cases, it would be better to have them restricted to word,
otherwise you would end up with ‹lsb (2 * k + 1)› for k :: int, which
will not do.  If restricted to word, ‹msb› might even remain a dedicated
operation.

> 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.

Thanks, that makes the situation clear.

> 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.

The morphisms in general can be exploited using the transfer method
nowadays.  This should indeed be the core message about Misc_Typedef.

> 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.

Yes, but the reverse order makes it painful to prove anything about it,
 The definitions of append and slicing operations on word use the direct
formulation without any reversal already.

> As for location: I’d be fine with the overview living in Word_Lib. From there it can reference everything in Word_Lib and HOL-Word, and it can provide a few comments on + a pointer to the Native_Word entry, which could contain its own overview.

OK.

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/20201009/8a9714ba/attachment.sig>