[isabelle-dev] simplifier and subgoaler not transitive
Thomas.Sewell at nicta.com.au
Thu May 24 04:14:14 CEST 2012
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.
More information about the isabelle-dev