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: ``` nipkow@68553 ` 17` ``` "a \ 0 \ a * x\<^sup>2 + b * x + c = 0 \ (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 \ 0" ``` wenzelm@63465 ` 23` ``` and "discrim a b c < 0" ``` lp15@60162 ` 24` ``` shows "a * x\<^sup>2 + b * x + c \ 0" ``` lp15@60162 ` 25` ```proof - ``` wenzelm@63465 ` 26` ``` have "(2 * a * x + b)\<^sup>2 \ 0" ``` wenzelm@63465 ` 27` ``` by simp ``` wenzelm@63465 ` 28` ``` with \discrim a b c < 0\ have "(2 * a * x + b)\<^sup>2 \ discrim a b c" ``` wenzelm@63465 ` 29` ``` by arith ``` wenzelm@63465 ` 30` ``` with complete_square and \a \ 0\ show "a * x\<^sup>2 + b * x + c \ 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 \ 0" ``` lp15@60162 ` 37` ``` shows "x\<^sup>2 = y \ x = sqrt y \ 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 = \x\" ``` wenzelm@63465 ` 43` ``` by simp ``` wenzelm@63465 ` 44` ``` then show "x = sqrt y \ x = - sqrt y" ``` wenzelm@63465 ` 45` ``` by auto ``` lp15@60162 ` 46` ```next ``` lp15@60162 ` 47` ``` assume "x = sqrt y \ x = - sqrt y" ``` wenzelm@63465 ` 48` ``` then have "x\<^sup>2 = (sqrt y)\<^sup>2 \ x\<^sup>2 = (- sqrt y)\<^sup>2" ``` wenzelm@63465 ` 49` ``` by auto ``` wenzelm@63465 ` 50` ``` with \y \ 0\ 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 \ 0" ``` lp15@60162 ` 57` ``` shows "x * y = z \ y = z / x" ``` lp15@60162 ` 58` ```proof ``` wenzelm@63465 ` 59` ``` show "y = z / x" if "x * y = z" ``` wenzelm@63465 ` 60` ``` using \x \ 0\ that by (simp add: field_simps) ``` wenzelm@63465 ` 61` ``` show "x * y = z" if "y = z / x" ``` wenzelm@63465 ` 62` ``` using \x \ 0\ 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 \ 0" ``` wenzelm@63465 ` 68` ``` and "discrim a b c \ 0" ``` lp15@60162 ` 69` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ ``` wenzelm@63465 ` 70` ``` x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ ``` lp15@60162 ` 75` ``` (2 * a) * x + b = sqrt (discrim a b c) \ ``` lp15@60162 ` 76` ``` (2 * a) * x + b = - sqrt (discrim a b c)" ``` lp15@60162 ` 77` ``` by simp ``` lp15@60162 ` 78` ``` also have "\ \ (2 * a) * x = (-b + sqrt (discrim a b c)) \ ``` lp15@60162 ` 79` ``` (2 * a) * x = (-b - sqrt (discrim a b c))" ``` lp15@60162 ` 80` ``` by auto ``` wenzelm@60500 ` 81` ``` also from \a \ 0\ and divide_non_zero [of "2 * a" x] ``` lp15@60162 ` 82` ``` have "\ \ x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ ``` lp15@60162 ` 86` ``` x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \ 0" ``` wenzelm@63465 ` 93` ``` and "discrim a b c = 0" ``` lp15@60162 ` 94` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ 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 \ 0" ``` lp15@60162 ` 100` ``` shows "a * x\<^sup>2 + b * x + c = 0 \ ``` wenzelm@63465 ` 101` ``` discrim a b c \ 0 \ ``` wenzelm@63465 ` 102` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \a \ 0\ have "\(discrim a b c < 0)" ``` wenzelm@63465 ` 107` ``` by auto ``` wenzelm@63465 ` 108` ``` then have "discrim a b c \ 0" ``` wenzelm@63465 ` 109` ``` by simp ``` wenzelm@60500 ` 110` ``` with discriminant_nonneg and \a * x\<^sup>2 + b * x + c = 0\ and \a \ 0\ ``` lp15@60162 ` 111` ``` have "x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` wenzelm@63465 ` 112` ``` x = (-b - sqrt (discrim a b c)) / (2 * a)" ``` lp15@60162 ` 113` ``` by simp ``` wenzelm@60500 ` 114` ``` with \discrim a b c \ 0\ ``` lp15@60162 ` 115` ``` show "discrim a b c \ 0 \ ``` lp15@60162 ` 116` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` wenzelm@63465 ` 117` ``` x = (-b - sqrt (discrim a b c)) / (2 * a))" .. ``` lp15@60162 ` 118` ```next ``` lp15@60162 ` 119` ``` assume "discrim a b c \ 0 \ ``` lp15@60162 ` 120` ``` (x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` wenzelm@63465 ` 121` ``` x = (-b - sqrt (discrim a b c)) / (2 * a))" ``` wenzelm@63465 ` 122` ``` then have "discrim a b c \ 0" and ``` lp15@60162 ` 123` ``` "x = (-b + sqrt (discrim a b c)) / (2 * a) \ ``` 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 \a \ 0\ 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 \ 0" ``` wenzelm@63465 ` 133` ``` and "discrim a b c \ 0" ``` lp15@60162 ` 134` ``` shows "\ 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 \ 0" ``` wenzelm@63465 ` 140` ``` and "discrim a b c > 0" ``` wenzelm@63465 ` 141` ``` shows "\x y. x \ y \ a * x\<^sup>2 + b * x + c = 0 \ 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 \discrim a b c > 0\ have "sqrt (discrim a b c) \ 0" ``` wenzelm@63465 ` 146` ``` by simp ``` wenzelm@63465 ` 147` ``` then have "sqrt (discrim a b c) \ - sqrt (discrim a b c)" ``` wenzelm@63465 ` 148` ``` by arith ``` wenzelm@63465 ` 149` ``` with \a \ 0\ have "?x \ ?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 \ 0" ``` wenzelm@63465 ` 162` ``` 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 ``` wenzelm@63465 ` 169` ``` show "\y. x \ y \ a * y\<^sup>2 + b * y + c = 0" ``` wenzelm@63465 ` 170` ``` proof (cases "x = w") ``` wenzelm@63465 ` 171` ``` case True ``` wenzelm@63465 ` 172` ``` with \w \ z\ have "x \ z" ``` wenzelm@63465 ` 173` ``` by simp ``` wenzelm@63465 ` 174` ``` with \a * z\<^sup>2 + b * z + c = 0\ show ?thesis ``` wenzelm@63465 ` 175` ``` by auto ``` lp15@60162 ` 176` ``` next ``` wenzelm@63465 ` 177` ``` case False ``` wenzelm@63465 ` 178` ``` with \a * w\<^sup>2 + b * w + c = 0\ 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 \ \" "b \ \" "a \ 0" ``` nipkow@68553 ` 185` ``` and "a*x^2 + b*x + c = 0" ``` nipkow@68553 ` 186` ``` and "sqrt (discrim a b c) \ \" ``` nipkow@68553 ` 187` ``` shows "x \ \" ``` 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 \ \" "b \ \" ``` nipkow@68553 ` 192` ``` and "a*x^2 + b*x + c = 0" ``` nipkow@68553 ` 193` ``` and "x \ \" ``` nipkow@68553 ` 194` ``` shows "sqrt (discrim a b c) \ \" ``` 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) = \2*a*x+b\" by (simp) ``` nipkow@68553 ` 198` ``` thus ?thesis using \a \ \\ \b \ \\ \x \ \\ by (simp) ``` nipkow@68553 ` 199` ```qed ``` nipkow@68553 ` 200` lp15@60162 ` 201` ```end ```