Re: [isabelle] difference between "using" versus auto simp:

Thanks all for the explanations on this!

On Wed, Feb 2, 2011 at 3:30 AM, Makarius <makarius at> wrote:

> On Wed, 2 Feb 2011, Christian Urban wrote:
>  If you use "using", then Isar will add the lemma to the context, but will
>> fix the type variables in the theorem. That usually makes the lemma useless.
> More precisely, Isar does nothing more than adding the facts to the "using"
> slot of the proof state.  It is then up to the subsequent proof method to
> make sense of it.  For semi-automated methods like simp, auto, blast etc.
> this means to insert the facts into the goal state and proceed as usual.
>  This effectively means that type variables cannot be instantiated under
> most circumstances.
> It is one of the many pitfalls of implicit polymorphism (or the lack
> thereof) in certain situations.
>        Makarius

Jeremy Siek <jeremy.siek at>
Assistant Professor
Dept. of Electrical, Computer, and Energy Engineering
University of Colorado at Boulder

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