*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] simp matching depends on lexicographic variable naming*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 13 Feb 2013 01:36:43 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <511A974F.20302@in.tum.de>*References*: <511A8E7C.4040702@gmx.com> <511A974F.20302@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 2/12/2013 1:26 PM, Tobias Nipkow wrote:

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.

Tobias,

Thanks again, GB

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

**Attachment:
Gnarly_nested_set_ordered.png**

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

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

**Re: [isabelle] simp matching depends on lexicographic variable naming***From:*Tobias Nipkow

- Previous by Date: [isabelle] ACL2 2013 - Last Call For Papers - Extended Deadline
- Next by Date: Re: [isabelle] simp matching depends on lexicographic variable naming
- Previous by Thread: Re: [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