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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev