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



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





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