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