Theory Cubic_Quartic

(*  Title:      HOL/ex/Cubic_Quartic.thy
    Author:     Amine Chaieb
*)

section ‹The Cubic and Quartic Root Formulas›

theory Cubic_Quartic
imports Complex_Main
begin

section ‹The Cubic Formula›

definition "ccbrt z = (SOME (w::complex). w^3 = z)"

lemma ccbrt: "(ccbrt z) ^ 3 = z"
proof -
  from rcis_Ex obtain r a where ra: "z = rcis r a"
    by blast
  let ?r' = "if r < 0 then - root 3 (-r) else root 3 r"
  let ?a' = "a/3"
  have "rcis ?r' ?a' ^ 3 = rcis r a"
    by (cases "r < 0") (simp_all add: DeMoivre2)
  then have *: "∃w. w^3 = z"
    unfolding ra by blast
  from someI_ex [OF *] show ?thesis
    unfolding ccbrt_def by blast
qed


text ‹The reduction to a simpler form:›

lemma cubic_reduction:
  fixes a :: complex
  assumes
    "a ≠ 0 ∧ x = y - b / (3 * a) ∧  p = (3* a * c - b^2) / (9 * a^2) ∧
      q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
  shows "a * x^3 + b * x^2 + c * x + d = 0 ⟷ y^3 + 3 * p * y - 2 * q = 0"
proof -
  from assms have "3 * a ≠ 0" "9 * a^2 ≠ 0" "54 * a^3 ≠ 0" by auto
  then have *:
      "x = y - b / (3 * a) ⟷ (3*a) * x = (3*a) * y - b"
      "p = (3* a * c - b^2) / (9 * a^2) ⟷ (9 * a^2) * p = (3* a * c - b^2)"
      "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) ⟷
        (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)"
    by (simp_all add: field_simps)
  from assms [unfolded *] show ?thesis
    by algebra
qed


text ‹The solutions of the special form:›

lemma cubic_basic:
  fixes s :: complex
  assumes
    "s^2 = q^2 + p^3 ∧
      s1^3 = (if p = 0 then 2 * q else q + s) ∧
      s2 = -s1 * (1 + i * t) / 2 ∧
      s3 = -s1 * (1 - i * t) / 2 ∧
      i^2 + 1 = 0 ∧
      t^2 = 3"
  shows
    "if p = 0
     then y^3 + 3 * p * y - 2 * q = 0 ⟷ y = s1 ∨ y = s2 ∨ y = s3
     else s1 ≠ 0 ∧
      (y^3 + 3 * p * y - 2 * q = 0 ⟷ (y = s1 - p / s1 ∨ y = s2 - p / s2 ∨ y = s3 - p / s3))"
proof (cases "p = 0")
  case True
  with assms show ?thesis
    by (simp add: field_simps) algebra
next
  case False
  with assms have *: "s1 ≠ 0" by (simp add: field_simps) algebra
  with assms False have "s2 ≠ 0" "s3 ≠ 0"
    by (simp_all add: field_simps) algebra+
  with * have **:
      "y = s1 - p / s1 ⟷ s1 * y = s1^2 - p"
      "y = s2 - p / s2 ⟷ s2 * y = s2^2 - p"
      "y = s3 - p / s3 ⟷ s3 * y = s3^2 - p"
    by (simp_all add: field_simps power2_eq_square)
  from assms False show ?thesis
    unfolding ** by (simp add: field_simps) algebra
qed


text ‹Explicit formula for the roots:›

lemma cubic:
  assumes a0: "a ≠ 0"
  shows
    "let
      p = (3 * a * c - b^2) / (9 * a^2);
      q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3);
      s = csqrt(q^2 + p^3);
      s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s));
      s2 = -s1 * (1 + 𝗂 * csqrt 3) / 2;
      s3 = -s1 * (1 - 𝗂 * csqrt 3) / 2
     in
      if p = 0 then
        a * x^3 + b * x^2 + c * x + d = 0 ⟷
          x = s1 - b / (3 * a) ∨
          x = s2 - b / (3 * a) ∨
          x = s3 - b / (3 * a)
      else
        s1 ≠ 0 ∧
          (a * x^3 + b * x^2 + c * x + d = 0 ⟷
            x = s1 - p / s1 - b / (3 * a) ∨
            x = s2 - p / s2 - b / (3 * a) ∨
            x = s3 - p / s3 - b / (3 * a))"
proof -
  let ?p = "(3 * a * c - b^2) / (9 * a^2)"
  let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)"
  let ?s = "csqrt (?q^2 + ?p^3)"
  let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)"
  let ?s2 = "- ?s1 * (1 + 𝗂 * csqrt 3) / 2"
  let ?s3 = "- ?s1 * (1 - 𝗂 * csqrt 3) / 2"
  let ?y = "x + b / (3 * a)"
  from a0 have zero: "9 * a^2 ≠ 0" "a^3 * 54 ≠ 0" "(a * 3) ≠ 0"
    by auto
  have eq: "a * x^3 + b * x^2 + c * x + d = 0 ⟷ ?y^3 + 3 * ?p * ?y - 2 * ?q = 0"
    by (rule cubic_reduction) (auto simp add: field_simps zero a0)
  have "csqrt 3^2 = 3" by (rule power2_csqrt)
  then have th0:
    "?s^2 = ?q^2 + ?p ^ 3 ∧ ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) ∧
      ?s2 = - ?s1 * (1 + 𝗂 * csqrt 3) / 2 ∧
      ?s3 = - ?s1 * (1 - 𝗂 * csqrt 3) / 2 ∧
      𝗂^2 + 1 = 0 ∧ csqrt 3^2 = 3"
    using zero by (simp add: field_simps ccbrt)
  from cubic_basic[OF th0, of ?y]
  show ?thesis
    apply (simp only: Let_def eq)
    using zero apply (simp add: field_simps ccbrt)
    using zero
    apply (cases "a * (c * 3) = b^2")
    apply (simp_all add: field_simps)
    done
qed


section ‹The Quartic Formula›

lemma quartic:
  "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 ∧
    R^2 = a^2 / 4 - b + y ∧
    s^2 = y^2 - 4 * d ∧
    (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s
                     else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) ∧
    (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s
                     else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R)))
  ⟹ x^4 + a * x^3 + b * x^2 + c * x + d = 0 ⟷
      x = -a / 4 + R / 2 + D / 2 ∨
      x = -a / 4 + R / 2 - D / 2 ∨
      x = -a / 4 - R / 2 + E / 2 ∨
      x = -a / 4 - R / 2 - E / 2"
  apply (cases "R = 0")
   apply (simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left)
   apply algebra
  apply algebra
  done

end