[isabelle-dev] Word Libraries

[Gerwin Klein]

> On 30 Oct 2021, at 21:04, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> Hi Gerwin et al.,
> 
> my report about the state of affairs reached inisabelle 8ab92e40dde6 /
> afp: 807c0639d73d tip
> 
> A. << >> >>> are back as conventional operations (constants)

That sounds good.


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

I'll have to get deeper into a proof update to see how that interacts. Might be Ok.


> 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.

Yes, that right, those were underdeveloped.


> 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.

Agreed, we have so far left mask abstract and not automatically reduced it for that reason.


> 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.

Also good.


> 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.

lemmas that can be phrased with machine_word usually should be, so that would be an improvement.


>> 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.

Yes, that would make sense and would clarify the setup. It is possible that some lemmas are not in the right place due to dependencies, but a lot of material has been generalised and moved into generic Word_Lemmas instead, so it is quite possible that this could now be applied consistently.

Cheers,
Gerwin


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211031/c854fac8/attachment.sig>