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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and