It looks like you want to implement a simproc.

`These procedures operate on a family of term patterns and generate`

`meta-equalities which the simplifier then applies. In this case I think`

`you want to produce rewrites of the form "a = b == False" and "atom v #`

`t == True". These rewrites can then be applied anywhere in your term,`

`not just the conclusion.`

`Note that the simproc code, which is passed to Simplifier.simproc, takes`

`the current simpset as an argument. Simplifier.prems_of_ss then tells`

`you which local assumptions you have to work with. You can hopefully`

`come up with some efficient check for whether you will be able to derive`

`the needed rewrite from what you have available.`

`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)".`

I've never tried adjusting the solver/subgoaler.

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

`Another workaround might be to put "atom v # (x, y) = (atom v # x & atom`

`v # y)" in dest and intro form and just use the classical solver.`

Yours, Thomas. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev