Re: [isabelle] need help by mod

On Tuesday 12 December 2006 03:32, 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.

For this one you will need a lemma about unary negation:

lemma zminus_zmod: "- ((x::int) mod p) mod p = - x mod p"
by (simp only: zmod_zminus1_eq_if mod_mod_trivial)

Now you can use transitive reasoning with this and other lemmas about mod and

lemma "((a::int) - b) mod p = (a mod p - b mod p) mod p"
proof -
have "(a - b) mod p = (a + - b) mod p" by (simp only: diff_def)
also have "... = (a mod p + - b) mod p" by (rule zmod_zadd_left_eq)
also have "... = (a mod p + - b mod p) mod p" by (rule zmod_zadd_right_eq)
also have "... = (a mod p + - (b mod p) mod p) mod p" by (simp only:
zminus_zmod)
also have "... = (a mod p + - (b mod p)) mod p" by (rule zmod_zadd_right_eq
[symmetric])
also have "... = (a mod p - b mod p) mod p" by (simp only: diff_def)
finally show ?thesis .
qed

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

This one follows easily from lemma zpower_zmod:

lemma "(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
proof -
assume "a mod p = b mod p"
hence "(a mod p) ^ k mod p = (b mod p) ^ k mod p" by simp
thus "a ^ k mod p = b ^ k mod p" by (simp only: zpower_zmod)
qed

- Brian

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