*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] need help by mod*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Thu, 14 Dec 2006 08:48:46 -0800*Cc*: kuecuek at rbg.informatik.tu-darmstadt.de, isabelle-users at cl.cam.ac.uk*In-reply-to*: <200612121232.15334.kuecuek@rbg.informatik.tu-darmstadt.de>*References*: <200612121232.15334.kuecuek@rbg.informatik.tu-darmstadt.de>*User-agent*: KMail/1.8

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 addition to build a proof: 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

**References**:**[isabelle] need help by mod***From:*kuecuek

- Previous by Date: Re: [isabelle] INstalling Isabelle / sudo and permissions
- Next by Date: [isabelle] simple lemma in ring theory
- Previous by Thread: Re: [isabelle] need help by mod
- Next by Thread: [isabelle] INstalling Isabelle / sudo and permissions
- Cl-isabelle-users December 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list