Theory Formal_Puiseux_Series

(*
  File:    Formal_Puiseux_Series.thy
  Author:  Manuel Eberl, TU München
*)
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 rsupp 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 rsupp 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 rsupp f. snd (quotient_of r))  0"
    by (auto simp: is_fpxs_def)
  moreover have "(LCM rsupp f. snd (quotient_of r))  0"
    by simp
  ultimately show "nat (LCM rsupp 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 rsupp 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 "xsupp 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 rsupp 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 rsupp (λx. f x + g x). snd (quotient_of r)) dvd
            (LCM rsupp f  supp g. snd (quotient_of r))"
      by (intro Lcm_subset image_mono supp)
    also have " = lcm (LCM rsupp f. snd (quotient_of r)) (LCM rsupp g. snd (quotient_of r))"
      unfolding image_Un Lcm_Un ..
    finally have "(LCM rsupp (λx. f x + g x). snd (quotient_of r)) dvd
                    lcm (LCM rsupp f. snd (quotient_of r)) (LCM rsupp g. snd (quotient_of r))" .
    moreover have "lcm (LCM rsupp f. snd (quotient_of r)) (LCM rsupp g. snd (quotient_of r))  0"
      using fg by (auto simp: is_fpxs_def)
    ultimately show "(LCM rsupp (λ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 rsupp (λ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 rsupp (λ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) = (xA. 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) = (xA. 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 rsupp (λx. f (x / r)). snd (quotient_of r)) =
            (LCM xsupp f. snd (quotient_of (x * r)))"
      by (simp add: eq [symmetric] image_image)
    also have " dvd (LCM xsupp 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 xsupp 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 xsupp f. snd (quotient_of x) * b) dvd
             b * (LCM xsupp f. snd (quotient_of x))" by simp
    finally show "(LCM rsupp (λ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 rsupp 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: "xsupp f. x  bnd1" "xsupp 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 rsupp f. snd (quotient_of r))"
    define d2 where "d2 = (LCM rsupp g. snd (quotient_of r))"
    have "(LCM rsupp ?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 rsupp ?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 rsupp (λ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 xsupp f. snd (quotient_of (x - r)))"
      by (simp only: eq image_image o_def)
    also have " dvd (LCM xsupp 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 xsupp f. snd (quotient_of x)))"
    proof (cases "supp f = {}")
      case False
      thus ?thesis by (subst Lcm_mult) auto
    qed auto
    finally show "(LCM rsupp (λ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)

(* TODO: Uniqueness of radical. Also: composition and composition inverse *)

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 classfield_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 classfield can easily be made an instance of classfield_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" "iN. 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 "iN. 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
    termlift_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 termp'_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 termp'_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 termp'_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 termp'_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 termp'_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)  (xU. 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)

lemma fpxs_const_eq_0_iff [simp]: "fpxs_const x = 0  x = 0"
  by (metis fpxs_const_0 fpxs_const_eq_iff)

lemma semiring_char_fpxs [simp]: "CHAR('a :: comm_semiring_1 fpxs) = CHAR('a)"
  by (rule CHAR_eqI; unfold of_nat_fpxs_eq) (auto simp: of_nat_eq_0_iff_char_dvd)

instance fpxs :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char
  by (rule semiring_prime_charI) auto
instance fpxs :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char
  by standard
instance fpxs :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char
  by standard
instance fpxs :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char
  by standard
instance fpxs :: ("field_prime_char") field_prime_char
  by standard auto

end