[isabelle-dev] simplifier and subgoaler not transitive
christian.urban at kcl.ac.uk
Thu May 24 08:29:38 CEST 2012
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
> 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
> 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.
More information about the isabelle-dev