> On 30 Oct 2021, at 21:04, Florian Haftmann > <[email protected]> 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
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
