This instance will be upgraded to Heptapod 0.31.0 (final) on 2022-05-24 at 14:00 UTC+2 (a few minutes of down time)

Commit aa5eb2f3 authored by AkihisaYamada's avatar AkihisaYamada
Browse files

Merging developments in Algebraic Number theory and refinements on other entries

parent 54fdb3942ec8
......@@ -33,9 +33,6 @@ fun show_factorization :: "'a :: {semiring_1,show} \<times> (('a poly \<times> n
| "show_factorization (c,((p,i) # ps)) = show_factorization (c,ps) @ '' * ('' @ show p @ '')'' @
(if i = 1 then [] else ''^'' @ show i)"
definition show_sf_factorization :: "'a :: {semiring_1,show} \<times> (('a poly \<times> nat)list) \<Rightarrow> string" where
"show_sf_factorization x = show_factorization (case x of (c,xs) \<Rightarrow> (c, map (\<lambda> (p,i). (p, Suc i)) xs))"
text \<open>Determine the roots over the rational, real, and complex numbers.\<close>
definition "testpoly = [:5/2, -7/2, 1/2, -5, 7, -1, 5/2, -7/2, 1/2:]"
......@@ -48,7 +45,7 @@ value [code] "show_lines (complex_roots_of_rat_poly testpoly)"
text \<open>Factorize polynomials over the rational, real, and complex numbers.\<close>
value [code] "show_sf_factorization (factorize_rat_poly testpoly)"
value [code] "show_factorization (factorize_rat_poly testpoly)"
value [code] "show_factorization (the (factorize_real_poly testpoly))"
value [code] "show_factorization (the (factorize_complex_poly testpoly))"
......
......@@ -16,26 +16,8 @@ imports
"../Containers/Set_Impl"
begin
declare [[code drop: Gcd_fin]]
declare [[code drop: Lcm_fin]]
definition gcds :: "'a::semiring_gcd list \<Rightarrow> 'a"
where [simp, code_abbrev]: "gcds xs = gcd_list xs"
lemma [code]:
"gcds xs = fold gcd xs 0"
by (simp add: Gcd_fin.set_eq_fold)
definition lcms :: "'a::semiring_gcd list \<Rightarrow> 'a"
where [simp, code_abbrev]: "lcms xs = lcm_list xs"
lemma [code]:
"lcms xs = fold lcm xs 1"
by (simp add: Lcm_fin.set_eq_fold)
lemma in_reals_code [code_unfold]:
"x \<in> \<real> \<longleftrightarrow> Im x = 0"
by (fact complex_is_Real_iff)
lemma in_reals_code[code_unfold]: "((x :: complex) \<in> \<real>) = (Im x = 0)"
by (rule complex_is_Real_iff)
definition is_norm_1 :: "complex \<Rightarrow> bool" where
"is_norm_1 z = ((Re z)\<^sup>2 + (Im z)\<^sup>2 = 1)"
......
......@@ -63,11 +63,11 @@ begin
lemma map_poly_Re_poly: fixes x :: real
shows "poly (map_poly Re p) x = poly p (of_real x)"
proof -
interpret cr: ring_hom complex_of_real by (unfold_locales, auto)
interpret cr: field_hom' complex_of_real by (unfold_locales, auto)
have id: "map_poly (of_real o Re) p = p"
by (rule map_poly_idI, insert coeffs, auto)
by (rule map_poly_eqI, insert coeffs, auto)
show ?thesis unfolding arg_cong[OF id, of poly, symmetric]
by (subst map_poly_map_poly[symmetric], force+)
by (subst map_poly_map_poly[symmetric], auto)
qed
lemma map_poly_Re_coeffs:
......@@ -161,55 +161,39 @@ lemma real_poly_minus:
using assms unfolding diff_conv_add_uminus
by (intro real_poly_uminus real_poly_add, auto)
lemma real_poly_pdivmod: fixes p :: "'a :: real_field poly"
assumes p: "set (coeffs p) \<subseteq> \<real>"
and *: "set (coeffs q) \<subseteq> \<real>"
"(q div p, q mod p) = (r,s)"
shows "set (coeffs r) \<subseteq> \<real> \<and> set (coeffs s) \<subseteq> \<real>"
using *
proof (induct q arbitrary: r s)
lemma fixes p :: "'a :: real_field poly"
assumes p: "set (coeffs p) \<subseteq> \<real>" and *: "set (coeffs q) \<subseteq> \<real>"
shows real_poly_div: "set (coeffs (q div p)) \<subseteq> \<real>"
and real_poly_mod: "set (coeffs (q mod p)) \<subseteq> \<real>"
proof (atomize(full), insert *, induct q)
case 0
then show ?case by auto
thus ?case by auto
next
case (pCons a q r s)
case (pCons a q)
from pCons(1,3) have a: "a \<in> \<real>" and q: "set (coeffs q) \<subseteq> \<real>" by auto
note res = pCons(4) [unfolded div_pCons_eq mod_pCons_eq]
note res = pCons
show ?case
proof (cases "p = 0")
case True
with res pCons(3) show ?thesis by auto
next
case False
obtain ss rr where r: "(q div p, q mod p) = (ss, rr)" by force
from pCons(2)[OF q r] have IH: "set (coeffs ss) \<subseteq> \<real>" "set (coeffs rr) \<subseteq> \<real>" by auto
define c where "c = coeff (pCons a rr) (degree p) / coeff p (degree p)"
from pCons have IH: "set (coeffs (q div p)) \<subseteq> \<real>" "set (coeffs (q mod p)) \<subseteq> \<real>" by auto
define c where "c = coeff (pCons a (q mod p)) (degree p) / coeff p (degree p)"
{
have "coeff (pCons a rr) (degree p) \<in> \<real>"
by (rule real_poly_real_coeff, insert IH(2) a, intro real_poly_pCons)
have "coeff (pCons a (q mod p)) (degree p) \<in> \<real>"
by (rule real_poly_real_coeff, insert IH a, intro real_poly_pCons)
moreover have "coeff p (degree p) \<in> \<real>"
by (rule real_poly_real_coeff[OF p])
ultimately have "c \<in> \<real>" unfolding c_def by simp
} note c = this
from res [symmetric] False r
have r: "r = pCons c ss" and s: "s = pCons a rr - smult c p"
using c_def by auto
have "set (coeffs r) \<subseteq> \<real>" using c IH unfolding r by (intro real_poly_pCons)
moreover have "set (coeffs s) \<subseteq> \<real>" using c IH unfolding s using c a p
by (intro real_poly_minus real_poly_smult real_poly_pCons, auto)
ultimately show ?thesis by auto
from False
have r: "pCons a q div p = pCons c (q div p)" and s: "pCons a q mod p = pCons a (q mod p) - smult c p"
unfolding c_def div_pCons_eq mod_pCons_eq by simp_all
show ?thesis unfolding r s using a p c IH by (intro conjI real_poly_pCons real_poly_minus real_poly_smult)
qed
qed
lemma real_poly_div: fixes p :: "'a :: real_field poly"
assumes p: "set (coeffs p) \<subseteq> \<real>"
and q: "set (coeffs q) \<subseteq> \<real>"
shows "set (coeffs (p div q)) \<subseteq> \<real>"
proof -
obtain r s where pq: "(p div q, p mod q) = (r, s)" by force
from real_poly_pdivmod [OF q p this]
show ?thesis using pq [unfolded] by auto
qed
lemma real_poly_factor: fixes p :: "'a :: real_field poly"
assumes "set (coeffs (p * q)) \<subseteq> \<real>"
"set (coeffs p) \<subseteq> \<real>"
......@@ -267,7 +251,7 @@ proof -
from `p \<noteq> 0` have nz: "?fac1 \<noteq> 0" "?fac2 \<noteq> 0" "?fac \<noteq> 0" "r \<noteq> 0" unfolding p by auto
have id: "?fac = [: ?c * c, - (?c + c), 1 :]" by simp
have cfac: "coeffs ?fac = [ ?c * c, - (?c + c), 1 ]" unfolding id by simp
have cfac: "set (coeffs ?fac) \<subseteq> \<real>" unfolding cfac by (auto simp: field_simps Reals_cnj_iff)
have cfac: "set (coeffs ?fac) \<subseteq> \<real>" unfolding cfac by (cases c, auto simp: Reals_cnj_iff)
have "degree p = degree ?fac + degree r" unfolding p
by (rule degree_mult_eq, insert nz, auto)
also have "degree ?fac = degree ?fac1 + degree ?fac2"
......@@ -307,21 +291,20 @@ qed
lemma map_poly_of_real_Re: assumes "set (coeffs p) \<subseteq> \<real>"
shows "map_poly of_real (map_poly Re p) = p"
by (subst map_poly_map_poly, force+, rule map_poly_idI, insert assms, auto)
by (subst map_poly_map_poly, force+, rule map_poly_eqI, insert assms, auto)
lemma map_poly_Re_of_real: "map_poly Re (map_poly of_real p) = p"
by (subst map_poly_map_poly, force+, rule map_poly_idI, auto)
by (subst map_poly_map_poly, force+, rule map_poly_eqI, auto)
lemma map_poly_Re_mult: assumes p: "set (coeffs p) \<subseteq> \<real>"
and q: "set (coeffs q) \<subseteq> \<real>" shows "map_poly Re (p * q) = map_poly Re p * map_poly Re q"
proof -
let ?r = "map_poly Re"
let ?c = "map_poly complex_of_real"
interpret c: inj_field_hom_0 complex_of_real by (unfold_locales, auto)
interpret c: field_hom' complex_of_real by (unfold_locales, auto)
have "?r (p * q) = ?r (?c (?r p) * ?c (?r q))"
unfolding map_poly_of_real_Re[OF p] map_poly_of_real_Re[OF q] by simp
also have "?c (?r p) * ?c (?r q) = ?c (?r p * ?r q)"
unfolding c.map_poly_mult ..
also have "?c (?r p) * ?c (?r q) = ?c (?r p * ?r q)" by simp
also have "?r \<dots> = ?r p * ?r q" unfolding map_poly_Re_of_real ..
finally show ?thesis .
qed
......@@ -402,16 +385,15 @@ qed
lemma real_degree_2_factorization_exists: fixes p :: "real poly"
shows "\<exists> qs. p = prod_list qs \<and> (\<forall> q \<in> set qs. degree q \<le> 2)"
proof -
interpret cr: inj_field_hom complex_of_real by (unfold_locales, auto)
let ?cp = "map_poly complex_of_real"
let ?rp = "map_poly Re"
let ?p = "?cp p"
have "set (coeffs ?p) \<subseteq> \<real>" unfolding cr.coeffs_map_poly by auto
have "set (coeffs ?p) \<subseteq> \<real>" unfolding of_real_hom.coeffs_map_poly by auto
from real_degree_2_factorization_exists_complex[OF this]
obtain qs where p: "?p = prod_list qs" and
qs: "\<And> q. q \<in> set qs \<Longrightarrow> set (coeffs q) \<subseteq> \<real> \<and> degree q \<le> 2" by auto
have p: "p = ?rp (prod_list qs)" unfolding arg_cong[OF p, of ?rp, symmetric]
by (subst map_poly_map_poly, force+, rule sym, rule map_poly_idI, auto)
by (subst map_poly_map_poly, force, rule sym, rule map_poly_eqI, auto)
from qs have "\<exists> rs. prod_list qs = ?cp (prod_list rs) \<and> (\<forall> r \<in> set rs. degree r \<le> 2)"
proof (induct qs)
case Nil
......@@ -423,14 +405,14 @@ proof -
from Cons(2)[of q] have q: "set (coeffs q) \<subseteq> \<real>" and dq: "degree q \<le> 2" by auto
define r where "r = ?rp q"
have q: "q = ?cp r" unfolding r_def
by (subst map_poly_map_poly, force+, rule sym, rule map_poly_idI, insert q, auto)
by (subst map_poly_map_poly, force, rule sym, rule map_poly_eqI, insert q, auto)
have dr: "degree r \<le> 2" using dq unfolding q by (simp add: degree_map_poly)
show ?case
by (rule exI[of _ "r # rs"], unfold prod_list.Cons cr.map_poly_mult qs q, insert dr rs, auto)
by (rule exI[of _ "r # rs"], unfold prod_list.Cons qs q, insert dr rs, auto)
qed
then obtain rs where id: "prod_list qs = ?cp (prod_list rs)" and deg: "\<forall> r \<in> set rs. degree r \<le> 2" by auto
show ?thesis unfolding p id
by (intro exI, rule conjI[OF _ deg], subst map_poly_map_poly, force+, rule map_poly_idI, auto)
by (intro exI, rule conjI[OF _ deg], subst map_poly_map_poly, force, rule map_poly_eqI, auto)
qed
......
section \<open>Real Factorization\<close>
text \<open>This theory contains an algorithm to completely factorize real polynomials with rational
coefficients. It internally does a complex-number factorization, and then combines the
coefficients. It internally does a complex polynomial factorization, and then combines
all non-real roots with their conjugates.\<close>
theory Real_Factorization
......@@ -29,6 +29,9 @@ definition factorize_real_poly :: "real poly \<Rightarrow> (real \<times> (real
(\<lambda> (c,ris). (Re c, complex_roots_to_real_factorization ris))
(factorize_complex_main (map_poly of_real p))"
lemma monic_imp_nonzero: "monic x \<Longrightarrow> x \<noteq> 0" for x :: "'a :: semiring_1 poly" by auto
lemma delete_cnj: assumes
"order x (\<Prod>(x, i)\<leftarrow>xis. [:- x, 1:] ^ Suc i) \<ge> si" "si \<noteq> 0"
shows "(\<Prod>(x, i)\<leftarrow>xis. [:- x, 1:] ^ Suc i) =
......@@ -49,8 +52,8 @@ next
let ?x = "[: - x, 1 :]"
let ?xi = "?x ^ i"
have "monic (\<Prod>(x,i)\<leftarrow>(y, j) # yjs. [:- x, 1:] ^ Suc i)"
by (rule monic_prod_list_pow)
hence yy0: "?yj * ?yjs \<noteq> 0" by auto
by (rule monic_prod_list_pow) then have "monic (?yj * ?yjs)" by simp
from monic_imp_nonzero[OF this] have yy0: "?yj * ?yjs \<noteq> 0" by auto
have id: "(\<Prod>(x,i)\<leftarrow>(y, j) # yjs. [:- x, 1:] ^ Suc i) = ?yj * ?yjs" by simp
from 1(3-) have ord: "i \<le> order x (?yj * ?yjs)" and i: "i \<noteq> 0" unfolding id by auto
from ord[unfolded order_mult[OF yy0]] have ord: "i \<le> order x ?yj + order x ?yjs" .
......@@ -102,7 +105,8 @@ lemma factorize_real_poly: assumes fp: "factorize_real_poly p = Some (c,qis)"
shows
"p = smult c (\<Prod>(q, i)\<leftarrow>qis. q ^ i)"
"(q,j) \<in> set qis \<Longrightarrow> irreducible q \<and> j \<noteq> 0 \<and> monic q \<and> degree q \<in> {1,2}"
proof -
proof -
interpret map_poly_inj_idom_hom of_real..
have "(p = smult c (\<Prod>(q, i)\<leftarrow>qis. q ^ i)) \<and> ((q,j) \<in> set qis \<longrightarrow> irreducible q \<and> j \<noteq> 0 \<and> monic q \<and> degree q \<in> {1,2})"
proof (cases "p = 0")
case True
......@@ -123,31 +127,27 @@ proof -
(is "_ = smult d ?q") .
from arg_cong[OF this, of "\<lambda> p. coeff p (degree p)"]
have "coeff ?p (degree ?p) = coeff (smult d ?q) (degree (smult d ?q))" .
also have "coeff ?p (degree ?p) = ?c (coeff p (degree p))"
by (subst degree_map_poly, simp, simp, auto simp: subst coeff_map_poly)
also have "coeff ?p (degree ?p) = ?c (coeff p (degree p))" by simp
also have "coeff (smult d ?q) (degree (smult d ?q)) = d * coeff ?q (degree ?q)"
by simp
also have "monic ?q" by (rule monic_prod_list_pow)
finally have d: "d = ?c (coeff p (degree p))" by auto
from arg_cong[OF this, of Re, folded c] have c: "c = coeff p (degree p)" by auto
have "set (coeffs ?p) \<subseteq> \<real>"
by (subst coeffs_map_poly, auto)
have "set (coeffs ?p) \<subseteq> \<real>" by auto
with p have q': "set (coeffs (smult d ?q)) \<subseteq> \<real>" by auto
from d p0 have d0: "d \<noteq> 0" by auto
interpret c: inj_field_hom_0' ?c by (unfold_locales, auto)
have "smult d ?q = [:d:] * ?q" by auto
from real_poly_factor[OF q'[unfolded this]] d0 d
have q: "set (coeffs ?q) \<subseteq> \<real>" by auto
have "p = ?rp ?p"
by (rule sym, subst map_poly_map_poly, force+, rule map_poly_idI, auto)
by (rule sym, subst map_poly_map_poly, force, rule map_poly_eqI, auto)
also have "\<dots> = ?rp (smult d ?q)" unfolding p ..
also have "?q = ?cp (?rp ?q)"
by (rule sym, rule map_poly_of_real_Re, insert q, auto)
also have "d = ?c c" unfolding d c ..
also have "smult (?c c) (?cp (?rp ?q)) = ?cp (smult c (?rp ?q))"
unfolding c.map_poly_smult ..
also have "smult (?c c) (?cp (?rp ?q)) = ?cp (smult c (?rp ?q))" by simp
also have "?rp \<dots> = smult c (?rp ?q)"
by (subst map_poly_map_poly, force+, rule map_poly_idI, auto)
by (subst map_poly_map_poly, force, rule map_poly_eqI, auto)
finally have p: "p = smult c (?rp ?q)" .
let ?fact = complex_roots_to_real_factorization
have "?rp ?q = (\<Prod>(q, i)\<leftarrow>qis. q ^ i) \<and>
......@@ -155,7 +155,7 @@ proof -
using q unfolding qis
proof (induct xis rule: complex_roots_to_real_factorization.induct)
case 1
show ?case by (simp add: one_poly_def)
show ?case by simp
next
case (2 x i xis)
note IH = 2(1-2)
......@@ -193,7 +193,7 @@ proof -
with IH show ?thesis by auto
next
assume "q = [:- Re x, 1:] \<and> j = Suc i"
with linear_irreducible[of "[:- Re x, 1:]"] show ?thesis by auto
with linear_irreducible_field[of "[:- Re x, 1:]"] show ?thesis by auto
qed
qed
next
......@@ -201,14 +201,16 @@ proof -
define xi where "xi = [:Re x * Re x + Im x * Im x, - (2 * Re x), 1:]"
obtain xx where xx: "xx = cnj x" by auto
have xi: "xi = ?rp ([:-x,1:] * [:-xx,1:])" unfolding xx xi_def by auto
have cpxi: "?cp xi = [:-x,1:] * [:-xx,1:]" unfolding xi_def
by (auto simp: xx complex_eq_iff)
have cpxi: "?cp xi = [:-x,1:] * [:-xx,1:]" unfolding xi_def
by (cases x, auto simp: xx legacy_Complex_simps)
obtain yis where yis: "yis = delete_cnj xx (Suc i) xis" by auto
from False have fact: "?fact ((x,i) # xis) = ((xi,Suc i) # ?fact yis)"
unfolding xi_def xx yis by simp
note IH = IH(2)[OF False xx yis xi]
have "irreducible xi"
proof (rule irreducibleI)
apply (fold irreducible_connect)
apply (rule Polynomial_Divisibility.irreducible_connect)
proof (rule Missing_Polynomial.irreducibleI)
show "degree xi \<noteq> 0" unfolding xi by auto
fix q :: "real poly"
assume "degree q \<noteq> 0" "degree q < degree xi"
......@@ -225,11 +227,10 @@ proof -
{
fix c :: complex
assume rt: "poly (?cp xi) c = 0"
hence "poly (?cp q * ?cp p) c = 0"
unfolding qp c.map_poly_mult[symmetric] by simp
hence "poly (?cp q * ?cp p) c = 0" by (simp add: qp)
hence "(poly (?cp q) c = 0 \<or> poly (?cp p) c = 0)" by auto
hence "c = roots1 (?cp q) \<or> c = roots1 (?cp p)"
using roots1[of "?cp q"] roots1[of "?cp p"] dp dq by (auto simp: degree_map_poly)
using roots1[of "?cp q"] roots1[of "?cp p"] dp dq by auto
hence "c \<in> \<real>" unfolding roots1_def by auto
hence "c \<noteq> x" using False by auto
}
......@@ -246,8 +247,8 @@ proof -
by (rule real_poly_power, auto simp: xi)
have mon: "monic (\<Prod>(x, i)\<leftarrow>(x, i) # xis. [:- x, 1:] ^ Suc i)"
by (rule monic_prod_list_pow)
hence xixis: "?xi * ?xis \<noteq> 0" unfolding id by auto
from False have xxx: "xx \<noteq> x" unfolding xx by (auto simp: Reals_cnj_iff)
from monic_imp_nonzero[OF this] have xixis: "?xi * ?xis \<noteq> 0" unfolding id by auto
from False have xxx: "xx \<noteq> x" unfolding xx by (cases x, auto simp: legacy_Complex_simps Reals_def)
from prems[unfolded id] have prems: "set (coeffs (?xi * ?xis)) \<subseteq> \<real>" .
from id have "[:- x, 1:] ^ Suc i dvd ?xi * ?xis" by auto
from xixis this[unfolded order_divides]
......@@ -270,8 +271,7 @@ proof -
note IH = IH[OF yis]
have "?rp (?xi * ?xis) = ?rp ?yi * ?rp ?yis" unfolding idd
by (rule map_poly_Re_mult[OF yi yis])
also have "?rp ?yi = xi^Suc i" unfolding c.map_poly_power[symmetric]
by (rule map_poly_Re_of_real)
also have "?rp ?yi = xi^Suc i" by (fold hom_distribs, rule map_poly_Re_of_real)
also have "?rp ?yis = (\<Prod> (a,b) \<leftarrow> ?fact yis. a ^ b)"
using IH by auto
also have "xi ^ Suc i * (\<Prod> (a,b) \<leftarrow> ?fact yis. a ^ b) =
......
This diff is collapsed.
......@@ -14,57 +14,115 @@ imports
Show_Real_Alg
"../Show/Show_Instances"
begin
datatype real_alg_show_info = Rat_Info rat | Sqrt_Info rat rat | Real_Alg_Info "int poly" nat
fun convert_info :: "rat + int poly \<times> nat \<Rightarrow> real_alg_show_info" where
"convert_info (Inl q) = Rat_Info q"
| "convert_info (Inr (f,n)) = (if degree f = 2 then (let a = coeff f 2; b = coeff f 1; c = coeff f 0;
b2a = Rat.Fract (-b) (2 * a);
below = Rat.Fract (b*b - 4 * a * c) (4 * a * a)
in Sqrt_Info b2a (if n = 1 then -below else below))
else Real_Alg_Info f n)"
fun info_radt :: "real_alg_dt \<Rightarrow> rat poly \<times> nat" where
"info_radt (Rational r) = info_rai (of_rat_rai r)"
| "info_radt (Irrational rai) = info_rai rai"
definition real_alg_show_info :: "real_alg \<Rightarrow> real_alg_show_info" where
"real_alg_show_info x = convert_info (info_real_alg x)"
lemma info_radt:
assumes x: "radt_cond x"
shows "\<exists> rai. real_of_radt x = real_of_rai rai \<and>
info_radt x = info_rai rai"
proof (cases x)
case (Rational r)
thus ?thesis by (intro exI[of _ "of_rat_rai r"], auto simp: of_rat_rai)
next
case (Irrational rai)
thus ?thesis using x by auto
text \<open>We prove that the extracted information for showing an algebraic real number is correct.\<close>
lemma real_alg_show_info: "real_alg_show_info x = Rat_Info r \<Longrightarrow> real_of x = of_rat r"
"real_alg_show_info x = Sqrt_Info r sq \<Longrightarrow> real_of x = of_rat r + sqrt (of_rat sq)"
"real_alg_show_info x = Real_Alg_Info p n \<Longrightarrow> p represents (real_of x) \<and> n = card {y. y \<le> real_of x \<and> ipoly p y = 0}"
(is "?l \<Longrightarrow> ?r")
proof (atomize(full), goal_cases)
case 1
note d = real_alg_show_info_def
show ?case
proof (cases "info_real_alg x")
case (Inl q)
from info_real_alg(2)[OF this] this show ?thesis unfolding d by auto
next
case (Inr qm)
then obtain p n where id: "info_real_alg x = Inr (p,n)" by (cases qm, auto)
from info_real_alg(1)[OF id]
have ap: "p represents (real_of x)" and n: "n = card {y. y \<le> real_of x \<and> ipoly p y = 0}"
and irr: "irreducible p" by auto
note id' = real_alg_show_info_def id convert_info.simps Fract_of_int_quotient Let_def
have last: "?l \<Longrightarrow> ?r" unfolding id' using ap n by (auto split: if_splits)
{
assume *: "real_alg_show_info x = Sqrt_Info r sq"
from this[unfolded id'] have deg: "degree p = 2" by (auto split: if_splits)
from degree2_coeffs[OF this] obtain a b c where p: "p = [:c,b,a:]" and a: "a \<noteq> 0" by auto
hence coeffs: "coeff p 0 = c" "coeff p 1 = b" "coeff p (Suc (Suc 0)) = a" "2 = Suc (Suc 0)" by auto
let ?a = "real_of_int a"
let ?b = "real_of_int b"
let ?c = "real_of_int c"
define A where "A = ?a"
define B where "B = ?b"
define C where "C = ?c"
let ?r = "- (B / (2 * A))"
define R where "R = ?r"
let ?sq = "(B * B - 4 * A * C) / (4 * A * A)"
let ?p = "real_of_int_poly p"
let ?disc = "(B / (2 * A)) ^ Suc (Suc 0) - C / A"
define D where "D = ?disc"
from arg_cong[OF p, of "map_poly real_of_int"]
have rp: "?p = [: C, B, A :]"
using a by (auto simp: A_def B_def C_def)
from a have A: "A \<noteq> 0" unfolding A_def by auto
from *[unfolded id' deg, unfolded coeffs of_int_minus of_int_minus of_int_mult of_int_diff, simplified]
have r: "real_of_rat r = R" and sq: "sqrt (of_rat sq) = (if n = 1 then - sqrt ?sq else sqrt ?sq)"
by (auto simp: A_def B_def C_def R_def real_sqrt_minus)
note sq
also have "?sq = D" using A by (auto simp: field_simps D_def)
finally have sq: "sqrt (of_rat sq) = (if n = 1 then - sqrt D else sqrt D)" by simp
with rp have coeffs': "coeff ?p 0 = C" "coeff ?p 1 = B" "coeff ?p (Suc (Suc 0)) = A" "2 = Suc (Suc 0)" by auto
from rp A have "degree (real_of_int_poly p) = 2" by auto
note roots = rroots2[OF this, unfolded rroots2_def Let_def coeffs', folded D_def R_def]
from ap[unfolded represents_def] have root: "ipoly p (real_of x) = 0" by auto
from root roots have D: "(D < 0) = False" by auto
note roots = roots[unfolded this if_False, folded R_def]
have "real_of x = of_rat r + sqrt (of_rat sq)"
proof (cases "D = 0")
case True
show ?thesis using roots root unfolding sq r True by auto
next
case False
with D have D: "D > 0" by auto
from roots False have roots: "{x. ipoly p x = 0} = {R + sqrt D, R - sqrt D}" by auto
let ?Roots = "{y. y \<le> real_of x \<and> ipoly p y = 0}"
have x: "real_of x \<in> ?Roots" using root by auto
from root roots have choice: "real_of x = R + sqrt D \<or> real_of x = R - sqrt D" by auto
hence small: "R - sqrt D \<in> ?Roots" using roots D by auto
show ?thesis
proof (cases "n = 1")
case True
from card_1_singletonE[OF n[symmetric, unfolded this]] obtain y where id: "?Roots = {y}" by auto
from x small show ?thesis unfolding sq r id using True by auto
next
case False
from x obtain Y where Y: "?Roots = insert (real_of x) (Y - {real_of x})" by auto
with False[unfolded n] obtain z Z where Z: "Y - {real_of x} = insert z Z" by (cases "Y - {real_of x} = {}", auto)
from Y[unfolded Z] Z have sub: "{real_of x, z} \<subseteq> ?Roots" and z: "z \<noteq> real_of x" by auto
with roots choice D have "real_of x = R + sqrt D" by force
thus ?thesis unfolding sq r id using False by auto
qed
qed
}
with last show ?thesis unfolding d by (auto simp: id Let_def)
qed
qed
lemma info_radt_fun: assumes x: "radt_cond x" and y: "radt_cond y"
and eq: "real_of_radt x = real_of_radt y"
shows "info_radt x = info_radt y"
proof -
from info_radt[OF x] obtain rai1 where x: "real_of_radt x = real_of_rai rai1" and
ix: "info_radt x = (info_rai rai1)" by auto
from info_radt[OF y] obtain rai2 where y: "real_of_radt y = real_of_rai rai2" and
iy: "info_radt y = info_rai rai2" by auto
from info_rai_fun[OF eq[unfolded x y]] ix iy eq x y
show ?thesis by auto
qed
lift_definition info_radtc :: "real_alg_dtc \<Rightarrow> rat poly \<times> nat" is info_radt .
lemma info_radtc_fun: "real_of_radtc x = real_of_radtc y \<Longrightarrow> info_radtc x = info_radtc y"
by (transfer, intro info_radt_fun, auto)
lift_definition real_alg_info :: "real_alg \<Rightarrow> rat poly \<times> nat" is info_radtc
by (metis info_radtc_fun)
fun show_rai_info :: "int \<Rightarrow> rat poly \<times> nat \<Rightarrow> string" where
"show_rai_info fl (p,n) = (if degree p = 1 then show (- coeff p 0) else
if degree p = 2 then (let p2 = coeff p 1 / 2; q = coeff p 0;
sqrt = ''sqrt('' @ show (p2 * p2 - q) @ '')'' in
if p2 = 0
then (if n = 1 then '' -'' else []) @ sqrt
else (''('' @ show (-p2) @ (if n = 1 then ''-'' else ''+'') @ sqrt @ '')''))
else ''(num in ('' @ show fl @ '','' @ show (fl + 1) @ ''), root #'' @ show n @ '' of '' @ show p @ '')'')"
fun show_rai_info :: "int \<Rightarrow> real_alg_show_info \<Rightarrow> string" where
"show_rai_info fl (Rat_Info r) = show r"
| "show_rai_info fl (Sqrt_Info r sq) = (let sqrt = ''sqrt('' @ show (abs sq) @ '')''
in if r = 0 then (if sq < 0 then '' -'' else []) @ sqrt
else (''('' @ show r @ (if sq < 0 then ''-'' else ''+'') @ sqrt @ '')''))"
| "show_rai_info fl (Real_Alg_Info p n) =
''(root #'' @ show n @ '' of '' @ show p @ '', in ('' @ show fl @ '','' @ show (fl + 1) @ ''))''"
overloading show_real_alg \<equiv> show_real_alg
begin
definition show_real_alg[code]:
"show_real_alg x \<equiv> show_rai_info (floor x) (real_alg_info x)"
end
"show_real_alg x \<equiv> show_rai_info (floor x) (real_alg_show_info x)"
end
end
This diff is collapsed.
......@@ -18,6 +18,8 @@ imports
Hensel_Lifting
begin
hide_const coeff monom
definition berlekamp_hensel :: "int \<Rightarrow> nat \<Rightarrow> int poly \<Rightarrow> int poly list" where
"berlekamp_hensel p n f = (case finite_field_factorization_int p f of
(_,fs) \<Rightarrow> hensel_lifting p n f fs)"
......
......@@ -18,6 +18,7 @@ imports
Poly_Mod_Finite_Field
begin
hide_const (open) up_ring.coeff up_ring.monom
subsection \<open>Auxiliary lemmas\<close>
......@@ -639,12 +640,10 @@ qed
lemma poly_identity_mod_p:
"v^(CARD('a)) - v = prod (\<lambda>x. v - [:x:]) (UNIV::'a mod_ring set)"
proof -
interpret r: ring_hom "\<lambda>q. q \<circ>\<^sub>p v"
using pcompose_add pcompose_mult pcompose_1 pcompose_uminus by (unfold_locales, auto)
have id: "monom 1 1 \<circ>\<^sub>p v = v" "[:0, 1:] \<circ>\<^sub>p v = v" unfolding pcompose_def by auto
have id2: "monom 1 (CARD('a)) \<circ>\<^sub>p v = v ^ (CARD('a))" by (metis id(1) r.hom_power x_pow_n)
have id2: "monom 1 (CARD('a)) \<circ>\<^sub>p v = v ^ (CARD('a))" by (metis id(1) pcompose_hom.hom_power x_pow_n)
show ?thesis using arg_cong[OF poly_monom_identity_mod_p, of "\<lambda> f. f \<circ>\<^sub>p v"]
unfolding r.hom_minus r.hom_prod id pcompose_const id2 .
unfolding pcompose_hom.hom_minus pcompose_hom.hom_prod id pcompose_const id2 .
qed
......
......@@ -84,7 +84,7 @@ theorem berlekamp_zassenhaus_factorization:
assumes res: "berlekamp_zassenhaus_factorization f = fs"
and sf: "square_free f"
and deg: "degree f \<noteq> 0"
shows "f = prod_list fs \<and> (\<forall> fi \<in> set fs. irreducible fi)"
shows "f = prod_list fs \<and> (\<forall> fi \<in> set fs. Missing_Polynomial.irreducible fi)"
proof -
let ?lc = "lead_coeff f"
define p where "p \<equiv> suitable_prime_bz f"
......@@ -100,6 +100,7 @@ proof -
define n where "n = find_exponent p (2 * abs ?lc * factor_bound f (degree_bound gs))"
note n = find_exponent[OF p1, of "2 * abs ?lc * factor_bound f (degree_bound gs)",
folded n_def]
note cop = cop[unfolded coprime_iff_gcd_one]
note bh = berlekamp_and_hensel_separated[OF prime cop sf refl berl n(2)]
have db: "degree_bound (berlekamp_hensel p n f) = degree_bound gs" unfolding bh
degree_bound_def max_factor_degree_def by simp
......@@ -108,4 +109,101 @@ proof -
by (rule zassenhaus_reconstruction[OF prime cop sf deg refl _ res], insert n db, auto)
qed
lemma content_free_prod_list:
fixes fs :: "'a :: {factorial_semiring,semiring_Gcd} poly list" (* where content_mult is proven. *)
assumes "content_free (prod_list fs)" and "f \<in> set fs" shows "content_free f"
proof (insert assms, induct fs arbitrary: f)
case Nil then show ?case by auto
next
case (Cons f' fs)
from Cons.prems
have "content f' * content (prod_list fs) dvd 1" by (auto simp: content_mult)
from this[unfolded zmult_eq_1_iff]
have "content f' = 1" and "content (prod_list fs) = 1" by auto
moreover from Cons.prems have "f = f' \<or> f \<in> set fs" by auto
ultimately show ?case using Cons.hyps[of f] by auto
qed
(*TODO:move*)
lemma irreducible_imp_content_free:
fixes f :: "'a :: {idom,semiring_gcd} poly"
assumes irr: "irreducible f" and deg: "degree f \<noteq> 0" shows "content_free f"
proof (rule ccontr)
assume not: "\<not> ?thesis"
then have "\<not> [:content f:] dvd 1" by simp
moreover have "f = [:content f:] * primitive_part f" by simp
note irreducibleD[OF irr this]
ultimately
have "primitive_part f dvd 1" by auto
from this[unfolded poly_dvd_1] have "degree f = 0" by auto
with deg show False by auto
qed
(*TODO:move*)
lemma irreducible_content_free_connect:
fixes f :: "'a :: {idom,semiring_gcd} poly"
assumes cf: "content_free f" shows "Missing_Polynomial.irreducible f \<longleftrightarrow> irreducible f" (is "?l \<longleftrightarrow> ?r")
proof
assume l: ?l show ?r
proof(rule ccontr, elim not_irreducibleE)
from l have deg: "degree f > 0" by (auto dest: Missing_Polynomial.irreducibleD)
from cf have f0: "f \<noteq> 0" by auto
then show "f = 0 \<Longrightarrow> False" by auto
show "f dvd 1 \<Longrightarrow> False" using deg by (auto simp:poly_dvd_1)
fix a b assume fab: "f = a * b" and a1: "\<not> a dvd 1" and b1: "\<not> b dvd 1"
then have af: "a dvd f" and bf: "b dvd f" by auto
with f0 have a0: "a \<noteq> 0" and b0: "b \<noteq> 0" by auto
from Missing_Polynomial.irreducibleD(2)[OF l, of a] af dvd_imp_degree_le[OF af f0]
have "degree a = 0 \<or> degree a = degree f" by force
then show False
proof(elim disjE)