[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.