*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Conjunctions commutative in function arguments?*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Fri, 3 Mar 2006 13:52:40 -0800*Cc*: "Karen K. Zee" <kkz at mit.edu>*In-reply-to*: <44076023.2000403@mit.edu>*References*: <16530916C2FEF64EBE4C333390E3BEFC04FB5DF8@beta.ad.stetson.edu> <20060302203704.689BC2C8D@atbroy30> <44076023.2000403@mit.edu>*User-agent*: KMail/1.8

On Thursday 02 March 2006 13:14, Viktor Kuncak wrote: > 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 One possibility is to use a set of rewrite rules that put expressions involving plus and minus into a canonical form. Here is a possible set of rules: lemmas linear_rews = add_assoc add_commute diff_def minus_add_distrib minus_minus minus_zero Using (simp add: linear_rews) will convert subtraction into addition and negation, push negation inward as far as possible, and sort all of the added terms according to the standard term ordering. With your example lemma, the result is that both sides become syntactically equal, so you don't need to apply any separate congruence rules. - Brian

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

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

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

- Previous by Date: Re: [isabelle] Conjunctions commutative in function arguments?
- Next by Date: [isabelle] LPAR 2006, 2nd Call For Papers
- Previous by Thread: Re: [isabelle] Conjunctions commutative in function arguments?
- Next by Thread: [isabelle] Automated Reasoning Workshop: Early Registration Deadline
- 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