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