[isabelle-dev] simplifier and subgoaler not transitive

[Christian Urban]

On Thursday, May 24, 2012 at 12:14:14 (+1000), Thomas Sewell wrote:
 > It looks like you want to implement a simproc.

Thanks a lot for the suggestion. My first "iteration"
was implemented via a solver. It worked. But then,
inspired by the neq-simproc in HOL.thy, I already 
modified my code to be a simproc. This seems the slightly
better solution.

 http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/nominal2/rev/8f51702e1f2e

 > Then you have to write some code to actually declare and prove the 
 > equality (e.g. with Goal.prove_internal). This may be as simple as 
 > resolving with "atom a # b ==> a = b == False" if necessary and then 
 > simplifying with "atom v # (x, y) = (atom v # x & atom v # y)".

That is roughly what I did.

 > I've never tried adjusting the solver/subgoaler.
 
It is not too complicated - you have to essentially 
write a tactic that will be tried during simplification. 
I am not sure what the overhead is for having a
custom solver. I did not notice any slowdown with my test 
repository using either version. But I guess the
simproc is called only in cases where it possibly
can apply.

 > If you implement the simproc as suggested above though, simp traces will 
 > become very confusing. They'll be interrupted at depth 3 where the 
 > simproc is called by a subtrace starting from depth 0 which describes 
 > the (uninteresting) inner proof. This is particularly annoying if you 
 > set a low tracing depth limit. There is a fix for this (which will put 
 > the subtrace at depth 4), possibly involving Simplifer.inherit_context. 
 
Thanks for the information. Since the simproc-pattern
is rather "specific", it is usually predictable what
should happen. And as usual inserting "val _ = tracing ..." 
judiciously helps. ;o) So I had no need yet to look again 
at the simplifier trace.

Best wishes and thanks again for all the helpful information.

Christian