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