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 ≡ b⇧2 - 4 * a * c"

lemma complete_square:
  "a ≠ 0 ⟹ a * x⇧2 + 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 * x⇧2 + b * x + c ≠ 0"
  by (metis assms complete_square power2_less_0) 

lemma plus_or_minus_sqrt:
  fixes x y :: real
  assumes "y ≥ 0"
  shows "x⇧2 = y ⟷ x = sqrt y ∨ x = - sqrt y"
  using assms by fastforce

lemma divide_non_zero:
  fixes x y z :: real
  assumes "x ≠ 0"
  shows "x * y = z ⟷ y = z / x"
  by (simp add: assms mult.commute nonzero_eq_divide_eq)

lemma discriminant_nonneg:
  fixes a b c x :: real
  assumes "a ≠ 0"
    and "discrim a b c ≥ 0"
  shows "a * x⇧2 + b * x + c = 0 ⟷
    x = (-b + sqrt (discrim a b c)) / (2 * a) ∨
    x = (-b - sqrt (discrim a b c)) / (2 * a)"  (is "?L = ?R")
proof
  assume ?L with assms show ?R
    by (smt (verit, ccfv_threshold) complete_square nonzero_mult_div_cancel_left real_sqrt_abs)
qed (use assms complete_square in auto)

lemma discriminant_zero:
  fixes a b c x :: real
  assumes "a ≠ 0"
    and "discrim a b c = 0"
  shows "a * x⇧2 + 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 * x⇧2 + 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))"
  by (smt (verit, best) assms discriminant_negative discriminant_nonneg)

lemma discriminant_nonneg_ex:
  fixes a b c :: real
  assumes "a ≠ 0"
    and "discrim a b c ≥ 0"
  shows "∃ x. a * x⇧2 + 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 * x⇧2 + b * x + c = 0 ∧ a * y⇧2 + 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 * ?x⇧2 + b * ?x + c = 0" and "a * ?y⇧2 + 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 * y⇧2 + b * y + c = 0"
  by (metis assms discriminant_pos_ex) 

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