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 sketis.net> 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.
Jeremy Siek <jeremy.siek at colorado.edu>
Dept. of Electrical, Computer, and Energy Engineering
University of Colorado at Boulder
This archive was generated by a fusion of
Pipermail (Mailman edition) and