*To*: Wenda Li <wl302 at cam.ac.uk>*Subject*: Re: [isabelle] nonnegative quadratic polynomial*From*: Omar Jasim <oajasim1 at sheffield.ac.uk>*Date*: Tue, 19 Jul 2016 17:25:08 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <e1c06e7cca532cebebc8cd9b5e00537e@cam.ac.uk>*References*: <CAAi=gevZ3jPsJSteprcnmdasPL57jYyky1pw+0gp1v3Zj42y5Q@mail.gmail.com> <e1c06e7cca532cebebc8cd9b5e00537e@cam.ac.uk>

Dear Wenda, now I see where I was stuck. Thank you very much for that, it's really helpful. Cheers. Omar On 19 July 2016 at 17:14, Wenda Li <wl302 at cam.ac.uk> wrote: > 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â > apply (auto simp add:field_simps) > 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 > > > On 2016-07-19 15:10, Omar Jasim wrote: > >> Dear all, >> >> >> Please I need to prove that for any nonnegative quadratic polynomial >> equation the discriminant will be nonpositive. I found a proposition in a >> text book bellow : >> >> https://books.google.co.uk/books?id=TPE0fXGnYtMC&pg=PA81&lpg=PA81&dq=if+f(x)+%3E0+then+b%5E2-4ac%3C0&source=bl&ots=eUAdjNvJpT&sig=KwJxcX_5RqIsCL4wJ3nrfvfZe9g&hl=en&sa=X&ved=0ahUKEwjlxpjm2ZjNAhWMLsAKHX2vAs8Q6AEILzAE#v=onepage&q&f=false >> >> 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 > PhD Candidate > Computer Laboratory > University of Cambridge >

**References**:**[isabelle] nonnegative quadratic polynomial***From:*Omar Jasim

**Re: [isabelle] nonnegative quadratic polynomial***From:*Wenda Li

- Previous by Date: Re: [isabelle] nonnegative quadratic polynomial
- Next by Date: [isabelle] Report from our Isabelle course
- Previous by Thread: Re: [isabelle] nonnegative quadratic polynomial
- Next by Thread: [isabelle] Report from our Isabelle course
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list