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


Am Dienstag, den 01.02.2011, 22:31 -0700 schrieb Jeremy Siek:
> 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?

heh, I’ve observed it the other way around and came up with this
explanation: When it is added via using, the simplifier will actually
simplify the fact and then consider it in its rules, making it more
likely to match. When adding it via "simp add:", the fact might be in a
form that never matches.

For your case, the explanation might be similar in that the fact matches
only in a non-simplified form. But I’m sure the experts can come up with
more explanations.

I cannot provide a general rule though.


Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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