[isabelle-dev] simplifier and subgoaler not transitive

[Thomas Sewell]

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.