Re: [isabelle] using and simp add:



There are also more subtle differences. AFAIK, if your fact is
polymorphic and you add it with "using", it is only applied for one
type. If you add it with "simp add" it can be applied with different
types.

In general I prefer "simp add", as this feels more deterministic. 

 - Johannes


Am Donnerstag, den 10.03.2016, 10:00 +0100 schrieb Lars Hupel:
> 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.