src/HOL/Library/Quadratic_Discriminant.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 60500 903bb1495239
child 62058 1cfd5d604937
permissions -rw-r--r--
more symbols;
     1 (*  Title:       Roots of real quadratics
     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,real,real] \<Rightarrow> real" where
    14   "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   thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
    27     unfolding discrim_def
    28     by (simp add: power2_eq_square algebra_simps)
    29 qed
    30 
    31 lemma discriminant_negative:
    32   fixes a b c x :: real
    33   assumes "a \<noteq> 0"
    34   and "discrim a b c < 0"
    35   shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
    36 proof -
    37   have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
    38   with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
    39   with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
    40 qed
    41 
    42 lemma plus_or_minus_sqrt:
    43   fixes x y :: real
    44   assumes "y \<ge> 0"
    45   shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
    46 proof
    47   assume "x\<^sup>2 = y"
    48   hence "sqrt (x\<^sup>2) = sqrt y" by simp
    49   hence "sqrt y = \<bar>x\<bar>" by simp
    50   thus "x = sqrt y \<or> x = - sqrt y" by auto
    51 next
    52   assume "x = sqrt y \<or> x = - sqrt y"
    53   hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
    54   with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y" by simp
    55 qed
    56 
    57 lemma divide_non_zero:
    58   fixes x y z :: real
    59   assumes "x \<noteq> 0"
    60   shows "x * y = z \<longleftrightarrow> y = z / x"
    61 proof
    62   assume "x * y = z"
    63   with \<open>x \<noteq> 0\<close> show "y = z / x" by (simp add: field_simps)
    64 next
    65   assume "y = z / x"
    66   with \<open>x \<noteq> 0\<close> show "x * y = z" by simp
    67 qed
    68 
    69 lemma discriminant_nonneg:
    70   fixes a b c x :: real
    71   assumes "a \<noteq> 0"
    72   and "discrim a b c \<ge> 0"
    73   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    74   x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    75   x = (-b - sqrt (discrim a b c)) / (2 * a)"
    76 proof -
    77   from complete_square and plus_or_minus_sqrt and assms
    78   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    79     (2 * a) * x + b = sqrt (discrim a b c) \<or>
    80     (2 * a) * x + b = - sqrt (discrim a b c)"
    81     by simp
    82   also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
    83     (2 * a) * x = (-b - sqrt (discrim a b c))"
    84     by auto
    85   also from \<open>a \<noteq> 0\<close> and divide_non_zero [of "2 * a" x]
    86   have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    87     x = (-b - sqrt (discrim a b c)) / (2 * a)"
    88     by simp
    89   finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
    90     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
    91     x = (-b - sqrt (discrim a b c)) / (2 * a)" .
    92 qed
    93 
    94 lemma discriminant_zero:
    95   fixes a b c x :: real
    96   assumes "a \<noteq> 0"
    97   and "discrim a b c = 0"
    98   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
    99   using discriminant_nonneg and assms
   100   by simp
   101 
   102 theorem discriminant_iff:
   103   fixes a b c x :: real
   104   assumes "a \<noteq> 0"
   105   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
   106   discrim a b c \<ge> 0 \<and>
   107   (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   108   x = (-b - sqrt (discrim a b c)) / (2 * a))"
   109 proof
   110   assume "a * x\<^sup>2 + b * x + c = 0"
   111   with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)" by auto
   112   hence "discrim a b c \<ge> 0" by simp
   113   with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
   114   have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   115     x = (-b - sqrt (discrim a b c)) / (2 * a)"
   116     by simp
   117   with \<open>discrim a b c \<ge> 0\<close>
   118   show "discrim a b c \<ge> 0 \<and>
   119     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
   120     x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
   121 next
   122   assume "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   hence "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     by simp_all
   129   with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0" by simp
   130 qed
   131 
   132 lemma discriminant_nonneg_ex:
   133   fixes a b c :: real
   134   assumes "a \<noteq> 0"
   135   and "discrim a b c \<ge> 0"
   136   shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
   137   using discriminant_nonneg and assms
   138   by auto
   139 
   140 lemma discriminant_pos_ex:
   141   fixes a b c :: real
   142   assumes "a \<noteq> 0"
   143   and "discrim a b c > 0"
   144   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"
   145 proof -
   146   let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
   147   let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
   148   from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0" by simp
   149   hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
   150   with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y" by simp
   151   moreover
   152   from discriminant_nonneg [of a b c ?x]
   153     and discriminant_nonneg [of a b c ?y]
   154     and assms
   155   have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
   156   ultimately
   157   show "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0" by blast
   158 qed
   159 
   160 lemma discriminant_pos_distinct:
   161   fixes a b c x :: real
   162   assumes "a \<noteq> 0" 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
   171     assume "x = w"
   172     with \<open>w \<noteq> z\<close> have "x \<noteq> z" by simp
   173     with \<open>a * z\<^sup>2 + b * z + c = 0\<close>
   174     show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
   175   next
   176     assume "x \<noteq> w"
   177     with \<open>a * w\<^sup>2 + b * w + c = 0\<close>
   178     show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
   179   qed
   180 qed
   181 
   182 end