[STATEMENT]
lemma solve_depressed_cubic_Cardano_real:
  assumes "solve_depressed_cubic_Cardano_real e f = Some y"
  shows "{y. y^3 + e * y + f = 0} = {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
proof (cases "e = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. e = 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
 2. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
e = 0

goal (2 subgoals):
 1. e = 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
 2. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
have "{y. y^3 + e * y + f = 0} = {y. y^3 = -f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. y ^ 3 + e * y + f = 0} = {y. y ^ 3 = - f}
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. y ^ 3 + 0 * y + f = 0} = {y. y ^ 3 = - f}
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
{y. y ^ 3 + e * y + f = 0} = {y. y ^ 3 = - f}

goal (2 subgoals):
 1. e = 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
 2. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y. y ^ 3 + e * y + f = 0} = {y. y ^ 3 = - f}

goal (2 subgoals):
 1. e = 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
 2. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
have "\<dots> = {root 3 (-f)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. y ^ 3 = - f} = {root 3 (- f)}
[PROOF STEP]
using odd_real_root_unique[of 3 _ "-f"] odd_real_root_pow[of 3]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>odd 3; ?y ^ 3 = - f\<rbrakk> \<Longrightarrow> root 3 (- f) = ?y
odd 3 \<Longrightarrow> root 3 ?x ^ 3 = ?x

goal (1 subgoal):
 1. {y. y ^ 3 = - f} = {root 3 (- f)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y. y ^ 3 = - f} = {root 3 (- f)}

goal (2 subgoals):
 1. e = 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
 2. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y. y ^ 3 = - f} = {root 3 (- f)}

goal (2 subgoals):
 1. e = 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
 2. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
have "root 3 (-f) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root 3 (- f) = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
solve_depressed_cubic_Cardano_real e f = Some y

goal (1 subgoal):
 1. root 3 (- f) = y
[PROOF STEP]
unfolding True solve_depressed_cubic_Cardano_real_def
[PROOF STATE]
proof (prove)
using this:
(if 0 = 0 then Some (root 3 (- f)) else let v = - (0 ^ 3 / 27) in case rroots2 [:v, f, 1:] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> let rt = root 3 u in Some (rt - 0 / (3 * rt)) | u # xa # ab # x \<Rightarrow> Map.empty x) = Some y

goal (1 subgoal):
 1. root 3 (- f) = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
root 3 (- f) = y

goal (2 subgoals):
 1. e = 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
 2. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{y. y ^ 3 + e * y + f = 0} = {y}

goal (1 subgoal):
 1. {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{y. y ^ 3 + e * y + f = 0} = {y}

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
e \<noteq> 0

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
define v where "v = - (e ^ 3 / 27)"
[PROOF STATE]
proof (state)
this:
v = - (e ^ 3 / 27)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
note * = assms[unfolded solve_depressed_cubic_Cardano_real_def Let_def, folded v_def]
[PROOF STATE]
proof (state)
this:
(if e = 0 then Some (root 3 (- f)) else case rroots2 [:v, f, 1:] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> Some (root 3 u - e / (3 * root 3 u)) | u # xa # ab # x \<Rightarrow> Map.empty x) = Some y

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
let ?rr = "rroots2 [:v,f,1:]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
from * False
[PROOF STATE]
proof (chain)
picking this:
(if e = 0 then Some (root 3 (- f)) else case rroots2 [:v, f, 1:] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> Some (root 3 u - e / (3 * root 3 u)) | u # xa # ab # x \<Rightarrow> Map.empty x) = Some y
e \<noteq> 0
[PROOF STEP]
obtain u u' where rr: "?rr = [u,u']"
[PROOF STATE]
proof (prove)
using this:
(if e = 0 then Some (root 3 (- f)) else case rroots2 [:v, f, 1:] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> Some (root 3 u - e / (3 * root 3 u)) | u # xa # ab # x \<Rightarrow> Map.empty x) = Some y
e \<noteq> 0

goal (1 subgoal):
 1. (\<And>u u'. rroots2 [:v, f, 1:] = [u, u'] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ?rr; cases "tl ?rr"; cases "tl (tl ?rr)"; auto split: if_splits)
[PROOF STATE]
proof (state)
this:
rroots2 [:v, f, 1:] = [u, u']

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
from *[unfolded rr list.simps] False
[PROOF STATE]
proof (chain)
picking this:
(if e = 0 then Some (root 3 (- f)) else Some (root 3 u - e / (3 * root 3 u))) = Some y
e \<noteq> 0
[PROOF STEP]
have y: "y = root 3 u - e / (3 * root 3 u)"
[PROOF STATE]
proof (prove)
using this:
(if e = 0 then Some (root 3 (- f)) else Some (root 3 u - e / (3 * root 3 u))) = Some y
e \<noteq> 0

goal (1 subgoal):
 1. y = root 3 u - e / (3 * root 3 u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = root 3 u - e / (3 * root 3 u)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
have "u \<in> set (rroots2 [:v,f,1:])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> set (rroots2 [:v, f, 1:])
[PROOF STEP]
unfolding rr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> set [u, u']
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> set (rroots2 [:v, f, 1:])

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u \<in> set (rroots2 [:v, f, 1:])

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
have "set (rroots2 [:v,f,1:]) = {u. poly [:v,f,1:] u = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rroots2 [:v, f, 1:]) = {u. poly [:v, f, 1:] u = 0}
[PROOF STEP]
by (subst rroots2, auto)
[PROOF STATE]
proof (state)
this:
set (rroots2 [:v, f, 1:]) = {u. poly [:v, f, 1:] u = 0}

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u \<in> {u. poly [:v, f, 1:] u = 0}
[PROOF STEP]
have u: "u^2 + f * u + v = 0"
[PROOF STATE]
proof (prove)
using this:
u \<in> {u. poly [:v, f, 1:] u = 0}

goal (1 subgoal):
 1. u\<^sup>2 + f * u + v = 0
[PROOF STEP]
by (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
u\<^sup>2 + f * u + v = 0

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
note Cardano = solve_cubic_depressed_Cardano_real[OF False v_def u]
[PROOF STATE]
proof (state)
this:
(root 3 u - e / (3 * root 3 u)) ^ 3 + e * (root 3 u - e / (3 * root 3 u)) + f = 0
\<lbrakk>discriminant_cubic_depressed e f \<noteq> 0; ?y ^ 3 + e * ?y + f = 0\<rbrakk> \<Longrightarrow> ?y = root 3 u - e / (3 * root 3 u)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
have 2: "2 = Suc (Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 = Suc (Suc 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 = Suc (Suc 0)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
from rr
[PROOF STATE]
proof (chain)
picking this:
rroots2 [:v, f, 1:] = [u, u']
[PROOF STEP]
have 0: "f\<^sup>2 - 4 * v \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
rroots2 [:v, f, 1:] = [u, u']

goal (1 subgoal):
 1. f\<^sup>2 - 4 * v \<noteq> 0
[PROOF STEP]
unfolding rroots2_def Let_def
[PROOF STATE]
proof (prove)
using this:
(if (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] 2))\<^sup>2 - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] 2 = 0 then [- (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] 2))] else if (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] 2))\<^sup>2 - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] 2 < 0 then [] else [- (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] 2)) + sqrt ((coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] 2))\<^sup>2 - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] 2), - (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] 2)) - sqrt ((coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] 2))\<^sup>2 - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] 2)]) = [u, u']

goal (1 subgoal):
 1. f\<^sup>2 - 4 * v \<noteq> 0
[PROOF STEP]
by (auto split: if_splits simp: 2)
[PROOF STATE]
proof (state)
this:
f\<^sup>2 - 4 * v \<noteq> 0

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
hence 0: "discriminant_cubic_depressed e f \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
f\<^sup>2 - 4 * v \<noteq> 0

goal (1 subgoal):
 1. discriminant_cubic_depressed e f \<noteq> 0
[PROOF STEP]
unfolding discriminant_cubic_depressed_def v_def
[PROOF STATE]
proof (prove)
using this:
f\<^sup>2 - 4 * - (e ^ 3 / 27) \<noteq> 0

goal (1 subgoal):
 1. - (4 * e ^ 3 + 27 * f\<^sup>2) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
discriminant_cubic_depressed e f \<noteq> 0

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
using Cardano(1) Cardano(2)[OF 0]
[PROOF STATE]
proof (prove)
using this:
(root 3 u - e / (3 * root 3 u)) ^ 3 + e * (root 3 u - e / (3 * root 3 u)) + f = 0
?y ^ 3 + e * ?y + f = 0 \<Longrightarrow> ?y = root 3 u - e / (3 * root 3 u)

goal (1 subgoal):
 1. {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
unfolding y[symmetric]
[PROOF STATE]
proof (prove)
using this:
y ^ 3 + e * y + f = 0
?y ^ 3 + e * ?y + f = 0 \<Longrightarrow> ?y = y

goal (1 subgoal):
 1. {y. y ^ 3 + e * y + f = 0} = {y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{y. y ^ 3 + e * y + f = 0} = {y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solve_depressed_cubic_complex_code[code]:
  "solve_depressed_cubic_complex e f = (let
          ys = (if e = 0 then all_croots 3 (- f) else (let
            f2 = f / 2;
            u = - f2 + csqrt (f2^2 + e ^ 3 / 27);
            zs = all_croots 3 u
            in map (\<lambda> z. z - e / (3 * z)) zs))
      in remdups ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solve_depressed_cubic_complex e f = Let (if e = 0 then all_croots 3 (- f) else let f2 = f / 2; u = - f2 + csqrt (f2\<^sup>2 + e ^ 3 / 27) in Let (all_croots 3 u) (map (\<lambda>z. z - e / (3 * z)))) remdups
[PROOF STEP]
unfolding solve_depressed_cubic_complex_def Let_def croots2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remdups (if e = 0 then all_croots 3 (- f) else map (\<lambda>z. z - e / (3 * z)) (all_croots 3 (hd (remdups [- (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) + csqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2), - (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) - csqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2)])))) = remdups (if e = 0 then all_croots 3 (- f) else map (\<lambda>z. z - e / (3 * z)) (all_croots 3 (- (f / 2) + csqrt ((f / 2)\<^sup>2 + e ^ 3 / 27))))
[PROOF STEP]
by (simp add: numeral_2_eq_2)


[STATEMENT]
lemma solve_depressed_cubic_complex: "y \<in> set (solve_depressed_cubic_complex e f)
  \<longleftrightarrow> (y^3 + e * y + f = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
proof (cases "e = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. e = 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
 2. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
e = 0

goal (2 subgoals):
 1. e = 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
 2. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
e = 0

goal (1 subgoal):
 1. (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
by (simp add: solve_depressed_cubic_complex_def Let_def all_croots eq_neg_iff_add_eq_0)
[PROOF STATE]
proof (state)
this:
(y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
case e0: False
[PROOF STATE]
proof (state)
this:
e \<noteq> 0

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
hence id: "(if e = 0 then x else y) = y" for x y :: "complex list"
[PROOF STATE]
proof (prove)
using this:
e \<noteq> 0

goal (1 subgoal):
 1. (if e = 0 then x else y) = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if e = 0 then ?x else ?y) = ?y

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
define v where "v = - (e ^ 3 / 27)"
[PROOF STATE]
proof (state)
this:
v = - (e ^ 3 / 27)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
define p where "p = [:v, f, 1:]"
[PROOF STATE]
proof (state)
this:
p = [:v, f, 1:]

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have p2: "degree p = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree p = 2
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree [:v, f, 1:] = 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree p = 2

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
let ?u = "hd (croots2 p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
define u where "u = ?u"
[PROOF STATE]
proof (state)
this:
u = hd (croots2 p)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have "u \<in> set (croots2 p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> set (croots2 p)
[PROOF STEP]
unfolding croots2_def Let_def u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (remdups [- (coeff p 1 / (2 * coeff p 2)) + csqrt ((coeff p 1 / (2 * coeff p 2))\<^sup>2 - coeff p 0 / coeff p 2), - (coeff p 1 / (2 * coeff p 2)) - csqrt ((coeff p 1 / (2 * coeff p 2))\<^sup>2 - coeff p 0 / coeff p 2)]) \<in> set (remdups [- (coeff p 1 / (2 * coeff p 2)) + csqrt ((coeff p 1 / (2 * coeff p 2))\<^sup>2 - coeff p 0 / coeff p 2), - (coeff p 1 / (2 * coeff p 2)) - csqrt ((coeff p 1 / (2 * coeff p 2))\<^sup>2 - coeff p 0 / coeff p 2)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> set (croots2 p)

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
with croots2[OF p2]
[PROOF STATE]
proof (chain)
picking this:
{x. poly p x = 0} = set (croots2 p)
u \<in> set (croots2 p)
[PROOF STEP]
have "poly p u = 0"
[PROOF STATE]
proof (prove)
using this:
{x. poly p x = 0} = set (croots2 p)
u \<in> set (croots2 p)

goal (1 subgoal):
 1. poly p u = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly p u = 0

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
hence u: "u^2 + f * u + v = 0"
[PROOF STATE]
proof (prove)
using this:
poly p u = 0

goal (1 subgoal):
 1. u\<^sup>2 + f * u + v = 0
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
poly [:v, f, 1:] u = 0

goal (1 subgoal):
 1. u\<^sup>2 + f * u + v = 0
[PROOF STEP]
by (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
u\<^sup>2 + f * u + v = 0

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
note cube_roots = all_croots[of 3, simplified]
[PROOF STATE]
proof (state)
this:
set (all_croots 3 ?x) = {y. y ^ 3 = ?x}

goal (1 subgoal):
 1. e \<noteq> 0 \<Longrightarrow> (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
unfolding solve_depressed_cubic_complex_def Let_def set_remdups set_map id cube_roots
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = hd (croots2 [:- (e ^ 3 / 27), f, 1:])}) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
unfolding v_def[symmetric] p_def[symmetric] set_concat set_map
      u_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have p: "{x. poly p x = 0} = {u. u^2 + f * u + v = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. poly p x = 0} = {u. u\<^sup>2 + f * u + v = 0}
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. poly [:v, f, 1:] x = 0} = {u. u\<^sup>2 + f * u + v = 0}
[PROOF STEP]
by (auto simp: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
{x. poly p x = 0} = {u. u\<^sup>2 + f * u + v = 0}

goal (1 subgoal):
 1. (y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have cube: "\<Union> (set ` all_croots 3 ` {x. poly p x = 0}) = {z. \<exists> u. u\<^sup>2 + f * u + v = 0 \<and> z ^ 3 = u}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set ` all_croots 3 ` {x. poly p x = 0}) = {z. \<exists>u. u\<^sup>2 + f * u + v = 0 \<and> z ^ 3 = u}
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set ` all_croots 3 ` {u. u\<^sup>2 + f * u + v = 0}) = {z. \<exists>u. u\<^sup>2 + f * u + v = 0 \<and> z ^ 3 = u}
[PROOF STEP]
by (auto simp: cube_roots)
[PROOF STATE]
proof (state)
this:
\<Union> (set ` all_croots 3 ` {x. poly p x = 0}) = {z. \<exists>u. u\<^sup>2 + f * u + v = 0 \<and> z ^ 3 = u}

goal (1 subgoal):
 1. (y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
show "(y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
using solve_cubic_depressed_Cardano_complex[OF e0 v_def u] cube
[PROOF STATE]
proof (prove)
using this:
(?y ^ 3 + e * ?y + f = 0) = (\<exists>z. z ^ 3 = u \<and> ?y = z - e / (3 * z))
\<Union> (set ` all_croots 3 ` {x. poly p x = 0}) = {z. \<exists>u. u\<^sup>2 + f * u + v = 0 \<and> z ^ 3 = u}

goal (1 subgoal):
 1. (y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(y \<in> (\<lambda>z. z - e / (3 * z)) ` {y. y ^ 3 = u}) = (y ^ 3 + e * y + f = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(y \<in> set (solve_depressed_cubic_complex e f)) = (y ^ 3 + e * y + f = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solve_depressed_cubic_real_code[code]: "solve_depressed_cubic_real e f =
  (if e = 0 then [root 3 (-f)] else
   let v = e ^ 3 / 27;
       f2 = f / 2;
       f2v = f2^2 + v in
   if f2v > 0 then
     let u = -f2 + sqrt f2v;
         rt = root 3 u
      in [rt - e / (3 * rt)]
  else
  let ce3 = of_real e / 3;
      u = - of_real f2 + csqrt (of_real f2v) in
   map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
have id: "rroots2 [:v, f, 1:] = (let
     f2 = f / 2;
     bac = f2\<^sup>2 - v in
     if bac = 0 then [- f2] else
     if bac < 0 then [] else let e = sqrt bac in [- f2 + e, - f2 - e])" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rroots2 [:v, f, 1:] = (let f2 = f / 2; bac = f2\<^sup>2 - v in if bac = 0 then [- f2] else if bac < 0 then [] else let e = sqrt bac in [- f2 + e, - f2 - e])
[PROOF STEP]
unfolding rroots2_def Let_def numeral_2_eq_2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] (Suc (Suc 0)))) ^ Suc (Suc 0) - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] (Suc (Suc 0)) = 0 then [- (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] (Suc (Suc 0))))] else if (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] (Suc (Suc 0)))) ^ Suc (Suc 0) - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] (Suc (Suc 0)) < 0 then [] else [- (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] (Suc (Suc 0)))) + sqrt ((coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] (Suc (Suc 0)))) ^ Suc (Suc 0) - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] (Suc (Suc 0))), - (coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] (Suc (Suc 0)))) - sqrt ((coeff [:v, f, 1:] 1 / (2 * coeff [:v, f, 1:] (Suc (Suc 0)))) ^ Suc (Suc 0) - coeff [:v, f, 1:] 0 / coeff [:v, f, 1:] (Suc (Suc 0)))]) = (if (f / 2) ^ Suc (Suc 0) - v = 0 then [- (f / 2)] else if (f / 2) ^ Suc (Suc 0) - v < 0 then [] else [- (f / 2) + sqrt ((f / 2) ^ Suc (Suc 0) - v), - (f / 2) - sqrt ((f / 2) ^ Suc (Suc 0) - v)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rroots2 [:?v, f, 1:] = (let f2 = f / 2; bac = f2\<^sup>2 - ?v in if bac = 0 then [- f2] else if bac < 0 then [] else let e = sqrt bac in [- f2 + e, - f2 - e])

goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
define foo :: "real \<Rightarrow> real \<Rightarrow> real option" where
    "foo f2v f2 = (case (if f2v = 0 then [- f2] else []) of [] \<Rightarrow> None | _ \<Rightarrow> None)"
    for f2v f2
[PROOF STATE]
proof (state)
this:
foo ?f2v ?f2.0 = (case if ?f2v = 0 then [- ?f2.0] else [] of [] \<Rightarrow> None | a # x \<Rightarrow> Map.empty x)

goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
have "solve_depressed_cubic_real e f = (if e = 0 then [root 3 (-f)] else
   let v = e ^ 3 / 27;
       f2 = f / 2;
       f2v = f2\<^sup>2 + v in
   if f2v > 0 then
     let u = -f2 + sqrt f2v;
         rt = root 3 u
      in [rt - e / (3 * rt)]
  else
  (case foo f2v f2 of
     None \<Rightarrow> let u = - cor f2 + csqrt (cor f2v) in
   map Re
    (remdups (map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 u)))
   | Some y \<Rightarrow> []))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else case foo f2v f2 of None \<Rightarrow> let u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 u))) | Some y \<Rightarrow> [])
[PROOF STEP]
unfolding solve_depressed_cubic_real_def solve_depressed_cubic_Cardano_real_def
      solve_depressed_cubic_complex_code
      Let_def id foo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case if e = 0 then Some (root 3 (- f)) else case if (f / 2)\<^sup>2 - - (e ^ 3 / 27) = 0 then [- (f / 2)] else if (f / 2)\<^sup>2 - - (e ^ 3 / 27) < 0 then [] else [- (f / 2) + sqrt ((f / 2)\<^sup>2 - - (e ^ 3 / 27)), - (f / 2) - sqrt ((f / 2)\<^sup>2 - - (e ^ 3 / 27))] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> Some (root 3 u - e / (3 * root 3 u)) | u # xa # ab # x \<Rightarrow> Map.empty x of None \<Rightarrow> map Re (remdups (if cor e = 0 then all_croots 3 (- cor f) else map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 (- (cor f / 2) + csqrt ((cor f / 2)\<^sup>2 + cor e ^ 3 / 27))))) | Some y \<Rightarrow> [y]) = (if e = 0 then [root 3 (- f)] else if 0 < (f / 2)\<^sup>2 + e ^ 3 / 27 then [root 3 (- (f / 2) + sqrt ((f / 2)\<^sup>2 + e ^ 3 / 27)) - e / (3 * root 3 (- (f / 2) + sqrt ((f / 2)\<^sup>2 + e ^ 3 / 27)))] else case case if (f / 2)\<^sup>2 + e ^ 3 / 27 = 0 then [- (f / 2)] else [] of [] \<Rightarrow> None | a # x \<Rightarrow> Map.empty x of None \<Rightarrow> map Re (remdups (map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 (- cor (f / 2) + csqrt (cor ((f / 2)\<^sup>2 + e ^ 3 / 27)))))) | Some y \<Rightarrow> [])
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else case foo f2v f2 of None \<Rightarrow> let u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 u))) | Some y \<Rightarrow> [])

goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else case foo f2v f2 of None \<Rightarrow> let u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 u))) | Some y \<Rightarrow> [])

goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
have id: "foo f2v f2 = None"
    for f2v f2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foo f2v f2 = None
[PROOF STEP]
unfolding foo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case if f2v = 0 then [- f2] else [] of [] \<Rightarrow> None | a # x \<Rightarrow> Map.empty x) = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foo ?f2v ?f2.0 = None

goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else case foo f2v f2 of None \<Rightarrow> let u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 u))) | Some y \<Rightarrow> [])
foo ?f2v ?f2.0 = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else case foo f2v f2 of None \<Rightarrow> let u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>z. z - cor e / (3 * z)) (all_croots 3 u))) | Some y \<Rightarrow> [])
foo ?f2v ?f2.0 = None

goal (1 subgoal):
 1. solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
solve_depressed_cubic_real e f = (if e = 0 then [root 3 (- f)] else let v = e ^ 3 / 27; f2 = f / 2; f2v = f2\<^sup>2 + v in if 0 < f2v then let u = - f2 + sqrt f2v; rt = root 3 u in [rt - e / (3 * rt)] else let ce3 = cor e / 3; u = - cor f2 + csqrt (cor f2v) in map Re (remdups (map (\<lambda>rt. rt - ce3 / rt) (all_croots 3 u))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solve_depressed_cubic_real: "y \<in> set (solve_depressed_cubic_real e f)
  \<longleftrightarrow> (y^3 + e * y + f = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
proof (cases "solve_depressed_cubic_Cardano_real e f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
 2. \<And>a. solve_depressed_cubic_Cardano_real e f = Some a \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
case (Some x)
[PROOF STATE]
proof (state)
this:
solve_depressed_cubic_Cardano_real e f = Some x

goal (2 subgoals):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
 2. \<And>a. solve_depressed_cubic_Cardano_real e f = Some a \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
unfolding solve_depressed_cubic_real_def Some option.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> set [x]) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
using solve_depressed_cubic_Cardano_real[OF Some]
[PROOF STATE]
proof (prove)
using this:
{y. y ^ 3 + e * y + f = 0} = {x}

goal (1 subgoal):
 1. (y \<in> set [x]) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
solve_depressed_cubic_Cardano_real e f = None

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
from this[unfolded solve_depressed_cubic_Cardano_real_def Let_def rroots2_def]
[PROOF STATE]
proof (chain)
picking this:
(if e = 0 then Some (root 3 (- f)) else case if (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2 = 0 then [- (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))] else if (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2 < 0 then [] else [- (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) + sqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2), - (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) - sqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2)] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> Some (root 3 u - e / (3 * root 3 u)) | u # xa # ab # x \<Rightarrow> Map.empty x) = None
[PROOF STEP]
have disc: "0 \<le> discriminant_cubic_depressed e f"
[PROOF STATE]
proof (prove)
using this:
(if e = 0 then Some (root 3 (- f)) else case if (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2 = 0 then [- (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))] else if (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2 < 0 then [] else [- (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) + sqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2), - (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) - sqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2)] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> Some (root 3 u - e / (3 * root 3 u)) | u # xa # ab # x \<Rightarrow> Map.empty x) = None

goal (1 subgoal):
 1. 0 \<le> discriminant_cubic_depressed e f
[PROOF STEP]
unfolding discriminant_cubic_depressed_def
[PROOF STATE]
proof (prove)
using this:
(if e = 0 then Some (root 3 (- f)) else case if (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2 = 0 then [- (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))] else if (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2 < 0 then [] else [- (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) + sqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2), - (coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2)) - sqrt ((coeff [:- (e ^ 3 / 27), f, 1:] 1 / (2 * coeff [:- (e ^ 3 / 27), f, 1:] 2))\<^sup>2 - coeff [:- (e ^ 3 / 27), f, 1:] 0 / coeff [:- (e ^ 3 / 27), f, 1:] 2)] of [] \<Rightarrow> None | [u] \<Rightarrow> None | [u, xa] \<Rightarrow> Some (root 3 u - e / (3 * root 3 u)) | u # xa # ab # x \<Rightarrow> Map.empty x) = None

goal (1 subgoal):
 1. 0 \<le> - (4 * e ^ 3 + 27 * f\<^sup>2)
[PROOF STEP]
by (auto split: if_splits simp: numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
0 \<le> discriminant_cubic_depressed e f

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
let ?c = "complex_of_real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
let ?y = "?c y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
let ?e = "?c e"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
let ?f = "?c f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have sub: "set (solve_depressed_cubic_complex ?e ?f) \<subseteq> \<real>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (solve_depressed_cubic_complex (cor e) (cor f)) \<subseteq> \<real>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (solve_depressed_cubic_complex (cor e) (cor f)) \<Longrightarrow> x \<in> \<real>
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (solve_depressed_cubic_complex (cor e) (cor f)) \<Longrightarrow> x \<in> \<real>
[PROOF STEP]
assume y: "y \<in> set (solve_depressed_cubic_complex ?e ?f)"
[PROOF STATE]
proof (state)
this:
y \<in> set (solve_depressed_cubic_complex (cor e) (cor f))

goal (1 subgoal):
 1. \<And>x. x \<in> set (solve_depressed_cubic_complex (cor e) (cor f)) \<Longrightarrow> x \<in> \<real>
[PROOF STEP]
show "y \<in> \<real>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> \<real>
[PROOF STEP]
by (rule solve_cubic_depressed_Cardano_all_real_roots[OF disc y[unfolded solve_depressed_cubic_complex]])
[PROOF STATE]
proof (state)
this:
y \<in> \<real>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (solve_depressed_cubic_complex (cor e) (cor f)) \<subseteq> \<real>

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have "y^3 + e * y + f = 0 \<longleftrightarrow> (?c (y^3 + e * y + f) = ?c 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y ^ 3 + e * y + f = 0) = (cor (y ^ 3 + e * y + f) = cor 0)
[PROOF STEP]
unfolding of_real_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y ^ 3 + e * y + f = 0) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(y ^ 3 + e * y + f = 0) = (cor (y ^ 3 + e * y + f) = cor 0)

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y ^ 3 + e * y + f = 0) = (cor (y ^ 3 + e * y + f) = cor 0)

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?y^3 + ?e * ?y + ?f = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cor (y ^ 3 + e * y + f) = cor 0) = (cor y ^ 3 + cor e * cor y + cor f = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(cor (y ^ 3 + e * y + f) = cor 0) = (cor y ^ 3 + cor e * cor y + cor f = 0)

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cor (y ^ 3 + e * y + f) = cor 0) = (cor y ^ 3 + cor e * cor y + cor f = 0)

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?y \<in> set (solve_depressed_cubic_complex ?e ?f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cor y ^ 3 + cor e * cor y + cor f = 0) = (cor y \<in> set (solve_depressed_cubic_complex (cor e) (cor f)))
[PROOF STEP]
unfolding solve_depressed_cubic_complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cor y ^ 3 + cor e * cor y + cor f = 0) = (cor y ^ 3 + cor e * cor y + cor f = 0)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(cor y ^ 3 + cor e * cor y + cor f = 0) = (cor y \<in> set (solve_depressed_cubic_complex (cor e) (cor f)))

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cor y ^ 3 + cor e * cor y + cor f = 0) = (cor y \<in> set (solve_depressed_cubic_complex (cor e) (cor f)))

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> y \<in> Re ` set (solve_depressed_cubic_complex ?e ?f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cor y \<in> set (solve_depressed_cubic_complex (cor e) (cor f))) = (y \<in> Re ` set (solve_depressed_cubic_complex (cor e) (cor f)))
[PROOF STEP]
using sub
[PROOF STATE]
proof (prove)
using this:
set (solve_depressed_cubic_complex (cor e) (cor f)) \<subseteq> \<real>

goal (1 subgoal):
 1. (cor y \<in> set (solve_depressed_cubic_complex (cor e) (cor f))) = (y \<in> Re ` set (solve_depressed_cubic_complex (cor e) (cor f)))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(cor y \<in> set (solve_depressed_cubic_complex (cor e) (cor f))) = (y \<in> Re ` set (solve_depressed_cubic_complex (cor e) (cor f)))

goal (1 subgoal):
 1. solve_depressed_cubic_Cardano_real e f = None \<Longrightarrow> (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(y ^ 3 + e * y + f = 0) = (y \<in> Re ` set (solve_depressed_cubic_complex (cor e) (cor f)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(y ^ 3 + e * y + f = 0) = (y \<in> Re ` set (solve_depressed_cubic_complex (cor e) (cor f)))

goal (1 subgoal):
 1. (y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
unfolding solve_depressed_cubic_real_def None
[PROOF STATE]
proof (prove)
using this:
(y ^ 3 + e * y + f = 0) = (y \<in> Re ` set (solve_depressed_cubic_complex (cor e) (cor f)))

goal (1 subgoal):
 1. (y \<in> set (case None of None \<Rightarrow> map Re (solve_depressed_cubic_complex (cor e) (cor f)) | Some y \<Rightarrow> [y])) = (y ^ 3 + e * y + f = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y \<in> set (solve_depressed_cubic_real e f)) = (y ^ 3 + e * y + f = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree3_coeffs: "degree p = 3 \<Longrightarrow>
  \<exists> a b c d. p = [: d, c, b, a :] \<and> a \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree p = 3 \<Longrightarrow> \<exists>a b c d. p = [:d, c, b, a:] \<and> a \<noteq> (0::'a)
[PROOF STEP]
by (metis One_nat_def Suc_1 degree2_coeffs degree_pCons_eq_if nat.inject numeral_3_eq_3 pCons_cases zero_neq_numeral)


[STATEMENT]
lemma roots3_generic: assumes deg: "degree p = 3"
  and solver: "\<And> e f y. y \<in> set (depressed_solver e f) \<longleftrightarrow> y^3 + e * y + f = 0"
  shows "set (roots3_generic depressed_solver p) = {x. poly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
note powers = field_simps power3_eq_cube power2_eq_square
[PROOF STATE]
proof (state)
this:
?a + ?b + ?c = ?a + (?b + ?c)
?a + ?b = ?b + ?a
?b + (?a + ?c) = ?a + (?b + ?c)
?a * ?b * ?c = ?a * (?b * ?c)
?a * ?b = ?b * ?a
?b * (?a * ?c) = ?a * (?b * ?c)
?a - ?b - ?c = ?a - (?b + ?c)
?a + (?b - ?c) = ?a + ?b - ?c
(?a - ?b = ?c) = (?a = ?c + ?b)
(?a = ?c - ?b) = (?a + ?b = ?c)
?a - (?b - ?c) = ?a + ?c - ?b
?a - ?b + ?c = ?a + ?c - ?b
(?a - ?b < ?c) = (?a < ?c + ?b)
(?a < ?c - ?b) = (?a + ?b < ?c)
(?a - ?b \<le> ?c) = (?a \<le> ?c + ?b)
(?a \<le> ?c - ?b) = (?a + ?b \<le> ?c)
NO_MATCH (?x div ?y) ?a \<Longrightarrow> ?a * (?b + ?c) = ?a * ?b + ?a * ?c
NO_MATCH (?x div ?y) ?c \<Longrightarrow> (?a + ?b) * ?c = ?a * ?c + ?b * ?c
NO_MATCH (?x div ?y) ?c \<Longrightarrow> (?a - ?b) * ?c = ?a * ?c - ?b * ?c
NO_MATCH (?x div ?y) ?a \<Longrightarrow> ?a * (?b - ?c) = ?a * ?b - ?a * ?c
inverse ?a = (1::?'a) / ?a
?c \<noteq> (0::?'a) \<Longrightarrow> (?a = ?b / ?c) = (?a * ?c = ?b)
?c \<noteq> (0::?'a) \<Longrightarrow> (?b / ?c = ?a) = (?b = ?a * ?c)
?b \<noteq> (0::?'a) \<Longrightarrow> (- (?a / ?b) = ?c) = (- ?a = ?c * ?b)
?b \<noteq> (0::?'a) \<Longrightarrow> (?c = - (?a / ?b)) = (?c * ?b = - ?a)
?z \<noteq> (0::?'a) \<Longrightarrow> ?x + ?y / ?z = (?x * ?z + ?y) / ?z
?z \<noteq> (0::?'a) \<Longrightarrow> ?x / ?z + ?y = (?x + ?y * ?z) / ?z
?z \<noteq> (0::?'a) \<Longrightarrow> ?x - ?y / ?z = (?x * ?z - ?y) / ?z
?z \<noteq> (0::?'a) \<Longrightarrow> - (?x / ?z) + ?y = (- ?x + ?y * ?z) / ?z
?z \<noteq> (0::?'a) \<Longrightarrow> ?x / ?z - ?y = (?x - ?y * ?z) / ?z
?z \<noteq> (0::?'a) \<Longrightarrow> - (?x / ?z) - ?y = (- ?x - ?y * ?z) / ?z
(0::?'a) < ?c \<Longrightarrow> (?a \<le> ?b / ?c) = (?a * ?c \<le> ?b)
(0::?'a) < ?c \<Longrightarrow> (?a < ?b / ?c) = (?a * ?c < ?b)
?c < (0::?'a) \<Longrightarrow> (?a < ?b / ?c) = (?b < ?a * ?c)
?c < (0::?'a) \<Longrightarrow> (?a \<le> ?b / ?c) = (?b \<le> ?a * ?c)
(0::?'a) < ?c \<Longrightarrow> (?b / ?c \<le> ?a) = (?b \<le> ?a * ?c)
(0::?'a) < ?c \<Longrightarrow> (?b / ?c < ?a) = (?b < ?a * ?c)
?c < (0::?'a) \<Longrightarrow> (?b / ?c \<le> ?a) = (?a * ?c \<le> ?b)
?c < (0::?'a) \<Longrightarrow> (?b / ?c < ?a) = (?a * ?c < ?b)
(0::?'a) < ?c \<Longrightarrow> (?a \<le> - (?b / ?c)) = (?a * ?c \<le> - ?b)
?c < (0::?'a) \<Longrightarrow> (?a \<le> - (?b / ?c)) = (- ?b \<le> ?a * ?c)
(0::?'a) < ?c \<Longrightarrow> (?a < - (?b / ?c)) = (?a * ?c < - ?b)
?c < (0::?'a) \<Longrightarrow> (?a < - (?b / ?c)) = (- ?b < ?a * ?c)
(0::?'a) < ?c \<Longrightarrow> (- (?b / ?c) < ?a) = (- ?b < ?a * ?c)
?c < (0::?'a) \<Longrightarrow> (- (?b / ?c) < ?a) = (?a * ?c < - ?b)
(0::?'a) < ?c \<Longrightarrow> (- (?b / ?c) \<le> ?a) = (- ?b \<le> ?a * ?c)
?c < (0::?'a) \<Longrightarrow> (- (?b / ?c) \<le> ?a) = (?a * ?c \<le> - ?b)
(?a * ?b) ^ ?n = ?a ^ ?n * ?b ^ ?n
inverse ?a ^ ?n = inverse (?a ^ ?n)
((1::?'a) / ?a) ^ ?n = (1::?'a) / ?a ^ ?n
(?a / ?b) ^ ?n = ?a ^ ?n / ?b ^ ?n
inverse ?x powi ?n = inverse (?x powi ?n)
((1::?'a) / ?x) powi ?n = (1::?'a) / ?x powi ?n
NO_MATCH (?x div ?y) ?c \<Longrightarrow> (?a + ?b) *\<^sub>R ?x = ?a *\<^sub>R ?x + ?b *\<^sub>R ?x
NO_MATCH (?x div ?y) ?a \<Longrightarrow> ?a *\<^sub>R (?x + ?y) = ?a *\<^sub>R ?x + ?a *\<^sub>R ?y
NO_MATCH (?x div ?y) ?c \<Longrightarrow> (?a - ?b) *\<^sub>R ?x = ?a *\<^sub>R ?x - ?b *\<^sub>R ?x
NO_MATCH (?x div ?y) ?a \<Longrightarrow> ?a *\<^sub>R (?x - ?y) = ?a *\<^sub>R ?x - ?a *\<^sub>R ?y
?c \<noteq> 0 \<Longrightarrow> (?a = ?b /\<^sub>R ?c) = (?c *\<^sub>R ?a = ?b)
?c \<noteq> 0 \<Longrightarrow> (?b /\<^sub>R ?c = ?a) = (?b = ?c *\<^sub>R ?a)
?c \<noteq> 0 \<Longrightarrow> ?a + ?b /\<^sub>R ?c = (?c *\<^sub>R ?a + ?b) /\<^sub>R ?c
?c \<noteq> 0 \<Longrightarrow> ?a /\<^sub>R ?c + ?b = (?a + ?c *\<^sub>R ?b) /\<^sub>R ?c
?c \<noteq> 0 \<Longrightarrow> ?a - ?b /\<^sub>R ?c = (?c *\<^sub>R ?a - ?b) /\<^sub>R ?c
?c \<noteq> 0 \<Longrightarrow> ?a /\<^sub>R ?c - ?b = (?a - ?c *\<^sub>R ?b) /\<^sub>R ?c
?c \<noteq> 0 \<Longrightarrow> - (?a /\<^sub>R ?c) + ?b = (- ?a + ?c *\<^sub>R ?b) /\<^sub>R ?c
?c \<noteq> 0 \<Longrightarrow> - (?a /\<^sub>R ?c) - ?b = (- ?a - ?c *\<^sub>R ?b) /\<^sub>R ?c
0 < ?c \<Longrightarrow> (?a \<le> ?b /\<^sub>R ?c) = (?c *\<^sub>R ?a \<le> ?b)
0 < ?c \<Longrightarrow> (?a < ?b /\<^sub>R ?c) = (?c *\<^sub>R ?a < ?b)
0 < ?c \<Longrightarrow> (?b /\<^sub>R ?c \<le> ?a) = (?b \<le> ?c *\<^sub>R ?a)
0 < ?c \<Longrightarrow> (?b /\<^sub>R ?c < ?a) = (?b < ?c *\<^sub>R ?a)
0 < ?c \<Longrightarrow> (?a \<le> - (?b /\<^sub>R ?c)) = (?c *\<^sub>R ?a \<le> - ?b)
0 < ?c \<Longrightarrow> (?a < - (?b /\<^sub>R ?c)) = (?c *\<^sub>R ?a < - ?b)
0 < ?c \<Longrightarrow> (- (?b /\<^sub>R ?c) \<le> ?a) = (- ?b \<le> ?c *\<^sub>R ?a)
0 < ?c \<Longrightarrow> (- (?b /\<^sub>R ?c) < ?a) = (- ?b < ?c *\<^sub>R ?a)
?c < 0 \<Longrightarrow> (?a \<le> ?b /\<^sub>R ?c) = (?b \<le> ?c *\<^sub>R ?a)
?c < 0 \<Longrightarrow> (?a < ?b /\<^sub>R ?c) = (?b < ?c *\<^sub>R ?a)
?c < 0 \<Longrightarrow> (?b /\<^sub>R ?c \<le> ?a) = (?c *\<^sub>R ?a \<le> ?b)
?c < 0 \<Longrightarrow> (?b /\<^sub>R ?c < ?a) = (?c *\<^sub>R ?a < ?b)
?c < 0 \<Longrightarrow> (?a \<le> - (?b /\<^sub>R ?c)) = (- ?b \<le> ?c *\<^sub>R ?a)
?c < 0 \<Longrightarrow> (?a < - (?b /\<^sub>R ?c)) = (- ?b < ?c *\<^sub>R ?a)
?c < 0 \<Longrightarrow> (- (?b /\<^sub>R ?c) \<le> ?a) = (?c *\<^sub>R ?a \<le> - ?b)
?c < 0 \<Longrightarrow> (- (?b /\<^sub>R ?c) < ?a) = (?c *\<^sub>R ?a < - ?b)
?a ^ 3 = ?a * ?a * ?a
?a\<^sup>2 = ?a * ?a

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
from degree3_coeffs[OF deg]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b c d. p = [:d, c, b, a:] \<and> a \<noteq> (0::'a)
[PROOF STEP]
obtain a b c d where
    p: "p = [:d,c,b,a:]" and a: "a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b c d. p = [:d, c, b, a:] \<and> a \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<And>d c b a. \<lbrakk>p = [:d, c, b, a:]; a \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = [:d, c, b, a:]
a \<noteq> (0::'a)

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
have coeffs: "coeffs p ! 3 = a" "coeffs p ! 2 = b" "coeffs p ! 1 = c" "coeffs p ! 0 = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (coeffs p ! 3 = a &&& coeffs p ! 2 = b) &&& coeffs p ! 1 = c &&& coeffs p ! 0 = d
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (coeffs [:d, c, b, a:] ! 3 = a &&& coeffs [:d, c, b, a:] ! 2 = b) &&& coeffs [:d, c, b, a:] ! 1 = c &&& coeffs [:d, c, b, a:] ! 0 = d
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'a)

goal (1 subgoal):
 1. (coeffs [:d, c, b, a:] ! 3 = a &&& coeffs [:d, c, b, a:] ! 2 = b) &&& coeffs [:d, c, b, a:] ! 1 = c &&& coeffs [:d, c, b, a:] ! 0 = d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeffs p ! 3 = a
coeffs p ! 2 = b
coeffs p ! 1 = c
coeffs p ! 0 = d

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
define e where "e = (c - b^2 / (3 * a)) / a"
[PROOF STATE]
proof (state)
this:
e = (c - b\<^sup>2 / ((3::'a) * a)) / a

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
define f where "f = (d + 2 * b^3 / (27 * a^2) - b * c / (3 * a)) / a"
[PROOF STATE]
proof (state)
this:
f = (d + (2::'a) * b ^ 3 / ((27::'a) * a\<^sup>2) - b * c / ((3::'a) * a)) / a

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
note def = roots3_generic_def[of depressed_solver p, unfolded Let_def coeffs,
      folded power3_eq_cube, folded power2_eq_square,  folded e_def f_def]
[PROOF STATE]
proof (state)
this:
roots3_generic depressed_solver p = map (\<lambda>y. y - b / ((3::'a) * a)) (depressed_solver e f)

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
roots3_generic depressed_solver p = map (\<lambda>y. y - b / ((3::'a) * a)) (depressed_solver e f)

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
fix x :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
define y where "y = x + b / (3 * a)"
[PROOF STATE]
proof (state)
this:
y = x + b / ((3::'a) * a)

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
have xy: "x = y - b / (3 * a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y - b / ((3::'a) * a)
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x + b / ((3::'a) * a) - b / ((3::'a) * a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y - b / ((3::'a) * a)

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
have "poly p x = 0 \<longleftrightarrow> a * x^3 + b * x^2 + c * x + d = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly p x = (0::'a)) = (a * x ^ 3 + b * x\<^sup>2 + c * x + d = (0::'a))
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly [:d, c, b, a:] x = (0::'a)) = (a * x ^ 3 + b * x\<^sup>2 + c * x + d = (0::'a))
[PROOF STEP]
by (simp add: powers)
[PROOF STATE]
proof (state)
this:
(poly p x = (0::'a)) = (a * x ^ 3 + b * x\<^sup>2 + c * x + d = (0::'a))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(poly p x = (0::'a)) = (a * x ^ 3 + b * x\<^sup>2 + c * x + d = (0::'a))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (y ^ 3 + e * y + f = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * x ^ 3 + b * x\<^sup>2 + c * x + d = (0::'a)) = (y ^ 3 + e * y + f = (0::'a))
[PROOF STEP]
unfolding to_depressed_cubic[OF a xy e_def f_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y ^ 3 + e * y + f = (0::'a)) = (y ^ 3 + e * y + f = (0::'a))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(a * x ^ 3 + b * x\<^sup>2 + c * x + d = (0::'a)) = (y ^ 3 + e * y + f = (0::'a))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a * x ^ 3 + b * x\<^sup>2 + c * x + d = (0::'a)) = (y ^ 3 + e * y + f = (0::'a))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
have "\<dots> \<longleftrightarrow> y \<in> set (depressed_solver e f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y ^ 3 + e * y + f = (0::'a)) = (y \<in> set (depressed_solver e f))
[PROOF STEP]
unfolding solver
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y ^ 3 + e * y + f = (0::'a)) = (y ^ 3 + e * y + f = (0::'a))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(y ^ 3 + e * y + f = (0::'a)) = (y \<in> set (depressed_solver e f))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(y ^ 3 + e * y + f = (0::'a)) = (y \<in> set (depressed_solver e f))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
have "\<dots> \<longleftrightarrow> x \<in> set (roots3_generic depressed_solver p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> set (depressed_solver e f)) = (x \<in> set (roots3_generic depressed_solver p))
[PROOF STEP]
unfolding xy def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> set (depressed_solver e f)) = (y - b / ((3::'a) * a) \<in> set (map (\<lambda>y. y - b / ((3::'a) * a)) (depressed_solver e f)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y \<in> set (depressed_solver e f)) = (x \<in> set (roots3_generic depressed_solver p))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(poly p x = (0::'a)) = (x \<in> set (roots3_generic depressed_solver p))
[PROOF STEP]
have "poly p x = 0 \<longleftrightarrow> x \<in> set (roots3_generic depressed_solver p)"
[PROOF STATE]
proof (prove)
using this:
(poly p x = (0::'a)) = (x \<in> set (roots3_generic depressed_solver p))

goal (1 subgoal):
 1. (poly p x = (0::'a)) = (x \<in> set (roots3_generic depressed_solver p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(poly p x = (0::'a)) = (x \<in> set (roots3_generic depressed_solver p))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(poly p ?x2 = (0::'a)) = (?x2 \<in> set (roots3_generic depressed_solver p))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(poly p ?x2 = (0::'a)) = (?x2 \<in> set (roots3_generic depressed_solver p))

goal (1 subgoal):
 1. set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (roots3_generic depressed_solver p) = {x. poly p x = (0::'a)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma croots3: assumes deg: "degree p = 3"
  shows "set (croots3 p) = { x. poly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (croots3 p) = {x. poly p x = 0}
[PROOF STEP]
unfolding croots3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (roots3_generic solve_depressed_cubic_complex p) = {x. poly p x = 0}
[PROOF STEP]
by (rule roots3_generic[OF deg solve_depressed_cubic_complex])


[STATEMENT]
lemma rroots3: assumes deg: "degree p = 3"
  shows "set (rroots3 p) = { x. poly p x = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rroots3 p) = {x. poly p x = 0}
[PROOF STEP]
unfolding rroots3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (roots3_generic solve_depressed_cubic_real p) = {x. poly p x = 0}
[PROOF STEP]
by (rule roots3_generic[OF deg solve_depressed_cubic_real])