Re: [isabelle] a simplifier question



On 05.06.2015 00:40, noam neer wrote:
>     lemma
>         fixes   a b c::real
>         assumes "a>0" "b>0" "c>0"
>         shows   "a+b+c > 0"
>     using [[simp_trace=true]]
>     using assms
>     apply (simp)

If the simplifier cannot rewrite anything in the goal anymore, it tries
to solve the goal by some decision procedure for arithmetic (the
"linarith" method, if I remember correctly). This method picks up all
the arithmetic facts from the goal ...

>     lemma
>         fixes   a b c::real
>         assumes "a>0" "b>0" "c>0"
>         shows   "a+b+c > 0"
>     using [[simp_trace=true]]
>     apply (simp add:assms)

but it does not look for lemmas in the simpset.

  -- Lars




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