Email Gateway (Aug 18 2022 at 17:09): Email Gateway (Aug 18 2022 at 17:09):From: Christian Urban <urbanc@in.tum.de>
Dear Jeremy,
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,
Christian
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
which?Best regards,
Jeremy--
Jeremy Siek <jeremy.siek@colorado.edu>
http://ecee.colorado.edu/~siek/
Assistant Professor
Dept. of Electrical, Computer, and Energy Engineering
University of Colorado at Boulder
Last updated: Apr 27 2024 at 01:05 UTC