# Re: [isabelle-dev] simplifier and subgoaler not transitive

```
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
```