src/HOL/ex/Cubic_Quartic.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 63054 1b237d147cc4 child 63589 58aab4745e85 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Title:      HOL/ex/Cubic_Quartic.thy
```
```     2     Author:     Amine Chaieb
```
```     3 *)
```
```     4
```
```     5 section \<open>The Cubic and Quartic Root Formulas\<close>
```
```     6
```
```     7 theory Cubic_Quartic
```
```     8 imports Complex_Main
```
```     9 begin
```
```    10
```
```    11 section \<open>The Cubic Formula\<close>
```
```    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"
```
```    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
```
```    27 qed
```
```    28
```
```    29
```
```    30 text \<open>The reduction to a simpler form:\<close>
```
```    31
```
```    32 lemma 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"
```
```    38 proof -
```
```    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
```
```    48 qed
```
```    49
```
```    50
```
```    51 text \<open>The solutions of the special form:\<close>
```
```    52
```
```    53 lemma 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))"
```
```    67 proof (cases "p = 0")
```
```    68   case True
```
```    69   with assms show ?thesis
```
```    70     by (simp add: field_simps) algebra
```
```    71 next
```
```    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
```
```    83 qed
```
```    84
```
```    85
```
```    86 text \<open>Explicit formula for the roots:\<close>
```
```    87
```
```    88 lemma 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 + ii * csqrt 3) / 2;
```
```    97       s3 = -s1 * (1 - ii * 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))"
```
```   110 proof -
```
```   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 + ii * csqrt 3) / 2"
```
```   116   let ?s3 = "- ?s1 * (1 - ii * 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 + ii * csqrt 3) / 2 \<and>
```
```   126       ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \<and>
```
```   127       ii^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
```
```   137 qed
```
```   138
```
```   139
```
```   140 section \<open>The Quartic Formula\<close>
```
```   141
```
```   142 lemma 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
```
```   161 end
```