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