Email Gateway (Aug 22 2022 at 10:31): Email Gateway (Aug 22 2022 at 10:31):From: noam neer <noamneer@gmail.com>
hi.
can someone explain to me why the first proof succeeds, while the second
fails?
I looked into the simplifier trace info but didn't understand too much.
thanx
theory tmp
imports Main Real NthRoot Transcendental
begin
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)
done
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)
done
end
Email Gateway (Aug 22 2022 at 10:31):From: Tobias Nipkow <nipkow@in.tum.de>
Always start with Main or Complex_Main (or other theories that build on them).
Importing individual subtheories on those two theories can lead to funny effects
because important material could be missing.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 10:31):From: Lars Noschinski <noschinl@in.tum.de>
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
Last updated: Apr 26 2024 at 08:19 UTC