Theory Complex_Algebraic_Numbers
section ‹Complex Algebraic Numbers›
text ‹Since currently there is no immediate analog of Sturm's theorem for the complex numbers,
we implement complex algebraic numbers via their real and imaginary part.
The major algorithm in this theory is a factorization algorithm which factors a rational
polynomial over the complex numbers.
For factorization of polynomials with complex algebraic coefficients, there
is a separate AFP entry "Factor-Algebraic-Polynomial".›
theory Complex_Algebraic_Numbers
imports
Real_Roots
Complex_Roots_Real_Poly
Compare_Complex
Jordan_Normal_Form.Char_Poly
Berlekamp_Zassenhaus.Code_Abort_Gcd
Interval_Arithmetic
begin
subsection ‹Complex Roots›
hide_const (open) UnivPoly.coeff
hide_const (open) Module.smult
hide_const (open) Coset.order
abbreviation complex_of_int_poly :: "int poly ⇒ complex poly" where
"complex_of_int_poly ≡ map_poly of_int"
abbreviation complex_of_rat_poly :: "rat poly ⇒ complex poly" where
"complex_of_rat_poly ≡ map_poly of_rat"
lemma poly_complex_to_real: "(poly (complex_of_int_poly p) (complex_of_real x) = 0)
= (poly (real_of_int_poly p) x = 0)"
proof -
have id: "of_int = complex_of_real o real_of_int" by auto
interpret cr: semiring_hom complex_of_real by (unfold_locales, auto)
show ?thesis unfolding id
by (subst map_poly_map_poly[symmetric], force+)
qed
lemma represents_cnj: assumes "p represents x" shows "p represents (cnj x)"
proof -
from assms have p: "p ≠ 0" and "ipoly p x = 0" by auto
hence rt: "poly (complex_of_int_poly p) x = 0" by auto
have "poly (complex_of_int_poly p) (cnj x) = 0"
by (rule complex_conjugate_root[OF _ rt], subst coeffs_map_poly, auto)
with p show ?thesis by auto
qed
definition poly_2i :: "int poly" where
"poly_2i ≡ [: 4, 0, 1:]"
lemma represents_2i: "poly_2i represents (2 * 𝗂)"
unfolding represents_def poly_2i_def by simp
definition root_poly_Re :: "int poly ⇒ int poly" where
"root_poly_Re p = cf_pos_poly (poly_mult_rat (inverse 2) (poly_add p p))"
lemma root_poly_Re_code[code]:
"root_poly_Re p = (let fs = coeffs (poly_add p p); k = length fs
in cf_pos_poly (poly_of_list (map (λ(fi, i). fi * 2 ^ i) (zip fs [0..<k]))))"
proof -
have [simp]: "quotient_of (1 / 2) = (1,2)" by eval
show ?thesis unfolding root_poly_Re_def poly_mult_rat_def poly_mult_rat_main_def Let_def by simp
qed
definition root_poly_Im :: "int poly ⇒ int poly list" where
"root_poly_Im p = (let fs = factors_of_int_poly
(poly_add p (poly_uminus p))
in remdups ((if (∃ f ∈ set fs. coeff f 0 = 0) then [[:0,1:]] else [])) @
[ cf_pos_poly (poly_div f poly_2i) . f ← fs, coeff f 0 ≠ 0])"
lemma represents_root_poly:
assumes "ipoly p x = 0" and p: "p ≠ 0"
shows "(root_poly_Re p) represents (Re x)"
and "∃ q ∈ set (root_poly_Im p). q represents (Im x)"
proof -
let ?Rep = "root_poly_Re p"
let ?Imp = "root_poly_Im p"
from assms have ap: "p represents x" by auto
from represents_cnj[OF this] have apc: "p represents (cnj x)" .
from represents_mult_rat[OF _ represents_add[OF ap apc], of "inverse 2"]
have "?Rep represents (1 / 2 * (x + cnj x))" unfolding root_poly_Re_def Let_def
by (auto simp: hom_distribs)
also have "1 / 2 * (x + cnj x) = of_real (Re x)"
by (simp add: complex_add_cnj)
finally have Rep: "?Rep ≠ 0" and rt: "ipoly ?Rep (complex_of_real (Re x)) = 0" unfolding represents_def by auto
from rt[unfolded poly_complex_to_real]
have "ipoly ?Rep (Re x) = 0" .
with Rep show "?Rep represents (Re x)" by auto
let ?q = "poly_add p (poly_uminus p)"
from represents_add[OF ap, of "poly_uminus p" "- cnj x"] represents_uminus[OF apc]
have apq: "?q represents (x - cnj x)" by auto
from factors_int_poly_represents[OF this] obtain pi where pi: "pi ∈ set (factors_of_int_poly ?q)"
and appi: "pi represents (x - cnj x)" and irr_pi: "irreducible pi" by auto
have id: "inverse (2 * 𝗂) * (x - cnj x) = of_real (Im x)"
apply (cases x) by (simp add: complex_split imaginary_unit.ctr legacy_Complex_simps)
from represents_2i have 12: "poly_2i represents (2 * 𝗂)" by simp
have "∃ qi ∈ set ?Imp. qi represents (inverse (2 * 𝗂) * (x - cnj x))"
proof (cases "x - cnj x = 0")
case False
have "poly poly_2i 0 ≠ 0" unfolding poly_2i_def by auto
from represents_div[OF appi 12 this]
represents_irr_non_0[OF irr_pi appi False, unfolded poly_0_coeff_0] pi
show ?thesis unfolding root_poly_Im_def Let_def by (auto intro: bexI[of _ "cf_pos_poly (poly_div pi poly_2i)"])
next
case True
hence id2: "Im x = 0" by (simp add: complex_eq_iff)
from appi[unfolded True represents_def] have "coeff pi 0 = 0" by (cases pi, auto)
with pi have mem: "[:0,1:] ∈ set ?Imp" unfolding root_poly_Im_def Let_def by auto
have "[:0,1:] represents (complex_of_real (Im x))" unfolding id2 represents_def by simp
with mem show ?thesis unfolding id by auto
qed
then obtain qi where qi: "qi ∈ set ?Imp" "qi ≠ 0" and rt: "ipoly qi (complex_of_real (Im x)) = 0"
unfolding id represents_def by auto
from qi rt[unfolded poly_complex_to_real]
show "∃ qi ∈ set ?Imp. qi represents (Im x)" by auto
qed
definition complex_poly :: "int poly ⇒ int poly ⇒ int poly list" where
"complex_poly re im = (let i = [:1,0,1:]
in factors_of_int_poly (poly_add re (poly_mult im i)))"
lemma complex_poly: assumes re: "re represents (Re x)"
and im: "im represents (Im x)"
shows "∃ f ∈ set (complex_poly re im). f represents x" "⋀ f. f ∈ set (complex_poly re im) ⟹ poly_cond f"
proof -
let ?p = "poly_add re (poly_mult im [:1, 0, 1:])"
from re have re: "re represents complex_of_real (Re x)" by simp
from im have im: "im represents complex_of_real (Im x)" by simp
have "[:1,0,1:] represents 𝗂" by auto
from represents_add[OF re represents_mult[OF im this]]
have "?p represents of_real (Re x) + complex_of_real (Im x) * 𝗂" by simp
also have "of_real (Re x) + complex_of_real (Im x) * 𝗂 = x"
by (metis complex_eq mult.commute)
finally have p: "?p represents x" by auto
have "factors_of_int_poly ?p = complex_poly re im"
unfolding complex_poly_def Let_def by simp
from factors_of_int_poly(1)[OF this] factors_of_int_poly(2)[OF this, of x] p
show "∃ f ∈ set (complex_poly re im). f represents x" "⋀ f. f ∈ set (complex_poly re im) ⟹ poly_cond f"
unfolding represents_def by auto
qed
lemma algebraic_complex_iff: "algebraic x = (algebraic (Re x) ∧ algebraic (Im x))"
proof
assume "algebraic x"
from this[unfolded algebraic_altdef_ipoly] obtain p where "ipoly p x = 0" "p ≠ 0" by auto
from represents_root_poly[OF this] show "algebraic (Re x) ∧ algebraic (Im x)"
unfolding represents_def algebraic_altdef_ipoly by auto
next
assume "algebraic (Re x) ∧ algebraic (Im x)"
from this[unfolded algebraic_altdef_ipoly] obtain re im where
"re represents (Re x)" "im represents (Im x)" by blast
from complex_poly[OF this] show "algebraic x"
unfolding represents_def algebraic_altdef_ipoly by auto
qed
definition algebraic_complex :: "complex ⇒ bool" where
[simp]: "algebraic_complex = algebraic"
lemma algebraic_complex_code_unfold[code_unfold]: "algebraic = algebraic_complex" by simp
lemma algebraic_complex_code[code]:
"algebraic_complex x = (algebraic (Re x) ∧ algebraic (Im x))"
unfolding algebraic_complex_def algebraic_complex_iff ..
text ‹Determine complex roots of a polynomial,
intended for polynomials of degree 3 or higher,
for lower degree polynomials use @{const roots1} or @{const croots2}›
hide_const (open) eq
primrec remdups_gen :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
"remdups_gen eq [] = []"
| "remdups_gen eq (x # xs) = (if (∃ y ∈ set xs. eq x y) then
remdups_gen eq xs else x # remdups_gen eq xs)"
lemma real_of_3_remdups_equal_3[simp]: "real_of_3 ` set (remdups_gen equal_3 xs) = real_of_3 ` set xs"
by (induct xs, auto simp: equal_3)
lemma distinct_remdups_equal_3: "distinct (map real_of_3 (remdups_gen equal_3 xs))"
by (induct xs, auto, auto simp: equal_3)
lemma real_of_3_code [code]: "real_of_3 x = real_of (Real_Alg_Quotient x)"
by (transfer, auto)
definition "real_parts_3 p = roots_of_3 (root_poly_Re p)"
definition "pos_imaginary_parts_3 p =
remdups_gen equal_3 (filter (λ x. sgn_3 x = 1) (concat (map roots_of_3 (root_poly_Im p))))"
lemma real_parts_3: assumes p: "p ≠ 0" and "ipoly p x = 0"
shows "Re x ∈ real_of_3 ` set (real_parts_3 p)"
unfolding real_parts_3_def using represents_root_poly(1)[OF assms(2,1)]
roots_of_3(1) unfolding represents_def by auto
lemma distinct_real_parts_3: "distinct (map real_of_3 (real_parts_3 p))"
unfolding real_parts_3_def using roots_of_3(2) .
lemma pos_imaginary_parts_3: assumes p: "p ≠ 0" and "ipoly p x = 0" and "Im x > 0"
shows "Im x ∈ real_of_3 ` set (pos_imaginary_parts_3 p)"
proof -
from represents_root_poly(2)[OF assms(2,1)] obtain q where
q: "q ∈ set (root_poly_Im p)" "q represents Im x" by auto
from roots_of_3(1)[of q] have "Im x ∈ real_of_3 ` set (roots_of_3 q)" using q
unfolding represents_def by auto
then obtain i3 where i3: "i3 ∈ set (roots_of_3 q)" and id: "Im x = real_of_3 i3" by auto
from ‹Im x > 0› have "sgn (Im x) = 1" by simp
hence sgn: "sgn_3 i3 = 1" unfolding id by (metis of_rat_eq_1_iff sgn_3)
show ?thesis unfolding pos_imaginary_parts_3_def real_of_3_remdups_equal_3 id
using sgn i3 q(1) by auto
qed
lemma distinct_pos_imaginary_parts_3: "distinct (map real_of_3 (pos_imaginary_parts_3 p))"
unfolding pos_imaginary_parts_3_def by (rule distinct_remdups_equal_3)
lemma remdups_gen_subset: "set (remdups_gen eq xs) ⊆ set xs"
by (induct xs, auto)
lemma positive_pos_imaginary_parts_3: assumes "x ∈ set (pos_imaginary_parts_3 p)"
shows "0 < real_of_3 x"
proof -
from subsetD[OF remdups_gen_subset assms[unfolded pos_imaginary_parts_3_def]]
have "sgn_3 x = 1" by auto
thus ?thesis using sgn_3[of x] by (simp add: sgn_1_pos)
qed
definition "pair_to_complex ri ≡ case ri of (r,i) ⇒ Complex (real_of_3 r) (real_of_3 i)"
fun get_itvl_2 :: "real_alg_2 ⇒ real interval" where
"get_itvl_2 (Irrational n (p,l,r)) = Interval (of_rat l) (of_rat r)"
| "get_itvl_2 (Rational r) = (let rr = of_rat r in Interval rr rr)"
lemma get_bounds_2: assumes "invariant_2 x"
shows "real_of_2 x ∈⇩i get_itvl_2 x"
proof (cases x)
case (Irrational n plr)
with assms obtain p l r where plr: "plr = (p,l,r)" by (cases plr, auto)
from assms Irrational plr have inv1: "invariant_1 (p,l,r)"
and id: "real_of_2 x = real_of_1 (p,l,r)" by auto
show ?thesis unfolding id using invariant_1D(1)[OF inv1] by (auto simp: plr Irrational)
qed (insert assms, auto simp: Let_def)
lift_definition get_itvl_3 :: "real_alg_3 ⇒ real interval" is get_itvl_2 .
lemma get_itvl_3: "real_of_3 x ∈⇩i get_itvl_3 x"
by (transfer, insert get_bounds_2, auto)
fun tighten_bounds_2 :: "real_alg_2 ⇒ real_alg_2" where
"tighten_bounds_2 (Irrational n (p,l,r)) = (case tighten_poly_bounds p l r (sgn (ipoly p r))
of (l',r',_) ⇒ Irrational n (p,l',r'))"
| "tighten_bounds_2 (Rational r) = Rational r"
lemma tighten_bounds_2: assumes inv: "invariant_2 x"
shows "real_of_2 (tighten_bounds_2 x) = real_of_2 x" "invariant_2 (tighten_bounds_2 x)"
"get_itvl_2 x = Interval l r ⟹
get_itvl_2 (tighten_bounds_2 x) = Interval l' r' ⟹ r' - l' = (r-l) / 2"
proof (atomize(full), cases x)
case (Irrational n plr)
show "real_of_2 (tighten_bounds_2 x) = real_of_2 x ∧
invariant_2 (tighten_bounds_2 x) ∧
(get_itvl_2 x = Interval l r ⟶
get_itvl_2 (tighten_bounds_2 x) = Interval l' r' ⟶ r' - l' = (r - l) / 2)"
proof -
obtain p l r where plr: "plr = (p,l,r)" by (cases plr, auto)
let ?tb = "tighten_poly_bounds p l r (sgn (ipoly p r))"
obtain l' r' sr' where tb: "?tb = (l',r',sr')" by (cases ?tb, auto)
have id: "tighten_bounds_2 x = Irrational n (p,l',r')" unfolding Irrational plr
using tb by auto
from inv[unfolded Irrational plr] have inv: "invariant_1_2 (p, l, r)"
"n = card {y. y ≤ real_of_1 (p, l, r) ∧ ipoly p y = 0}" by auto
have rof: "real_of_2 x = real_of_1 (p, l, r)"
"real_of_2 (tighten_bounds_2 x) = real_of_1 (p, l', r')" using Irrational plr id by auto
from inv have inv1: "invariant_1 (p, l, r)" and "poly_cond2 p" by auto
hence rc: "∃!x. root_cond (p, l, r) x" "poly_cond2 p" by auto
note tb' = tighten_poly_bounds[OF tb rc refl]
have eq: "real_of_1 (p, l, r) = real_of_1 (p, l', r')" using tb' inv1
using invariant_1_sub_interval(2) by presburger
from inv1 tb' have "invariant_1 (p, l', r')" by (metis invariant_1_sub_interval(1))
hence inv2: "invariant_2 (tighten_bounds_2 x)" unfolding id using inv eq by auto
thus ?thesis unfolding rof eq unfolding id unfolding Irrational plr
using tb'(1-4) arg_cong[OF tb'(5), of real_of_rat] by (auto simp: hom_distribs)
qed
qed (auto simp: Let_def)
lift_definition tighten_bounds_3 :: "real_alg_3 ⇒ real_alg_3" is tighten_bounds_2
using tighten_bounds_2 by auto
lemma tighten_bounds_3:
"real_of_3 (tighten_bounds_3 x) = real_of_3 x"
"get_itvl_3 x = Interval l r ⟹
get_itvl_3 (tighten_bounds_3 x) = Interval l' r' ⟹ r' - l' = (r-l) / 2"
by (transfer, insert tighten_bounds_2, auto)+
partial_function (tailrec) filter_list_length
:: "('a ⇒ 'a) ⇒ ('a ⇒ bool) ⇒ nat ⇒ 'a list ⇒ 'a list" where
[code]: "filter_list_length f p n xs = (let ys = filter p xs
in if length ys = n then ys else
filter_list_length f p n (map f ys))"
lemma filter_list_length: assumes "length (filter P xs) = n"
and "⋀ i x. x ∈ set xs ⟹ P x ⟹ p ((f ^^ i) x)"
and "⋀ x. x ∈ set xs ⟹ ¬ P x ⟹ ∃ i. ¬ p ((f ^^ i) x)"
and g: "⋀ x. g (f x) = g x"
and P: "⋀ x. P (f x) = P x"
shows "map g (filter_list_length f p n xs) = map g (filter P xs)"
proof -
from assms(3) have "∀ x. ∃ i. x ∈ set xs ⟶ ¬ P x ⟶ ¬ p ((f ^^ i) x)"
by auto
from choice[OF this] obtain i where i: "⋀ x. x ∈ set xs ⟹ ¬ P x ⟹ ¬ p ((f ^^ (i x)) x)"
by auto
define m where "m = max_list (map i xs)"
have m: "⋀ x. x ∈ set xs ⟹ ¬ P x ⟹ ∃ i ≤ m. ¬ p ((f ^^ i) x)"
using max_list[of _ "map i xs", folded m_def] i by auto
show ?thesis using assms(1-2) m
proof (induct m arbitrary: xs rule: less_induct)
case (less m xs)
define ys where "ys = filter p xs"
have xs_ys: "filter P xs = filter P ys" unfolding ys_def filter_filter
by (rule filter_cong[OF refl], insert less(3)[of _ 0], auto)
have "filter (P ∘ f) ys = filter P ys" using P unfolding o_def by auto
hence id3: "filter P (map f ys) = map f (filter P ys)" unfolding filter_map by simp
hence id2: "map g (filter P (map f ys)) = map g (filter P ys)" by (simp add: g)
show ?case
proof (cases "length ys = n")
case True
hence id: "filter_list_length f p n xs = ys" unfolding ys_def
filter_list_length.simps[of _ _ _ xs] Let_def by auto
show ?thesis using True unfolding id xs_ys using less(2)
by (metis filter_id_conv length_filter_less less_le xs_ys)
next
case False
{
assume "m = 0"
from less(4)[unfolded this] have Pp: "x ∈ set xs ⟹ ¬ P x ⟹ ¬ p x" for x by auto
with xs_ys False[folded less(2)] have False
by (metis (mono_tags, lifting) filter_True mem_Collect_eq set_filter ys_def)
} note m0 = this
then obtain M where mM: "m = Suc M" by (cases m, auto)
hence m: "M < m" by simp
from False have id: "filter_list_length f p n xs = filter_list_length f p n (map f ys)"
unfolding ys_def filter_list_length.simps[of _ _ _ xs] Let_def by auto
show ?thesis unfolding id xs_ys id2[symmetric]
proof (rule less(1)[OF m])
fix y
assume "y ∈ set (map f ys)"
then obtain x where x: "x ∈ set xs" "p x" and y: "y = f x" unfolding ys_def by auto
{
assume "¬ P y"
hence "¬ P x" unfolding y P .
from less(4)[OF x(1) this] obtain i where i: "i ≤ m" and p: "¬ p ((f ^^ i) x)" by auto
with x obtain j where ij: "i = Suc j" by (cases i, auto)
with i have j: "j ≤ M" unfolding mM by auto
have "¬ p ((f ^^ j) y)" using p unfolding ij y funpow_Suc_right by simp
thus "∃i≤ M. ¬ p ((f ^^ i) y)" using j by auto
}
{
fix i
assume "P y"
hence "P x" unfolding y P .
from less(3)[OF x(1) this, of "Suc i"]
show "p ((f ^^ i) y)" unfolding y funpow_Suc_right by simp
}
next
show "length (filter P (map f ys)) = n" unfolding id3 length_map using xs_ys less(2) by auto
qed
qed
qed
qed
definition complex_roots_of_int_poly3 :: "int poly ⇒ complex list" where
"complex_roots_of_int_poly3 p ≡ let n = degree p;
rrts = real_roots_of_int_poly p;
nr = length rrts;
crts = map (λ r. Complex r 0) rrts
in
if n = nr then crts
else let nr_crts = n - nr in if nr_crts = 2 then
let pp = real_of_int_poly p div (prod_list (map (λ x. [:-x,1:]) rrts));
cpp = map_poly (λ r. Complex r 0) pp
in crts @ croots2 cpp else
let
nr_pos_crts = nr_crts div 2;
rxs = real_parts_3 p;
ixs = pos_imaginary_parts_3 p;
rts = [(rx, ix). rx <- rxs, ix <- ixs];
crts' = map pair_to_complex
(filter_list_length (map_prod tighten_bounds_3 tighten_bounds_3)
(λ (r, i). 0 ∈⇩c ipoly_complex_interval p (Complex_Interval (get_itvl_3 r) (get_itvl_3 i))) nr_pos_crts rts)
in crts @ (concat (map (λ x. [x, cnj x]) crts'))"
definition complex_roots_of_int_poly_all :: "int poly ⇒ complex list" where
"complex_roots_of_int_poly_all p = (let n = degree p in
if n ≥ 3 then complex_roots_of_int_poly3 p
else if n = 1 then [roots1 (map_poly of_int p)] else if n = 2 then croots2 (map_poly of_int p)
else [])"
lemma in_real_itvl_get_bounds_tighten: "real_of_3 x ∈⇩i get_itvl_3 ((tighten_bounds_3 ^^ n) x)"
proof (induct n arbitrary: x)
case 0
thus ?case using get_itvl_3[of x] by simp
next
case (Suc n x)
have id: "(tighten_bounds_3 ^^ (Suc n)) x = (tighten_bounds_3 ^^ n) (tighten_bounds_3 x)"
by (metis comp_apply funpow_Suc_right)
show ?case unfolding id tighten_bounds_3(1)[of x, symmetric] by (rule Suc)
qed
lemma sandwitch_real:
fixes l r :: "nat ⇒ real"
assumes la: "l ⇢ a" and ra: "r ⇢ a"
and lm: "⋀i. l i ≤ m i" and mr: "⋀i. m i ≤ r i"
shows "m ⇢ a"
proof (rule LIMSEQ_I)
fix e :: real
assume "0 < e"
hence e: "0 < e / 2" by simp
from LIMSEQ_D[OF la e] obtain n1 where n1: "⋀ n. n ≥ n1 ⟹ norm (l n - a) < e/2" by auto
from LIMSEQ_D[OF ra e] obtain n2 where n2: "⋀ n. n ≥ n2 ⟹ norm (r n - a) < e/2" by auto
show "∃no. ∀n≥no. norm (m n - a) < e"
proof (rule exI[of _ "max n1 n2"], intro allI impI)
fix n
assume "max n1 n2 ≤ n"
with n1 n2 have *: "norm (l n - a) < e/2" "norm (r n - a) < e/2" by auto
from lm[of n] mr[of n] have "norm (m n - a) ≤ norm (l n - a) + norm (r n - a)" by simp
with * show "norm (m n - a) < e" by auto
qed
qed
lemma real_of_tighten_bounds_many[simp]: "real_of_3 ((tighten_bounds_3 ^^ i) x) = real_of_3 x"
apply (induct i) using tighten_bounds_3 by auto
definition lower_3 where "lower_3 x i ≡ interval.lower (get_itvl_3 ((tighten_bounds_3 ^^ i) x))"
definition upper_3 where "upper_3 x i ≡ interval.upper (get_itvl_3 ((tighten_bounds_3 ^^ i) x))"
lemma interval_size_3: "upper_3 x i - lower_3 x i = (upper_3 x 0 - lower_3 x 0)/2^i"
proof (induct i)
case (Suc i)
have "upper_3 x (Suc i) - lower_3 x (Suc i) = (upper_3 x i - lower_3 x i) / 2"
unfolding upper_3_def lower_3_def using tighten_bounds_3 get_itvl_3 by auto
with Suc show ?case by auto
qed auto
lemma interval_size_3_tendsto_0: "(λi. (upper_3 x i - lower_3 x i)) ⇢ 0"
by (subst interval_size_3, auto intro: LIMSEQ_divide_realpow_zero)
lemma dist_tendsto_0_imp_tendsto: "(λi. ¦f i - a¦ :: real) ⇢ 0 ⟹ f ⇢ a"
using LIM_zero_cancel tendsto_rabs_zero_iff by blast
lemma upper_3_tendsto: "upper_3 x ⇢ real_of_3 x"
proof(rule dist_tendsto_0_imp_tendsto, rule sandwitch_real)
fix i
obtain l r where lr: "get_itvl_3 ((tighten_bounds_3 ^^ i) x) = Interval l r"
by (metis interval.collapse)
with get_itvl_3[of "(tighten_bounds_3 ^^ i) x"]
show "¦(upper_3 x) i - real_of_3 x¦ ≤ (upper_3 x i - lower_3 x i)"
unfolding upper_3_def lower_3_def by auto
qed (insert interval_size_3_tendsto_0, auto)
lemma lower_3_tendsto: "lower_3 x ⇢ real_of_3 x"
proof(rule dist_tendsto_0_imp_tendsto, rule sandwitch_real)
fix i
obtain l r where lr: "get_itvl_3 ((tighten_bounds_3 ^^ i) x) = Interval l r"
by (metis interval.collapse)
with get_itvl_3[of "(tighten_bounds_3 ^^ i) x"]
show "¦lower_3 x i - real_of_3 x¦ ≤ (upper_3 x i - lower_3 x i)"
unfolding upper_3_def lower_3_def by auto
qed (insert interval_size_3_tendsto_0, auto)
lemma tends_to_tight_bounds_3: "(λx. get_itvl_3 ((tighten_bounds_3 ^^ x) y)) ⇢⇩i real_of_3 y"
using lower_3_tendsto[of y] upper_3_tendsto[of y] unfolding lower_3_def upper_3_def
interval_tendsto_def o_def by auto
lemma complex_roots_of_int_poly3: assumes p: "p ≠ 0" and sf: "square_free p"
shows "set (complex_roots_of_int_poly3 p) = {x. ipoly p x = 0}" (is "?l = ?r")
"distinct (complex_roots_of_int_poly3 p)"
proof -
interpret map_poly_inj_idom_hom of_real..
define q where "q = real_of_int_poly p"
let ?q = "map_poly complex_of_real q"
from p have q0: "q ≠ 0" unfolding q_def by auto
hence q: "?q ≠ 0" by auto
define rr where "rr = real_roots_of_int_poly p"
define rrts where "rrts = map (λr. Complex r 0) rr"
note d = complex_roots_of_int_poly3_def[of p, unfolded Let_def, folded rr_def, folded rrts_def]
have rr: "set rr = {x. ipoly p x = 0}" unfolding rr_def
using real_roots_of_int_poly(1)[OF p] .
have rrts: "set rrts = {x. poly ?q x = 0 ∧ x ∈ ℝ}" unfolding rrts_def set_map rr q_def
complex_of_real_def[symmetric] by (auto elim: Reals_cases)
have dist: "distinct rr" unfolding rr_def using real_roots_of_int_poly(2) .
from dist have dist1: "distinct rrts" unfolding rrts_def distinct_map inj_on_def by auto
have lrr: "length rr = card {x. poly (real_of_int_poly p) x = 0}"
unfolding rr_def using real_roots_of_int_poly[of p] p distinct_card by fastforce
have cr: "length rr = card {x. poly ?q x = 0 ∧ x ∈ ℝ}" unfolding lrr q_def[symmetric]
proof -
have "card {x. poly q x = 0} ≤ card {x. poly (map_poly complex_of_real q) x = 0 ∧ x ∈ ℝ}" (is "?l ≤ ?r")
by (rule card_inj_on_le[of of_real], insert poly_roots_finite[OF q], auto simp: inj_on_def)
moreover have "?l ≥ ?r"
by (rule card_inj_on_le[of Re, OF _ _ poly_roots_finite[OF q0]], auto simp: inj_on_def elim!: Reals_cases)
ultimately show "?l = ?r" by simp
qed
have conv: "⋀ x. ipoly p x = 0 ⟷ poly ?q x = 0"
unfolding q_def by (subst map_poly_map_poly, auto simp: o_def)
have r: "?r = {x. poly ?q x = 0}" unfolding conv ..
have "?l = {x. ipoly p x = 0} ∧ distinct (complex_roots_of_int_poly3 p)"
proof (cases "degree p = length rr")
case False note oFalse = this
show ?thesis
proof (cases "degree p - length rr = 2")
case False
let ?nr = "(degree p - length rr) div 2"
define cpxI where "cpxI = pos_imaginary_parts_3 p"
define cpxR where "cpxR = real_parts_3 p"
let ?rts = "[(rx,ix). rx <- cpxR, ix <- cpxI]"
define cpx where "cpx = map pair_to_complex (filter (λ c. ipoly p (pair_to_complex c) = 0)
?rts)"
let ?LL = "cpx @ map cnj cpx"
let ?LL' = "concat (map (λ x. [x,cnj x]) cpx)"
let ?ll = "rrts @ ?LL"
let ?ll' = "rrts @ ?LL'"
have cpx: "set cpx ⊆ ?r" unfolding cpx_def by auto
have ccpx: "cnj ` set cpx ⊆ ?r" using cpx unfolding r
by (auto intro!: complex_conjugate_root[of ?q] simp: Reals_def)
have "set ?ll ⊆ ?r" using rrts cpx ccpx unfolding r by auto
moreover
{
fix x :: complex
assume rt: "ipoly p x = 0"
{
fix x
assume rt: "ipoly p x = 0"
and gt: "Im x > 0"
define rx where "rx = Re x"
let ?x = "Complex rx (Im x)"
have x: "x = ?x" by (cases x, auto simp: rx_def)
from rt x have rt': "ipoly p ?x = 0" by auto
from real_parts_3[OF p rt, folded rx_def] pos_imaginary_parts_3[OF p rt gt] rt'
have "?x ∈ set cpx" unfolding cpx_def cpxI_def cpxR_def
by (force simp: pair_to_complex_def[abs_def])
hence "x ∈ set cpx" using x by simp
} note gt = this
have cases: "Im x = 0 ∨ Im x > 0 ∨ Im x < 0" by auto
from rt have rt': "ipoly p (cnj x) = 0" unfolding conv
by (intro complex_conjugate_root[of ?q x], auto simp: Reals_def)
{
assume "Im x > 0"
from gt[OF rt this] have "x ∈ set ?ll" by auto
}
moreover
{
assume "Im x < 0"
hence "Im (cnj x) > 0" by simp
from gt[OF rt' this] have "cnj (cnj x) ∈ set ?ll" unfolding set_append set_map by blast
hence "x ∈ set ?ll" by simp
}
moreover
{
assume "Im x = 0"
hence "x ∈ ℝ" using complex_is_Real_iff by blast
with rt rrts have "x ∈ set ?ll" unfolding conv by auto
}
ultimately have "x ∈ set ?ll" using cases by blast
}
ultimately have lr: "set ?ll = {x. ipoly p x = 0}" by blast
let ?rr = "map real_of_3 cpxR"
let ?pi = "map real_of_3 cpxI"
have dist2: "distinct ?rr" unfolding cpxR_def by (rule distinct_real_parts_3)
have dist3: "distinct ?pi" unfolding cpxI_def by (rule distinct_pos_imaginary_parts_3)
have idd: "concat (map (map pair_to_complex) (map (λrx. map (Pair rx) cpxI) cpxR))
= concat (map (λr. map (λ i. Complex (real_of_3 r) (real_of_3 i)) cpxI) cpxR)"
unfolding pair_to_complex_def by (auto simp: o_def)
have dist4: "distinct cpx" unfolding cpx_def
proof (rule distinct_map_filter, unfold map_concat idd, unfold distinct_conv_nth, intro allI impI, goal_cases)
case (1 i j)
from nth_concat_diff[OF 1, unfolded length_map] dist2[unfolded distinct_conv_nth]
dist3[unfolded distinct_conv_nth] show ?case by auto
qed
have dist5: "distinct (map cnj cpx)" using dist4 unfolding distinct_map by (auto simp: inj_on_def)
{
fix x :: complex
have rrts: "x ∈ set rrts ⟹ Im x = 0" unfolding rrts_def by auto
have cpx: "⋀ x. x ∈ set cpx ⟹ Im x > 0" unfolding cpx_def cpxI_def
by (auto simp: pair_to_complex_def[abs_def] positive_pos_imaginary_parts_3)
have cpx': "x ∈ cnj ` set cpx ⟹ sgn (Im x) = -1" using cpx by auto
have "x ∉ set rrts ∩ set cpx ∪ set rrts ∩ cnj ` set cpx ∪ set cpx ∩ cnj ` set cpx"
using rrts cpx[of x] cpx' by auto
} note dist6 = this
have dist: "distinct ?ll"
unfolding distinct_append using dist6 by (auto simp: dist1 dist4 dist5)
let ?p = "complex_of_int_poly p"
have pp: "?p ≠ 0" using p by auto
from p square_free_of_int_poly[OF sf] square_free_rsquarefree
have rsf:"rsquarefree ?p" by auto
from dist lr have "length ?ll = card {x. poly ?p x = 0}"
by (metis distinct_card)
also have "… = degree p"
using rsf unfolding rsquarefree_card_degree[OF pp] by simp
finally have deg_len: "degree p = length ?ll" by simp
let ?P = "λ c. ipoly p (pair_to_complex c) = 0"
let ?itvl = "λ r i. ipoly_complex_interval p (Complex_Interval (get_itvl_3 r) (get_itvl_3 i))"
let ?itv = "λ (r,i). ?itvl r i"
let ?p = "(λ (r,i). 0 ∈⇩c (?itvl r i))"
let ?tb = tighten_bounds_3
let ?f = "map_prod ?tb ?tb"
have filter: "map pair_to_complex (filter_list_length ?f ?p ?nr ?rts) = map pair_to_complex (filter ?P ?rts)"
proof (rule filter_list_length)
have "length (filter ?P ?rts) = length cpx"
unfolding cpx_def by simp
also have "… = ?nr" unfolding deg_len by (simp add: rrts_def)
finally show "length (filter ?P ?rts) = ?nr" by auto
next
fix n x
assume x: "?P x"
obtain r i where xri: "x = (r,i)" by force
have id: "(?f ^^ n) x = ((?tb ^^ n) r, (?tb ^^ n) i)" unfolding xri
by (induct n, auto)
have px: "pair_to_complex x = Complex (real_of_3 r) (real_of_3 i)"
unfolding xri pair_to_complex_def by auto
show "?p ((?f ^^ n) x)"
unfolding id split
by (rule ipoly_complex_interval[of "pair_to_complex x" _ p, unfolded x], unfold px,
auto simp: in_complex_interval_def in_real_itvl_get_bounds_tighten)
next
fix x
assume x: "x ∈ set ?rts" "¬ ?P x"
let ?x = "pair_to_complex x"
obtain r i where xri: "x = (r,i)" by force
have id: "(?f ^^ n) x = ((?tb ^^ n) r, (?tb ^^ n) i)" for n unfolding xri
by (induct n, auto)
have px: "?x = Complex (real_of_3 r) (real_of_3 i)"
unfolding xri pair_to_complex_def by auto
have cvg: "(λ n. ?itv ((?f ^^ n) x)) ⇢⇩c ipoly p ?x"
unfolding id split px
proof (rule ipoly_complex_interval_tendsto)
show "(λia. Complex_Interval (get_itvl_3 ((?tb ^^ ia) r)) (get_itvl_3 ((?tb ^^ ia) i))) ⇢⇩c
Complex (real_of_3 r) (real_of_3 i)"
unfolding complex_interval_tendsto_def by (simp add: tends_to_tight_bounds_3 o_def)
qed
from complex_interval_tendsto_neq[OF this x(2)]
show "∃ i. ¬ ?p ((?f ^^ i) x)" unfolding id by auto
next
show "pair_to_complex (?f x) = pair_to_complex x" for x
by (cases x, auto simp: pair_to_complex_def tighten_bounds_3(1))
next
show "?P (?f x) = ?P x" for x
by (cases x, auto simp: pair_to_complex_def tighten_bounds_3(1))
qed
have l: "complex_roots_of_int_poly3 p = ?ll'"
unfolding d filter cpx_def[symmetric] cpxI_def[symmetric] cpxR_def[symmetric] using False oFalse
by auto
have "distinct ?ll' = (distinct rrts ∧ distinct ?LL' ∧ set rrts ∩ set ?LL' = {})"
unfolding distinct_append ..
also have "set ?LL' = set ?LL" by auto
also have "distinct ?LL' = distinct ?LL" by (induct cpx, auto)
finally have "distinct ?ll' = distinct ?ll" unfolding distinct_append by auto
with dist have "distinct ?ll'" by auto
with lr l show ?thesis by auto
next
case True
let ?cr = "map_poly of_real :: real poly ⇒ complex poly"
define pp where "pp = complex_of_int_poly p"
have id: "pp = map_poly of_real q" unfolding q_def pp_def
by (subst map_poly_map_poly, auto simp: o_def)
let ?rts = "map (λ x. [:-x,1:]) rr"
define rts where "rts = prod_list ?rts"
let ?c2 = "?cr (q div rts)"
have pq: "⋀ x. ipoly p x = 0 ⟷ poly q x = 0" unfolding q_def by simp
from True have 2: "degree q - card {x. poly q x = 0} = 2" unfolding pq[symmetric] lrr
unfolding q_def by simp
from True have id: "degree p = length rr ⟷ False"
"degree p - length rr = 2 ⟷ True" by auto
have l: "?l = of_real ` {x. poly q x = 0} ∪ set (croots2 ?c2)"
unfolding d rts_def id if_False if_True set_append rrts Reals_def
by (fold complex_of_real_def q_def, auto)
from dist
have len_rr: "length rr = card {x. poly q x = 0}" unfolding rr[unfolded pq, symmetric]
by (simp add: distinct_card)
have rr': "⋀ r. r ∈ set rr ⟹ poly q r = 0" using rr unfolding q_def by simp
with dist have "q = q div prod_list ?rts * prod_list ?rts"
proof (induct rr arbitrary: q)
case (Cons r rr q)
note dist = Cons(2)
let ?p = "q div [:-r,1:]"
from Cons.prems(2) have "poly q r = 0" by simp
hence "[:-r,1:] dvd q" using poly_eq_0_iff_dvd by blast
from dvd_mult_div_cancel[OF this]
have "q = ?p * [:-r,1:]" by simp
moreover have "?p = ?p div (∏x←rr. [:- x, 1:]) * (∏x←rr. [:- x, 1:])"
proof (rule Cons.hyps)
show "distinct rr" using dist by auto
fix s
assume "s ∈ set rr"
with dist Cons(3) have "s ≠ r" "poly q s = 0" by auto
hence "poly (?p * [:- 1 * r, 1:]) s = 0" using calculation by force
thus "poly ?p s = 0" by (simp add: ‹s ≠ r›)
qed
ultimately have q: "q = ?p div (∏x←rr. [:- x, 1:]) * (∏x←rr. [:- x, 1:]) * [:-r,1:]"
by auto
also have "… = (?p div (∏x←rr. [:- x, 1:])) * (∏x←r # rr. [:- x, 1:])"
unfolding mult.assoc by simp
also have "?p div (∏x←rr. [:- x, 1:]) = q div (∏x←r # rr. [:- x, 1:])"
unfolding poly_div_mult_right[symmetric] by simp
finally show ?case .
qed simp
hence q_div: "q = q div rts * rts" unfolding rts_def .
from q_div q0 have "q div rts ≠ 0" "rts ≠ 0" by auto
from degree_mult_eq[OF this] have "degree q = degree (q div rts) + degree rts"
using q_div by simp
also have "degree rts = length rr" unfolding rts_def by (rule degree_linear_factors)
also have "… = card {x. poly q x = 0}" unfolding len_rr by simp
finally have deg2: "degree ?c2 = 2" using 2 by simp
note croots2 = croots2[OF deg2, symmetric]
have "?q = ?cr (q div rts * rts)" using q_div by simp
also have "… = ?cr rts * ?c2" unfolding hom_distribs by simp
finally have q_prod: "?q = ?cr rts * ?c2" .
from croots2 l
have l: "?l = of_real ` {x. poly q x = 0} ∪ {x. poly ?c2 x = 0}" by simp
from r[unfolded q_prod]
have r: "?r = {x. poly (?cr rts) x = 0} ∪ {x. poly ?c2 x = 0}" by auto
also have "?cr rts = (∏x←rr. ?cr [:- x, 1:])" by (simp add: rts_def o_def of_real_poly_hom.hom_prod_list)
also have "{x. poly … x = 0} = of_real ` set rr"
unfolding poly_prod_list_zero_iff by auto
also have "set rr = {x. poly q x = 0}" unfolding rr q_def by simp
finally have lr: "?l = ?r" unfolding l by simp
show ?thesis
proof (intro conjI[OF lr])
from sf have sf: "square_free q" unfolding q_def by (rule square_free_of_int_poly)
{
interpret field_hom_0' complex_of_real ..
from sf have "square_free ?q" unfolding square_free_map_poly .
} note sf = this
have l: "complex_roots_of_int_poly3 p = rrts @ croots2 ?c2"
unfolding d rts_def id if_False if_True set_append rrts q_def complex_of_real_def by auto
have dist2: "distinct (croots2 ?c2)" unfolding croots2_def Let_def by auto
{
fix x
assume x: "x ∈ set (croots2 ?c2)" "x ∈ set rrts"
from x(1)[unfolded croots2] have x1: "poly ?c2 x = 0" by auto
from x(2) have x2: "poly (?cr rts) x = 0"
unfolding rrts_def rts_def complex_of_real_def[symmetric]
by (auto simp: poly_prod_list_zero_iff o_def)
from square_free_multD(1)[OF sf[unfolded q_prod], of "[: -x, 1:]"]
x1 x2 have False unfolding poly_eq_0_iff_dvd by auto
} note dist3 = this
show "distinct (complex_roots_of_int_poly3 p)" unfolding l distinct_append
by (intro conjI dist1 dist2, insert dist3, auto)
qed
qed
next
case True
have "card {x. poly ?q x = 0} ≤ degree ?q" by (rule poly_roots_degree[OF q])
also have "… = degree p" unfolding q_def by simp
also have "… = card {x. poly ?q x = 0 ∧ x ∈ ℝ}" using True cr by simp
finally have le: "card {x. poly ?q x = 0} ≤ card {x. poly ?q x = 0 ∧ x ∈ ℝ}" by auto
have "{x. poly ?q x = 0 ∧ x ∈ ℝ} = {x. poly ?q x = 0}"
by (rule card_seteq[OF _ _ le], insert poly_roots_finite[OF q], auto)
with True rrts dist1 show ?thesis unfolding r d by auto
qed
thus "distinct (complex_roots_of_int_poly3 p)" "?l = ?r" by auto
qed
lemma complex_roots_of_int_poly_all: assumes sf: "degree p ≥ 3 ⟹ square_free p"
shows "p ≠ 0 ⟹ set (complex_roots_of_int_poly_all p) = {x. ipoly p x = 0}" (is "_ ⟹ set ?l = ?r")
and "distinct (complex_roots_of_int_poly_all p)"
proof -
note d = complex_roots_of_int_poly_all_def Let_def
have "(p ≠ 0 ⟶ set ?l = ?r) ∧ (distinct (complex_roots_of_int_poly_all p))"
proof (cases "degree p ≥ 3")
case True
hence p: "p ≠ 0" by auto
from True complex_roots_of_int_poly3[OF p] sf show ?thesis unfolding d by auto
next
case False
let ?p = "map_poly (of_int :: int ⇒ complex) p"
have deg: "degree ?p = degree p"
by (simp add: degree_map_poly)
show ?thesis
proof (cases "degree p = 1")
case True
hence l: "?l = [roots1 ?p]" unfolding d by auto
from True have "degree ?p = 1" unfolding deg by auto
from roots1[OF this] show ?thesis unfolding l roots1_def by auto
next
case False
show ?thesis
proof (cases "degree p = 2")
case True
hence l: "?l = croots2 ?p" unfolding d by auto
from True have "degree ?p = 2" unfolding deg by auto
from croots2[OF this] show ?thesis unfolding l by (simp add: croots2_def Let_def)
next
case False
with ‹degree p ≠ 1› ‹degree p ≠ 2› ‹¬ (degree p ≥ 3)› have True: "degree p = 0" by auto
hence l: "?l = []" unfolding d by auto
from True have "degree ?p = 0" unfolding deg by auto
from roots0[OF _ this] show ?thesis unfolding l by simp
qed
qed
qed
thus "p ≠ 0 ⟹ set ?l = ?r" "distinct (complex_roots_of_int_poly_all p)" by auto
qed
text ‹It now comes the preferred function to compute complex roots of an integer polynomial.›
definition complex_roots_of_int_poly :: "int poly ⇒ complex list" where
"complex_roots_of_int_poly p = (
let ps = (if degree p ≥ 3 then factors_of_int_poly p else [p])
in concat (map complex_roots_of_int_poly_all ps))"
definition complex_roots_of_rat_poly :: "rat poly ⇒ complex list" where
"complex_roots_of_rat_poly p = complex_roots_of_int_poly (snd (rat_to_int_poly p))"
lemma complex_roots_of_int_poly:
shows "p ≠ 0 ⟹ set (complex_roots_of_int_poly p) = {x. ipoly p x = 0}" (is "_ ⟹ ?l = ?r")
and "distinct (complex_roots_of_int_poly p)"
proof -
have "(p ≠ 0 ⟶ ?l = ?r) ∧ (distinct (complex_roots_of_int_poly p))"
proof (cases "degree p ≥ 3")
case False
hence "complex_roots_of_int_poly p = complex_roots_of_int_poly_all p"
unfolding complex_roots_of_int_poly_def Let_def by auto
with complex_roots_of_int_poly_all[of p] False show ?thesis by auto
next
case True
{
fix q
assume "q ∈ set (factors_of_int_poly p)"
from factors_of_int_poly(1)[OF refl this] irreducible_imp_square_free[of q]
have 0: "q ≠ 0" and sf: "square_free q" by auto
from complex_roots_of_int_poly_all(1)[OF sf 0] complex_roots_of_int_poly_all(2)[OF sf]
have "set (complex_roots_of_int_poly_all q) = {x. ipoly q x = 0}"
"distinct (complex_roots_of_int_poly_all q)" by auto
} note all = this
from True have
"?l = (⋃ ((λ p. set (complex_roots_of_int_poly_all p)) ` set (factors_of_int_poly p)))"
unfolding complex_roots_of_int_poly_def Let_def by auto
also have "… = (⋃ ((λ p. {x. ipoly p x = 0}) ` set (factors_of_int_poly p)))"
using all by blast
finally have l: "?l = (⋃ ((λ p. {x. ipoly p x = 0}) ` set (factors_of_int_poly p)))" .
have lr: "p ≠ 0 ⟶ ?l = ?r" using l factors_of_int_poly(2)[OF refl, of p] by auto
show ?thesis
proof (rule conjI[OF lr])
from True have id: "complex_roots_of_int_poly p =
concat (map complex_roots_of_int_poly_all (factors_of_int_poly p))"
unfolding complex_roots_of_int_poly_def Let_def by auto
show "distinct (complex_roots_of_int_poly p)" unfolding id distinct_conv_nth
proof (intro allI impI, goal_cases)
case (1 i j)
let ?fp = "factors_of_int_poly p"
let ?rr = "complex_roots_of_int_poly_all"
let ?cc = "concat (map ?rr (factors_of_int_poly p))"
from nth_concat_diff[OF 1, unfolded length_map]
obtain j1 k1 j2 k2 where
*: "(j1,k1) ≠ (j2,k2)"
"j1 < length ?fp" "j2 < length ?fp" and
"k1 < length (map ?rr ?fp ! j1)"
"k2 < length (map ?rr ?fp ! j2)"
"?cc ! i = map ?rr ?fp ! j1 ! k1"
"?cc ! j = map ?rr ?fp ! j2 ! k2" by blast
hence **: "k1 < length (?rr (?fp ! j1))"
"k2 < length (?rr (?fp ! j2))"
"?cc ! i = ?rr (?fp ! j1) ! k1"
"?cc ! j = ?rr (?fp ! j2) ! k2"
by auto
from * have mem: "?fp ! j1 ∈ set ?fp" "?fp ! j2 ∈ set ?fp" by auto
show "?cc ! i ≠ ?cc ! j"
proof (cases "j1 = j2")
case True
with * have "k1 ≠ k2" by auto
with all(2)[OF mem(2)] **(1-2) show ?thesis unfolding **(3-4) unfolding True
distinct_conv_nth by auto
next
case False
from ‹degree p ≥ 3› have p: "p ≠ 0" by auto
note fip = factors_of_int_poly(2-3)[OF refl this]
show ?thesis unfolding **(3-4)
proof
define x where "x = ?rr (?fp ! j2) ! k2"
assume id: "?rr (?fp ! j1) ! k1 = ?rr (?fp ! j2) ! k2"
from ** have x1: "x ∈ set (?rr (?fp ! j1))" unfolding x_def id[symmetric] by auto
from ** have x2: "x ∈ set (?rr (?fp ! j2))" unfolding x_def by auto
from all(1)[OF mem(1)] x1 have x1: "ipoly (?fp ! j1) x = 0" by auto
from all(1)[OF mem(2)] x2 have x2: "ipoly (?fp ! j2) x = 0" by auto
from False factors_of_int_poly(4)[OF refl, of p] have neq: "?fp ! j1 ≠ ?fp ! j2"
using * unfolding distinct_conv_nth by auto
have "poly (complex_of_int_poly p) x = 0" by (meson fip(1) mem(2) x2)
from fip(2)[OF this] mem x1 x2 neq
show False by blast
qed
qed
qed
qed
qed
thus "p ≠ 0 ⟹ ?l = ?r" "distinct (complex_roots_of_int_poly p)" by auto
qed
lemma complex_roots_of_rat_poly:
"p ≠ 0 ⟹ set (complex_roots_of_rat_poly p) = {x. rpoly p x = 0}" (is "_ ⟹ ?l = ?r")
"distinct (complex_roots_of_rat_poly p)"
proof -
obtain c q where cq: "rat_to_int_poly p = (c,q)" by force
from rat_to_int_poly[OF this]
have pq: "p = smult (inverse (of_int c)) (of_int_poly q)"
and c: "c ≠ 0" by auto
show "distinct (complex_roots_of_rat_poly p)" unfolding complex_roots_of_rat_poly_def
using complex_roots_of_int_poly(2) .
assume p: "p ≠ 0"
with pq c have q: "q ≠ 0" by auto
have id: "{x. rpoly p x = (0 :: complex)} = {x. ipoly q x = 0}"
unfolding pq by (simp add: c of_rat_of_int_poly hom_distribs)
show "?l = ?r" unfolding complex_roots_of_rat_poly_def cq snd_conv id
complex_roots_of_int_poly(1)[OF q] ..
qed
lemma min_int_poly_complex_of_real[simp]: "min_int_poly (complex_of_real x) = min_int_poly x"
proof (cases "algebraic x")
case False
hence "¬ algebraic (complex_of_real x)" unfolding algebraic_complex_iff by auto
with False show ?thesis unfolding min_int_poly_def by auto
next
case True
from min_int_poly_represents[OF True]
have "min_int_poly x represents x" by auto
thus ?thesis
by (intro min_int_poly_unique, auto simp: lead_coeff_min_int_poly_pos)
qed
text ‹TODO: the implemention might be tuned, since the search process should be faster when
using interval arithmetic to figure out the correct factor.
(One might also implement the search via checking @{term "ipoly f x = 0"}, but because of complex-algebraic-number
arithmetic, I think that search would be slower than the current one via "@{term "x ∈ set (complex_roots_of_int_poly f)"}›
definition min_int_poly_complex :: "complex ⇒ int poly" where
"min_int_poly_complex x = (if algebraic x then if Im x = 0 then min_int_poly_real (Re x)
else the (find (λ f. x ∈ set (complex_roots_of_int_poly f)) (complex_poly (min_int_poly (Re x)) (min_int_poly (Im x))))
else [:0,1:])"
lemma min_int_poly_complex[code_unfold]: "min_int_poly = min_int_poly_complex"
proof (standard)
fix x
define fs where "fs = complex_poly (min_int_poly (Re x)) (min_int_poly (Im x))"
let ?f = "min_int_poly_complex x"
show "min_int_poly x = ?f"
proof (cases "algebraic x")
case False
thus ?thesis unfolding min_int_poly_def min_int_poly_complex_def by auto
next
case True
show ?thesis
proof (cases "Im x = 0")
case *: True
have id: "?f = min_int_poly_real (Re x)" unfolding min_int_poly_complex_def * using True by auto
show ?thesis unfolding id min_int_poly_real_code_unfold[symmetric] min_int_poly_complex_of_real[symmetric]
using * by (intro arg_cong[of _ _ min_int_poly] complex_eqI, auto)
next
case False
from True[unfolded algebraic_complex_iff] have "algebraic (Re x)" "algebraic (Im x)" by auto
from complex_poly[OF min_int_poly_represents[OF this(1)] min_int_poly_represents[OF this(2)]]
have fs: "∃ f ∈ set fs. ipoly f x = 0" "⋀ f. f ∈ set fs ⟹ poly_cond f" unfolding fs_def by auto
let ?fs = "find (λ f. ipoly f x = 0) fs"
let ?fs' = "find (λ f. x ∈ set (complex_roots_of_int_poly f)) fs"
have "?f = the ?fs'" unfolding min_int_poly_complex_def fs_def
using True False by auto
also have "?fs' = ?fs"
by (rule find_cong[OF refl], subst complex_roots_of_int_poly, insert fs, auto)
finally have id: "?f = the ?fs" .
from fs(1) have "?fs ≠ None" unfolding find_None_iff by auto
then obtain f where Some: "?fs = Some f" by auto
from find_Some_D[OF this] fs(2)[of f]
show ?thesis unfolding id Some
by (intro min_int_poly_unique, auto)
qed
qed
qed
end