Re: [isabelle] A note on recent renovations in session HOL-Word



Hi Florian,

I think that is a good endeavour, there is indeed much that can be expressed more nicely these days. Keeping larger changes to after Isabelle2019 would be good.

For testing, I guess we are one of the biggest users of Word proofs, so it might make sense to have a look at https://github.com/seL4/l4v/ and run that for at least the ARM architecture settings. Of course this is on Isabelle2018. There is another round of material accumulated there that I was planning to contribute to the AFP Word entry before the Isabelle2019 release, but I will probably run out of time (project deadlines, haven’t even managed yet to test RC1) and have to move it to the next one.

Are your current HOL-Word changes already in RC1 or planned for RC2? Was there much impact on AFP.Word_Lib?

I’m also happy to help with testing later changes and be involved in the content evolution of HOL-Word.

Cheers,
Gerwin

On 4 May 2019, at 05:07, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de<mailto:florian.haftmann at informatik.tu-muenchen.de>> wrote:

Hi all,

recently I had a closer look at the session HOL-Word; what started as a
mere analysis out of curiousity turned into a substantial overhaul of
existing material resulting in a plan for the time after the next release.

What is relevant for the next release:
* The traditional entry point HOL-Word.Word is supposed to be
meta-stable: there might be issues due to things like additional simp
rules and oscillating full theorem names etc. as not uncommon for new
releases, but there are no intentional changes in scope there.
* HOL-Word.More_Word is an additional »sumo« enty point into HOL-Word.
* Other theories in HOL-Word have undergone a massive internal
re-structuring and re-grouping of material, absorbing material from AFP
sessions, particulary Native_Word.

Some time after the release I would attempt a de-baroquification
(purification?) of HOL-Word: there is evidence that the essentially
needed things can be expressed quite compactly using state-of-the-art
tools in Isabelle/HOL; preliminary case studies can be found in
src/HOL/ex/Bit_Lists.thy and src/HOL/ex/Word_Type.thy (which are just a
start, there is much more in the pipeline).  Hence I hope that in the
long run bit and word types and operations can take place in two
theories in HOL-Library, which HOL-Word that just builds upon; we will
see which applications then still need full HOL-Word.

Cheers,
Florian




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.