Re: [isabelle] Telling auto to use an eisbach method

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)?



On 09/01/2016 11:17 PM, Joachim Breitner wrote:
> 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
> as:
>  - 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?
> Greetings,
> Joachim

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