Discussion:
Omar Jasim
2016-07-19 14:15:18 UTC
Raw Message
Dear all,

equation the discriminant will be nonpositive. I found a proposition in a
text book bellow :

but for this one, the equality hold iff x=-b/2*a and I don't want to put
this as an assumption as I need this lemma in another work. the lemma I'm
trying is:

lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. a*x^2 + b*x + c≥0 "
shows " discrim a b c ≤0"

I proved that for strictly positive equation as bellow:

lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. (a*(x)^2 + b*x + c) >0 "
shows " discrim a b c ≤0"
using assms by (metis discriminant_pos_ex less_le not_less)

but for nonnegative equation (the first lemma) I couldn't and way. please
could any one help me in this because I spend alot of time trying to prove
it but unfortunately I failed.

Omar
Wenda Li
2016-07-19 16:20:19 UTC
Raw Message
Dear Omar,

Here you are,

lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. a*x^2 + b*x + c≥0 "
shows "discrim a b c ≤0"
proof -
have "∃x. a*x^2 + b*x + c<0 " when "discrim a b c > 0" "a>0"
proof -
let ?P="λx. a*x^2 + b*x +c"
have "?P (- b / (2*a)) = (4*a*c-b^2)/(4*a)" using ‹a>0›
by algebra
also have "... <0"
using that unfolding discrim_def by (simp add: divide_neg_pos)
finally show ?thesis by blast
qed
then show ?thesis using assms
using not_less by blast
qed

Best,
Wenda
Post by Omar Jasim
Dear all,
equation the discriminant will be nonpositive. I found a proposition in a
but for this one, the equality hold iff x=-b/2*a and I don't want to put
this as an assumption as I need this lemma in another work. the lemma I'm
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. a*x^2 + b*x + c≥0 "
shows " discrim a b c ≤0"
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. (a*(x)^2 + b*x + c) >0 "
shows " discrim a b c ≤0"
using assms by (metis discriminant_pos_ex less_le not_less)
but for nonnegative equation (the first lemma) I couldn't and way. please
could any one help me in this because I spend alot of time trying to prove
it but unfortunately I failed.
Omar
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge
Omar Jasim
2016-07-19 16:30:59 UTC
Raw Message
Dear Wenda,

now I see where I was stuck. Thank you very much for that, it's really

Cheers.

Omar
Post by Wenda Li
Dear Omar,
Here you are,
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. a*x^2 + b*x + c≥0 "
shows "discrim a b c ≤0"
proof -
have "∃x. a*x^2 + b*x + c<0 " when "discrim a b c > 0" "a>0"
proof -
let ?P="λx. a*x^2 + b*x +c"
have "?P (- b / (2*a)) = (4*a*c-b^2)/(4*a)" using ‹a>0›
by algebra
also have "... <0"
using that unfolding discrim_def by (simp add: divide_neg_pos)
finally show ?thesis by blast
qed
then show ?thesis using assms
using not_less by blast
qed
Best,
Wenda
Post by Omar Jasim
Dear all,
equation the discriminant will be nonpositive. I found a proposition in a
but for this one, the equality hold iff x=-b/2*a and I don't want to put
this as an assumption as I need this lemma in another work. the lemma I'm
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. a*x^2 + b*x + c≥0 "
shows " discrim a b c ≤0"
lemma
fixes a b c x :: real
assumes "a > 0"
and "⋀x. (a*(x)^2 + b*x + c) >0 "
shows " discrim a b c ≤0"
using assms by (metis discriminant_pos_ex less_le not_less)
but for nonnegative equation (the first lemma) I couldn't and way. please
could any one help me in this because I spend alot of time trying to prove
it but unfortunately I failed.
Omar
--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge