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

Originally from the AFP entry Tarskis_Geometry
*)

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"

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"
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 * x⇧2 + b * x + c ≠ 0"
by simp
qed

lemma plus_or_minus_sqrt:
fixes x y :: real
assumes "y ≥ 0"
shows "x⇧2 = y ⟷ x = sqrt y ∨ x = - sqrt y"
proof
assume "x⇧2 = y"
then have "sqrt (x⇧2) = 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 "x⇧2 = (sqrt y)⇧2 ∨ x⇧2 = (- sqrt y)⇧2"
by auto
with ‹y ≥ 0› show "x⇧2 = 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 * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + b * x + c = 0 ⟷ x = -b / (2 * a)"

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))"
proof
assume "a * x⇧2 + 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 * x⇧2 + 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 * x⇧2 + 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 * 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"
proof -
from discriminant_pos_ex and ‹a ≠ 0› and ‹discrim a b c > 0›
obtain w and z where "w ≠ z"
and "a * w⇧2 + b * w + c = 0" and "a * z⇧2 + b * z + c = 0"
by blast
show "∃y. x ≠ y ∧ a * y⇧2 + b * y + c = 0"
proof (cases "x = w")
case True
with ‹w ≠ z› have "x ≠ z"
by simp
with ‹a * z⇧2 + b * z + c = 0› show ?thesis
by auto
next
case False
with ‹a * w⇧2 + 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
```