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