[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.

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.



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"
    by (subst zmod_zadd1_eq,rule refl)
  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.