src/HOL/Library/Quadratic_Discriminant.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 68553 333998becebe
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*  Title:       HOL/Library/Quadratic_Discriminant.thy
     2     Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
     3 
     4 Originally from the AFP entry Tarskis_Geometry
     5 *)
     6 
     7 section "Roots of real quadratics"
     8 
     9 theory Quadratic_Discriminant
    10 imports Complex_Main
    11 begin
    12 
    13 definition discrim :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
    14   where "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
    15 
    16 lemma complete_square:
    17   "a \<noteq> 0 \<Longrightarrow> a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
    18 by (simp add: discrim_def) algebra
    19 
    20 lemma discriminant_negative:
    21   fixes a b c x :: real
    22   assumes "a \<noteq> 0"
    23     and "discrim a b c < 0"
    24   shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
    25 proof -
    26   have "(2 * a * x + b)\<^sup>2 \<ge> 0"
    27     by simp
    28   with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c"
    29     by arith
    30   with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0"
    31     by simp
    32 qed
    33 
    34 lemma plus_or_minus_sqrt:
    35   fixes x y :: real
    36   assumes "y \<ge> 0"
    37   shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
    38 proof
    39   assume "x\<^sup>2 = y"
    40   then have "sqrt (x\<^sup>2) = sqrt y"
    41     by simp
    42   then have "sqrt y = \<bar>x\<bar>"
    43     by simp
    44   then show "x = sqrt y \<or> x = - sqrt y"
    45     by auto
    46 next
    47   assume "x = sqrt y \<or> x = - sqrt y"
    48   then have "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2"
    49     by auto
    50   with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y"
    51     by simp
    52 qed
    53 
    54 lemma divide_non_zero:
    55   fixes x y z :: real
    56   assumes "x \<noteq> 0"
    57   shows "x * y = z \<longleftrightarrow> y = z / x"
    58 proof
    59   show "y = z / x" if "x * y = z"
    60     using \<open>x \<noteq> 0\<close> that by (simp add: field_simps)
    61   show "x * y = z" if "y = z / x"
    62     using \<open>x \<noteq> 0\<close> that by simp
    63 qed
    64 
    65 lemma discriminant_nonneg:
    66   fixes a b c x :: real
    67   assumes "a \<noteq> 0"
    68     and "discrim a b c \<ge> 0"
    69   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    70     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    71     x = (-b - sqrt (discrim a b c)) / (2 * a)"
    72 proof -
    73   from complete_square and plus_or_minus_sqrt and assms
    74   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    75     (2 * a) * x + b = sqrt (discrim a b c) \<or>
    76     (2 * a) * x + b = - sqrt (discrim a b c)"
    77     by simp
    78   also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
    79     (2 * a) * x = (-b - sqrt (discrim a b c))"
    80     by auto
    81   also from \<open>a \<noteq> 0\<close> and divide_non_zero [of "2 * a" x]
    82   have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    83     x = (-b - sqrt (discrim a b c)) / (2 * a)"
    84     by simp
    85   finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    86     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    87     x = (-b - sqrt (discrim a b c)) / (2 * a)" .
    88 qed
    89 
    90 lemma discriminant_zero:
    91   fixes a b c x :: real
    92   assumes "a \<noteq> 0"
    93     and "discrim a b c = 0"
    94   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
    95   by (simp add: discriminant_nonneg assms)
    96 
    97 theorem discriminant_iff:
    98   fixes a b c x :: real
    99   assumes "a \<noteq> 0"
   100   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
   101     discrim a b c \<ge> 0 \<and>
   102     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   103      x = (-b - sqrt (discrim a b c)) / (2 * a))"
   104 proof
   105   assume "a * x\<^sup>2 + b * x + c = 0"
   106   with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)"
   107     by auto
   108   then have "discrim a b c \<ge> 0"
   109     by simp
   110   with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
   111   have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   112       x = (-b - sqrt (discrim a b c)) / (2 * a)"
   113     by simp
   114   with \<open>discrim a b c \<ge> 0\<close>
   115   show "discrim a b c \<ge> 0 \<and>
   116     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   117      x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
   118 next
   119   assume "discrim a b c \<ge> 0 \<and>
   120     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   121      x = (-b - sqrt (discrim a b c)) / (2 * a))"
   122   then have "discrim a b c \<ge> 0" and
   123     "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   124      x = (-b - sqrt (discrim a b c)) / (2 * a)"
   125     by simp_all
   126   with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0"
   127     by simp
   128 qed
   129 
   130 lemma discriminant_nonneg_ex:
   131   fixes a b c :: real
   132   assumes "a \<noteq> 0"
   133     and "discrim a b c \<ge> 0"
   134   shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
   135   by (auto simp: discriminant_nonneg assms)
   136 
   137 lemma discriminant_pos_ex:
   138   fixes a b c :: real
   139   assumes "a \<noteq> 0"
   140     and "discrim a b c > 0"
   141   shows "\<exists>x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0"
   142 proof -
   143   let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
   144   let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
   145   from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0"
   146     by simp
   147   then have "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)"
   148     by arith
   149   with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y"
   150     by simp
   151   moreover from assms have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0"
   152     using discriminant_nonneg [of a b c ?x]
   153       and discriminant_nonneg [of a b c ?y]
   154     by simp_all
   155   ultimately show ?thesis
   156     by blast
   157 qed
   158 
   159 lemma discriminant_pos_distinct:
   160   fixes a b c x :: real
   161   assumes "a \<noteq> 0"
   162     and "discrim a b c > 0"
   163   shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
   164 proof -
   165   from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
   166   obtain w and z where "w \<noteq> z"
   167     and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
   168     by blast
   169   show "\<exists>y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
   170   proof (cases "x = w")
   171     case True
   172     with \<open>w \<noteq> z\<close> have "x \<noteq> z"
   173       by simp
   174     with \<open>a * z\<^sup>2 + b * z + c = 0\<close> show ?thesis
   175       by auto
   176   next
   177     case False
   178     with \<open>a * w\<^sup>2 + b * w + c = 0\<close> show ?thesis
   179       by auto
   180   qed
   181 qed
   182 
   183 lemma Rats_solution_QE:
   184   assumes "a \<in> \<rat>" "b \<in> \<rat>" "a \<noteq> 0"
   185   and "a*x^2 + b*x + c = 0"
   186   and "sqrt (discrim a b c) \<in> \<rat>"
   187   shows "x \<in> \<rat>" 
   188 using assms(1,2,5) discriminant_iff[THEN iffD1, OF assms(3,4)] by auto
   189 
   190 lemma Rats_solution_QE_converse:
   191   assumes "a \<in> \<rat>" "b \<in> \<rat>"
   192   and "a*x^2 + b*x + c = 0"
   193   and "x \<in> \<rat>"
   194   shows "sqrt (discrim a b c) \<in> \<rat>"
   195 proof -
   196   from assms(3) have "discrim a b c = (2*a*x+b)^2" unfolding discrim_def by algebra
   197   hence "sqrt (discrim a b c) = \<bar>2*a*x+b\<bar>" by (simp)
   198   thus ?thesis using \<open>a \<in> \<rat>\<close> \<open>b \<in> \<rat>\<close> \<open>x \<in> \<rat>\<close> by (simp)
   199 qed
   200 
   201 end