lp15@60162 ` 1` ```(* Title: Roots of real quadratics ``` lp15@60162 ` 2` ``` Author: Tim Makarios , 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] \ real" where ``` lp15@60162 ` 14` ``` "discrim a b c \ 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 \ 0" ``` lp15@60162 ` 19` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ (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 \a \ 0\ ``` lp15@60162 ` 24` ``` have "a * x\<^sup>2 + b * x + c = 0 \ 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 \ (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 \ 0" ``` lp15@60162 ` 34` ``` and "discrim a b c < 0" ``` lp15@60162 ` 35` ``` shows "a * x\<^sup>2 + b * x + c \ 0" ``` lp15@60162 ` 36` ```proof - ``` lp15@60162 ` 37` ``` have "(2 * a * x + b)\<^sup>2 \ 0" by simp ``` wenzelm@60500 ` 38` ``` with \discrim a b c < 0\ have "(2 * a * x + b)\<^sup>2 \ discrim a b c" by arith ``` wenzelm@60500 ` 39` ``` with complete_square and \a \ 0\ show "a * x\<^sup>2 + b * x + c \ 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 \ 0" ``` lp15@60162 ` 45` ``` shows "x\<^sup>2 = y \ x = sqrt y \ 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 = \x\" by simp ``` lp15@60162 ` 50` ``` thus "x = sqrt y \ x = - sqrt y" by auto ``` lp15@60162 ` 51` ```next ``` lp15@60162 ` 52` ``` assume "x = sqrt y \ x = - sqrt y" ``` lp15@60162 ` 53` ``` hence "x\<^sup>2 = (sqrt y)\<^sup>2 \ x\<^sup>2 = (- sqrt y)\<^sup>2" by auto ``` wenzelm@60500 ` 54` ``` with \y \ 0\ 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 \ 0" ``` lp15@60162 ` 60` ``` shows "x * y = z \ y = z / x" ``` lp15@60162 ` 61` ```proof ``` lp15@60162 ` 62` ``` assume "x * y = z" ``` wenzelm@60500 ` 63` ``` with \x \ 0\ show "y = z / x" by (simp add: field_simps) ``` lp15@60162 ` 64` ```next ``` lp15@60162 ` 65` ``` assume "y = z / x" ``` wenzelm@60500 ` 66` ``` with \x \ 0\ 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 \ 0" ``` lp15@60162 ` 72` ``` and "discrim a b c \ 0" ``` lp15@60162 ` 73` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ ``` lp15@60162 ` 74` ``` x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ ``` lp15@60162 ` 79` ``` (2 * a) * x + b = sqrt (discrim a b c) \ ``` lp15@60162 ` 80` ``` (2 * a) * x + b = - sqrt (discrim a b c)" ``` lp15@60162 ` 81` ``` by simp ``` lp15@60162 ` 82` ``` also have "\ \ (2 * a) * x = (-b + sqrt (discrim a b c)) \ ``` lp15@60162 ` 83` ``` (2 * a) * x = (-b - sqrt (discrim a b c))" ``` lp15@60162 ` 84` ``` by auto ``` wenzelm@60500 ` 85` ``` also from \a \ 0\ and divide_non_zero [of "2 * a" x] ``` lp15@60162 ` 86` ``` have "\ \ x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ ``` lp15@60162 ` 90` ``` x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ 0" ``` lp15@60162 ` 97` ``` and "discrim a b c = 0" ``` lp15@60162 ` 98` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ 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 \ 0" ``` lp15@60162 ` 105` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ ``` lp15@60162 ` 106` ``` discrim a b c \ 0 \ ``` lp15@60162 ` 107` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \a \ 0\ have "\(discrim a b c < 0)" by auto ``` lp15@60162 ` 112` ``` hence "discrim a b c \ 0" by simp ``` wenzelm@60500 ` 113` ``` with discriminant_nonneg and \a * x\<^sup>2 + b * x + c = 0\ and \a \ 0\ ``` lp15@60162 ` 114` ``` have "x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` lp15@60162 ` 115` ``` x = (-b - sqrt (discrim a b c)) / (2 * a)" ``` lp15@60162 ` 116` ``` by simp ``` wenzelm@60500 ` 117` ``` with \discrim a b c \ 0\ ``` lp15@60162 ` 118` ``` show "discrim a b c \ 0 \ ``` lp15@60162 ` 119` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` lp15@60162 ` 120` ``` x = (-b - sqrt (discrim a b c)) / (2 * a))" .. ``` lp15@60162 ` 121` ```next ``` lp15@60162 ` 122` ``` assume "discrim a b c \ 0 \ ``` lp15@60162 ` 123` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` lp15@60162 ` 124` ``` x = (-b - sqrt (discrim a b c)) / (2 * a))" ``` lp15@60162 ` 125` ``` hence "discrim a b c \ 0" and ``` lp15@60162 ` 126` ``` "x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \a \ 0\ 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 \ 0" ``` lp15@60162 ` 135` ``` and "discrim a b c \ 0" ``` lp15@60162 ` 136` ``` shows "\ 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 \ 0" ``` lp15@60162 ` 143` ``` and "discrim a b c > 0" ``` lp15@60162 ` 144` ``` shows "\ x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ 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 \discrim a b c > 0\ have "sqrt (discrim a b c) \ 0" by simp ``` lp15@60162 ` 149` ``` hence "sqrt (discrim a b c) \ - sqrt (discrim a b c)" by arith ``` wenzelm@60500 ` 150` ``` with \a \ 0\ have "?x \ ?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 "\ x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ 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 \ 0" and "discrim a b c > 0" ``` lp15@60162 ` 163` ``` shows "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" ``` lp15@60162 ` 164` ```proof - ``` wenzelm@60500 ` 165` ``` from discriminant_pos_ex and \a \ 0\ and \discrim a b c > 0\ ``` lp15@60162 ` 166` ``` obtain w and z where "w \ 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 "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" ``` lp15@60162 ` 170` ``` proof cases ``` lp15@60162 ` 171` ``` assume "x = w" ``` wenzelm@60500 ` 172` ``` with \w \ z\ have "x \ z" by simp ``` wenzelm@60500 ` 173` ``` with \a * z\<^sup>2 + b * z + c = 0\ ``` lp15@60162 ` 174` ``` show "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" by auto ``` lp15@60162 ` 175` ``` next ``` lp15@60162 ` 176` ``` assume "x \ w" ``` wenzelm@60500 ` 177` ``` with \a * w\<^sup>2 + b * w + c = 0\ ``` lp15@60162 ` 178` ``` show "\ y. x \ y \ 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 ```