1(* Title: HOL/ex/Cubic_Quartic.thy 2 Author: Amine Chaieb 3*) 4 5section \<open>The Cubic and Quartic Root Formulas\<close> 6 7theory Cubic_Quartic 8imports Complex_Main 9begin 10 11section \<open>The Cubic Formula\<close> 12 13definition "ccbrt z = (SOME (w::complex). w^3 = z)" 14 15lemma ccbrt: "(ccbrt z) ^ 3 = z" 16proof - 17 from rcis_Ex obtain r a where ra: "z = rcis r a" 18 by blast 19 let ?r' = "if r < 0 then - root 3 (-r) else root 3 r" 20 let ?a' = "a/3" 21 have "rcis ?r' ?a' ^ 3 = rcis r a" 22 by (cases "r < 0") (simp_all add: DeMoivre2) 23 then have *: "\<exists>w. w^3 = z" 24 unfolding ra by blast 25 from someI_ex [OF *] show ?thesis 26 unfolding ccbrt_def by blast 27qed 28 29 30text \<open>The reduction to a simpler form:\<close> 31 32lemma cubic_reduction: 33 fixes a :: complex 34 assumes 35 "a \<noteq> 0 \<and> x = y - b / (3 * a) \<and> p = (3* a * c - b^2) / (9 * a^2) \<and> 36 q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)" 37 shows "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> y^3 + 3 * p * y - 2 * q = 0" 38proof - 39 from assms have "3 * a \<noteq> 0" "9 * a^2 \<noteq> 0" "54 * a^3 \<noteq> 0" by auto 40 then have *: 41 "x = y - b / (3 * a) \<longleftrightarrow> (3*a) * x = (3*a) * y - b" 42 "p = (3* a * c - b^2) / (9 * a^2) \<longleftrightarrow> (9 * a^2) * p = (3* a * c - b^2)" 43 "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \<longleftrightarrow> 44 (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)" 45 by (simp_all add: field_simps) 46 from assms [unfolded *] show ?thesis 47 by algebra 48qed 49 50 51text \<open>The solutions of the special form:\<close> 52 53lemma cubic_basic: 54 fixes s :: complex 55 assumes 56 "s^2 = q^2 + p^3 \<and> 57 s1^3 = (if p = 0 then 2 * q else q + s) \<and> 58 s2 = -s1 * (1 + i * t) / 2 \<and> 59 s3 = -s1 * (1 - i * t) / 2 \<and> 60 i^2 + 1 = 0 \<and> 61 t^2 = 3" 62 shows 63 "if p = 0 64 then y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> y = s1 \<or> y = s2 \<or> y = s3 65 else s1 \<noteq> 0 \<and> 66 (y^3 + 3 * p * y - 2 * q = 0 \<longleftrightarrow> (y = s1 - p / s1 \<or> y = s2 - p / s2 \<or> y = s3 - p / s3))" 67proof (cases "p = 0") 68 case True 69 with assms show ?thesis 70 by (simp add: field_simps) algebra 71next 72 case False 73 with assms have *: "s1 \<noteq> 0" by (simp add: field_simps) algebra 74 with assms False have "s2 \<noteq> 0" "s3 \<noteq> 0" 75 by (simp_all add: field_simps) algebra+ 76 with * have **: 77 "y = s1 - p / s1 \<longleftrightarrow> s1 * y = s1^2 - p" 78 "y = s2 - p / s2 \<longleftrightarrow> s2 * y = s2^2 - p" 79 "y = s3 - p / s3 \<longleftrightarrow> s3 * y = s3^2 - p" 80 by (simp_all add: field_simps power2_eq_square) 81 from assms False show ?thesis 82 unfolding ** by (simp add: field_simps) algebra 83qed 84 85 86text \<open>Explicit formula for the roots:\<close> 87 88lemma cubic: 89 assumes a0: "a \<noteq> 0" 90 shows 91 "let 92 p = (3 * a * c - b^2) / (9 * a^2); 93 q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3); 94 s = csqrt(q^2 + p^3); 95 s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s)); 96 s2 = -s1 * (1 + \<i> * csqrt 3) / 2; 97 s3 = -s1 * (1 - \<i> * csqrt 3) / 2 98 in 99 if p = 0 then 100 a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> 101 x = s1 - b / (3 * a) \<or> 102 x = s2 - b / (3 * a) \<or> 103 x = s3 - b / (3 * a) 104 else 105 s1 \<noteq> 0 \<and> 106 (a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> 107 x = s1 - p / s1 - b / (3 * a) \<or> 108 x = s2 - p / s2 - b / (3 * a) \<or> 109 x = s3 - p / s3 - b / (3 * a))" 110proof - 111 let ?p = "(3 * a * c - b^2) / (9 * a^2)" 112 let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)" 113 let ?s = "csqrt (?q^2 + ?p^3)" 114 let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)" 115 let ?s2 = "- ?s1 * (1 + \<i> * csqrt 3) / 2" 116 let ?s3 = "- ?s1 * (1 - \<i> * csqrt 3) / 2" 117 let ?y = "x + b / (3 * a)" 118 from a0 have zero: "9 * a^2 \<noteq> 0" "a^3 * 54 \<noteq> 0" "(a * 3) \<noteq> 0" 119 by auto 120 have eq: "a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> ?y^3 + 3 * ?p * ?y - 2 * ?q = 0" 121 by (rule cubic_reduction) (auto simp add: field_simps zero a0) 122 have "csqrt 3^2 = 3" by (rule power2_csqrt) 123 then have th0: 124 "?s^2 = ?q^2 + ?p ^ 3 \<and> ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \<and> 125 ?s2 = - ?s1 * (1 + \<i> * csqrt 3) / 2 \<and> 126 ?s3 = - ?s1 * (1 - \<i> * csqrt 3) / 2 \<and> 127 \<i>^2 + 1 = 0 \<and> csqrt 3^2 = 3" 128 using zero by (simp add: field_simps ccbrt) 129 from cubic_basic[OF th0, of ?y] 130 show ?thesis 131 apply (simp only: Let_def eq) 132 using zero apply (simp add: field_simps ccbrt) 133 using zero 134 apply (cases "a * (c * 3) = b^2") 135 apply (simp_all add: field_simps) 136 done 137qed 138 139 140section \<open>The Quartic Formula\<close> 141 142lemma quartic: 143 "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \<and> 144 R^2 = a^2 / 4 - b + y \<and> 145 s^2 = y^2 - 4 * d \<and> 146 (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s 147 else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \<and> 148 (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s 149 else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R))) 150 \<Longrightarrow> x^4 + a * x^3 + b * x^2 + c * x + d = 0 \<longleftrightarrow> 151 x = -a / 4 + R / 2 + D / 2 \<or> 152 x = -a / 4 + R / 2 - D / 2 \<or> 153 x = -a / 4 - R / 2 + E / 2 \<or> 154 x = -a / 4 - R / 2 - E / 2" 155 apply (cases "R = 0") 156 apply (simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left) 157 apply algebra 158 apply algebra 159 done 160 161end 162