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



Dear Larry,


Am Freitag, den 02.09.2016, 13:34 +0100 schrieb Lawrence Paulson:
> 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.

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.

Thanks,
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.