Theory HOL-Library.Quadratic_Discriminant

(*  Title:       HOL/Library/Quadratic_Discriminant.thy
    Author:      Tim Makarios <tjm1983 at gmail.com>, 2012

Originally from the AFP entry Tarskis_Geometry
*)

section "Roots of real quadratics"

theory Quadratic_Discriminant
imports Complex_Main
begin

definition discrim :: "real  real  real  real"
  where "discrim a b c  b2 - 4 * a * c"

lemma complete_square:
  "a  0  a * x2 + b * x + c = 0  (2 * a * x + b)2 = discrim a b c"
by (simp add: discrim_def) algebra

lemma discriminant_negative:
  fixes a b c x :: real
  assumes "a  0"
    and "discrim a b c < 0"
  shows "a * x2 + b * x + c  0"
proof -
  have "(2 * a * x + b)2  0"
    by simp
  with discrim a b c < 0 have "(2 * a * x + b)2  discrim a b c"
    by arith
  with complete_square and a  0 show "a * x2 + b * x + c  0"
    by simp
qed

lemma plus_or_minus_sqrt:
  fixes x y :: real
  assumes "y  0"
  shows "x2 = y  x = sqrt y  x = - sqrt y"
proof
  assume "x2 = y"
  then have "sqrt (x2) = sqrt y"
    by simp
  then have "sqrt y = ¦x¦"
    by simp
  then show "x = sqrt y  x = - sqrt y"
    by auto
next
  assume "x = sqrt y  x = - sqrt y"
  then have "x2 = (sqrt y)2  x2 = (- sqrt y)2"
    by auto
  with y  0 show "x2 = y"
    by simp
qed

lemma divide_non_zero:
  fixes x y z :: real
  assumes "x  0"
  shows "x * y = z  y = z / x"
proof
  show "y = z / x" if "x * y = z"
    using x  0 that by (simp add: field_simps)
  show "x * y = z" if "y = z / x"
    using x  0 that by simp
qed

lemma discriminant_nonneg:
  fixes a b c x :: real
  assumes "a  0"
    and "discrim a b c  0"
  shows "a * x2 + b * x + c = 0 
    x = (-b + sqrt (discrim a b c)) / (2 * a) 
    x = (-b - sqrt (discrim a b c)) / (2 * a)"
proof -
  from complete_square and plus_or_minus_sqrt and assms
  have "a * x2 + b * x + c = 0 
    (2 * a) * x + b = sqrt (discrim a b c) 
    (2 * a) * x + b = - sqrt (discrim a b c)"
    by simp
  also have "  (2 * a) * x = (-b + sqrt (discrim a b c)) 
    (2 * a) * x = (-b - sqrt (discrim a b c))"
    by auto
  also from a  0 and divide_non_zero [of "2 * a" x]
  have "  x = (-b + sqrt (discrim a b c)) / (2 * a) 
    x = (-b - sqrt (discrim a b c)) / (2 * a)"
    by simp
  finally show "a * x2 + b * x + c = 0 
    x = (-b + sqrt (discrim a b c)) / (2 * a) 
    x = (-b - sqrt (discrim a b c)) / (2 * a)" .
qed

lemma discriminant_zero:
  fixes a b c x :: real
  assumes "a  0"
    and "discrim a b c = 0"
  shows "a * x2 + b * x + c = 0  x = -b / (2 * a)"
  by (simp add: discriminant_nonneg assms)

theorem discriminant_iff:
  fixes a b c x :: real
  assumes "a  0"
  shows "a * x2 + b * x + c = 0 
    discrim a b c  0 
    (x = (-b + sqrt (discrim a b c)) / (2 * a) 
     x = (-b - sqrt (discrim a b c)) / (2 * a))"
proof
  assume "a * x2 + b * x + c = 0"
  with discriminant_negative and a  0 have "¬(discrim a b c < 0)"
    by auto
  then have "discrim a b c  0"
    by simp
  with discriminant_nonneg and a * x2 + b * x + c = 0 and a  0
  have "x = (-b + sqrt (discrim a b c)) / (2 * a) 
      x = (-b - sqrt (discrim a b c)) / (2 * a)"
    by simp
  with discrim a b c  0
  show "discrim a b c  0 
    (x = (-b + sqrt (discrim a b c)) / (2 * a) 
     x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
next
  assume "discrim a b c  0 
    (x = (-b + sqrt (discrim a b c)) / (2 * a) 
     x = (-b - sqrt (discrim a b c)) / (2 * a))"
  then have "discrim a b c  0" and
    "x = (-b + sqrt (discrim a b c)) / (2 * a) 
     x = (-b - sqrt (discrim a b c)) / (2 * a)"
    by simp_all
  with discriminant_nonneg and a  0 show "a * x2 + b * x + c = 0"
    by simp
qed

lemma discriminant_nonneg_ex:
  fixes a b c :: real
  assumes "a  0"
    and "discrim a b c  0"
  shows " x. a * x2 + b * x + c = 0"
  by (auto simp: discriminant_nonneg assms)

lemma discriminant_pos_ex:
  fixes a b c :: real
  assumes "a  0"
    and "discrim a b c > 0"
  shows "x y. x  y  a * x2 + b * x + c = 0  a * y2 + b * y + c = 0"
proof -
  let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
  let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
  from discrim a b c > 0 have "sqrt (discrim a b c)  0"
    by simp
  then have "sqrt (discrim a b c)  - sqrt (discrim a b c)"
    by arith
  with a  0 have "?x  ?y"
    by simp
  moreover from assms have "a * ?x2 + b * ?x + c = 0" and "a * ?y2 + b * ?y + c = 0"
    using discriminant_nonneg [of a b c ?x]
      and discriminant_nonneg [of a b c ?y]
    by simp_all
  ultimately show ?thesis
    by blast
qed

lemma discriminant_pos_distinct:
  fixes a b c x :: real
  assumes "a  0"
    and "discrim a b c > 0"
  shows " y. x  y  a * y2 + b * y + c = 0"
proof -
  from discriminant_pos_ex and a  0 and discrim a b c > 0
  obtain w and z where "w  z"
    and "a * w2 + b * w + c = 0" and "a * z2 + b * z + c = 0"
    by blast
  show "y. x  y  a * y2 + b * y + c = 0"
  proof (cases "x = w")
    case True
    with w  z have "x  z"
      by simp
    with a * z2 + b * z + c = 0 show ?thesis
      by auto
  next
    case False
    with a * w2 + b * w + c = 0 show ?thesis
      by auto
  qed
qed

lemma Rats_solution_QE:
  assumes "a  " "b  " "a  0"
  and "a*x^2 + b*x + c = 0"
  and "sqrt (discrim a b c)  "
  shows "x  " 
using assms(1,2,5) discriminant_iff[THEN iffD1, OF assms(3,4)] by auto

lemma Rats_solution_QE_converse:
  assumes "a  " "b  "
  and "a*x^2 + b*x + c = 0"
  and "x  "
  shows "sqrt (discrim a b c)  "
proof -
  from assms(3) have "discrim a b c = (2*a*x+b)^2" unfolding discrim_def by algebra
  hence "sqrt (discrim a b c) = ¦2*a*x+b¦" by (simp)
  thus ?thesis using a   b   x   by (simp)
qed

end