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



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