src/HOL/Library/Quadratic_Discriminant.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63465 d7610beb98bc
child 68553 333998becebe
permissions -rw-r--r--
executable domain membership checks
     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   fixes a b c x :: "real"
    18   assumes "a \<noteq> 0"
    19   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
    20 proof -
    21   have "4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 4 * a * (a * x\<^sup>2 + b * x + c)"
    22     by (simp add: algebra_simps power2_eq_square)
    23   with \<open>a \<noteq> 0\<close>
    24   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> 4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 0"
    25     by simp
    26   then show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
    27     by (simp add: discrim_def power2_eq_square algebra_simps)
    28 qed
    29 
    30 lemma discriminant_negative:
    31   fixes a b c x :: real
    32   assumes "a \<noteq> 0"
    33     and "discrim a b c < 0"
    34   shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
    35 proof -
    36   have "(2 * a * x + b)\<^sup>2 \<ge> 0"
    37     by simp
    38   with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c"
    39     by arith
    40   with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0"
    41     by simp
    42 qed
    43 
    44 lemma plus_or_minus_sqrt:
    45   fixes x y :: real
    46   assumes "y \<ge> 0"
    47   shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
    48 proof
    49   assume "x\<^sup>2 = y"
    50   then have "sqrt (x\<^sup>2) = sqrt y"
    51     by simp
    52   then have "sqrt y = \<bar>x\<bar>"
    53     by simp
    54   then show "x = sqrt y \<or> x = - sqrt y"
    55     by auto
    56 next
    57   assume "x = sqrt y \<or> x = - sqrt y"
    58   then have "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2"
    59     by auto
    60   with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y"
    61     by simp
    62 qed
    63 
    64 lemma divide_non_zero:
    65   fixes x y z :: real
    66   assumes "x \<noteq> 0"
    67   shows "x * y = z \<longleftrightarrow> y = z / x"
    68 proof
    69   show "y = z / x" if "x * y = z"
    70     using \<open>x \<noteq> 0\<close> that by (simp add: field_simps)
    71   show "x * y = z" if "y = z / x"
    72     using \<open>x \<noteq> 0\<close> that by simp
    73 qed
    74 
    75 lemma discriminant_nonneg:
    76   fixes a b c x :: real
    77   assumes "a \<noteq> 0"
    78     and "discrim a b c \<ge> 0"
    79   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    80     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    81     x = (-b - sqrt (discrim a b c)) / (2 * a)"
    82 proof -
    83   from complete_square and plus_or_minus_sqrt and assms
    84   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    85     (2 * a) * x + b = sqrt (discrim a b c) \<or>
    86     (2 * a) * x + b = - sqrt (discrim a b c)"
    87     by simp
    88   also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
    89     (2 * a) * x = (-b - sqrt (discrim a b c))"
    90     by auto
    91   also from \<open>a \<noteq> 0\<close> and divide_non_zero [of "2 * a" x]
    92   have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    93     x = (-b - sqrt (discrim a b c)) / (2 * a)"
    94     by simp
    95   finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    96     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    97     x = (-b - sqrt (discrim a b c)) / (2 * a)" .
    98 qed
    99 
   100 lemma discriminant_zero:
   101   fixes a b c x :: real
   102   assumes "a \<noteq> 0"
   103     and "discrim a b c = 0"
   104   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
   105   by (simp add: discriminant_nonneg assms)
   106 
   107 theorem discriminant_iff:
   108   fixes a b c x :: real
   109   assumes "a \<noteq> 0"
   110   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
   111     discrim a b c \<ge> 0 \<and>
   112     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   113      x = (-b - sqrt (discrim a b c)) / (2 * a))"
   114 proof
   115   assume "a * x\<^sup>2 + b * x + c = 0"
   116   with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)"
   117     by auto
   118   then have "discrim a b c \<ge> 0"
   119     by simp
   120   with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
   121   have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   122       x = (-b - sqrt (discrim a b c)) / (2 * a)"
   123     by simp
   124   with \<open>discrim a b c \<ge> 0\<close>
   125   show "discrim a b c \<ge> 0 \<and>
   126     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   127      x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
   128 next
   129   assume "discrim a b c \<ge> 0 \<and>
   130     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   131      x = (-b - sqrt (discrim a b c)) / (2 * a))"
   132   then have "discrim a b c \<ge> 0" and
   133     "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   134      x = (-b - sqrt (discrim a b c)) / (2 * a)"
   135     by simp_all
   136   with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0"
   137     by simp
   138 qed
   139 
   140 lemma discriminant_nonneg_ex:
   141   fixes a b c :: real
   142   assumes "a \<noteq> 0"
   143     and "discrim a b c \<ge> 0"
   144   shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
   145   by (auto simp: discriminant_nonneg assms)
   146 
   147 lemma discriminant_pos_ex:
   148   fixes a b c :: real
   149   assumes "a \<noteq> 0"
   150     and "discrim a b c > 0"
   151   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"
   152 proof -
   153   let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
   154   let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
   155   from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0"
   156     by simp
   157   then have "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)"
   158     by arith
   159   with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y"
   160     by simp
   161   moreover from assms have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0"
   162     using discriminant_nonneg [of a b c ?x]
   163       and discriminant_nonneg [of a b c ?y]
   164     by simp_all
   165   ultimately show ?thesis
   166     by blast
   167 qed
   168 
   169 lemma discriminant_pos_distinct:
   170   fixes a b c x :: real
   171   assumes "a \<noteq> 0"
   172     and "discrim a b c > 0"
   173   shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
   174 proof -
   175   from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
   176   obtain w and z where "w \<noteq> z"
   177     and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
   178     by blast
   179   show "\<exists>y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
   180   proof (cases "x = w")
   181     case True
   182     with \<open>w \<noteq> z\<close> have "x \<noteq> z"
   183       by simp
   184     with \<open>a * z\<^sup>2 + b * z + c = 0\<close> show ?thesis
   185       by auto
   186   next
   187     case False
   188     with \<open>a * w\<^sup>2 + b * w + c = 0\<close> show ?thesis
   189       by auto
   190   qed
   191 qed
   192 
   193 end