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
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
