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



On 2/13/2013 3:21 AM, Tobias Nipkow wrote:
Such a tool is in the making. For the time being you can prefix your "apply simp" by "using [[simp_trace]]". This gives you a very detailed trace, probably much more than what you want.

No, "using [[simp_trace]]" works perfect for simple test cases. Using a fancy debugger wouldn't be any easier. Figuring out where to set the break points for a debugger can be no easy task, not I've used a debugger much, or any, because it's easier to just print to screen, and then prompt the user, than learn how to use a debugger.

So reducing a formula down more and more can serve the purpose of single stepping or setting break points.

But, I was wanting to confirm whether this sentence, page 178,

   "Permutative rewrite rules can be turned into simplication rules in
   the usual manner via the simp attribute; the simplifer recognizes
   their special status automatically."

means it does the permutative rewrite rules first, and it does mean that. The commutative and left-commutative rules end up doing together what I had as one rule.

Regards,
GB





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