Re: [isabelle] Congruence rules for modular arithmetic
Amine Chaieb wrote:
For e.g. (x mod 256 + 8) mod 256 = (x + 8) mod 256
one would need more than simple rewriting with zmod_simps (maybe a
special simproc or tactic to convert 8 into 8 mod 256 or generally y
into y mod m provided we can prove y < m and m >= 0 for the integers).
For integers, the statement above doesn't depend on 8 being equal to 8
In fact it is one of the simplifications in the list rdmods, in
Num_Lemmas.thy in src/HOL/Word.
Incidentally, the stuff I put into Num_Lemmas.thy was stuff I thought
was of more general interest than just to be used within the
This archive was generated by a fusion of
Pipermail (Mailman edition) and