Re: [isabelle] Proofs involving Integers



Hi,

These are simple instances of simple rewriting with AC, so simp add: ring_simps would do the job. For more complicated instances including only equality and disequality (~=) try the algebra method.

Amine.

George Karabotsos wrote:
Hello,

I am having trouble proving the following lemmas that involve integers.
For example, the following:

lemma "-(x * (i + (1::int))) = - ((x * i)+x)"

or

lemma "- (x * (i + (1::int))) + x = - (x * i)"

I was looking for a distribution rule for mult. and add. to try to simplify these lemmas but I was not able to locate something appropriate.

Any help is appreciated.

TIA

George





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