src/HOL/Library/Quadratic_Discriminant.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 60500 903bb1495239
child 62058 1cfd5d604937
permissions -rw-r--r--
tuned references
lp15@60162
     1
(*  Title:       Roots of real quadratics
lp15@60162
     2
    Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
lp15@60162
     3
lp15@60162
     4
Originally from the AFP entry Tarskis_Geometry
lp15@60162
     5
*)
lp15@60162
     6
lp15@60162
     7
section "Roots of real quadratics"
lp15@60162
     8
lp15@60162
     9
theory Quadratic_Discriminant
lp15@60162
    10
imports Complex_Main
lp15@60162
    11
begin
lp15@60162
    12
lp15@60162
    13
definition discrim :: "[real,real,real] \<Rightarrow> real" where
lp15@60162
    14
  "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
lp15@60162
    15
lp15@60162
    16
lemma complete_square:
lp15@60162
    17
  fixes a b c x :: "real"
lp15@60162
    18
  assumes "a \<noteq> 0"
lp15@60162
    19
  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
lp15@60162
    20
proof -
lp15@60162
    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)"
lp15@60162
    22
    by (simp add: algebra_simps power2_eq_square)
wenzelm@60500
    23
  with \<open>a \<noteq> 0\<close>
lp15@60162
    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"
lp15@60162
    25
    by simp
lp15@60162
    26
  thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
lp15@60162
    27
    unfolding discrim_def
lp15@60162
    28
    by (simp add: power2_eq_square algebra_simps)
lp15@60162
    29
qed
lp15@60162
    30
lp15@60162
    31
lemma discriminant_negative:
lp15@60162
    32
  fixes a b c x :: real
lp15@60162
    33
  assumes "a \<noteq> 0"
lp15@60162
    34
  and "discrim a b c < 0"
lp15@60162
    35
  shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
lp15@60162
    36
proof -
lp15@60162
    37
  have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
wenzelm@60500
    38
  with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
wenzelm@60500
    39
  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
lp15@60162
    40
qed
lp15@60162
    41
lp15@60162
    42
lemma plus_or_minus_sqrt:
lp15@60162
    43
  fixes x y :: real
lp15@60162
    44
  assumes "y \<ge> 0"
lp15@60162
    45
  shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
lp15@60162
    46
proof
lp15@60162
    47
  assume "x\<^sup>2 = y"
lp15@60162
    48
  hence "sqrt (x\<^sup>2) = sqrt y" by simp
lp15@60162
    49
  hence "sqrt y = \<bar>x\<bar>" by simp
lp15@60162
    50
  thus "x = sqrt y \<or> x = - sqrt y" by auto
lp15@60162
    51
next
lp15@60162
    52
  assume "x = sqrt y \<or> x = - sqrt y"
lp15@60162
    53
  hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
wenzelm@60500
    54
  with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y" by simp
lp15@60162
    55
qed
lp15@60162
    56
lp15@60162
    57
lemma divide_non_zero:
lp15@60162
    58
  fixes x y z :: real
lp15@60162
    59
  assumes "x \<noteq> 0"
lp15@60162
    60
  shows "x * y = z \<longleftrightarrow> y = z / x"
lp15@60162
    61
proof
lp15@60162
    62
  assume "x * y = z"
wenzelm@60500
    63
  with \<open>x \<noteq> 0\<close> show "y = z / x" by (simp add: field_simps)
lp15@60162
    64
next
lp15@60162
    65
  assume "y = z / x"
wenzelm@60500
    66
  with \<open>x \<noteq> 0\<close> show "x * y = z" by simp
lp15@60162
    67
qed
lp15@60162
    68
lp15@60162
    69
lemma discriminant_nonneg:
lp15@60162
    70
  fixes a b c x :: real
lp15@60162
    71
  assumes "a \<noteq> 0"
lp15@60162
    72
  and "discrim a b c \<ge> 0"
lp15@60162
    73
  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
lp15@60162
    74
  x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
    75
  x = (-b - sqrt (discrim a b c)) / (2 * a)"
lp15@60162
    76
proof -
lp15@60162
    77
  from complete_square and plus_or_minus_sqrt and assms
lp15@60162
    78
  have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
lp15@60162
    79
    (2 * a) * x + b = sqrt (discrim a b c) \<or>
lp15@60162
    80
    (2 * a) * x + b = - sqrt (discrim a b c)"
lp15@60162
    81
    by simp
lp15@60162
    82
  also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
lp15@60162
    83
    (2 * a) * x = (-b - sqrt (discrim a b c))"
lp15@60162
    84
    by auto
wenzelm@60500
    85
  also from \<open>a \<noteq> 0\<close> and divide_non_zero [of "2 * a" x]
lp15@60162
    86
  have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
    87
    x = (-b - sqrt (discrim a b c)) / (2 * a)"
lp15@60162
    88
    by simp
lp15@60162
    89
  finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
lp15@60162
    90
    x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
    91
    x = (-b - sqrt (discrim a b c)) / (2 * a)" .
lp15@60162
    92
qed
lp15@60162
    93
lp15@60162
    94
lemma discriminant_zero:
lp15@60162
    95
  fixes a b c x :: real
lp15@60162
    96
  assumes "a \<noteq> 0"
lp15@60162
    97
  and "discrim a b c = 0"
lp15@60162
    98
  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
lp15@60162
    99
  using discriminant_nonneg and assms
lp15@60162
   100
  by simp
lp15@60162
   101
lp15@60162
   102
theorem discriminant_iff:
lp15@60162
   103
  fixes a b c x :: real
lp15@60162
   104
  assumes "a \<noteq> 0"
lp15@60162
   105
  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
lp15@60162
   106
  discrim a b c \<ge> 0 \<and>
lp15@60162
   107
  (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
   108
  x = (-b - sqrt (discrim a b c)) / (2 * a))"
lp15@60162
   109
proof
lp15@60162
   110
  assume "a * x\<^sup>2 + b * x + c = 0"
wenzelm@60500
   111
  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)" by auto
lp15@60162
   112
  hence "discrim a b c \<ge> 0" by simp
wenzelm@60500
   113
  with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
lp15@60162
   114
  have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
   115
    x = (-b - sqrt (discrim a b c)) / (2 * a)"
lp15@60162
   116
    by simp
wenzelm@60500
   117
  with \<open>discrim a b c \<ge> 0\<close>
lp15@60162
   118
  show "discrim a b c \<ge> 0 \<and>
lp15@60162
   119
    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
   120
    x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
lp15@60162
   121
next
lp15@60162
   122
  assume "discrim a b c \<ge> 0 \<and>
lp15@60162
   123
    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
   124
    x = (-b - sqrt (discrim a b c)) / (2 * a))"
lp15@60162
   125
  hence "discrim a b c \<ge> 0" and
lp15@60162
   126
    "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
lp15@60162
   127
    x = (-b - sqrt (discrim a b c)) / (2 * a)"
lp15@60162
   128
    by simp_all
wenzelm@60500
   129
  with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0" by simp
lp15@60162
   130
qed
lp15@60162
   131
lp15@60162
   132
lemma discriminant_nonneg_ex:
lp15@60162
   133
  fixes a b c :: real
lp15@60162
   134
  assumes "a \<noteq> 0"
lp15@60162
   135
  and "discrim a b c \<ge> 0"
lp15@60162
   136
  shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
lp15@60162
   137
  using discriminant_nonneg and assms
lp15@60162
   138
  by auto
lp15@60162
   139
lp15@60162
   140
lemma discriminant_pos_ex:
lp15@60162
   141
  fixes a b c :: real
lp15@60162
   142
  assumes "a \<noteq> 0"
lp15@60162
   143
  and "discrim a b c > 0"
lp15@60162
   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"
lp15@60162
   145
proof -
lp15@60162
   146
  let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
lp15@60162
   147
  let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
wenzelm@60500
   148
  from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0" by simp
lp15@60162
   149
  hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
wenzelm@60500
   150
  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y" by simp
lp15@60162
   151
  moreover
lp15@60162
   152
  from discriminant_nonneg [of a b c ?x]
lp15@60162
   153
    and discriminant_nonneg [of a b c ?y]
lp15@60162
   154
    and assms
lp15@60162
   155
  have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
lp15@60162
   156
  ultimately
lp15@60162
   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
lp15@60162
   158
qed
lp15@60162
   159
lp15@60162
   160
lemma discriminant_pos_distinct:
lp15@60162
   161
  fixes a b c x :: real
lp15@60162
   162
  assumes "a \<noteq> 0" and "discrim a b c > 0"
lp15@60162
   163
  shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
lp15@60162
   164
proof -
wenzelm@60500
   165
  from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
lp15@60162
   166
  obtain w and z where "w \<noteq> z"
lp15@60162
   167
    and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
lp15@60162
   168
    by blast
lp15@60162
   169
  show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
lp15@60162
   170
  proof cases
lp15@60162
   171
    assume "x = w"
wenzelm@60500
   172
    with \<open>w \<noteq> z\<close> have "x \<noteq> z" by simp
wenzelm@60500
   173
    with \<open>a * z\<^sup>2 + b * z + c = 0\<close>
lp15@60162
   174
    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
lp15@60162
   175
  next
lp15@60162
   176
    assume "x \<noteq> w"
wenzelm@60500
   177
    with \<open>a * w\<^sup>2 + b * w + c = 0\<close>
lp15@60162
   178
    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
lp15@60162
   179
  qed
lp15@60162
   180
qed
lp15@60162
   181
lp15@60162
   182
end