*To*: George Karabotsos <g_karab at cs.concordia.ca>*Subject*: Re: [isabelle] Proofs involving Integers*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Mon, 05 May 2008 18:53:24 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <481B20F3.6040202@cs.concordia.ca>*References*: <481B20F3.6040202@cs.concordia.ca>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 1.5.0.8 (Macintosh/20061025)

Hi,

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 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] Post-doc position (Paris and Orsay) Trustworthy Decision Procedures
- Next by Date: [isabelle] Option case and pairs with the function package
- Previous by Thread: Re: [isabelle] Proofs involving Integers
- Next by Thread: [isabelle] TPHOLs 2008
- 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