*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Conjunctions commutative in function arguments?*From*: Viktor Kuncak <vkuncak at MIT.EDU>*Date*: Thu, 02 Mar 2006 16:14:11 -0500*Cc*: "Karen K. Zee" <kkz at mit.edu>*In-reply-to*: <20060302203704.689BC2C8D@atbroy30>*References*: <16530916C2FEF64EBE4C333390E3BEFC04FB5DF8@beta.ad.stetson.edu> <20060302203704.689BC2C8D@atbroy30>*User-agent*: Debian Thunderbird 1.0.7 (X11/20051017)

Speaking of equality, what is a robust way to prove combinations of linear arithmetic and uninterpreted function symbols? For example, we would like to prove this simple lemma: (g (j - (2::int)) :: int) = g ((-2::int) + j) Thanks, Viktor and Karen nipkow at in.tum.de wrote: > lemma conj_commute: "P & Q ==> Q & P" by auto > > is not a very useful lemma in your context. It is just not true that "A ==> > B" implies "f A ==> f B", sorry. If you replace "==>" by "=" it becomes > true. Hence the popularity of "=", one of the greatest inventions of > mathematics. > > Tobias >

**Follow-Ups**:**Re: [isabelle] Conjunctions commutative in function arguments?***From:*Tjark Weber

**Re: [isabelle] Conjunctions commutative in function arguments?***From:*Brian Huffman

**References**:**Re: [isabelle] Conjunctions commutative in function arguments?***From:*Robert Lamar

**Re: [isabelle] Conjunctions commutative in function arguments?***From:*nipkow

- Previous by Date: Re: [isabelle] Conjunctions commutative in function arguments?
- Next by Date: Re: [isabelle] Conjunctions commutative in function arguments?
- Previous by Thread: Re: [isabelle] Conjunctions commutative in function arguments?
- Next by Thread: Re: [isabelle] Conjunctions commutative in function arguments?
- Cl-isabelle-users March 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