[isabelle-dev] Word Libraries

[Florian Haftmann]

Hi Gerwin,

>> Maybe consolidations for Word_Lib could also happen on a dedicated AFP
>> branch
>> *after* the Isabelle release and later converge to the (then) next AFP
>> release.
> 
> Yes, that would be a possibility.

At the moment I am optimistic we won’t need this.

>>> - things started breaking immediately for 64-bit architectures,
>>> because the Sumo concept alone does not quite work. It is not enough
>>> to make all lemmas for all word lengths available. The point of the
>>> Word_SetupXX theories is to additionally establish a set of common
>>> names that refer to the default word type of the program (basically,
>>> whatever "unsigned int" is in C for that architecture, and what the
>>> register width is for the machine). Having these names common means
>>> that the same proof text can work on different concrete types. This
>>> is different to actually generic lemmas that work for any word length
>>> or that need to resolve preconditions on the word length before they
>>> can be applied (the latter can be solved in theories like Word8 etc).
>>> It is not the prettiest form of genericity, but it is crucial for not
>>> having to duplicate thousands of lemmas that for other reasons do
>>> need to refer to a concrete word length (which is known in the proof
>>> state, but unknown to the proof text). Ultimately this is comes from
>>> C, which as painful as it is, works on exactly that principle that
>>> the same type name can refer to different representations, depending
>>> on architecture.
>>
>> My proposal:
>> * Theories Word_SetupXX re-appear offering the same name bindings as
>> pre-Isabelle2021
>> * Their purpose is documented in the Guide.thy
> 
> Sounds good.

After having a second look, the story appears more delicate: there is
not only Word_Setup_ARCH.thy, but also Word_Lemmas_ARCH.thy; while
Word_Lemmas_32.thy and Word_Lemmas_64.thy mimic each other, they contain
both »generic« lemmas with same name like

lemma word_bits_len_of:
  "len_of TYPE (32) = word_bits"
  by (simp add: word_bits_conv)

vs.

lemma word_bits_len_of:
  "len_of TYPE (64) = word_bits"
  by (simp add: word_bits_conv)

and »specific« lemmas with differentiated name like

lemma of_nat32_0:
  "\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk>
\<Longrightarrow> n = 0"
  by (erule of_nat_0, simp add: word_bits_def)

vs.

lemma of_nat64_0:
  "\<lbrakk>of_nat n = (0::word64); n < 2 ^ word_bits\<rbrakk>
\<Longrightarrow> n = 0"
  by (erule of_nat_0, simp add: word_bits_def)

And none of them uses the »generic« type alias machine_word introduced
in the corresponding Word_Setup_ARCH.thy theory.

What is the state supposed to be achieved here?  Naively I would think
that Word_Setup_ARCH.thy should contain all »generic« lemmas and make
use of the »generic« type alias, wheres »specific« lemmas should stay in
Word_32 / Word_64.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211014/139e8885/attachment.sig>