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



Dear Chris,

For an example, see
https://github.com/nomeata/cis670-16fa/blob/926a15752522836620dde10076132879aa83b2a3/isa/Ch4.thy#L366-L382
(this file has no dependencies outside of HOL and HOL/Library)

In essence, I want to replace

    apply(induction "[x \<leadsto> u] e" arbitrary: x e rule: lc.induct)
    apply(auto elim!: subst.elims[OF sym])
    apply(lc_let_with_find_fresh; auto)
    done

with "by (induction ...) (auto ...)".

Quite possible that simprocs are the way to go, although judging from
the name, they are not: 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
anywhere.

Greetings,
Joachim

Am Freitag, den 02.09.2016, 12:51 +0200 schrieb Christian Sternagel:
> 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)?
> 
> cheers
> 
> chris
> 
> 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
> > http://stackoverflow.com/q/39280314/946226
> > (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
> > 
> > 
> 
> 
-- 
Joachim Breitner
Post-Doctoral researcher
http://cis.upenn.edu/~joachim

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



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