Quelle Quadratic_Discriminant.thy Sprache: Isabelle

(*  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 \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c"
    by arith
  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 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 \<open>y \<ge> 0\<close> 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 \<open>x \<noteq> 0\<close> that by (simp add: field_simps)
  show "x * y = z" if "y = z / x"
    using \<open>x \<noteq> 0\<close> 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) \<or>
    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) \<or>
    (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 \<open>a \<noteq> 0\<close> 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) \<or>
    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 \<ge> 0 \<and>
    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
     x = (-b - sqrt (discrim a b c)) / (2 * a))"
proof
  assume "a * x\<^sup>2 + b * x + c = 0"
  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)"
    by auto
  then have "discrim a b c \ 0"
    by simp
  with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
  have "x = (-b + sqrt (discrim a b c)) / (2 * a) \
      x = (-b - sqrt (discrim a b c)) / (2 * a)"
    by simp
  with \<open>discrim a b c \<ge> 0\<close>
  show "discrim a b c \ 0 \
    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
     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) \<or>
     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 \<open>a \<noteq> 0\<close> 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 \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0"
    by simp
  then have "sqrt (discrim a b c) \ - sqrt (discrim a b c)"
    by arith
  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?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 \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
  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 \<open>w \<noteq> z\<close> have "x \<noteq> z"
      by simp
    with \<open>a * z\<^sup>2 + b * z + c = 0\<close> show ?thesis
      by auto
  next
    case False
    with \<open>a * w\<^sup>2 + b * w + c = 0\<close> 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 \<open>a \<in> \<rat>\<close> \<open>b \<in> \<rat>\<close> \<open>x \<in> \<rat>\<close> by (simp)
qed

end

quality98%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.