(* 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\<^sup>2 - 4 * a * c"
lemma complete_square:
"a \ 0 \ a * x\<^sup>2 + b * x + c = 0 \ (2 * a * x + b)\<^sup>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\<^sup>2 + b * x + c \ 0"
proof -
have "(2 * a * x + b)\<^sup>2 \ 0"
by simp
with ‹discrim a b c < 0
› have "(2 * a * x + b)\<^sup>2 \ discrim a b c"
by arith
with complete_square
and ‹a
≠ 0
› show "a * x\<^sup>2 + b * x + c \ 0"
by simp
qed
lemma plus_or_minus_sqrt:
fixes x y :: real
assumes "y \ 0"
shows "x\<^sup>2 = y \ x = sqrt y \ x = - sqrt y"
proof
assume "x\<^sup>2 = y"
then have "sqrt (x\<^sup>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\<^sup>2 = (sqrt y)\<^sup>2 \ x\<^sup>2 = (- sqrt y)\<^sup>2"
by auto
with ‹y
≥ 0
› show "x\<^sup>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\<^sup>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\<^sup>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\<^sup>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\<^sup>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\<^sup>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\<^sup>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\<^sup>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\<^sup>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\<^sup>2 + b * x + c = 0 \ a * y\<^sup>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\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>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\<^sup>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\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
by blast
show "\y. x \ y \ a * y\<^sup>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
