[isabelle] Telling auto to use an eisbach method

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
(and now there is an Eisbach tag), but I am also wondering:

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?


Joachim Breitner
Post-Doctoral researcher

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.