wenzelm@62058 ` 1` ```(* Title: HOL/Library/Quadratic_Discriminant.thy ``` 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` wenzelm@63465 ` 13` ```definition discrim :: "real \ real \ real \ real" ``` wenzelm@63465 ` 14` ``` where "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 ``` wenzelm@63465 ` 26` ``` then show "a * x\<^sup>2 + b * x + c = 0 \ (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 \ 0" ``` wenzelm@63465 ` 33` ``` and "discrim a b c < 0" ``` lp15@60162 ` 34` ``` shows "a * x\<^sup>2 + b * x + c \ 0" ``` lp15@60162 ` 35` ```proof - ``` wenzelm@63465 ` 36` ``` have "(2 * a * x + b)\<^sup>2 \ 0" ``` wenzelm@63465 ` 37` ``` by simp ``` wenzelm@63465 ` 38` ``` with \discrim a b c < 0\ have "(2 * a * x + b)\<^sup>2 \ discrim a b c" ``` wenzelm@63465 ` 39` ``` by arith ``` wenzelm@63465 ` 40` ``` with complete_square and \a \ 0\ show "a * x\<^sup>2 + b * x + c \ 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 \ 0" ``` lp15@60162 ` 47` ``` shows "x\<^sup>2 = y \ x = sqrt y \ 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 = \x\" ``` wenzelm@63465 ` 53` ``` by simp ``` wenzelm@63465 ` 54` ``` then show "x = sqrt y \ x = - sqrt y" ``` wenzelm@63465 ` 55` ``` by auto ``` lp15@60162 ` 56` ```next ``` lp15@60162 ` 57` ``` assume "x = sqrt y \ x = - sqrt y" ``` wenzelm@63465 ` 58` ``` then have "x\<^sup>2 = (sqrt y)\<^sup>2 \ x\<^sup>2 = (- sqrt y)\<^sup>2" ``` wenzelm@63465 ` 59` ``` by auto ``` wenzelm@63465 ` 60` ``` with \y \ 0\ 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 \ 0" ``` lp15@60162 ` 67` ``` shows "x * y = z \ y = z / x" ``` lp15@60162 ` 68` ```proof ``` wenzelm@63465 ` 69` ``` show "y = z / x" if "x * y = z" ``` wenzelm@63465 ` 70` ``` using \x \ 0\ that by (simp add: field_simps) ``` wenzelm@63465 ` 71` ``` show "x * y = z" if "y = z / x" ``` wenzelm@63465 ` 72` ``` using \x \ 0\ 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 \ 0" ``` wenzelm@63465 ` 78` ``` and "discrim a b c \ 0" ``` lp15@60162 ` 79` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ ``` wenzelm@63465 ` 80` ``` x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ ``` lp15@60162 ` 85` ``` (2 * a) * x + b = sqrt (discrim a b c) \ ``` lp15@60162 ` 86` ``` (2 * a) * x + b = - sqrt (discrim a b c)" ``` lp15@60162 ` 87` ``` by simp ``` lp15@60162 ` 88` ``` also have "\ \ (2 * a) * x = (-b + sqrt (discrim a b c)) \ ``` lp15@60162 ` 89` ``` (2 * a) * x = (-b - sqrt (discrim a b c))" ``` lp15@60162 ` 90` ``` by auto ``` wenzelm@60500 ` 91` ``` also from \a \ 0\ and divide_non_zero [of "2 * a" x] ``` lp15@60162 ` 92` ``` have "\ \ x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ ``` lp15@60162 ` 96` ``` x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ 0" ``` wenzelm@63465 ` 103` ``` and "discrim a b c = 0" ``` lp15@60162 ` 104` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ 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 \ 0" ``` lp15@60162 ` 110` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ ``` wenzelm@63465 ` 111` ``` discrim a b c \ 0 \ ``` wenzelm@63465 ` 112` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \a \ 0\ have "\(discrim a b c < 0)" ``` wenzelm@63465 ` 117` ``` by auto ``` wenzelm@63465 ` 118` ``` then have "discrim a b c \ 0" ``` wenzelm@63465 ` 119` ``` by simp ``` wenzelm@60500 ` 120` ``` with discriminant_nonneg and \a * x\<^sup>2 + b * x + c = 0\ and \a \ 0\ ``` lp15@60162 ` 121` ``` have "x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` wenzelm@63465 ` 122` ``` x = (-b - sqrt (discrim a b c)) / (2 * a)" ``` lp15@60162 ` 123` ``` by simp ``` wenzelm@60500 ` 124` ``` with \discrim a b c \ 0\ ``` lp15@60162 ` 125` ``` show "discrim a b c \ 0 \ ``` lp15@60162 ` 126` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` wenzelm@63465 ` 127` ``` x = (-b - sqrt (discrim a b c)) / (2 * a))" .. ``` lp15@60162 ` 128` ```next ``` lp15@60162 ` 129` ``` assume "discrim a b c \ 0 \ ``` lp15@60162 ` 130` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` wenzelm@63465 ` 131` ``` x = (-b - sqrt (discrim a b c)) / (2 * a))" ``` wenzelm@63465 ` 132` ``` then have "discrim a b c \ 0" and ``` lp15@60162 ` 133` ``` "x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \a \ 0\ 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 \ 0" ``` wenzelm@63465 ` 143` ``` and "discrim a b c \ 0" ``` lp15@60162 ` 144` ``` shows "\ 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 \ 0" ``` wenzelm@63465 ` 150` ``` and "discrim a b c > 0" ``` wenzelm@63465 ` 151` ``` shows "\x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ 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 \discrim a b c > 0\ have "sqrt (discrim a b c) \ 0" ``` wenzelm@63465 ` 156` ``` by simp ``` wenzelm@63465 ` 157` ``` then have "sqrt (discrim a b c) \ - sqrt (discrim a b c)" ``` wenzelm@63465 ` 158` ``` by arith ``` wenzelm@63465 ` 159` ``` with \a \ 0\ have "?x \ ?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 \ 0" ``` wenzelm@63465 ` 172` ``` and "discrim a b c > 0" ``` lp15@60162 ` 173` ``` shows "\ y. x \ y \ a * y\<^sup>2 + b * y + c = 0" ``` lp15@60162 ` 174` ```proof - ``` wenzelm@60500 ` 175` ``` from discriminant_pos_ex and \a \ 0\ and \discrim a b c > 0\ ``` lp15@60162 ` 176` ``` obtain w and z where "w \ 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 "\y. x \ y \ a * y\<^sup>2 + b * y + c = 0" ``` wenzelm@63465 ` 180` ``` proof (cases "x = w") ``` wenzelm@63465 ` 181` ``` case True ``` wenzelm@63465 ` 182` ``` with \w \ z\ have "x \ z" ``` wenzelm@63465 ` 183` ``` by simp ``` wenzelm@63465 ` 184` ``` with \a * z\<^sup>2 + b * z + c = 0\ show ?thesis ``` wenzelm@63465 ` 185` ``` by auto ``` lp15@60162 ` 186` ``` next ``` wenzelm@63465 ` 187` ``` case False ``` wenzelm@63465 ` 188` ``` with \a * w\<^sup>2 + b * w + c = 0\ show ?thesis ``` wenzelm@63465 ` 189` ``` by auto ``` lp15@60162 ` 190` ``` qed ``` lp15@60162 ` 191` ```qed ``` lp15@60162 ` 192` lp15@60162 ` 193` ```end ```