# [isabelle] simp matching depends on lexicographic variable naming

```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

```
```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 "{{c,d},{e,e}} = z"
apply simp
--"Output: {{e}, {a, d}} = z"
oops
end
```

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