Re: [isabelle] need help by mod



kuecuek at rbg.informatik.tu-darmstadt.de wrote:
Hallo everybody

i have some problems with modulo and power :(

i need following prooofs but i couldn't show these. 1) ((a::int) - b) mod p = (a mod p - b mod p) mod p there is a lemma called zmod_zadd1_eq in IntDiv. i have tried to use this lemma with the variable "-b" but it doesn't help.

[zmod_zsub_left_eq, zmod_zsub_right_eq] MRS trans RS sym

2)"(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
by this lemma i have problems too.

This would be proved by induction on k, I think for the induction step you would use the corresponding theorem for multiplication which would be
[zmod_zmult1_eq, zmod_zmult1_eq_rev] MRS trans RS sym ;

Regards,

Jeremy


could anyone help me?

thanks for your helps

best regards








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