*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] simp matching depends on lexicographic variable naming*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 12 Feb 2013 20:26:07 +0100*In-reply-to*: <511A8E7C.4040702@gmx.com>*References*: <511A8E7C.4040702@gmx.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130107 Thunderbird/17.0.2

Yes. You have discovered a feature called "ordered rewriting". It is described in the Tutorial "Isabelle/HOL - A Proof Assistant for Higher-Order Logic" in 9.1.1 under Permutative Rewrite Rules. Regards Tobias Am 12/02/2013 19:48, schrieb Gottfried Barrow: > Hi, > > I'm trying to add a simp rule, but it doesn't do any matching unless, for > subsequent theorems, I name my variables in a certain, lexicographic order. > > I set up the syntax and theorem as next shown, where I've converted \<lbrace> > and \<rbrace> to "{" and "}", except in the syntax command. > > syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)") > translations > "\<lbrace>r,s\<rbrace>" == "CONST paS r s" > > theorem lrbrace_notation [simp]: > "{{r,s},{p,p}} = {{p,p},{r,s}}" > sorry > > The simp rule works for the following: > > theorem "{{f,d},{e,e}} = z" > apply simp > --"Output: {{e,e},{f,d}} = z" > oops > > However, if I replace "f" with anything lexicographically less than "f", it > doesn't match, and doesn't simplify the goal, such as for the following: > > theorem "{{a,d},{e,e}} = z" > apply simp > oops > > In the theory, I replace "f" with variables named from "a" to "e", and it > doesn't match, but when I get to "f", it matches. > > I attach theory, and I include it below. > > Thanks, > GB > > > theory simp_pair_singleton_switch_alphabet_dependent > > imports Complex_Main > begin > typedecl sT > consts paS :: "sT => sT => sT" > > syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)") > translations > "\<lbrace>r,s\<rbrace>" == "CONST paS r s" > > theorem lrbrace_notation [simp]: > "\<lbrace>\<lbrace>r,s\<rbrace>,\<lbrace>p,p\<rbrace>\<rbrace> = > \<lbrace>\<lbrace>p,p\<rbrace>,\<lbrace>r,s\<rbrace>\<rbrace>" > sorry > > theorem "\<lbrace>\<lbrace>f,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z" > apply simp > --"Output: \<lbrace>\<lbrace>e,e\<rbrace>,\<lbrace>f,d\<rbrace>\<rbrace> = z" > oops > > theorem "\<lbrace>\<lbrace>a,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z" > apply simp > oops > theorem "\<lbrace>\<lbrace>b,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z" > apply simp > oops > theorem "\<lbrace>\<lbrace>c,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z" > apply simp > oops > theorem "\<lbrace>\<lbrace>d,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z" > apply simp > oops > theorem "\<lbrace>\<lbrace>e,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z" > apply simp > oops > > theorem regular_braces [simp]: > "{{r,s},{p}} = {{p},{r,s}}" > sorry > theorem "{{a,d},{e,e}} = z" > apply simp > --"Output: {{e}, {a, d}} = z" > oops > end >

**Follow-Ups**:**Re: [isabelle] simp matching depends on lexicographic variable naming***From:*Gottfried Barrow

**References**:**[isabelle] simp matching depends on lexicographic variable naming***From:*Gottfried Barrow

- Previous by Date: [isabelle] simp matching depends on lexicographic variable naming
- Next by Date: Re: [isabelle] Sandboxed evaluation of Isabelle theories?
- Previous by Thread: [isabelle] simp matching depends on lexicographic variable naming
- Next by Thread: Re: [isabelle] simp matching depends on lexicographic variable naming
- Cl-isabelle-users February 2013 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