Email Gateway (Oct 08 2020 at 13:22): Email Gateway (Oct 08 2020 at 13:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
Email Gateway (Oct 08 2020 at 23:39):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Hi Florian,
Thanks for making a start with this, an overview for the Word libraries is long overdue.
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?
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.
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.
Cheers,
Gerwin
signature.asc
Email Gateway (Oct 09 2020 at 11:41):From: Lawrence Paulson <lp15@cam.ac.uk>
I totally agree with this point.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 09 2020 at 11:47):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
Email Gateway (Oct 17 2020 at 17:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
Email Gateway (Oct 18 2020 at 22:44):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
On 18 Oct 2020, at 03:35, Florian Haftmann <florian.haftmann@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
signature.asc
Last updated: Dec 21 2024 at 16:20 UTC