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.
>
>
>        Makarius
>



-- 
____________________________________
Jeremy Siek <jeremy.siek at colorado.edu>
http://ecee.colorado.edu/~siek/
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.