[isabelle] difference between "using" versus auto simp:
There is indeed a difference when your lemmas have
polymorphic type. 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. On the other hand, if you add the lemma
via "simp" or "auto simp" then the lemma is under the
control, so to say, of the automatic tool, which will
find the right type-instantiation of the lemma.
Because of Isabelle's limited type-language the problem
with fixing type-variables cannot easily be circumvented,
if at all. I also stumbled over this problem recently.
So the rule of thumb is, do not use "using" with
lemmas having polymorphic type. For consistency,
"using" should perhaps only be used with local facts,
not with lemmas at all. But I am also guilty of violating
this rule all the time.
Hope this helps,
Jeremy Siek writes:
> I've noticed that on a few occasions, referencing a lemma with
> a "using" followed by auto didn't work, whereas adding the
> lemma to the simp set via "auto simp:" did work.
> Are there some general rules of thumb regarding when to use
> Best regards,
> Jeremy Siek <jeremy.siek at colorado.edu>
> 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