[isabelle] Telling auto to use an eisbach method
(too old to reply)
Christian Sternagel
2016-09-02 10:57:34 UTC
Raw Message
Dear Joachim,

I don't know the details of what you are trying to do. Maybe it could be
tackled by a simproc (which basically also says, do something special on
goals of a specific shape)?


Dear list,
I’m current in the process of following a Coq course using Isabelle
(more as a Fingerübung), and there I see some nice use of tactics, such
- If you find a goal of this shape,
- invoke that particular rule
- with an instantiation calculated from the current goal state.
In this case, the instantiation includes a set of names to avoid. I
have posed my question about that part at
How do I best integrate this into an (otherwise) nicely automated proof
using our beloved auto?
Conceptually, to me, the custom method is just a smart version of an
introduction rule. But clearly I cannot just give a method as an
argument to auto’s "intro:".
Is there any other way to tell auto: „When you try introduction rules,
well, also try running this given method?“
If not, should there be such a way?
Lawrence Paulson
2016-09-02 12:38:38 UTC
Raw Message
Could you please be more specific? That sounds pretty much like what auto/force/blast do anyway if you use intro/elim/dest without the (!) modifier.

Larry Paulson
It is not (safe) simplification that I want to
instrument, but rather the part of auto that does proof search, i.e.
undoes a rule application if it turned out that it did not lead
Lawrence Paulson
2016-09-02 14:24:48 UTC
Raw Message
Possibly you could accomplish what you want using a “wrapper”. Unfortunately, they are very obscure. See The Isabelle/Isar Reference Manual, section 9.4.7, Modifying the search step.

Larry Paulson
precisely – but auto (AFAIK) can only invoke _rules_, not _methods_. I
want it to invoke a (custom eisbach-defined) method in this way.
The introduction rule in my example requires picking a “sufficiently
fresh” variable, by specifying a set of variables to avoid. Such an
intro rule does not work well with "auto", as it would leave a
schematic variable around.
But almost always, this set of variables can be calculated from the
context, i.e. the current goal statement. I (more or less) have a
method that does that, and I want auto to try that.