[isabelle-dev] Word Libraries

[Florian Haftmann]

Hi Gerwin et al.,

my report about the state of affairs reached inisabelle 8ab92e40dde6 /
afp: 807c0639d73d tip

A. << >> >>> are back as conventional operations (constants)

The glitch of two different sets of bit shift operations naturally
sometimes produces unclear situations.

An ideal solution would be available if abbreviations could be organized
in bundles.

B. A confluent set of rewrite rules on ground terms

Particularly for signed operations like <s <=s sdiv smod this has not
been present even for int so far.

An explicit exception is the mask :: nat => 'a, where there is too
little context to determine whether it is supposed to be understood as
abstract or concrete value.

A related cause is the singleton bit expression 2 ^ numeral _ which
normalizes due to the conventional rules on exponentiation – but this
has never been different.

C. Poor man's genericity 32 vs. 64

I still need feedback on this -- my further post maybe got lost due to
my ongoing confusion of mail adresses.

>>> My proposal:
>>> * Theories Word_SetupXX re-appear offering the same name bindings as
>>> pre-Isabelle2021
>>> * Their purpose is documented in the Guide.thy
> 
> 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, whereas »specific« lemmas should stay in
> Word_32 / Word_64.

Cheers,
	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/20211030/46eea49c/attachment.sig>