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



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
> 





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