[isabelle] [Fwd: Re: need help by mod]

Sorry, I forgot to CC.

Cheers,
Amine.
--- Begin Message ---
Hi Kuecuek,

Not so nice proofs, but they work.

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.

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
also have "\<dots> = (a mod p + (- b) mod p) mod p"
also have "\<dots> = (a mod p - b mod p) mod p"
apply (simp only: zmod_zminus1_eq_if[where a="b" and b="p"])
apply (cases "b mod p = 0", simp_all add: ring_eq_simps)
proof-
assume H: "b mod p \<noteq> 0"
have "(p + a mod p - b mod p) mod p = (p + (a mod p - b mod p)) mod p"
by (simp only: ring_eq_simps)
also have "\<dots> = (a mod p - b mod p ) mod p" by simp
finally show "(p + a mod p - b mod p) mod p = (a mod p - b mod p) mod p" .
qed
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.

lemma assumes H: "(a::int) mod p = b mod p" shows "a ^ k mod p = b ^ k mod p"
using H
proof(induct k)
case (Suc k)
have "a ^ (Suc k) mod p = a * a ^ k mod p" by simp
also have "\<dots> = (a mod p) * (a ^ k mod p) mod p" using zmod_zmult_distrib by simp
also have "\<dots> = (b mod p) * (b ^ k mod p) mod p" using prems by simp
also have "\<dots> = b ^ (Suc k) mod p" using zmod_zmult_distrib by simp
finally show ?case by blast
qed auto

Cheers,
Amine

--- End Message ---

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