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



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

Attachment: signature.asc
Description: OpenPGP digital signature



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