*To*: George Karabotsos <g_karab at cs.concordia.ca>*Subject*: Re: [isabelle] Proofs involving Integers*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 03 May 2008 17:50:10 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <481B20F3.6040202@cs.concordia.ca>*References*: <481B20F3.6040202@cs.concordia.ca>*User-agent*: Thunderbird 2.0.0.9 (Macintosh/20071031)

Tobias George Karabotsos schrieb:

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 tosimplify these lemmas but I was not able to locate something appropriate.Any help is appreciated. TIA George

**References**:**[isabelle] Proofs involving Integers***From:*George Karabotsos

- Previous by Date: [isabelle] Proofs involving Integers
- Next by Date: [isabelle] TPHOLs 2008
- Previous by Thread: [isabelle] Proofs involving Integers
- Next by Thread: Re: [isabelle] Proofs involving Integers
- Cl-isabelle-users May 2008 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