Re: [isabelle] mod_mult_distrib



Note that Proof General allows you to search for theorems using the Find button. If you type `intro', it will find all the theorems whose conclusion matches your current goal. If you install sledgehammer http://isabelle.in.tum.de/sledgehammer.html, it would have proved your goal automatically (and trivially).

Tobias

Florian Haftmann wrote:
Dear Stefania,

I want to prove mod_mult_distrib: "(a*b) mod (c::int)= ((a mod c) * (b mod c)) mod c". A similar property is already proved for a, b c natural numbers. I will like to have it for positive, nonzero integers. Can someone give me an idea how to prove it? (maybe by using the property for nat)

Others have already done the work you :-)  The theorem is named
zmod_zmult_distrib:

lemma
  "(a * b) mod (c::int)= ((a mod c) * (b mod c)) mod c"
  by (fact zmod_zmult_distrib)

Hope this helps
	Florian

P.S. tested with Isabelle 2008






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