# Re: [isabelle] simp matching depends on lexicographic variable naming

```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 for the help. That opened up lots more possibilities that hadn't even occurred to me, and that I was neglecting.
```
```
I implemented about two forms each of the associativity and left-commutativity rules, like it said to do in the book, and then some other rules. I wouldn't even have thought about the left-commutative rule.
```
```
The rewriting seems to put priority on the associativity and commutativity rules; I put a rule before them that simplified things, but then it wasn't used for a simple test case, and the other rules expanded something I tried to eliminate.
```
```
It all works out though, for now. I got finite sets with no repetitions and equality in about 8 hours instead of two months or never. I thought I would have to dig through Sets.thy to figure all that out.
```
```
When I do a command "apply simp", is there a command to tell me what rules it applied for that command? All I know about is "print_simpset". A great debugger tool would be able to single step through the simp rules for an "apply simp".
```
```
I attach a screenshot at 22Kbytes of a big, gnarly, nested set equality with repetitions that's proved by simp.
```
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
Description: PNG image

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.