[isabelle-dev] Fwd: Word Libraries

[Florian Haftmann]

>>> - similarly, there is a rule that automatically rewrites "x = 0" to something in the direction of "x dvd 2^len". This is rarely useful with concrete len, and preventing these terms from being produced is similarly manual as take_bit.
> 
> Plain lemma ‹w = 0› for w :: ‹'a::len word› apply simp does not exhibit
> this.  In which examples does this happen?  (I agree that shouldn't).

No need to investigate that further – the critical rules are
word_of_nat_eq_0_iff and word_of_int_eq_0_iff

	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/20211009/1efdc5a6/attachment.sig>