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.