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.


isabelle-dev mailing list

Reply via email to