[isabelle-dev] Fwd: Word Libraries
florian.haftmann at informatik.tu-muenchen.de
Sat Oct 9 19:09:38 CEST 2021
>>> - 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev