Theory Formal_Puiseux_Series
section ‹Formal Puiseux Series›
theory Formal_Puiseux_Series
imports FPS_Hensel
begin
subsection ‹Auxiliary facts and definitions›
lemma div_dvd_self:
fixes a b :: "'a :: {semidom_divide}"
shows "b dvd a ⟹ a div b dvd a"
by (elim dvdE; cases "b = 0") simp_all
lemma quotient_of_int [simp]: "quotient_of (of_int n) = (n, 1)"
using Rat.of_int_def quotient_of_int by auto
lemma of_int_div_of_int_in_Ints_iff:
"(of_int n / of_int m :: 'a :: field_char_0) ∈ ℤ ⟷ m = 0 ∨ m dvd n"
proof
assume *: "(of_int n / of_int m :: 'a) ∈ ℤ"
{
assume "m ≠ 0"
from * obtain k where k: "(of_int n / of_int m :: 'a) = of_int k"
by (auto elim!: Ints_cases)
hence "of_int n = (of_int k * of_int m :: 'a)"
using ‹m ≠ 0› by (simp add: field_simps)
also have "… = of_int (k * m)"
by simp
finally have "n = k * m"
by (subst (asm) of_int_eq_iff)
hence "m dvd n" by auto
}
thus "m = 0 ∨ m dvd n" by blast
qed auto
lemma rat_eq_quotientD:
assumes "r = rat_of_int a / rat_of_int b" "b ≠ 0"
shows "fst (quotient_of r) dvd a" "snd (quotient_of r) dvd b"
proof -
define a' b' where "a' = fst (quotient_of r)" and "b' = snd (quotient_of r)"
define d where "d = gcd a b"
have "b' > 0"
by (auto simp: b'_def quotient_of_denom_pos')
have "coprime a' b'"
by (rule quotient_of_coprime[of r]) (simp add: a'_def b'_def)
have r: "r = rat_of_int a' / rat_of_int b'"
by (simp add: a'_def b'_def quotient_of_div)
from assms ‹b' > 0› have "rat_of_int (a' * b) = rat_of_int (a * b')"
unfolding of_int_mult by (simp add: field_simps r)
hence eq: "a' * b = a * b'"
by (subst (asm) of_int_eq_iff)
have "a' dvd a * b'"
by (simp flip: eq)
hence "a' dvd a"
by (subst (asm) coprime_dvd_mult_left_iff) fact
moreover have "b' dvd a' * b"
by (simp add: eq)
hence "b' dvd b"
by (subst (asm) coprime_dvd_mult_right_iff) (use ‹coprime a' b'› in ‹simp add: coprime_commute›)
ultimately show "fst (quotient_of r) dvd a" "snd (quotient_of r) dvd b"
unfolding a'_def b'_def by blast+
qed
lemma quotient_of_denom_add_dvd:
"snd (quotient_of (x + y)) dvd snd (quotient_of x) * snd (quotient_of y)"
proof -
define a b where "a = fst (quotient_of x)" and "b = snd (quotient_of x)"
define c d where "c = fst (quotient_of y)" and "d = snd (quotient_of y)"
have "b > 0" "d > 0"
by (auto simp: b_def d_def quotient_of_denom_pos')
have xy: "x = rat_of_int a / rat_of_int b" "y = rat_of_int c / rat_of_int d"
unfolding a_def b_def c_def d_def by (simp_all add: quotient_of_div)
show "snd (quotient_of (x + y)) dvd b * d"
proof (rule rat_eq_quotientD)
show "x + y = rat_of_int (a * d + c * b) / rat_of_int (b * d)"
using ‹b > 0› ‹d > 0› by (simp add: field_simps xy)
qed (use ‹b > 0› ‹d > 0› in auto)
qed
lemma quotient_of_denom_diff_dvd:
"snd (quotient_of (x - y)) dvd snd (quotient_of x) * snd (quotient_of y)"
using quotient_of_denom_add_dvd[of x "-y"]
by (simp add: rat_uminus_code Let_def case_prod_unfold)
definition supp :: "('a ⇒ ('b :: zero)) ⇒ 'a set" where
"supp f = f -` (-{0})"
lemma supp_0 [simp]: "supp (λ_. 0) = {}"
and supp_const: "supp (λ_. c) = (if c = 0 then {} else UNIV)"
and supp_singleton [simp]: "c ≠ 0 ⟹ supp (λx. if x = d then c else 0) = {d}"
by (auto simp: supp_def)
lemma supp_uminus [simp]: "supp (λx. -f x :: 'a :: group_add) = supp f"
by (auto simp: supp_def)
subsection ‹Definition›
text ‹
Similarly to formal power series $R[[X]]$ and formal Laurent series $R((X))$, we define the ring
of formal Puiseux series $R\{\{X\}\}$ as functions from the rationals into a ring such that
▸ the support is bounded from below, and
▸ the denominators of the numbers in the support have a common multiple other than 0
One can also think of a formal Puiseux series in the paramter $X$ as a formal Laurent series
in the parameter $X^{1/d}$ for some positive integer $d$. This is often written in the
following suggestive notation:
\[ R\{\{X\}\} = \bigcup_{d\geq 1} R((X^{1/d})) \]
Many operations will be defined in terms of this correspondence between Puiseux and Laurent
series, and many of the simple properties proven that way.
›
definition is_fpxs :: "(rat ⇒ 'a :: zero) ⇒ bool" where
"is_fpxs f ⟷ bdd_below (supp f) ∧ (LCM r∈supp f. snd (quotient_of r)) ≠ 0"
typedef (overloaded) 'a fpxs = "{f::rat ⇒ 'a :: zero. is_fpxs f}"
morphisms fpxs_nth Abs_fpxs
by (rule exI[of _ "λ_. 0"]) (auto simp: is_fpxs_def supp_def)
setup_lifting type_definition_fpxs
lemma fpxs_ext: "(⋀r. fpxs_nth f r = fpxs_nth g r) ⟹ f = g"
by transfer auto
lemma fpxs_eq_iff: "f = g ⟷ (∀r. fpxs_nth f r = fpxs_nth g r)"
by transfer auto
lift_definition fpxs_supp :: "'a :: zero fpxs ⇒ rat set" is supp .
lemma fpxs_supp_altdef: "fpxs_supp f = {x. fpxs_nth f x ≠ 0}"
by transfer (auto simp: supp_def)
text ‹
The following gives us the ``root order'' of ‹f›i, i.e. the smallest positive integer ‹d›
such that ‹f› is in $R((X^{1/p}))$.
›
lift_definition fpxs_root_order :: "'a :: zero fpxs ⇒ nat" is
"λf. nat (LCM r∈supp f. snd (quotient_of r))" .
lemma fpxs_root_order_pos [simp]: "fpxs_root_order f > 0"
proof transfer
fix f :: "rat ⇒ 'a" assume f: "is_fpxs f"
hence "(LCM r∈supp f. snd (quotient_of r)) ≠ 0"
by (auto simp: is_fpxs_def)
moreover have "(LCM r∈supp f. snd (quotient_of r)) ≥ 0"
by simp
ultimately show "nat (LCM r∈supp f. snd (quotient_of r)) > 0"
by linarith
qed
lemma fpxs_root_order_nonzero [simp]: "fpxs_root_order f ≠ 0"
using fpxs_root_order_pos[of f] by linarith
text ‹
Let ‹d› denote the root order of a Puiseux series ‹f›, i.e. the smallest number ‹d› such that
all monomials with non-zero coefficients can be written in the form $X^{n/d}$ for some ‹n›.
Then ‹f› can be written as a Laurent series in ‹X^{1/d}›. The following operation gives us
this Laurent series.
›
lift_definition fls_of_fpxs :: "'a :: zero fpxs ⇒ 'a fls" is
"λf n. f (of_int n / of_int (LCM r∈supp f. snd (quotient_of r)))"
proof -
fix f :: "rat ⇒ 'a"
assume f: "is_fpxs f"
hence "bdd_below (supp f)"
by (auto simp: is_fpxs_def)
then obtain r0 where "∀x∈supp f. r0 ≤ x"
by (auto simp: bdd_below_def)
hence r0: "f x = 0" if "x < r0" for x
using that by (auto simp: supp_def vimage_def)
define d :: int where "d = (LCM r∈supp f. snd (quotient_of r))"
have "d ≥ 0" by (simp add: d_def)
moreover have "d ≠ 0"
using f by (auto simp: d_def is_fpxs_def)
ultimately have "d > 0" by linarith
have *: "f (of_int n / of_int d) = 0" if "n < ⌊r0 * of_int d⌋" for n
proof -
have "rat_of_int n < r0 * rat_of_int d"
using that by linarith
thus ?thesis
using ‹d > 0› by (intro r0) (auto simp: field_simps)
qed
have "eventually (λn. n > -⌊r0 * of_int d⌋) at_top"
by (rule eventually_gt_at_top)
hence "eventually (λn. f (of_int (-n) / of_int d) = 0) at_top"
by (eventually_elim) (rule *, auto)
hence "eventually (λn. f (of_int (-int n) / of_int d) = 0) at_top"
by (rule eventually_compose_filterlim) (rule filterlim_int_sequentially)
thus "eventually (λn. f (of_int (-int n) / of_int d) = 0) cofinite"
by (simp add: cofinite_eq_sequentially)
qed
lemma fls_nth_of_fpxs:
"fls_nth (fls_of_fpxs f) n = fpxs_nth f (of_int n / of_nat (fpxs_root_order f))"
by transfer simp
subsection ‹Basic algebraic typeclass instances›
instantiation fpxs :: (zero) zero
begin
lift_definition zero_fpxs :: "'a fpxs" is "λr::rat. 0 :: 'a"
by (auto simp: is_fpxs_def supp_def)
instance ..
end
instantiation fpxs :: ("{one, zero}") one
begin
lift_definition one_fpxs :: "'a fpxs" is "λr::rat. if r = 0 then 1 else 0 :: 'a"
by (cases "(1 :: 'a) = 0") (auto simp: is_fpxs_def cong: if_cong)
instance ..
end
lemma fls_of_fpxs_0 [simp]: "fls_of_fpxs 0 = 0"
by transfer auto
lemma fpxs_nth_0 [simp]: "fpxs_nth 0 r = 0"
by transfer auto
lemma fpxs_nth_1: "fpxs_nth 1 r = (if r = 0 then 1 else 0)"
by transfer auto
lemma fpxs_nth_1': "fpxs_nth 1 0 = 1" "r ≠ 0 ⟹ fpxs_nth 1 r = 0"
by (auto simp: fpxs_nth_1)
instantiation fpxs :: (monoid_add) monoid_add
begin
lift_definition plus_fpxs :: "'a fpxs ⇒ 'a fpxs ⇒ 'a fpxs" is
"λf g x. f x + g x"
proof -
fix f g :: "rat ⇒ 'a"
assume fg: "is_fpxs f" "is_fpxs g"
show "is_fpxs (λx. f x + g x)"
unfolding is_fpxs_def
proof
have supp: "supp (λx. f x + g x) ⊆ supp f ∪ supp g"
by (auto simp: supp_def)
show "bdd_below (supp (λx. f x + g x))"
by (rule bdd_below_mono[OF _ supp]) (use fg in ‹auto simp: is_fpxs_def›)
have "(LCM r∈supp (λx. f x + g x). snd (quotient_of r)) dvd
(LCM r∈supp f ∪ supp g. snd (quotient_of r))"
by (intro Lcm_subset image_mono supp)
also have "… = lcm (LCM r∈supp f. snd (quotient_of r)) (LCM r∈supp g. snd (quotient_of r))"
unfolding image_Un Lcm_Un ..
finally have "(LCM r∈supp (λx. f x + g x). snd (quotient_of r)) dvd
lcm (LCM r∈supp f. snd (quotient_of r)) (LCM r∈supp g. snd (quotient_of r))" .
moreover have "lcm (LCM r∈supp f. snd (quotient_of r)) (LCM r∈supp g. snd (quotient_of r)) ≠ 0"
using fg by (auto simp: is_fpxs_def)
ultimately show "(LCM r∈supp (λx. f x + g x). snd (quotient_of r)) ≠ 0"
by auto
qed
qed
instance
by standard (transfer; simp add: algebra_simps fun_eq_iff)+
end
instance fpxs :: (comm_monoid_add) comm_monoid_add
proof
fix f g :: "'a fpxs"
show "f + g = g + f"
by transfer (auto simp: add_ac)
qed simp_all
lemma fpxs_nth_add [simp]: "fpxs_nth (f + g) r = fpxs_nth f r + fpxs_nth g r"
by transfer auto
lift_definition fpxs_of_fls :: "'a :: zero fls ⇒ 'a fpxs" is
"λf r. if r ∈ ℤ then f ⌊r⌋ else 0"
proof -
fix f :: "int ⇒ 'a"
assume "eventually (λn. f (-int n) = 0) cofinite"
hence "eventually (λn. f (-int n) = 0) at_top"
by (simp add: cofinite_eq_sequentially)
then obtain N where N: "f (-int n) = 0" if "n ≥ N" for n
by (auto simp: eventually_at_top_linorder)
show "is_fpxs (λr. if r ∈ ℤ then f ⌊r⌋ else 0)"
unfolding is_fpxs_def
proof
have "bdd_below {-(of_nat N::rat)..}"
by simp
moreover have "supp (λr::rat. if r ∈ ℤ then f ⌊r⌋ else 0) ⊆ {-of_nat N..}"
proof
fix r :: rat assume "r ∈ supp (λr. if r ∈ ℤ then f ⌊r⌋ else 0)"
then obtain m where [simp]: "r = of_int m" "f m ≠ 0"
by (auto simp: supp_def elim!: Ints_cases split: if_splits)
have "m ≥ -int N"
using N[of "nat (-m)"] by (cases "m ≥ 0"; cases "-int N ≤ m") (auto simp: le_nat_iff)
thus "r ∈ {-of_nat N..}" by simp
qed
ultimately show "bdd_below (supp (λr::rat. if r ∈ ℤ then f ⌊r⌋ else 0))"
by (rule bdd_below_mono)
next
have "(LCM r∈supp (λr. if r ∈ ℤ then f ⌊r⌋ else 0). snd (quotient_of r)) dvd 1"
by (intro Lcm_least) (auto simp: supp_def elim!: Ints_cases split: if_splits)
thus "(LCM r∈supp (λr. if r ∈ ℤ then f ⌊r⌋ else 0). snd (quotient_of r)) ≠ 0"
by (intro notI) simp
qed
qed
instantiation fpxs :: (group_add) group_add
begin
lift_definition uminus_fpxs :: "'a fpxs ⇒ 'a fpxs" is "λf x. -f x"
by (auto simp: is_fpxs_def)
definition minus_fpxs :: "'a fpxs ⇒ 'a fpxs ⇒ 'a fpxs" where
"minus_fpxs f g = f + (-g)"
instance proof
fix f :: "'a fpxs"
show "-f + f = 0"
by transfer auto
qed (auto simp: minus_fpxs_def)
end
lemma fpxs_nth_uminus [simp]: "fpxs_nth (-f) r = -fpxs_nth f r"
by transfer auto
lemma fpxs_nth_minus [simp]: "fpxs_nth (f - g) r = fpxs_nth f r - fpxs_nth g r"
unfolding minus_fpxs_def fpxs_nth_add fpxs_nth_uminus by simp
lemma fpxs_of_fls_eq_iff [simp]: "fpxs_of_fls f = fpxs_of_fls g ⟷ f = g"
by transfer (force simp: fun_eq_iff Ints_def)
lemma fpxs_of_fls_0 [simp]: "fpxs_of_fls 0 = 0"
by transfer auto
lemma fpxs_of_fls_1 [simp]: "fpxs_of_fls 1 = 1"
by transfer (auto simp: fun_eq_iff elim!: Ints_cases)
lemma fpxs_of_fls_add [simp]: "fpxs_of_fls (f + g) = fpxs_of_fls f + fpxs_of_fls g"
by transfer (auto simp: fun_eq_iff elim!: Ints_cases)
lemma fps_to_fls_sum [simp]: "fps_to_fls (sum f A) = (∑x∈A. fps_to_fls (f x))"
by (induction A rule: infinite_finite_induct) auto
lemma fpxs_of_fls_sum [simp]: "fpxs_of_fls (sum f A) = (∑x∈A. fpxs_of_fls (f x))"
by (induction A rule: infinite_finite_induct) auto
lemma fpxs_nth_of_fls:
"fpxs_nth (fpxs_of_fls f) r = (if r ∈ ℤ then fls_nth f ⌊r⌋ else 0)"
by transfer auto
lemma fpxs_of_fls_eq_0_iff [simp]: "fpxs_of_fls f = 0 ⟷ f = 0"
using fpxs_of_fls_eq_iff[of f 0] by (simp del: fpxs_of_fls_eq_iff)
lemma fpxs_of_fls_eq_1_iff [simp]: "fpxs_of_fls f = 1 ⟷ f = 1"
using fpxs_of_fls_eq_iff[of f 1] by (simp del: fpxs_of_fls_eq_iff)
lemma fpxs_root_order_of_fls [simp]: "fpxs_root_order (fpxs_of_fls f) = 1"
proof (transfer, goal_cases)
case (1 f)
have "supp (λr. if r ∈ ℤ then f ⌊r⌋ else 0) = rat_of_int ` {n. f n ≠ 0}"
by (force simp: supp_def Ints_def)
also have "(LCM r∈…. snd (quotient_of r)) = nat (LCM x∈{n. f n ≠ 0}. 1)"
by (simp add: image_image)
also have "… = 1"
by simp
also have "nat 1 = 1"
by simp
finally show ?case .
qed
subsection ‹The substitution $X \mapsto X^r$›
text ‹
This operation turns a formal Puiseux series $f(X)$ into $f(X^r)$, where
$r$ can be any positive rational number:
›
lift_definition fpxs_compose_power :: "'a :: zero fpxs ⇒ rat ⇒ 'a fpxs" is
"λf r x. if r > 0 then f (x / r) else 0"
proof -
fix f :: "rat ⇒ 'a" and r :: rat
assume f: "is_fpxs f"
have "is_fpxs (λx. f (x / r))" if "r > 0"
unfolding is_fpxs_def
proof
define r' where "r' = inverse r"
have "r' > 0"
using ‹r > 0› by (auto simp: r'_def)
have "(λx. x / r') ` supp f = supp (λx. f (x * r'))"
using ‹r' > 0› by (auto simp: supp_def image_iff vimage_def field_simps)
hence eq: "(λx. x * r) ` supp f = supp (λx. f (x / r))"
using ‹r > 0› by (simp add: r'_def field_simps)
from f have "bdd_below (supp f)"
by (auto simp: is_fpxs_def)
hence "bdd_below ((λx. x * r) ` supp f)"
using ‹r > 0› by (intro bdd_below_image_mono) (auto simp: mono_def divide_right_mono)
also note eq
finally show "bdd_below (supp (λx. f (x / r)))" .
define a b where "a = fst (quotient_of r)" and "b = snd (quotient_of r)"
have "b > 0" by (simp add: b_def quotient_of_denom_pos')
have [simp]: "quotient_of r = (a, b)"
by (simp add: a_def b_def)
have "r = of_int a / of_int b"
by (simp add: quotient_of_div)
with ‹r > 0› and ‹b > 0› have ‹a > 0›
by (simp add: field_simps)
have "(LCM r∈supp (λx. f (x / r)). snd (quotient_of r)) =
(LCM x∈supp f. snd (quotient_of (x * r)))"
by (simp add: eq [symmetric] image_image)
also have "… dvd (LCM x∈supp f. snd (quotient_of x) * b)"
using ‹a > 0› ‹b > 0›
by (intro Lcm_mono)
(simp add: rat_times_code case_prod_unfold Let_def Rat.normalize_def
quotient_of_denom_pos' div_dvd_self)
also have "… dvd normalize (b * (LCM x∈supp f. snd (quotient_of x)))"
proof (cases "supp f = {}")
case False
thus ?thesis using Lcm_mult[of "(λx. snd (quotient_of x)) ` supp f" b]
by (simp add: mult_ac image_image)
qed auto
hence "(LCM x∈supp f. snd (quotient_of x) * b) dvd
b * (LCM x∈supp f. snd (quotient_of x))" by simp
finally show "(LCM r∈supp (λx. f (x / r)). snd (quotient_of r)) ≠ 0"
using ‹b > 0› f by (auto simp: is_fpxs_def)
qed
thus "is_fpxs (λx. if r > 0 then f (x / r) else 0)"
by (cases "r > 0") (auto simp: is_fpxs_def supp_def)
qed
lemma fpxs_as_fls:
"fpxs_compose_power (fpxs_of_fls (fls_of_fpxs f)) (1 / of_nat (fpxs_root_order f)) = f"
proof (transfer, goal_cases)
case (1 f)
define d where "d = (LCM r∈supp f. snd (quotient_of r))"
have "d ≥ 0" by (simp add: d_def)
moreover have "d ≠ 0" using 1 by (simp add: is_fpxs_def d_def)
ultimately have "d > 0" by linarith
have "(if rat_of_int d * x ∈ ℤ then f (rat_of_int ⌊rat_of_int d * x⌋ / rat_of_int d) else 0) = f x" for x
proof (cases "rat_of_int d * x ∈ ℤ")
case True
then obtain n where n: "rat_of_int d * x = of_int n"
by (auto elim!: Ints_cases)
have "f (rat_of_int ⌊rat_of_int d * x⌋ / rat_of_int d) = f (rat_of_int n / rat_of_int d)"
by (simp add: n)
also have "rat_of_int n / rat_of_int d = x"
using n ‹d > 0› by (simp add: field_simps)
finally show ?thesis
using True by simp
next
case False
have "x ∉ supp f"
proof
assume "x ∈ supp f"
hence "snd (quotient_of x) dvd d"
by (simp add: d_def)
hence "rat_of_int (fst (quotient_of x) * d) / rat_of_int (snd (quotient_of x)) ∈ ℤ"
by (intro of_int_divide_in_Ints) auto
also have "rat_of_int (fst (quotient_of x) * d) / rat_of_int (snd (quotient_of x)) =
rat_of_int d * (rat_of_int (fst (quotient_of x)) / rat_of_int (snd (quotient_of x)))"
by (simp only: of_int_mult mult_ac times_divide_eq_right)
also have "… = rat_of_int d * x"
by (metis Fract_of_int_quotient Rat_cases normalize_stable prod.sel(1) prod.sel(2) quotient_of_Fract)
finally have "rat_of_int d * x ∈ ℤ" .
with False show False by contradiction
qed
thus ?thesis using False by (simp add: supp_def)
qed
thus ?case
using ‹d > 0› by (simp add: is_fpxs_def d_def mult_ac fun_eq_iff cong: if_cong)
qed
lemma fpxs_compose_power_0 [simp]: "fpxs_compose_power 0 r = 0"
by transfer simp
lemma fpxs_compose_power_1 [simp]: "r > 0 ⟹ fpxs_compose_power 1 r = 1"
by transfer (auto simp: fun_eq_iff)
lemma fls_of_fpxs_eq_0_iff [simp]: "fls_of_fpxs x = 0 ⟷ x = 0"
by (metis fls_of_fpxs_0 fpxs_as_fls fpxs_compose_power_0 fpxs_of_fls_0)
lemma fpxs_of_fls_compose_power [simp]:
"fpxs_of_fls (fls_compose_power f d) = fpxs_compose_power (fpxs_of_fls f) (of_nat d)"
proof (transfer, goal_cases)
case (1 f d)
show ?case
proof (cases "d = 0")
case False
show ?thesis
proof (intro ext, goal_cases)
case (1 r)
show ?case
proof (cases "r ∈ ℤ")
case True
then obtain n where [simp]: "r = of_int n"
by (cases r rule: Ints_cases)
show ?thesis
proof (cases "d dvd n")
case True
thus ?thesis by (auto elim!: Ints_cases)
next
case False
hence "rat_of_int n / rat_of_int (int d) ∉ ℤ"
using ‹d ≠ 0› by (subst of_int_div_of_int_in_Ints_iff) auto
thus ?thesis using False by auto
qed
next
case False
hence "r / rat_of_nat d ∉ ℤ"
using ‹d ≠ 0› by (auto elim!: Ints_cases simp: field_simps)
thus ?thesis using False by auto
qed
qed
qed auto
qed
lemma fpxs_compose_power_add [simp]:
"fpxs_compose_power (f + g) r = fpxs_compose_power f r + fpxs_compose_power g r"
by transfer (auto simp: fun_eq_iff)
lemma fpxs_compose_power_distrib:
"r1 > 0 ∨ r2 > 0 ⟹
fpxs_compose_power (fpxs_compose_power f r1) r2 = fpxs_compose_power f (r1 * r2)"
by transfer (auto simp: fun_eq_iff algebra_simps zero_less_mult_iff)
lemma fpxs_compose_power_divide_right:
"r1 > 0 ⟹ r2 > 0 ⟹
fpxs_compose_power f (r1 / r2) = fpxs_compose_power (fpxs_compose_power f r1) (inverse r2)"
by (simp add: fpxs_compose_power_distrib field_simps)
lemma fpxs_compose_power_1_right [simp]: "fpxs_compose_power f 1 = f"
by transfer auto
lemma fpxs_compose_power_eq_iff [simp]:
assumes "r > 0"
shows "fpxs_compose_power f r = fpxs_compose_power g r ⟷ f = g"
using assms
proof (transfer, goal_cases)
case (1 r f g)
have "f x = g x" if "⋀x. f (x / r) = g (x / r)" for x
using that[of "x * r"] ‹r > 0› by auto
thus ?case using ‹r > 0› by (auto simp: fun_eq_iff)
qed
lemma fpxs_compose_power_eq_1_iff [simp]:
assumes "l > 0"
shows "fpxs_compose_power p l = 1 ⟷ p = 1"
proof -
have "fpxs_compose_power p l = 1 ⟷ fpxs_compose_power p l = fpxs_compose_power 1 l"
by (subst fpxs_compose_power_1) (use assms in auto)
also have "… ⟷ p = 1"
using assms by (subst fpxs_compose_power_eq_iff) auto
finally show ?thesis .
qed
lemma fpxs_compose_power_eq_0_iff [simp]:
assumes "r > 0"
shows "fpxs_compose_power f r = 0 ⟷ f = 0"
using fpxs_compose_power_eq_iff[of r f 0] assms by (simp del: fpxs_compose_power_eq_iff)
lemma fls_of_fpxs_of_fls [simp]: "fls_of_fpxs (fpxs_of_fls f) = f"
using fpxs_as_fls[of "fpxs_of_fls f"] by simp
lemma fpxs_as_fls':
assumes "fpxs_root_order f dvd d" "d > 0"
obtains f' where "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)"
proof -
define D where "D = fpxs_root_order f"
have "D > 0"
by (auto simp: D_def)
define f' where "f' = fls_of_fpxs f"
from assms obtain d' where d': "d = D * d'"
by (auto simp: D_def)
have "d' > 0"
using assms by (auto intro!: Nat.gr0I simp: d')
define f'' where "f'' = fls_compose_power f' d'"
have "fpxs_compose_power (fpxs_of_fls f'') (1 / of_nat d) = f"
using ‹D > 0› ‹d' > 0›
by (simp add: d' D_def f''_def f'_def fpxs_as_fls fpxs_compose_power_distrib)
thus ?thesis using that[of f''] by blast
qed
subsection ‹Mutiplication and ring properties›
instantiation fpxs :: (comm_semiring_1) comm_semiring_1
begin
lift_definition times_fpxs :: "'a fpxs ⇒ 'a fpxs ⇒ 'a fpxs" is
"λf g x. (∑(y,z) | y ∈ supp f ∧ z ∈ supp g ∧ x = y + z. f y * g z)"
proof -
fix f g :: "rat ⇒ 'a"
assume fg: "is_fpxs f" "is_fpxs g"
show "is_fpxs (λx. ∑(y,z) | y ∈ supp f ∧ z ∈ supp g ∧ x = y + z. f y * g z)"
(is "is_fpxs ?h") unfolding is_fpxs_def
proof
from fg obtain bnd1 bnd2 where bnds: "∀x∈supp f. x ≥ bnd1" "∀x∈supp g. x ≥ bnd2"
by (auto simp: is_fpxs_def bdd_below_def)
have "supp ?h ⊆ (λ(x,y). x + y) ` (supp f × supp g)"
proof
fix x :: rat
assume "x ∈ supp ?h"
have "{(y,z). y ∈ supp f ∧ z ∈ supp g ∧ x = y + z} ≠ {}"
proof
assume eq: "{(y,z). y ∈ supp f ∧ z ∈ supp g ∧ x = y + z} = {}"
hence "?h x = 0"
by (simp only:) auto
with ‹x ∈ supp ?h› show False by (auto simp: supp_def)
qed
thus "x ∈ (λ(x,y). x + y) ` (supp f × supp g)"
by auto
qed
also have "… ⊆ {bnd1 + bnd2..}"
using bnds by (auto intro: add_mono)
finally show "bdd_below (supp ?h)"
by auto
next
define d1 where "d1 = (LCM r∈supp f. snd (quotient_of r))"
define d2 where "d2 = (LCM r∈supp g. snd (quotient_of r))"
have "(LCM r∈supp ?h. snd (quotient_of r)) dvd (d1 * d2)"
proof (intro Lcm_least, safe)
fix r :: rat
assume "r ∈ supp ?h"
hence "(∑(y, z) | y ∈ supp f ∧ z ∈ supp g ∧ r = y + z. f y * g z) ≠ 0"
by (auto simp: supp_def)
hence "{(y, z). y ∈ supp f ∧ z ∈ supp g ∧ r = y + z} ≠ {}"
by (intro notI) simp_all
then obtain y z where yz: "y ∈ supp f" "z ∈ supp g" "r = y + z"
by auto
have "snd (quotient_of r) = snd (quotient_of y) * snd (quotient_of z) div
gcd (fst (quotient_of y) * snd (quotient_of z) +
fst (quotient_of z) * snd (quotient_of y))
(snd (quotient_of y) * snd (quotient_of z))"
by (simp add: ‹r = _› rat_plus_code case_prod_unfold Let_def
Rat.normalize_def quotient_of_denom_pos')
also have "… dvd snd (quotient_of y) * snd (quotient_of z)"
by (metis dvd_def dvd_div_mult_self gcd_dvd2)
also have "… dvd d1 * d2"
using yz by (auto simp: d1_def d2_def intro!: mult_dvd_mono)
finally show "snd (quotient_of r) dvd d1 * d2"
by (simp add: d1_def d2_def)
qed
moreover have "d1 * d2 ≠ 0"
using fg by (auto simp: d1_def d2_def is_fpxs_def)
ultimately show "(LCM r∈supp ?h. snd (quotient_of r)) ≠ 0"
by auto
qed
qed
lemma fpxs_nth_mult:
"fpxs_nth (f * g) r =
(∑(y,z) | y ∈ fpxs_supp f ∧ z ∈ fpxs_supp g ∧ r = y + z. fpxs_nth f y * fpxs_nth g z)"
by transfer simp
lemma fpxs_compose_power_mult [simp]:
"fpxs_compose_power (f * g) r = fpxs_compose_power f r * fpxs_compose_power g r"
proof (transfer, rule ext, goal_cases)
case (1 f g r x)
show ?case
proof (cases "r > 0")
case True
have "(∑x∈{(y, z). y ∈ supp f ∧ z ∈ supp g ∧ x / r = y + z}.
case x of (y, z) ⇒ f y * g z) =
(∑x∈{(y, z). y ∈ supp (λx. f (x / r)) ∧ z ∈ supp (λx. g (x / r)) ∧ x = y + z}.
case x of (y, z) ⇒ f (y / r) * g (z / r))"
by (rule sum.reindex_bij_witness[of _ "λ(x,y). (x/r,y/r)" "λ(x,y). (x*r,y*r)"])
(use ‹r > 0› in ‹auto simp: supp_def field_simps›)
thus ?thesis
by (auto simp: fun_eq_iff)
qed auto
qed
lemma fpxs_supp_of_fls: "fpxs_supp (fpxs_of_fls f) = of_int ` supp (fls_nth f)"
by (force simp: fpxs_supp_def fpxs_nth_of_fls supp_def elim!: Ints_cases)
lemma fpxs_of_fls_mult [simp]: "fpxs_of_fls (f * g) = fpxs_of_fls f * fpxs_of_fls g"
proof (rule fpxs_ext)
fix r :: rat
show "fpxs_nth (fpxs_of_fls (f * g)) r = fpxs_nth (fpxs_of_fls f * fpxs_of_fls g) r"
proof (cases "r ∈ ℤ")
case True
define h1 where "h1 = (λ(x, y). (⌊x::rat⌋, ⌊y::rat⌋))"
define h2 where "h2 = (λ(x, y). (of_int x :: rat, of_int y :: rat))"
define df dg where [simp]: "df = fls_subdegree f" "dg = fls_subdegree g"
from True obtain n where [simp]: "r = of_int n"
by (cases rule: Ints_cases)
have "fpxs_nth (fpxs_of_fls f * fpxs_of_fls g) r =
(∑(y,z) | y ∈ fpxs_supp (fpxs_of_fls f) ∧ z ∈ fpxs_supp (fpxs_of_fls g) ∧ rat_of_int n = y + z.
(if y ∈ ℤ then fls_nth f ⌊y⌋ else 0) * (if z ∈ ℤ then fls_nth g ⌊z⌋ else 0))"
by (auto simp: fpxs_nth_mult fpxs_nth_of_fls)
also have "… = (∑(y,z) | y ∈ supp (fls_nth f) ∧ z ∈ supp (fls_nth g) ∧ n = y + z.
fls_nth f y * fls_nth g z)"
by (rule sum.reindex_bij_witness[of _ h2 h1]) (auto simp: h1_def h2_def fpxs_supp_of_fls)
also have "… = (∑y | y - fls_subdegree g ∈ supp (fls_nth f) ∧ fls_subdegree g + n - y ∈ supp (fls_nth g).
fls_nth f (y - fls_subdegree g) * fls_nth g (fls_subdegree g + n - y))"
by (rule sum.reindex_bij_witness[of _ "λy. (y - fls_subdegree g, fls_subdegree g + n - y)" "λz. fst z + fls_subdegree g"])
auto
also have "… = (∑i = fls_subdegree f + fls_subdegree g..n.
fls_nth f (i - fls_subdegree g) * fls_nth g (fls_subdegree g + n - i))"
using fls_subdegree_leI[of f] fls_subdegree_leI [of g]
by (intro sum.mono_neutral_left; force simp: supp_def)
also have "… = fpxs_nth (fpxs_of_fls (f * g)) r"
by (auto simp: fls_times_nth fpxs_nth_of_fls)
finally show ?thesis ..
next
case False
have "fpxs_nth (fpxs_of_fls f * fpxs_of_fls g) r =
(∑(y,z) | y ∈ fpxs_supp (fpxs_of_fls f) ∧ z ∈ fpxs_supp (fpxs_of_fls g) ∧ r = y + z.
(if y ∈ ℤ then fls_nth f ⌊y⌋ else 0) * (if z ∈ ℤ then fls_nth g ⌊z⌋ else 0))"
by (simp add: fpxs_nth_mult fpxs_nth_of_fls)
also have "… = 0"
using False by (intro sum.neutral ballI) auto
also have "0 = fpxs_nth (fpxs_of_fls (f * g)) r"
using False by (simp add: fpxs_nth_of_fls)
finally show ?thesis ..
qed
qed
instance proof
show "0 ≠ (1 :: 'a fpxs)"
by transfer (auto simp: fun_eq_iff)
next
fix f :: "'a fpxs"
show "1 * f = f"
proof (transfer, goal_cases)
case (1 f)
have "{(y, z). y ∈ supp (λr. if r = 0 then (1::'a) else 0) ∧ z ∈ supp f ∧ x = y + z} =
(if x ∈ supp f then {(0, x)} else {})" for x
by (auto simp: supp_def split: if_splits)
thus ?case
by (auto simp: fun_eq_iff supp_def)
qed
next
fix f :: "'a fpxs"
show "0 * f = 0"
by transfer (auto simp: fun_eq_iff supp_def)
show "f * 0 = 0"
by transfer (auto simp: fun_eq_iff supp_def)
next
fix f g :: "'a fpxs"
show "f * g = g * f"
proof (transfer, rule ext, goal_cases)
case (1 f g x)
show "(∑(y, z)∈{(y, z). y ∈ supp f ∧ z ∈ supp g ∧ x = y + z}. f y * g z) =
(∑(y, z)∈{(y, z). y ∈ supp g ∧ z ∈ supp f ∧ x = y + z}. g y * f z)"
by (rule sum.reindex_bij_witness[of _ "λ(x,y). (y,x)" "λ(x,y). (y,x)"])
(auto simp: mult_ac)
qed
next
fix f g h :: "'a fpxs"
define d where "d = (LCM F∈{f,g,h}. fpxs_root_order F)"
have "d > 0"
by (auto simp: d_def intro!: Nat.gr0I)
obtain f' where f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)"
using fpxs_as_fls'[of f d] ‹d > 0› by (auto simp: d_def)
obtain g' where g: "g = fpxs_compose_power (fpxs_of_fls g') (1 / of_nat d)"
using fpxs_as_fls'[of g d] ‹d > 0› by (auto simp: d_def)
obtain h' where h: "h = fpxs_compose_power (fpxs_of_fls h') (1 / of_nat d)"
using fpxs_as_fls'[of h d] ‹d > 0› by (auto simp: d_def)
show "(f * g) * h = f * (g * h)"
by (simp add: f g h mult_ac
flip: fpxs_compose_power_mult fpxs_compose_power_add fpxs_of_fls_mult)
show "(f + g) * h = f * h + g * h"
by (simp add: f g h ring_distribs
flip: fpxs_compose_power_mult fpxs_compose_power_add fpxs_of_fls_mult fpxs_of_fls_add)
qed
end
instance fpxs :: (comm_ring_1) comm_ring_1
by intro_classes auto
instance fpxs :: ("{comm_semiring_1,semiring_no_zero_divisors}") semiring_no_zero_divisors
proof
fix f g :: "'a fpxs"
assume fg: "f ≠ 0" "g ≠ 0"
define d where "d = lcm (fpxs_root_order f) (fpxs_root_order g)"
have "d > 0"
by (auto simp: d_def intro!: lcm_pos_nat)
obtain f' where f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)"
using fpxs_as_fls'[of f d] ‹d > 0› by (auto simp: d_def)
obtain g' where g: "g = fpxs_compose_power (fpxs_of_fls g') (1 / of_nat d)"
using fpxs_as_fls'[of g d] ‹d > 0› by (auto simp: d_def)
show "f * g ≠ 0"
using ‹d > 0› fg
by (simp add: f g flip: fpxs_compose_power_mult fpxs_of_fls_mult)
qed
lemma fpxs_of_fls_power [simp]: "fpxs_of_fls (f ^ n) = fpxs_of_fls f ^ n"
by (induction n) auto
lemma fpxs_compose_power_power [simp]:
"r > 0 ⟹ fpxs_compose_power (f ^ n) r = fpxs_compose_power f r ^ n"
by (induction n) simp_all
subsection ‹Constant Puiseux series and the series ‹X››
lift_definition fpxs_const :: "'a :: zero ⇒ 'a fpxs" is
"λc n. if n = 0 then c else 0"
proof -
fix c :: 'a
have "supp (λn::rat. if n = 0 then c else 0) = (if c = 0 then {} else {0})"
by auto
thus "is_fpxs (λn::rat. if n = 0 then c else 0)"
unfolding is_fpxs_def by auto
qed
lemma fpxs_const_0 [simp]: "fpxs_const 0 = 0"
by transfer auto
lemma fpxs_const_1 [simp]: "fpxs_const 1 = 1"
by transfer auto
lemma fpxs_of_fls_const [simp]: "fpxs_of_fls (fls_const c) = fpxs_const c"
by transfer (auto simp: fun_eq_iff Ints_def)
lemma fls_of_fpxs_const [simp]: "fls_of_fpxs (fpxs_const c) = fls_const c"
by (metis fls_of_fpxs_of_fls fpxs_of_fls_const)
lemma fls_of_fpxs_1 [simp]: "fls_of_fpxs 1 = 1"
using fls_of_fpxs_const[of 1] by (simp del: fls_of_fpxs_const)
lift_definition fpxs_X :: "'a :: {one, zero} fpxs" is
"λx. if x = 1 then (1::'a) else 0"
by (cases "1 = (0 :: 'a)") (auto simp: is_fpxs_def cong: if_cong)
lemma fpxs_const_altdef: "fpxs_const x = fpxs_of_fls (fls_const x)"
by transfer auto
lemma fpxs_const_add [simp]: "fpxs_const (x + y) = fpxs_const x + fpxs_const y"
by transfer auto
lemma fpxs_const_mult [simp]:
fixes x y :: "'a::{comm_semiring_1}"
shows "fpxs_const (x * y) = fpxs_const x * fpxs_const y"
unfolding fpxs_const_altdef fls_const_mult_const[symmetric] fpxs_of_fls_mult ..
lemma fpxs_const_eq_iff [simp]:
"fpxs_const x = fpxs_const y ⟷ x = y"
by transfer (auto simp: fun_eq_iff)
lemma of_nat_fpxs_eq: "of_nat n = fpxs_const (of_nat n)"
by (induction n) auto
lemma fpxs_const_uminus [simp]: "fpxs_const (-x) = -fpxs_const x"
by transfer auto
lemma fpxs_const_diff [simp]: "fpxs_const (x - y) = fpxs_const x - fpxs_const y"
unfolding minus_fpxs_def by transfer auto
lemma of_int_fpxs_eq: "of_int n = fpxs_const (of_int n)"
by (induction n) (auto simp: of_nat_fpxs_eq)
subsection ‹More algebraic typeclass instances›
instance fpxs :: ("{comm_semiring_1,semiring_char_0}") semiring_char_0
proof
show "inj (of_nat :: nat ⇒ 'a fpxs)"
by (intro injI) (auto simp: of_nat_fpxs_eq)
qed
instance fpxs :: ("{comm_ring_1,ring_char_0}") ring_char_0 ..
instance fpxs :: (idom) idom ..
instantiation fpxs :: (field) field
begin
definition inverse_fpxs :: "'a fpxs ⇒ 'a fpxs" where
"inverse_fpxs f =
fpxs_compose_power (fpxs_of_fls (inverse (fls_of_fpxs f))) (1 / of_nat (fpxs_root_order f))"
definition divide_fpxs :: "'a fpxs ⇒ 'a fpxs ⇒ 'a fpxs" where
"divide_fpxs f g = f * inverse g"
instance proof
fix f :: "'a fpxs"
assume "f ≠ 0"
define f' where "f' = fls_of_fpxs f"
define d where "d = fpxs_root_order f"
have "d > 0" by (auto simp: d_def)
have f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / of_nat d)"
by (simp add: f'_def d_def fpxs_as_fls)
have "inverse f * f = fpxs_compose_power (fpxs_of_fls (inverse f')) (1 / of_nat d) * f"
by (simp add: inverse_fpxs_def f'_def d_def)
also have "fpxs_compose_power (fpxs_of_fls (inverse f')) (1 / of_nat d) * f =
fpxs_compose_power (fpxs_of_fls (inverse f' * f')) (1 / of_nat d)"
by (simp add: f)
also have "inverse f' * f' = 1"
using ‹f ≠ 0› ‹d > 0› by (simp add: f field_simps)
finally show "inverse f * f = 1"
using ‹d > 0› by simp
qed (auto simp: divide_fpxs_def inverse_fpxs_def)
end
instance fpxs :: (field_char_0) field_char_0 ..
subsection ‹Valuation›
definition fpxs_val :: "'a :: zero fpxs ⇒ rat" where
"fpxs_val f =
of_int (fls_subdegree (fls_of_fpxs f)) / rat_of_nat (fpxs_root_order f)"
lemma fpxs_val_of_fls [simp]: "fpxs_val (fpxs_of_fls f) = of_int (fls_subdegree f)"
by (simp add: fpxs_val_def)
lemma fpxs_nth_compose_power [simp]:
assumes "r > 0"
shows "fpxs_nth (fpxs_compose_power f r) n = fpxs_nth f (n / r)"
using assms by transfer auto
lemma fls_of_fpxs_uminus [simp]: "fls_of_fpxs (-f) = -fls_of_fpxs f"
by transfer auto
lemma fpxs_root_order_uminus [simp]: "fpxs_root_order (-f) = fpxs_root_order f"
by transfer auto
lemma fpxs_val_uminus [simp]: "fpxs_val (-f) = fpxs_val f"
unfolding fpxs_val_def by simp
lemma fpxs_val_minus_commute: "fpxs_val (f - g) = fpxs_val (g - f)"
by (subst fpxs_val_uminus [symmetric]) (simp del: fpxs_val_uminus)
lemma fpxs_val_const [simp]: "fpxs_val (fpxs_const c) = 0"
by (simp add: fpxs_val_def)
lemma fpxs_val_1 [simp]: "fpxs_val 1 = 0"
by (simp add: fpxs_val_def)
lemma of_int_fls_subdegree_of_fpxs:
"rat_of_int (fls_subdegree (fls_of_fpxs f)) = fpxs_val f * of_nat (fpxs_root_order f)"
by (simp add: fpxs_val_def)
lemma fpxs_nth_val_nonzero:
assumes "f ≠ 0"
shows "fpxs_nth f (fpxs_val f) ≠ 0"
proof -
define N where "N = fpxs_root_order f"
define f' where "f' = fls_of_fpxs f"
define M where "M = fls_subdegree f'"
have val: "fpxs_val f = of_int M / of_nat N"
by (simp add: M_def fpxs_val_def N_def f'_def)
have *: "f = fpxs_compose_power (fpxs_of_fls f') (1 / rat_of_nat N)"
by (simp add: fpxs_as_fls N_def f'_def)
also have "fpxs_nth … (fpxs_val f) =
fpxs_nth (fpxs_of_fls f') (fpxs_val f * rat_of_nat (fpxs_root_order f))"
by (subst fpxs_nth_compose_power) (auto simp: N_def)
also have "… = fls_nth f' M"
by (subst fpxs_nth_of_fls) (auto simp: val N_def)
also have "f' ≠ 0"
using * assms by auto
hence "fls_nth f' M ≠ 0"
unfolding M_def by simp
finally show "fpxs_nth f (fpxs_val f) ≠ 0" .
qed
lemma fpxs_nth_below_val:
assumes n: "n < fpxs_val f"
shows "fpxs_nth f n = 0"
proof (cases "f = 0")
case False
define N where "N = fpxs_root_order f"
define f' where "f' = fls_of_fpxs f"
define M where "M = fls_subdegree f'"
have val: "fpxs_val f = of_int M / of_nat N"
by (simp add: M_def fpxs_val_def N_def f'_def)
have *: "f = fpxs_compose_power (fpxs_of_fls f') (1 / rat_of_nat N)"
by (simp add: fpxs_as_fls N_def f'_def)
have "fpxs_nth f n = fpxs_nth (fpxs_of_fls f') (n * rat_of_nat N)"
by (subst *, subst fpxs_nth_compose_power) (auto simp: N_def)
also have "… = 0"
proof (cases "rat_of_nat N * n ∈ ℤ")
case True
then obtain n' where n': "of_int n' = rat_of_nat N * n"
by (elim Ints_cases) auto
have "of_int n' < rat_of_nat N * fpxs_val f"
unfolding n' using n by (intro mult_strict_left_mono) (auto simp: N_def)
also have "… = of_int M"
by (simp add: val N_def)
finally have "n' < M" by linarith
have "fpxs_nth (fpxs_of_fls f') (rat_of_nat N * n) = fls_nth f' n'"
unfolding n'[symmetric] by (subst fpxs_nth_of_fls) (auto simp: N_def)
also from ‹n' < M› have "… = 0"
unfolding M_def by simp
finally show ?thesis by (simp add: mult_ac)
qed (auto simp: fpxs_nth_of_fls mult_ac)
finally show "fpxs_nth f n = 0" .
qed auto
lemma fpxs_val_leI: "fpxs_nth f r ≠ 0 ⟹ fpxs_val f ≤ r"
using fpxs_nth_below_val[of r f]
by (cases "f = 0"; cases "fpxs_val f" r rule: linorder_cases) auto
lemma fpxs_val_0 [simp]: "fpxs_val 0 = 0"
by (simp add: fpxs_val_def)
lemma fpxs_val_geI:
assumes "f ≠ 0" "⋀r. r < r' ⟹ fpxs_nth f r = 0"
shows "fpxs_val f ≥ r'"
using fpxs_nth_val_nonzero[of f] assms by force
lemma fpxs_val_compose_power [simp]:
assumes "r > 0"
shows "fpxs_val (fpxs_compose_power f r) = fpxs_val f * r"
proof (cases "f = 0")
case [simp]: False
show ?thesis
proof (intro antisym)
show "fpxs_val (fpxs_compose_power f r) ≤ fpxs_val f * r"
using assms by (intro fpxs_val_leI) (simp add: fpxs_nth_val_nonzero)
next
show "fpxs_val f * r ≤ fpxs_val (fpxs_compose_power f r)"
proof (intro fpxs_val_geI)
show "fpxs_nth (fpxs_compose_power f r) r' = 0" if "r' < fpxs_val f * r" for r'
unfolding fpxs_nth_compose_power[OF assms]
by (rule fpxs_nth_below_val) (use that assms in ‹auto simp: field_simps›)
qed (use assms in auto)
qed
qed auto
lemma fpxs_val_add_ge:
assumes "f + g ≠ 0"
shows "fpxs_val (f + g) ≥ min (fpxs_val f) (fpxs_val g)"
proof (rule ccontr)
assume "¬(fpxs_val (f + g) ≥ min (fpxs_val f) (fpxs_val g))" (is "¬(?n ≥ _)")
hence "?n < fpxs_val f" "?n < fpxs_val g"
by auto
hence "fpxs_nth f ?n = 0" "fpxs_nth g ?n = 0"
by (intro fpxs_nth_below_val; simp; fail)+
hence "fpxs_nth (f + g) ?n = 0"
by simp
moreover have "fpxs_nth (f + g) ?n ≠ 0"
by (intro fpxs_nth_val_nonzero assms)
ultimately show False by contradiction
qed
lemma fpxs_val_diff_ge:
assumes "f ≠ g"
shows "fpxs_val (f - g) ≥ min (fpxs_val f) (fpxs_val g)"
using fpxs_val_add_ge[of f "-g"] assms by simp
lemma fpxs_nth_mult_val:
"fpxs_nth (f * g) (fpxs_val f + fpxs_val g) = fpxs_nth f (fpxs_val f) * fpxs_nth g (fpxs_val g)"
proof (cases "f = 0 ∨ g = 0")
case False
have "{(y, z). y ∈ fpxs_supp f ∧ z ∈ fpxs_supp g ∧ fpxs_val f + fpxs_val g = y + z} ⊆
{(fpxs_val f, fpxs_val g)}"
using False fpxs_val_leI[of f] fpxs_val_leI[of g] by (force simp: fpxs_supp_def supp_def)
hence "fpxs_nth (f * g) (fpxs_val f + fpxs_val g) =
(∑(y, z)∈{(fpxs_val f, fpxs_val g)}. fpxs_nth f y * fpxs_nth g z)"
unfolding fpxs_nth_mult
by (intro sum.mono_neutral_left) (auto simp: fpxs_supp_def supp_def)
thus ?thesis by simp
qed auto
lemma fpxs_val_mult [simp]:
fixes f g :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs"
assumes "f ≠ 0" "g ≠ 0"
shows "fpxs_val (f * g) = fpxs_val f + fpxs_val g"
proof (intro antisym fpxs_val_leI fpxs_val_geI)
fix r :: rat
assume r: "r < fpxs_val f + fpxs_val g"
show "fpxs_nth (f * g) r = 0"
unfolding fpxs_nth_mult using assms fpxs_val_leI[of f] fpxs_val_leI[of g] r
by (intro sum.neutral; force)
qed (use assms in ‹auto simp: fpxs_nth_mult_val fpxs_nth_val_nonzero›)
lemma fpxs_val_power [simp]:
fixes f :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs"
assumes "f ≠ 0 ∨ n > 0"
shows "fpxs_val (f ^ n) = of_nat n * fpxs_val f"
proof (cases "f = 0")
case False
have [simp]: "f ^ n ≠ 0" for n
using False by (induction n) auto
thus ?thesis using False
by (induction n) (auto simp: algebra_simps)
qed (use assms in ‹auto simp: power_0_left›)
lemma fpxs_nth_power_val [simp]:
fixes f :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs"
shows "fpxs_nth (f ^ r) (rat_of_nat r * fpxs_val f) = fpxs_nth f (fpxs_val f) ^ r"
proof (cases "f ≠ 0")
case True
show ?thesis
proof (induction r)
case (Suc r)
have "fpxs_nth (f ^ Suc r) (rat_of_nat (Suc r) * fpxs_val f) =
fpxs_nth (f * f ^ r) (fpxs_val f + fpxs_val (f ^ r))"
using True by (simp add: fpxs_nth_mult_val ring_distribs)
also have "… = fpxs_nth f (fpxs_val f) ^ Suc r"
using Suc True by (subst fpxs_nth_mult_val) auto
finally show ?case .
qed (auto simp: fpxs_nth_1')
next
case False
thus ?thesis
by (cases r) (auto simp: fpxs_nth_1')
qed
subsection ‹Powers of ‹X› and shifting›
lift_definition fpxs_X_power :: "rat ⇒ 'a :: {zero, one} fpxs" is
"λr n :: rat. if n = r then 1 else (0 :: 'a)"
proof -
fix r :: rat
have "supp (λn. if n = r then 1 else (0 :: 'a)) = (if (1 :: 'a) = 0 then {} else {r})"
by (auto simp: supp_def)
thus "is_fpxs (λn. if n = r then 1 else (0 :: 'a))"
using quotient_of_denom_pos'[of r] by (auto simp: is_fpxs_def)
qed
lemma fpxs_X_power_0 [simp]: "fpxs_X_power 0 = 1"
by transfer auto
lemma fpxs_X_power_add: "fpxs_X_power (a + b) = fpxs_X_power a * fpxs_X_power b"
proof (transfer, goal_cases)
case (1 a b)
have *: "{(y,z). y ∈ supp (λn. if n=a then (1::'a) else 0) ∧
z ∈ supp (λn. if n=b then (1::'a) else 0) ∧ x=y+z} =
(if x = a + b then {(a, b)} else {})" for x
by (auto simp: supp_def fun_eq_iff)
show ?case
unfolding * by (auto simp: fun_eq_iff case_prod_unfold)
qed
lemma fpxs_X_power_mult: "fpxs_X_power (rat_of_nat n * m) = fpxs_X_power m ^ n"
by (induction n) (auto simp: ring_distribs fpxs_X_power_add)
lemma fpxs_of_fls_X_power [simp]: "fpxs_of_fls (fls_shift n 1) = fpxs_X_power (-rat_of_int n)"
by transfer (auto simp: fun_eq_iff Ints_def simp flip: of_int_minus)
lemma fpxs_X_power_neq_0 [simp]: "fpxs_X_power r ≠ (0 :: 'a :: zero_neq_one fpxs)"
by transfer (auto simp: fun_eq_iff)
lemma fpxs_X_power_eq_1_iff [simp]: "fpxs_X_power r = (1 :: 'a :: zero_neq_one fpxs) ⟷ r = 0"
by transfer (auto simp: fun_eq_iff)
lift_definition fpxs_shift :: "rat ⇒ 'a :: zero fpxs ⇒ 'a fpxs" is
"λr f n. f (n + r)"
proof -
fix r :: rat and f :: "rat ⇒ 'a"
assume f: "is_fpxs f"
have subset: "supp (λn. f (n + r)) ⊆ (λn. n + r) -` supp f"
by (auto simp: supp_def)
have eq: "(λn. n + r) -` supp f = (λn. n - r) ` supp f"
by (auto simp: image_iff algebra_simps)
show "is_fpxs (λn. f (n + r))"
unfolding is_fpxs_def
proof
have "bdd_below ((λn. n + r) -` supp f)"
unfolding eq by (rule bdd_below_image_mono) (use f in ‹auto simp: is_fpxs_def mono_def›)
thus "bdd_below (supp (λn. f (n + r)))"
by (rule bdd_below_mono[OF _ subset])
next
have "(LCM r∈supp (λn. f (n + r)). snd (quotient_of r)) dvd
(LCM r∈(λn. n + r) -` supp f. snd (quotient_of r))"
by (intro Lcm_subset image_mono subset)
also have "… = (LCM x∈supp f. snd (quotient_of (x - r)))"
by (simp only: eq image_image o_def)
also have "… dvd (LCM x∈supp f. snd (quotient_of r) * snd (quotient_of x))"
by (subst mult.commute, intro Lcm_mono quotient_of_denom_diff_dvd)
also have "… = Lcm ((λx. snd (quotient_of r) * x) ` (λx. snd (quotient_of x)) ` supp f)"
by (simp add: image_image o_def)
also have "… dvd normalize (snd (quotient_of r) * (LCM x∈supp f. snd (quotient_of x)))"
proof (cases "supp f = {}")
case False
thus ?thesis by (subst Lcm_mult) auto
qed auto
finally show "(LCM r∈supp (λn. f (n + r)). snd (quotient_of r)) ≠ 0"
using quotient_of_denom_pos'[of r] f by (auto simp: is_fpxs_def)
qed
qed
lemma fpxs_nth_shift [simp]: "fpxs_nth (fpxs_shift r f) n = fpxs_nth f (n + r)"
by transfer simp_all
lemma fpxs_shift_0_left [simp]: "fpxs_shift 0 f = f"
by transfer auto
lemma fpxs_shift_add_left: "fpxs_shift (m + n) f = fpxs_shift m (fpxs_shift n f)"
by transfer (simp_all add: add_ac)
lemma fpxs_shift_diff_left: "fpxs_shift (m - n) f = fpxs_shift m (fpxs_shift (-n) f)"
by (subst fpxs_shift_add_left [symmetric]) auto
lemma fpxs_shift_0 [simp]: "fpxs_shift r 0 = 0"
by transfer simp_all
lemma fpxs_shift_add [simp]: "fpxs_shift r (f + g) = fpxs_shift r f + fpxs_shift r g"
by transfer auto
lemma fpxs_shift_uminus [simp]: "fpxs_shift r (-f) = -fpxs_shift r f"
by transfer auto
lemma fpxs_shift_shift_uminus [simp]: "fpxs_shift r (fpxs_shift (-r) f) = f"
by (simp flip: fpxs_shift_add_left)
lemma fpxs_shift_shift_uminus' [simp]: "fpxs_shift (-r) (fpxs_shift r f) = f"
by (simp flip: fpxs_shift_add_left)
lemma fpxs_shift_diff [simp]: "fpxs_shift r (f - g) = fpxs_shift r f - fpxs_shift r g"
unfolding minus_fpxs_def by (subst fpxs_shift_add) auto
lemma fpxs_shift_compose_power [simp]:
"fpxs_shift r (fpxs_compose_power f s) = fpxs_compose_power (fpxs_shift (r / s) f) s"
by transfer (simp_all add: add_divide_distrib add_ac cong: if_cong)
lemma rat_of_int_div_dvd: "d dvd n ⟹ rat_of_int (n div d) = rat_of_int n / rat_of_int d"
by auto
lemma fpxs_of_fls_shift [simp]:
"fpxs_of_fls (fls_shift n f) = fpxs_shift (of_int n) (fpxs_of_fls f)"
proof (transfer, goal_cases)
case (1 n f)
show ?case
proof
fix r :: rat
have eq: "r + rat_of_int n ∈ ℤ ⟷ r ∈ ℤ"
by (metis Ints_add Ints_diff Ints_of_int add_diff_cancel_right')
show "(if r ∈ ℤ then f (⌊r⌋ + n) else 0) =
(if r + rat_of_int n ∈ ℤ then f ⌊r + rat_of_int n⌋ else 0)"
unfolding eq by auto
qed
qed
lemma fpxs_shift_mult: "f * fpxs_shift r g = fpxs_shift r (f * g)"
"fpxs_shift r f * g = fpxs_shift r (f * g)"
proof -
obtain a b where ab: "r = of_int a / of_nat b" and "b > 0"
by (metis Fract_of_int_quotient of_int_of_nat_eq quotient_of_unique zero_less_imp_eq_int)
define s where "s = lcm b (lcm (fpxs_root_order f) (fpxs_root_order g))"
have "s > 0" using ‹b > 0›
by (auto simp: s_def intro!: Nat.gr0I)
obtain f' where f: "f = fpxs_compose_power (fpxs_of_fls f') (1 / rat_of_nat s)"
using fpxs_as_fls'[of f s] ‹s > 0› by (auto simp: s_def)
obtain g' where g: "g = fpxs_compose_power (fpxs_of_fls g') (1 / rat_of_nat s)"
using fpxs_as_fls'[of g s] ‹s > 0› by (auto simp: s_def)
define n where "n = (a * s) div b"
have "b dvd s"
by (auto simp: s_def)
have sr_eq: "r * rat_of_nat s = rat_of_int n"
using ‹b > 0› ‹b dvd s›
by (simp add: ab field_simps of_rat_divide of_rat_mult n_def rat_of_int_div_dvd)
show "f * fpxs_shift r g = fpxs_shift r (f * g)" "fpxs_shift r f * g = fpxs_shift r (f * g)"
unfolding f g using ‹s > 0›
by (simp_all flip: fpxs_compose_power_mult fpxs_of_fls_mult fpxs_of_fls_shift
add: sr_eq fls_shifted_times_simps mult_ac)
qed
lemma fpxs_shift_1: "fpxs_shift r 1 = fpxs_X_power (-r)"
by transfer (auto simp: fun_eq_iff)
lemma fpxs_X_power_conv_shift: "fpxs_X_power r = fpxs_shift (-r) 1"
by (simp add: fpxs_shift_1)
lemma fpxs_shift_power [simp]: "fpxs_shift n x ^ m = fpxs_shift (of_nat m * n) (x ^ m)"
by (induction m) (simp_all add: algebra_simps fpxs_shift_mult flip: fpxs_shift_add_left)
lemma fpxs_compose_power_X_power [simp]:
"s > 0 ⟹ fpxs_compose_power (fpxs_X_power r) s = fpxs_X_power (r * s)"
by transfer (simp add: field_simps)
subsection ‹The ‹n›-th root of a Puiseux series›
text ‹
In this section, we define the formal root of a Puiseux series. This is done using the
same concept for formal power series. There is still one interesting theorems that is missing
here, e.g.\ the uniqueness (which could probably be lifted over from FPSs) somehow.
›
definition fpxs_radical :: "(nat ⇒ 'a :: field_char_0 ⇒ 'a) ⇒ nat ⇒ 'a fpxs ⇒ 'a fpxs" where
"fpxs_radical rt r f = (if f = 0 then 0 else
(let f' = fls_base_factor_to_fps (fls_of_fpxs f);
f'' = fpxs_of_fls (fps_to_fls (fps_radical rt r f'))
in fpxs_shift (-fpxs_val f / rat_of_nat r)
(fpxs_compose_power f'' (1 / rat_of_nat (fpxs_root_order f)))))"
lemma fpxs_radical_0 [simp]: "fpxs_radical rt r 0 = 0"
by (simp add: fpxs_radical_def)
lemma
fixes r :: nat
assumes r: "r > 0"
shows fpxs_power_radical:
"rt r (fpxs_nth f (fpxs_val f)) ^ r = fpxs_nth f (fpxs_val f) ⟹ fpxs_radical rt r f ^ r = f"
and fpxs_radical_lead_coeff:
"f ≠ 0 ⟹ fpxs_nth (fpxs_radical rt r f) (fpxs_val f / rat_of_nat r) =
rt r (fpxs_nth f (fpxs_val f))"
proof -
define q where "q = fpxs_root_order f"
define f' where "f' = fls_base_factor_to_fps (fls_of_fpxs f)"
have [simp]: "fps_nth f' 0 = fpxs_nth f (fpxs_val f)"
by (simp add: f'_def fls_nth_of_fpxs of_int_fls_subdegree_of_fpxs)
define f'' where "f'' = fpxs_of_fls (fps_to_fls (fps_radical rt r f'))"
have eq1: "fls_of_fpxs f = fls_shift (-fls_subdegree (fls_of_fpxs f)) (fps_to_fls f')"
by (subst fls_conv_base_factor_to_fps_shift_subdegree) (simp add: f'_def)
have eq2: "fpxs_compose_power (fpxs_of_fls (fls_of_fpxs f)) (1 / of_nat q) = f"
unfolding q_def by (rule fpxs_as_fls)
also note eq1
also have "fpxs_of_fls (fls_shift (- fls_subdegree (fls_of_fpxs f)) (fps_to_fls f')) =
fpxs_shift (- (fpxs_val f * rat_of_nat q)) (fpxs_of_fls (fps_to_fls f'))"
by (simp add: of_int_fls_subdegree_of_fpxs q_def)
finally have eq3: "fpxs_compose_power (fpxs_shift (- (fpxs_val f * rat_of_nat q))
(fpxs_of_fls (fps_to_fls f'))) (1 / rat_of_nat q) = f" .
{
assume rt: "rt r (fpxs_nth f (fpxs_val f)) ^ r = fpxs_nth f (fpxs_val f)"
show "fpxs_radical rt r f ^ r = f"
proof (cases "f = 0")
case [simp]: False
have "f'' ^ r = fpxs_of_fls (fps_to_fls (fps_radical rt r f' ^ r))"
by (simp add: fps_to_fls_power f''_def)
also have "fps_radical rt r f' ^ r = f'"
using power_radical[of f' rt "r - 1"] r rt by (simp add: fpxs_nth_val_nonzero)
finally have "f'' ^ r = fpxs_of_fls (fps_to_fls f')" .
have "fpxs_shift (-fpxs_val f / rat_of_nat r) (fpxs_compose_power f'' (1 / of_nat q)) ^ r =
fpxs_shift (-fpxs_val f) (fpxs_compose_power (f'' ^ r) (1 / of_nat q))"
unfolding q_def using r
by (subst fpxs_shift_power, subst fpxs_compose_power_power [symmetric]) simp_all
also have "f'' ^ r = fpxs_of_fls (fps_to_fls f')"
by fact
also have "fpxs_shift (-fpxs_val f) (fpxs_compose_power
(fpxs_of_fls (fps_to_fls f')) (1 / of_nat q)) = f"
using r eq3 by simp
finally show "fpxs_radical rt r f ^ r = f"
by (simp add: fpxs_radical_def f'_def f''_def q_def)
qed (use r in auto)
}
assume [simp]: "f ≠ 0"
have "fpxs_nth (fpxs_shift (-fpxs_val f / of_nat r) (fpxs_compose_power f'' (1 / of_nat q)))
(fpxs_val f / of_nat r) = fpxs_nth f'' 0"
using r by (simp add: q_def)
also have "fpxs_shift (-fpxs_val f / of_nat r) (fpxs_compose_power f'' (1 / of_nat q)) =
fpxs_radical rt r f"
by (simp add: fpxs_radical_def q_def f'_def f''_def)
also have "fpxs_nth f'' 0 = rt r (fpxs_nth f (fpxs_val f))"
using r by (simp add: f''_def fpxs_nth_of_fls)
finally show "fpxs_nth (fpxs_radical rt r f) (fpxs_val f / rat_of_nat r) =
rt r (fpxs_nth f (fpxs_val f))" .
qed
lemma fls_base_factor_power:
fixes f :: "'a::{semiring_1, semiring_no_zero_divisors} fls"
shows "fls_base_factor (f ^ n) = fls_base_factor f ^ n"
proof (cases "f = 0")
case False
have [simp]: "f ^ n ≠ 0" for n
by (induction n) (use False in auto)
show ?thesis using False
by (induction n) (auto simp: fls_base_factor_mult simp flip: fls_times_both_shifted_simp)
qed (cases n; simp)
hide_const (open) supp
subsection ‹Algebraic closedness›
text ‹
We will now show that the field of formal Puiseux series over an algebraically closed field of
characteristic 0 is again algebraically closed.
The typeclass constraint \<^class>‹field_gcd› is a technical constraint that mandates that
the field has a (trivial) GCD operation defined on it. It comes from some peculiarities of
Isabelle's typeclass system and can be considered unimportant, since any concrete type of
class \<^class>‹field› can easily be made an instance of \<^class>‹field_gcd›.
It would be possible to get rid of this constraint entirely here, but it is not worth
the effort.
The proof is a fairly standard one that uses Hensel's lemma. Some preliminary tricks are
required to be able to use it, however, namely a number of non-obvious changes of variables
to turn the polynomial with Puiseux coefficients into one with formal power series coefficients.
The overall approach was taken from an article by Nowak~\<^cite>‹"nowak2000"›.
Basically, what we need to show is this: Let
\[p(X,Z) = a_n(Z) X^n + a_{n-1}(Z) X^{n-1} + \ldots + a_0(Z)\]
be a polynomial in ‹X› of degree at least 2
with coefficients that are formal Puiseux series in ‹Z›. Then ‹p› is reducible, i.e. it splits
into two non-constant factors.
Due to work we have already done elsewhere, we may assume here that $a_n = 1$, $a_{n-1} = 0$, and
$a_0 \neq 0$, all of which will come in very useful.
›
instance fpxs :: ("{alg_closed_field, field_char_0, field_gcd}") alg_closed_field
proof (rule alg_closedI_reducible_coeff_deg_minus_one_eq_0)
fix p :: "'a fpxs poly"
assume deg_p: "degree p > 1" and lc_p: "lead_coeff p = 1"
assume coeff_deg_minus_1: "coeff p (degree p - 1) = 0"
assume "coeff p 0 ≠ 0"
define N where "N = degree p"
text ‹
Let $a_0, \ldots, a_n$ be the coefficients of ‹p› with $a_n = 1$. Now let ‹r› be the maximum of
$-\frac{\text{val}(a_i)}{n-i}$ ranging over all $i < n$ such that $a_i \neq 0$.
›
define r :: rat
where "r = (MAX i∈{i∈{..<N}. coeff p i ≠ 0}.
-fpxs_val (poly.coeff p i) / (rat_of_nat N - rat_of_nat i))"
text ‹
We write $r = a / b$ such that all the $a_i$ can be written as Laurent series in
$X^{1/b}$, i.e. the root orders of all the $a_i$ divide $b$:
›
obtain a b where ab: "b > 0" "r = of_int a / of_nat b" "∀i≤N. fpxs_root_order (coeff p i) dvd b"
proof -
define b where "b = lcm (nat (snd (quotient_of r))) (LCM i∈{..N}. fpxs_root_order (coeff p i))"
define x where "x = b div nat (snd (quotient_of r))"
define a where "a = fst (quotient_of r) * int x"
show ?thesis
proof (rule that)
show "b > 0"
using quotient_of_denom_pos'[of r] by (auto simp: b_def intro!: Nat.gr0I)
have b_eq: "b = nat (snd (quotient_of r)) * x"
by (simp add: x_def b_def)
have "x > 0"
using b_eq ‹b > 0› by (auto intro!: Nat.gr0I)
have "r = rat_of_int (fst (quotient_of r)) / rat_of_int (int (nat (snd (quotient_of r))))"
using quotient_of_denom_pos'[of r] quotient_of_div[of r] by simp
also have "… = rat_of_int a / rat_of_nat b"
using ‹x > 0› by (simp add: a_def b_eq)
finally show "r = rat_of_int a / rat_of_nat b" .
show "∀i≤N. fpxs_root_order (poly.coeff p i) dvd b"
by (auto simp: b_def)
qed
qed
text ‹
We write all the coefficients of ‹p› as Laurent series in $X^{1/b}$:
›
have "∃c. coeff p i = fpxs_compose_power (fpxs_of_fls c) (1 / rat_of_nat b)" if i: "i ≤ N" for i
proof -
have "fpxs_root_order (coeff p i) dvd b"
using ab(3) i by auto
from fpxs_as_fls'[OF this ‹b > 0›] show ?thesis by metis
qed
then obtain c_aux where c_aux:
"coeff p i = fpxs_compose_power (fpxs_of_fls (c_aux i)) (1 / rat_of_nat b)" if "i ≤ N" for i
by metis
define c where "c = (λi. if i ≤ N then c_aux i else 0)"
have c: "coeff p i = fpxs_compose_power (fpxs_of_fls (c i)) (1 / rat_of_nat b)" for i
using c_aux[of i] by (auto simp: c_def N_def coeff_eq_0)
have c_eq_0 [simp]: "c i = 0" if "i > N" for i
using that by (auto simp: c_def)
have c_eq: "fpxs_of_fls (c i) = fpxs_compose_power (coeff p i) (rat_of_nat b)" for i
using c[of i] ‹b > 0› by (simp add: fpxs_compose_power_distrib)
text ‹
We perform another change of variables and multiply with a suitable power of ‹X› to turn our
Laurent coefficients into FPS coefficients:
›
define c' where "c' = (λi. fls_X_intpow ((int N - int i) * a) * c i)"
have "c' N = 1"
using c[of N] ‹lead_coeff p = 1› ‹b > 0› by (simp add: c'_def N_def)
have subdegree_c: "of_int (fls_subdegree (c i)) = fpxs_val (coeff p i) * rat_of_nat b"
if i: "i ≤ N" for i
proof -
have "rat_of_int (fls_subdegree (c i)) = fpxs_val (fpxs_of_fls (c i))"
by simp
also have "fpxs_of_fls (c i) = fpxs_compose_power (poly.coeff p i) (rat_of_nat b)"
by (subst c_eq) auto
also have "fpxs_val … = fpxs_val (coeff p i) * rat_of_nat b"
using ‹b > 0› by simp
finally show ?thesis .
qed
text ‹
We now write all the coefficients as FPSs:
›
have "∃c''. c' i = fps_to_fls c''" if "i ≤ N" for i
proof (cases "i = N")
case True
hence "c' i = fps_to_fls 1"
using ‹c' N = 1› by simp
thus ?thesis by metis
next
case i: False
show ?thesis
proof (cases "c i = 0")
case True
hence "c' i = 0" by (auto simp: c'_def)
thus ?thesis
by (metis fps_zero_to_fls)
next
case False
hence "coeff p i ≠ 0"
using c_eq[of i] by auto
hence r_ge: "r ≥ -fpxs_val (poly.coeff p i) / (rat_of_nat N - rat_of_nat i)"
unfolding r_def using i that False by (intro Max.coboundedI) auto
have "fls_subdegree (c' i) = fls_subdegree (c i) + (int N - int i) * a"
using i that False by (simp add: c'_def fls_X_intpow_times_conv_shift subdegree_c)
also have "rat_of_int … =
fpxs_val (poly.coeff p i) * of_nat b + (of_nat N - of_nat i) * of_int a"
using i that False by (simp add: subdegree_c)
also have "… = of_nat b * (of_nat N - of_nat i) *
(fpxs_val (poly.coeff p i) / (of_nat N - of_nat i) + r)"
using ‹b > 0› i by (auto simp: field_simps ab(2))
also have "… ≥ 0"
using r_ge that by (intro mult_nonneg_nonneg) auto
finally have "fls_subdegree (c' i) ≥ 0" by simp
hence "∃c''. c' i = fls_shift 0 (fps_to_fls c'')"
by (intro fls_as_fps') (auto simp: algebra_simps)
thus ?thesis by simp
qed
qed
then obtain c''_aux where c''_aux: "c' i = fps_to_fls (c''_aux i)" if "i ≤ N" for i
by metis
define c'' where "c'' = (λi. if i ≤ N then c''_aux i else 0)"
have c': "c' i = fps_to_fls (c'' i)" for i
proof (cases "i ≤ N")
case False
thus ?thesis by (auto simp: c'_def c''_def)
qed (auto simp: c''_def c''_aux)
have c''_eq: "fps_to_fls (c'' i) = c' i" for i
using c'[of i] by simp
define p' where "p' = Abs_poly c''"
have coeff_p': "coeff p' = c''"
unfolding p'_def
proof (rule coeff_Abs_poly)
fix i assume "i > N"
hence "coeff p i = 0"
by (simp add: N_def coeff_eq_0)
thus "c'' i = 0" using c'[of i] c[of i] ‹b > 0› ‹N < i› c''_def by auto
qed
text ‹
We set up some homomorphisms to convert between the two polynomials:
›
interpret comppow: map_poly_inj_idom_hom "(λx::'a fpxs. fpxs_compose_power x (1/rat_of_nat b))"
by unfold_locales (use ‹b > 0› in simp_all)
define lift_poly :: "'a fps poly ⇒ 'a fpxs poly" where
"lift_poly = (λp. pcompose p [:0, fpxs_X_power r:]) ∘
(map_poly ((λx. fpxs_compose_power x (1/rat_of_nat b)) ∘ fpxs_of_fls ∘ fps_to_fls))"
have [simp]: "degree (lift_poly q) = degree q" for q
unfolding lift_poly_def by (simp add: degree_map_poly)
interpret fps_to_fls: map_poly_inj_idom_hom fps_to_fls
by unfold_locales (simp_all add: fls_times_fps_to_fls)
interpret fpxs_of_fls: map_poly_inj_idom_hom fpxs_of_fls
by unfold_locales simp_all
interpret lift_poly: inj_idom_hom lift_poly
unfolding lift_poly_def
by (intro inj_idom_hom_compose inj_idom_hom_pcompose inj_idom_hom.inj_idom_hom_map_poly
fps_to_fls.base.inj_idom_hom_axioms fpxs_of_fls.base.inj_idom_hom_axioms
comppow.base.inj_idom_hom_axioms) simp_all
interpret lift_poly: map_poly_inj_idom_hom lift_poly
by unfold_locales
define C :: "'a fpxs" where "C = fpxs_X_power (- (rat_of_nat N * r))"
have [simp]: "C ≠ 0"
by (auto simp: C_def)
text ‹
Now, finally: the original polynomial and the new polynomial are related through the
\<^term>‹lift_poly› homomorphism:
›
have p_eq: "p = smult C (lift_poly p')"
using ‹b > 0›
by (intro poly_eqI)
(simp_all add: coeff_map_poly coeff_pcompose_linear coeff_p' c c''_eq c'_def C_def
ring_distribs fpxs_X_power_conv_shift fpxs_shift_mult lift_poly_def ab(2)
flip: fpxs_X_power_add fpxs_X_power_mult fpxs_shift_add_left)
have [simp]: "degree p' = N"
unfolding N_def using ‹b > 0› by (simp add: p_eq)
have lc_p': "lead_coeff p' = 1"
using c''_eq[of N] by (simp add: coeff_p' ‹c' N = 1›)
have "coeff p' (N - 1) = 0"
using coeff_deg_minus_1 ‹b > 0› unfolding N_def [symmetric]
by (simp add: p_eq lift_poly_def coeff_map_poly coeff_pcompose_linear)
text ‹
We reduce $p'(X,Z)$ to $p'(X,0)$:
›
define p'_proj where "p'_proj = reduce_fps_poly p'"
have [simp]: "degree p'_proj = N"
unfolding p'_proj_def using lc_p' by (subst degree_reduce_fps_poly_monic) simp_all
have lc_p'_proj: "lead_coeff p'_proj = 1"
unfolding p'_proj_def using lc_p' by (subst reduce_fps_poly_monic) simp_all
hence [simp]: "p'_proj ≠ 0"
by auto
have "coeff p'_proj (N - 1) = 0"
using ‹coeff p' (N - 1) = 0› by (simp add: p'_proj_def reduce_fps_poly_def)
text ‹
We now show that \<^term>‹p'_proj› splits into non-trivial coprime factors. To do this, we
have to show that it has two distinct roots, i.e. that it is not of the form $(X - c)^n$.
›
obtain g h where gh: "degree g > 0" "degree h > 0" "coprime g h" "p'_proj = g * h"
proof -
have "degree p'_proj > 1"
using deg_p by (auto simp: N_def)
text ‹Let ‹x› be an arbitrary root of \<^term>‹p'_proj›:›
then obtain x where x: "poly p'_proj x = 0"
using alg_closed_imp_poly_has_root[of p'_proj] by force
text ‹Assume for the sake of contradiction that \<^term>‹p'_proj› were equal to $(1-x)^n$:›
have not_only_one_root: "p'_proj ≠ [:-x, 1:] ^ N"
proof safe
assume *: "p'_proj = [:-x, 1:] ^ N"
text ‹
If ‹x› were non-zero, all the coefficients of ‹p'_proj› would also be non-zero by the
Binomial Theorem. Since we know that the coefficient of ‹n - 1› ∗‹is› zero, this means
that ‹x› must be zero:
›
have "coeff p'_proj (N - 1) = 0" by fact
hence "x = 0"
by (subst (asm) *, subst (asm) coeff_linear_poly_power) auto
text ‹
However, by our choice of ‹r›, we know that there is an index ‹i› such that ‹c' i› has
is non-zero and has valuation (i.e. subdegree) 0, which means that the ‹i›-th coefficient
of \<^term>‹p'_proj› must also be non-zero.
›
have "0 < N ∧ coeff p 0 ≠ 0"
using deg_p ‹coeff p 0 ≠ 0› by (auto simp: N_def)
hence "{i∈{..<N}. coeff p i ≠ 0} ≠ {}"
by blast
hence "r ∈ (λi. -fpxs_val (poly.coeff p i) / (rat_of_nat N - rat_of_nat i)) `
{i∈{..<N}. coeff p i ≠ 0}"
unfolding r_def using deg_p by (intro Max_in) (auto simp: N_def)
then obtain i where i: "i < N" "coeff p i ≠ 0"
"-fpxs_val (coeff p i) / (rat_of_nat N - rat_of_nat i) = r"
by blast
hence [simp]: "c' i ≠ 0"
using i c[of i] by (auto simp: c'_def)
have "fpxs_val (poly.coeff p i) = rat_of_int (fls_subdegree (c i)) / rat_of_nat b"
using subdegree_c[of i] i ‹b > 0› by (simp add: field_simps)
also have "fpxs_val (coeff p i) = -r * (rat_of_nat N - rat_of_nat i)"
using i by (simp add: field_simps)
finally have "rat_of_int (fls_subdegree (c i)) = - r * (of_nat N - of_nat i) * of_nat b"
using ‹b > 0› by (simp add: field_simps)
also have "c i = fls_shift ((int N - int i) * a) (c' i)"
using i by (simp add: c'_def ring_distribs fls_X_intpow_times_conv_shift
flip: fls_shifted_times_simps(2))
also have "fls_subdegree … = fls_subdegree (c' i) - (int N - int i) * a"
by (subst fls_shift_subdegree) auto
finally have "fls_subdegree (c' i) = 0"
using ‹b > 0› by (simp add: ab(2))
hence "subdegree (coeff p' i) = 0"
by (simp flip: c''_eq add: fls_subdegree_fls_to_fps coeff_p')
moreover have "coeff p' i ≠ 0"
using ‹c' i ≠ 0› c' coeff_p' by auto
ultimately have "coeff p' i $ 0 ≠ 0"
using subdegree_eq_0_iff by blast
also have "coeff p' i $ 0 = coeff p'_proj i"
by (simp add: p'_proj_def reduce_fps_poly_def)
also have "… = 0"
by (subst *, subst coeff_linear_poly_power) (use i ‹x = 0› in auto)
finally show False by simp
qed
text ‹
We can thus obtain our second root ‹y› from the factorisation:
›
have "∃y. x ≠ y ∧ poly p'_proj y = 0"
proof (rule ccontr)
assume *: "¬(∃y. x ≠ y ∧ poly p'_proj y = 0)"
have "p'_proj ≠ 0" by simp
then obtain A where A: "size A = degree p'_proj"
"p'_proj = smult (lead_coeff p'_proj) (∏x∈#A. [:-x, 1:])"
using alg_closed_imp_factorization[of p'_proj] by blast
have "set_mset A = {x. poly p'_proj x = 0}"
using lc_p'_proj by (subst A) (auto simp: poly_prod_mset)
also have "… = {x}"
using x * by auto
finally have "A = replicate_mset N x"
using set_mset_subset_singletonD[of A x] A(1) by simp
with A(2) have "p'_proj = [:- x, 1:] ^ N"
using lc_p'_proj by simp
with not_only_one_root show False
by contradiction
qed
then obtain y where "x ≠ y" "poly p'_proj y = 0"
by blast
text ‹
It now follows easily that \<^term>‹p'_proj› splits into non-trivial and coprime factors:
›
show ?thesis
proof (rule alg_closed_imp_poly_splits_coprime)
show "degree p'_proj > 1"
using deg_p by (simp add: N_def)
show "x ≠ y" "poly p'_proj x = 0" "poly p'_proj y = 0"
by fact+
qed (use that in metis)
qed
text ‹
By Hensel's lemma, these factors give rise to corresponding factors of ‹p'›:
›
interpret hensel: fps_hensel p' p'_proj g h
proof unfold_locales
show "lead_coeff p' = 1"
using lc_p' by simp
qed (use gh ‹coprime g h› in ‹simp_all add: p'_proj_def›)
text ‹All that remains now is to undo the variable substitutions we did above:›
have "p = [:C:] * lift_poly hensel.G * lift_poly hensel.H"
unfolding p_eq by (subst hensel.F_splits) (simp add: hom_distribs)
thus "¬irreducible p"
by (rule reducible_polyI) (use hensel.deg_G hensel.deg_H gh in simp_all)
qed
text ‹
We do not actually show that this is the algebraic closure since this cannot be stated
idiomatically in the typeclass setting and is probably not very useful either, but it can
be motivated like this:
Suppose we have an algebraically closed extension $L$ of the field of Laurent series. Clearly,
$X^{a/b}\in L$ for any integer ‹a› and any positive integer ‹b› since
$(X^{a/b})^b - X^a = 0$. But any Puiseux series $F(X)$ with root order ‹b› can
be written as
\[F(X) = \sum_{k=0}^{b-1} X^{k/b} F_k(X)\]
where the Laurent series $F_k(X)$ are defined as follows:
\[F_k(X) := \sum_{n = n_{0,k}}^\infty [X^{n + k/b}] F(X) X^n\]
Thus, $F(X)$ can be written as a finite sum of products of elements in $L$ and must therefore
also be in $L$. Thus, the Puiseux series are all contained in $L$.
›
subsection ‹Metric and topology›
text ‹
Formal Puiseux series form a metric space with the usual metric for formal series:
Two series are ``close'' to one another if they have many initial coefficients in common.
›
instantiation fpxs :: (zero) norm
begin
definition norm_fpxs :: "'a fpxs ⇒ real" where
"norm f = (if f = 0 then 0 else 2 powr (-of_rat (fpxs_val f)))"
instance ..
end
instantiation fpxs :: (group_add) dist
begin
definition dist_fpxs :: "'a fpxs ⇒ 'a fpxs ⇒ real" where
"dist f g = (if f = g then 0 else 2 powr (-of_rat (fpxs_val (f - g))))"
instance ..
end
instantiation fpxs :: (group_add) metric_space
begin
definition uniformity_fpxs_def [code del]:
"(uniformity :: ('a fpxs × 'a fpxs) filter) = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"
definition open_fpxs_def [code del]:
"open (U :: 'a fpxs set) ⟷ (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"
instance proof
fix f g h :: "'a fpxs"
show "dist f g ≤ dist f h + dist g h"
proof (cases "f ≠ g ∧ f ≠ h ∧ g ≠ h")
case True
have "dist f g ≤ 2 powr -real_of_rat (min (fpxs_val (f - h)) (fpxs_val (g - h)))"
using fpxs_val_add_ge[of "f - h" "h - g"] True
by (auto simp: algebra_simps fpxs_val_minus_commute dist_fpxs_def of_rat_less_eq)
also have "… ≤ dist f h + dist g h"
using True by (simp add: dist_fpxs_def min_def)
finally show ?thesis .
qed (auto simp: dist_fpxs_def fpxs_val_minus_commute)
qed (simp_all add: uniformity_fpxs_def open_fpxs_def dist_fpxs_def)
end
instance fpxs :: (group_add) dist_norm
by standard (auto simp: dist_fpxs_def norm_fpxs_def)
end