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 mod 256.

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 machine-word library.

Jeremy Dawson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.