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