(* 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" 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)" 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))" 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