Re: [isabelle] using and simp add:



In many cases, these forms are equivalent, but there are subtle differences.

> show "lemma" using fact1 and fact 2 by simp

"using" adds facts locally. Some methods treat local facts specially,
others don't. "simp" just inserts them as premises to the goal:

  P_fact1 ==> P_fact2 ==> lemma

Because of the way polymorphism works in Isabelle/Pure, this means the
facts you specified can only be used monomorphically. Also, because the
simplifier simplifies premises, your facts are subject to simplification
themselves.

> show "lemma" by (simp add: fact1 fact2)

This adds facts to the simpset. That means the simplifier may rewrite
occurrences of the left-hand sides of your facts in your lemma.

Cheers
Lars




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