Theory FLS_Prime_Equiv_Depth

(*  Title:       Computational p-Adics: Prime-Indexed Equivalence and Depth of Formal Laurent Series
    Author:      Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>, 2025
    Maintainer:  Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>
*)

theory FLS_Prime_Equiv_Depth

imports
  Parametric_Equiv_Depth
  "HOL.Equiv_Relations"
  "HOL-Computational_Algebra.Formal_Laurent_Series"

begin

unbundle fps_syntax

section ‹
  Equivalence of sequences of formal Laurent series relative to divisibility of partial sums by a
  fixed prime
›

subsection ‹Preliminaries›

subsubsection ‹Lift/transfer of equivalence relations.›

lemma relfp_transfer:
  "reflp r ⟹ reflp (λx y. r (f x) (f y))"
  unfolding reflp_def by fast

lemma symp_transfer:
  "symp r ⟹ symp (λx y. r (f x) (f y))"
  unfolding symp_def by fast

lemma transp_transfer:
  "transp r ⟹ transp (λx y. r (f x) (f y))"
  unfolding transp_def by fast

lemma equivp_transfer:
  "equivp r ⟹ equivp (λx y. r (f x) (f y))"
  using relfp_transfer symp_transfer transp_transfer
        equivp_reflp_symp_transp[of r] equivp_reflp_symp_transp[of "λx y. r (f x) (f y)"]
  by    fast

subsubsection ‹An additional fact about products/sums›

lemma (in comm_monoid_set) atLeastAtMost_int_shift_bounds:
  "F g {m..n} = F (g ∘ plus m ∘ int) {..nat (n - m)}"
  if  "m ≤ n"
  for m n :: int
proof (rule reindex_bij_witness)
  define i :: "nat ⇒ int" and j :: "int ⇒ nat"
    where "i ≡ plus m ∘ int"
    and   "j ≡ (λx. nat (x - m))"
  fix a b from i_def j_def that
    show  "a ∈ {m..n} ⟹ i (j a) = a"
    and   "a ∈ {m..n} ⟹ j a ∈ {..nat (n - m)}"
    and   "b ∈ {..nat (n - m)} ⟹ j (i b) = b"
    and   "b ∈ {..nat (n - m)} ⟹ i b ∈ {m..n}"
    and   "a ∈ {m..n} ⟹ (g ∘ (+) m ∘ int) (j a) = g a"
    by auto
qed

subsubsection ‹An additional fact about algebraic powers of functions›

lemma pow_fun_apply: "(f ^ n) x = (f x) ^ n"
  by (induct n, simp_all)

subsubsection ‹Some additional facts about formal power and Laurent series›

lemma fps_shift_fps_mult_by_fps_const:
  fixes c :: "'a::{comm_monoid_add,mult_zero}"
  shows "fps_shift n (fps_const c * f) = fps_const c * fps_shift n f"
  and   "fps_shift n (f * fps_const c) = fps_shift n f * fps_const c"
  by    (auto intro: fps_ext)

lemma fps_shift_mult_Suc:
  fixes f g :: "'a::{comm_monoid_add,mult_zero} fps"
  shows "fps_shift (Suc n) (f*g)
          = fps_const (f$0) * fps_shift (Suc n) g + fps_shift n (fps_shift 1 f * g)"
  and   "fps_shift (Suc n) (f*g)
          = fps_shift n (f * fps_shift 1 g) + fps_shift (Suc n) f * fps_const (g$0)"
proof-
  show "fps_shift (Suc n) (f*g)
          = fps_const (f$0) * fps_shift (Suc n) g + fps_shift n (fps_shift 1 f * g)"
  proof (intro fps_ext)
    fix k
    have "{0<..Suc (k + n)} = {Suc 0..Suc (k + n)}" by auto
    thus
      "fps_shift (Suc n) (f*g) $ k
        = (fps_const (f$0) * fps_shift (Suc n) g + fps_shift n (fps_shift 1 f * g)) $ k"
      using fps_mult_nth[of _ g]
            sum.head[of 0 "k + Suc n" "λi. f$i * g$(k + Suc n - i)"]
            sum.atLeast_Suc_atMost_Suc_shift[of "λi. f$i * g$(k + Suc n - i)" 0 "k+n"]
      by    simp
  qed
  show "fps_shift (Suc n) (f*g)
          = fps_shift n (f * fps_shift 1 g) + fps_shift (Suc n) f * fps_const (g$0)"
  proof (intro fps_ext)
    fix k
    have "∀i∈{0..k + n}. Suc (k + n) - i = Suc (k + n -i)" by auto
    thus "fps_shift (Suc n) (f*g) $ k
          = (fps_shift n (f * fps_shift 1 g) + fps_shift (Suc n) f * fps_const (g$0)) $ k"
      using fps_mult_nth[of f] by simp
  qed
qed

lemma fls_subdegree_minus':
  "fls_subdegree (f - g) = fls_subdegree f"
  if "f ≠ 0" and "fls_subdegree g > fls_subdegree f"
  using that by (auto intro: fls_subdegree_eqI)

lemma fls_regpart_times_fps_X:
  fixes   f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
  assumes "fls_subdegree f ≥ 0"
  shows   "fls_regpart f * fps_X = fls_regpart (fls_shift (-1) f)"
  and     "fps_X * fls_regpart f = fls_regpart (fls_shift (-1) f)"
proof-
  show "fls_regpart f * fps_X  = fls_regpart (fls_shift (-1) f)"
  proof (intro fps_ext)
    fix n show "(fls_regpart f * fps_X) $ n = fls_regpart (fls_shift (-1) f) $ n"
      using assms by (cases n) auto
  qed
  thus "fps_X * fls_regpart f = fls_regpart (fls_shift (-1) f)"
    by (simp add: fps_mult_fps_X_commute)
qed

lemma fls_regpart_times_fps_X_power:
  fixes   f :: "'a::semiring_1 fls"
  assumes "fls_subdegree f ≥ 0"
  shows   "fls_regpart f * fps_X ^ n = fls_regpart (fls_shift (-n) f)"
  and     "fps_X ^ n * fls_regpart f = fls_regpart (fls_shift (-n) f)"
proof-
  show "fps_X ^ n * fls_regpart f = fls_regpart (fls_shift (-n) f)"
  proof (induct n)
    case (Suc n)
    from assms Suc
      have  A: "fps_X ^ Suc n * fls_regpart f = fls_regpart (fls_shift (-(int n + 1)) f)"
      using fls_shift_nonneg_subdegree[of "-int n" f]
      by    (simp add: mult.assoc fls_regpart_times_fps_X(2))
    have B: "- (int n + 1) = - int (Suc n)" by simp
    have "fls_regpart (fls_shift (-(int n + 1)) f) = fls_regpart (fls_shift (- int (Suc n)) f)"
      using arg_cong[OF B] by simp
    with A show ?case by simp
  qed simp
  thus "fls_regpart f * fps_X ^ n = fls_regpart (fls_shift (-n) f)"
    by (simp flip: fps_mult_fps_X_power_commute)
qed

lemma fls_base_factor_uminus: "fls_base_factor (-f) = - fls_base_factor f"
  unfolding fls_base_factor_def by simp


subsection ‹Partial evaluation of formal power series›

text ‹Make a degree-n polynomial out of a formal power series.›
definition poly_of_fps
  where "poly_of_fps f n = Abs_poly (λi. if i ≤ n then f$i else 0)"

lemma if_then_MOST_zero:
  "∀⇩∞x. (if P x then f x else 0) = 0"
  if "∀⇩∞x. ¬ P x"
proof (rule iffD2, rule MOST_iff_cofinite)
  have "{x. (if P x then f x else 0) ≠ 0} ⊆ {x. ¬ ¬ P x}" by auto
  with that show "finite {x. (if P x then f x else 0) ≠ 0}"
    using iffD1[OF MOST_iff_cofinite] finite_subset by blast
qed

lemma truncated_fps_eventually_zero:
  "(λi. if i ≤ n then f$i else 0) ∈ {g. ∀⇩∞n. g n = 0}"
  by (auto intro: if_then_MOST_zero iffD2[OF eventually_cofinite])

lemma coeff_poly_of_fps[simp]:
  "coeff (poly_of_fps f n) i = (if i ≤ n then f$i else 0)"
  unfolding poly_of_fps_def
  using     truncated_fps_eventually_zero[of n f]
            Abs_poly_inverse[of "λi. if i ≤ n then f$i else 0"]
  by        simp

lemma poly_of_fps_0[simp]: "poly_of_fps 0 n = 0"
  by (auto intro: poly_eqI)

lemma poly_of_fps_0th_conv_pCons[simp]: "poly_of_fps f 0 = [:f$0:]"
proof (intro poly_eqI)
  fix i
  show "coeff (poly_of_fps f 0) i = coeff [:f$0:] i"
    by (cases i) auto
qed

lemma poly_of_fps_degree: "degree (poly_of_fps f n) ≤ n"
  by (auto intro: degree_le)

lemma poly_of_fps_Suc:
  "poly_of_fps f (Suc n) = poly_of_fps f n + monom (f $ Suc n) (Suc n)"
proof (intro poly_eqI)
  fix m
  show
    "coeff (poly_of_fps f (Suc n)) m =
      coeff (poly_of_fps f n + monom (f $ Suc n) (Suc n)) m"
    by (cases "m ≤ Suc n") auto
qed

lemma poly_of_fps_Suc_nth_eq0:
  "poly_of_fps f (Suc n) = poly_of_fps f n" if "f $ Suc n = 0"
proof (intro poly_eqI)
  fix i from that show "coeff (poly_of_fps f (Suc n)) i = coeff (poly_of_fps f n) i"
    by (cases i "Suc n" rule: linorder_cases) auto
qed

lemma poly_of_fps_Suc_conv_pCons_shift:
  "poly_of_fps f (Suc n) = pCons (f$0) (poly_of_fps (fps_shift 1 f) n)"
proof (intro poly_eqI)
  fix i
  show "coeff (poly_of_fps f (Suc n)) i
          = coeff (pCons (f$0) (poly_of_fps (fps_shift 1 f) n)) i"
    by (cases i) auto
qed

abbreviation "fps_parteval f x n ≡ poly (poly_of_fps f n) x"
abbreviation "fls_base_parteval f ≡ fps_parteval (fls_base_factor_to_fps f)"

lemma fps_parteval_0[simp]: "fps_parteval 0 x n = 0"
  by (induct n) auto

lemma fps_parteval_0th[simp]: "fps_parteval f x 0 = f $ 0"
  by simp

lemma fps_parteval_Suc:
  "fps_parteval f x (Suc n) = fps_parteval f x n + (f $ Suc n) * x ^ Suc n"
  for f :: "'a::comm_semiring_1 fps"
  by  (simp add: poly_of_fps_Suc poly_monom)

lemma fps_parteval_Suc_cons:
  "fps_parteval f x (Suc n) = f$0 + x * fps_parteval (fps_shift 1 f) x n"
  by (simp add: poly_of_fps_Suc_conv_pCons_shift)

lemma fps_parteval_at_0[simp]: "fps_parteval f 0 n = f $ 0"
  by (cases n) (auto simp add: fps_parteval_Suc_cons)

lemma fps_parteval_conv_sum:
  "fps_parteval f x n = (∑k≤n. f$k * x^k)" for x :: "'a::comm_semiring_1"
  by (induct n) (auto simp add: fps_parteval_Suc)

lemma fls_base_parteval_conv_sum:
  "fls_base_parteval f x n = (∑k≤n. f$$(fls_subdegree f + int k) * x^k)"
  for f :: "'a::comm_semiring_1 fls" and x :: 'a and n :: nat
  using fps_parteval_conv_sum[of "fls_base_factor_to_fps f"] fls_base_factor_to_fps_nth[of f]
  by    presburger

lemma fps_parteval_fps_const[simp]:
  "fps_parteval (fps_const c) x n = c"
  by (induct n) (auto simp add: fps_parteval_Suc_cons fps_shift_fps_const)

lemma fps_parteval_1[simp]: "fps_parteval 1 x n = 1"
  using fps_parteval_fps_const[of 1] by simp

lemma fps_parteval_mult_by_fps_const:
  "fps_parteval (fps_const c * f) x n = c * fps_parteval f x n"
  using mult.commute[of c x] mult.assoc[of x c] mult.assoc[of c x]
  by    (induct n arbitrary: f)
        (auto simp add: fps_parteval_Suc_cons fps_shift_fps_mult_by_fps_const(1) distrib_left)

lemma fps_parteval_plus[simp]:
  "fps_parteval (f + g) x n = fps_parteval f x n + fps_parteval g x n"
  by  (induct n arbitrary: f g)
      (auto simp add: fps_parteval_Suc_cons fps_shift_add algebra_simps)

lemma fps_parteval_uminus[simp]:
  "fps_parteval (-f) x n = - fps_parteval f x n" for f :: "'a::comm_ring fps"
  by  (induct n arbitrary: f) (auto simp add: fps_parteval_Suc_cons fps_shift_uminus)

lemma fps_parteval_minus[simp]:
  "fps_parteval (f - g) x n = fps_parteval f x n - fps_parteval g x n"
  for f :: "'a::comm_ring fps"
  using fps_parteval_plus[of f "-g"] by simp

lemma fps_parteval_mult_fps_X:
  fixes f :: "'a::comm_semiring_1 fps"
  shows "fps_parteval (f * fps_X) x (Suc n) = x * fps_parteval f x n"
  and   "fps_parteval (fps_X * f) x (Suc n) = x * fps_parteval f x n"
  using fps_shift_times_fps_X'[of f]
  by    (auto simp add: fps_parteval_Suc_cons simp flip: fps_mult_fps_X_commute)

lemma fps_parteval_mult_fps_X_power:
  fixes f :: "'a::comm_semiring_1 fps"
  assumes "n ≥ m"
  shows   "fps_parteval (f * fps_X ^ m) x n = x^m * fps_parteval f x (n - m)"
  and     "fps_parteval (fps_X ^ m * f) x n = x^m * fps_parteval f x (n - m)"
proof-
  have
    "n ≥ m ⟹ fps_parteval (f * fps_X ^ m) x n = x^m * fps_parteval f x (n - m)"
  proof (induct m arbitrary: n)
    case (Suc m) thus ?case
      using fps_shift_times_fps_X'[of "f * fps_X^m"]
      by    (cases n)
            (auto simp add: fps_parteval_Suc_cons mult.assoc simp flip: power_Suc2)
  qed simp
  with assms show "fps_parteval (f * fps_X ^ m) x n = x^m * fps_parteval f x (n - m)"
    by fast
  thus "fps_parteval (fps_X ^ m * f) x n = x^m * fps_parteval f x (n - m)"
    by (simp add: fps_mult_fps_X_power_commute)
qed

lemma fps_parteval_mult_right:
  "fps_parteval (f * g) x n =
    fps_parteval (Abs_fps (λi. f$i * fps_parteval g x (n - i))) x n"
proof (induct n arbitrary: f)
  case (Suc n)
  have 1:
    "poly_of_fps (Abs_fps (λi. f $ Suc i * fps_parteval g x (n - i))) n
      = poly_of_fps (Abs_fps (λi. f $ Suc i * fps_parteval g x (Suc n - Suc i))) n"
    by (intro poly_eqI) auto
  from Suc have
    "fps_parteval (fps_shift 1 f * g) x n
      = fps_parteval (Abs_fps (λi. f $ Suc i * fps_parteval g x (n - i))) x n"
    by simp
  with 1 have
    "fps_parteval (f * g) x (Suc n)
      = f$0 * fps_parteval g x (Suc n)
      + x * fps_parteval (Abs_fps (λi. f $ Suc i * fps_parteval g x (n - i))) x n
    "
    using fps_shift_mult_Suc(1)[of 0 f g]
    by (simp add: fps_parteval_Suc_cons fps_parteval_mult_by_fps_const algebra_simps)
  thus ?case by (simp add: fps_parteval_Suc_cons fps_shift_def)
qed simp

lemma fps_parteval_mult_left:
  "fps_parteval (f * g) x n =
    fps_parteval (Abs_fps (λi. fps_parteval f x (n - i) * g$i)) x n"
  using fps_parteval_mult_right[of g f]
  by    (simp add: mult.commute)

lemma fps_parteval_mult_conv_sum:
  fixes f g :: "'a::comm_semiring_1 fps"
  shows "fps_parteval (f * g) x n = (∑k≤n. f$k * fps_parteval g x (n - k) * x^k)"
  and   "fps_parteval (f * g) x n = (∑k≤n. fps_parteval f x (n - k) * g$k * x^k)"
  using fps_parteval_mult_right[of f g n x]
        fps_parteval_conv_sum[of "Abs_fps (λi. f$i * fps_parteval g x (n - i))"]
        fps_parteval_mult_left[of f g n x]
        fps_parteval_conv_sum[of "Abs_fps (λi. fps_parteval f x (n - i) * g$i)"]
  by    auto

lemma fps_parteval_fls_base_factor_to_fps_diff:
  "fls_base_parteval (f - g) x n = fls_base_parteval f x n"
  if "f ≠ 0" and "fls_subdegree g > fls_subdegree f + (int n)"
  for f g :: "'a::comm_ring_1 fls"
  using that
  by    (induct n) (auto simp add: fps_parteval_Suc fls_subdegree_minus')


subsection ‹
  Vanishing of formal power series relative to divisibility of all partial sums
›

definition fps_pvanishes :: "'a::comm_semiring_1 ⇒ 'a fps ⇒ bool"
  where "fps_pvanishes p f ≡ (∀n::nat. p ^ Suc n dvd (fps_parteval f p n))"

lemma fps_pvanishesD: "fps_pvanishes p f ⟹ p ^ Suc n dvd (fps_parteval f p n)"
  unfolding fps_pvanishes_def by simp

lemma fps_pvanishesI:
  "fps_pvanishes p f" if "⋀n::nat. p ^ Suc n dvd (fps_parteval f p n)"
  using that unfolding fps_pvanishes_def by simp

lemma fps_pvanishes_0[simp]: "fps_pvanishes p 0"
  by (auto intro: fps_pvanishesI)

lemma fps_pvanishes_at_0[simp]: "fps_pvanishes 0 f = (f$0 = 0)"
  unfolding fps_pvanishes_def by auto

lemma fps_pvanishes_at_unit: "fps_pvanishes p f" if "is_unit p"
  by (metis that is_unit_power_iff unit_imp_dvd fps_pvanishesI)

lemma fps_pvanishes_one_iff:
  "fps_pvanishes p 1 = is_unit p"
  using fps_pvanishes_def is_unit_power_iff[of p "Suc _"] by auto

lemma fps_pvanishes_uminus[simp]:
  "fps_pvanishes p (-f)" if "fps_pvanishes p f" for f :: "'a::comm_ring_1 fps"
  using fps_pvanishesD[OF that] iffD2[OF dvd_minus_iff] by (fastforce intro: fps_pvanishesI)

lemma fps_pvanishes_add[simp]:
  "fps_pvanishes p (f + g)" if "fps_pvanishes p f" and "fps_pvanishes p g"
  for f :: "'a::comm_semiring_1 fps"
proof (intro fps_pvanishesI)
  fix n from that show "p ^ Suc n dvd fps_parteval (f+g) p n"
    using fps_pvanishesD[of p _ n]
          dvd_add[of "p^Suc n" "fps_parteval f p n" "fps_parteval g p n"]
    by    auto
qed

lemma fps_pvanishes_minus[simp]:
  "fps_pvanishes p (f - g)" if "fps_pvanishes p f" and "fps_pvanishes p g"
  for f :: "'a::comm_ring_1 fps"
  using that fps_pvanishes_uminus[of p g] fps_pvanishes_add[of p f "-g"] by simp

lemma fps_pvanishes_mult: "fps_pvanishes p (f * g)" if "fps_pvanishes p g"
proof (intro fps_pvanishesI)
  fix n
  have "p ^ Suc n dvd (∑i≤n. f$i * fps_parteval g p (n - i) * p^i)"
  proof (intro dvd_sum)
    fix k assume "k ∈ {..n}"
    with that show "p ^ Suc n dvd f $ k * fps_parteval g p (n - k) * p ^ k"
      using fps_pvanishesD[of p g] power_add[of p "Suc (n - k)" k] by (simp add: mult_dvd_mono)
  qed
  thus "p ^ Suc n dvd fps_parteval (f * g) p n" by (simp add: fps_parteval_mult_conv_sum(1))
qed

lemma fps_pvanishes_mult_fps_X_iff:
  assumes "(p::'a::idom) ≠ 0"
  shows "fps_pvanishes p f ⟷ fps_pvanishes p (f * fps_X)"
  and   "fps_pvanishes p f ⟷ fps_pvanishes p (fps_X * f)"
proof-
  show "fps_pvanishes p f ⟷ fps_pvanishes p (f * fps_X)"
  proof
    assume b: "fps_pvanishes p (f * fps_X)"
    show "fps_pvanishes p f"
    proof (intro fps_pvanishesI)
      fix n from b assms show "p ^ Suc n dvd fps_parteval f p n"
        using fps_pvanishesD[of p "f * fps_X" "Suc n"] fps_parteval_mult_fps_X(1)[of f n p]
        by    simp
    qed
  qed (auto intro: fps_pvanishes_mult simp add: mult.commute)
  thus "fps_pvanishes p f ⟷ fps_pvanishes p (fps_X * f)"
    by (simp add: fps_mult_fps_X_commute)
qed

lemma fps_pvanishes_mult_fps_X_power_iff:
  assumes "(p::'a::idom) ≠ 0"
  shows   "fps_pvanishes p f ⟷ fps_pvanishes p (f * fps_X ^ n)"
  and     "fps_pvanishes p f ⟷ fps_pvanishes p (fps_X ^ n * f)"
proof-
  show "fps_pvanishes p f ⟷ fps_pvanishes p (fps_X ^ n * f)"
  proof (induct n)
    case (Suc n) with assms show ?case
      using fps_pvanishes_mult_fps_X_iff(2)[of p "fps_X ^ n * f"]
      by    (simp add: mult.assoc)
  qed simp
  thus "fps_pvanishes p f ⟷ fps_pvanishes p (f * fps_X ^ n)"
    by (simp flip: fps_mult_fps_X_power_commute)
qed


subsection ‹Equivalence and depth of formal Laurent series relative to a prime›

subsubsection ‹Definition of equivalence and basic facts›

abbreviation "fps_primevanishes p ≡ fps_pvanishes (Rep_prime p)"

overloading
  p_equal_fls ≡
    "p_equal :: 'a::nontrivial_factorial_comm_ring prime ⇒
      'a fls ⇒ 'a fls ⇒ bool"
begin

definition p_equal_fls ::
  "'a::nontrivial_factorial_comm_ring prime ⇒
    'a fls ⇒ 'a fls ⇒ bool"
  where
    "p_equal_fls p f g ≡ fps_primevanishes p (fls_base_factor_to_fps (f - g))"

end  (* overloading *)

context
  fixes p :: "'a :: nontrivial_factorial_comm_ring prime"
begin

lemma p_equal_flsD:
  "f ≃⇩p g ⟹ fps_primevanishes p (fls_base_factor_to_fps (f - g))"
  for f g :: "'a fls"
  unfolding p_equal_fls_def by simp

lemma p_equal_fls_imp_p_dvd: "p pdvd ((f - g) $$ (fls_subdegree (f - g)))"
  if "f ≃⇩p g"
  for f g :: "'a fls"
proof-
  have "int (0::nat) = 0" by simp
  thus ?thesis
    by (metis
          that p_equal_flsD fps_pvanishesD power_Suc0_right fps_parteval_0th
          fls_base_factor_to_fps_nth add_0_right
    )
qed

lemma p_equal_flsI:
  "fps_primevanishes p (fls_base_factor_to_fps (f - g)) ⟹ f ≃⇩p g"
  for f g :: "'a fls"
  unfolding p_equal_fls_def by simp

lemma p_equal_fls_conv_p_equal_0:
  "f ≃⇩p g ⟷ (f - g) ≃⇩p 0"
  for f g :: "'a fls"
  unfolding p_equal_fls_def by auto

lemma p_equal_fls_refl: "f ≃⇩p f" for f:: "'a fls"
  by (auto intro: p_equal_flsI)

lemma p_equal_fls_sym:
  "f ≃⇩p g ⟹ g ≃⇩p f" for f g :: "'a fls"
  using     p_equal_flsD fps_pvanishes_uminus fls_uminus_subdegree[of "f-g"]
  unfolding p_equal_fls_def
  by        fastforce

lemma p_equal_fls_shift_iff:
  "f ≃⇩p g ⟷ (fls_shift n f) ≃⇩p (fls_shift n g)"
  for f g :: "'a fls"
  using fls_base_factor_shift[of n "f - g"] unfolding p_equal_fls_def by auto

lemma p_equal_fls_extended_sum_iff:
  "f ≃⇩p g ⟷
    (∀n. (Rep_prime p) ^ Suc n dvd
      (∑k≤n. (f - g)$$(N + int k) * (Rep_prime p)^k))"
  if "N ≤ min (fls_subdegree f) (fls_subdegree g)"
proof-
  define pp where "pp ≡ Rep_prime p"
  define dfg where "dfg ≡ fls_subdegree (f - g)"
  define D where "D ≡ nat (dfg - N - 1)"
  from that dfg_def D_def
    have  D: "f ≠ g ⟹ N ≠ dfg ⟹ dfg - N - 1 ≥ 0"
    using fls_subdegree_minus
    by    force
  have
    "(f ≃⇩p g) =
      (∀n. pp ^ Suc n dvd (∑k≤n. (f - g) $$ (N + int k) * pp ^ k))"
  proof (standard, standard)
    fix n :: nat
    assume fg: "f ≃⇩p g"
    consider
               "f = g"                    |
               "N = dfg"                  |
      (n_le_D) "f ≠ g" "N ≠ dfg" "n ≤ D" |
      (n_gt_D) "f ≠ g" "N ≠ dfg" "n > D"
      by fastforce
    thus "pp ^ Suc n dvd (∑k≤n. (f - g) $$ (N + int k) * pp ^ k)"
    proof cases
      case n_le_D
      with D_def have "∀k≤n. N + int k < dfg" using D by linarith
      with dfg_def show ?thesis using fls_eq0_below_subdegree[of _ "f - g"] by simp
    next
      case n_gt_D
      with D_def that
        have  N_k  : "∀k≤D. N + int k < dfg"
        and   N_D_k: "∀k. N + int (Suc D + k) = dfg + int k"
        using D
        by    (force, linarith)
      from dfg_def have "∀k≤D. (f - g)$$(N + int k) = 0"
        using N_k fls_eq0_below_subdegree[of _ "f - g"] by blast
      hence partsum: "(∑k≤D. (f - g)$$(N + int k) * pp^k) = 0" by force
      from pp_def ‹f ≃⇩p g› obtain k
        where k: "fls_base_parteval (f - g) pp (n - Suc D) = pp ^ Suc (n - Suc D) * k"
        using p_equal_flsD fps_pvanishesD by blast
      from ‹n > D› have exp: "Suc D + Suc (n - Suc D) = Suc n" by auto
      from ‹n > D› have
        "(∑k≤n. (f - g)$$(N + int k) * pp^k) =
          (∑k≤D. (f - g)$$(N + int k) * pp^k) +
          (∑k=Suc D..n. (f - g)$$(N + int k) * pp^k)"
        using sum_up_index_split[of _ D "n - D"] by auto
      also from ‹n > D› have
        "… = (∑k≤n - Suc D.
          (f - g) $$ (N + int (Suc D + k)) * pp ^ (Suc D + k))"
        using partsum atLeast0AtMost[of "n - Suc D"]
              sum.atLeastAtMost_shift_bounds[
                of "λk. (f-g)$$(N + int k) * pp^k" 0 "Suc D" "n - Suc D"
              ]
        by    auto
      also from D_def have
        "… = (∑k≤n - Suc D. (f - g) $$ (dfg + int k) * (pp ^ Suc D * pp ^ k))"
        using N_D_k power_add[of pp "Suc D"] by force
      also have
        "… = pp ^ Suc D * (∑k≤n - Suc D. (f - g) $$ (dfg + int k) * pp ^ k)"
        by (simp add: algebra_simps sum_distrib_left)
      also have "… = pp ^ Suc D * (pp ^ Suc (n - Suc D) * k)"
        using k dfg_def fls_base_parteval_conv_sum[of "f - g" "n - Suc D" pp] by presburger
      also have "… = pp ^ (Suc D + Suc (n - Suc D)) * k"
        by (simp add: algebra_simps power_add)
      finally have "(∑k≤n. (f - g)$$(N + int k) * pp^k) = pp ^ Suc n * k"
        using ‹n > D› by auto
      thus ?thesis by auto
    qed (simp, metis fg dfg_def pp_def fls_base_parteval_conv_sum p_equal_flsD fps_pvanishesD)
  next
    assume *: "∀n. pp ^ Suc n dvd (∑k≤n. (f - g)$$(N + int k) * pp^k)"
    consider "f = g" | "N = dfg" |  "f ≠ g" "N ≠ dfg" by blast
    thus "f ≃⇩p g"
    proof cases
      case 1 thus ?thesis by (simp add: p_equal_fls_refl)
    next
      case 2 with pp_def dfg_def * show ?thesis
        using p_equal_flsI fps_pvanishesI fls_base_parteval_conv_sum by metis
    next
      case 3 show ?thesis
      proof (intro p_equal_flsI fps_pvanishesI)
        fix n
        from 3 dfg_def D_def
          have  ND     : "∀k. N + int (Suc D + k) = dfg + int k"
          and   dfg_N_n: "nat (dfg - N) + n = Suc D + n"
          and   sum_0  : "(∑k≤D. (f - g) $$ (N + int k) * pp ^ k) = 0"
          using D fls_eq0_below_subdegree[of _ "f - g"]
          by    (fastforce, simp, simp)
        have
          "(∑k≤nat (dfg - N) + n. (f - g)$$(N + int k) * pp^k) =
            (∑k = Suc D..Suc D + n. (f - g) $$ (N + int k) * pp ^ k)"
          using dfg_N_n sum_0
                sum_up_index_split[of "λk. (f - g)$$(N + int k) * pp^k" D "Suc n"]
          by    auto
        also have
          "… = sum ((λk. (f - g) $$ (N + int k) * pp ^ k) ∘ (+) (Suc D))
            {0..n}"
          using add.commute[of "Suc D" n] add_0_left[of "Suc D"]
                sum.atLeastAtMost_shift_bounds[
                  of "λk. (f-g)$$(N + int k) * pp^k" 0 "Suc D" n
                ]
          by    argo
        also have "… = pp ^ Suc D * (∑k≤n. (f - g) $$ (dfg + int k) * pp ^ k)"
          using ND by (force simp add: algebra_simps atLeast0AtMost power_add sum_distrib_left)
        finally have
          "(∑k≤nat (dfg - N) + n. (f - g)$$(N + int k) * pp^k) =
            pp ^ Suc D * fls_base_parteval (f - g) pp n"
          using dfg_def fls_base_parteval_conv_sum[of "f - g" n pp] by force
        moreover have "Suc (nat (dfg - N) + n) = Suc D + Suc n" using dfg_N_n by presburger
        moreover from pp_def have "pp ^ Suc D ≠ 0" using Rep_prime_n0 by auto
        ultimately have "pp ^ Suc n dvd fls_base_parteval (f - g) pp n"
          using * power_add dvd_times_left_cancel_iff by metis
        with pp_def show "Rep_prime p ^ Suc n dvd fls_base_parteval (f - g) (Rep_prime p) n"
          by blast
      qed
    qed
  qed
  with pp_def show ?thesis by fast
qed

lemma p_equal_fls_extended_intsum_iff:
  "f ≃⇩p g ⟷
    (∀n≥N. (Rep_prime p) ^ Suc (nat (n - N)) dvd
      (∑k=N..n. (f - g)$$k * (Rep_prime p) ^ nat (k - N)))"
  if "N ≤ min (fls_subdegree f) (fls_subdegree g)"
proof (standard, clarify)
  assume fg: "f ≃⇩p g"
  fix n::int assume n: "n ≥ N"
  define m where "m ≡ nat (n - N)"
  from that fg have
    "(Rep_prime p) ^ Suc m dvd (∑k≤m. (f - g)$$(N + int k) * (Rep_prime p)^k)"
    using p_equal_fls_extended_sum_iff by blast
  moreover from n m_def have
    "(∑k=N..n. (f - g)$$k * (Rep_prime p) ^ nat( k - N)) =
      (∑k≤m. (f - g)$$(N + int k) * (Rep_prime p)^k)"
    by (simp add: sum.atLeastAtMost_int_shift_bounds algebra_simps)
  ultimately show
    "(Rep_prime p) ^ Suc (nat (n - N)) dvd
      (∑k=N..n. (f - g)$$k * (Rep_prime p) ^ nat (k - N))"
    using m_def by argo
next
  assume dvd_sum:
    "∀n≥N. (Rep_prime p) ^ Suc (nat (n - N)) dvd
      (∑k=N..n. (f - g)$$k * (Rep_prime p) ^ nat (k - N))"
  show "f ≃⇩p g"
  proof (rule iffD2, rule p_equal_fls_extended_sum_iff, rule that, safe)
    fix n::nat
    have N_n: "N + int n ≥ N" by fastforce
    moreover have "nat (N + int n - N) = n" by simp
    ultimately have
      "(Rep_prime p) ^ Suc n dvd
        (∑k=N..N + int n. (f - g)$$k * (Rep_prime p) ^ nat (k - N))"
      using dvd_sum by fastforce
    moreover from N_n have
      "(∑k≤n. (f - g) $$ (N + int k) * Rep_prime p ^ k) =
        (∑k=N..N + int n. (f - g)$$k * (Rep_prime p) ^ nat (k - N))"
      by (simp add: sum.atLeastAtMost_int_shift_bounds)
    ultimately show
      "Rep_prime p ^ Suc n dvd (∑k≤n. (f - g) $$ (N + int k) * Rep_prime p ^ k)"
      by presburger
  qed
qed

lemma fls_p_equal0_extended_sum_iff:
  "f ≃⇩p 0 ⟷
    (∀n. (Rep_prime p) ^ Suc n dvd
      (∑k≤n. f$$(N + int k) * (Rep_prime p)^k))"
  if "N ≤ fls_subdegree f"
proof-
  define pp where "pp ≡ Rep_prime p"
  have d0_case:
    "⋀f N. fls_subdegree f = 0 ⟹ N ≤ 0 ⟹
      f ≃⇩p 0 ⟷
        (∀n. pp ^ Suc n dvd (∑k≤n. f$$(N + int k) * pp^k))"
  proof-
    fix f N from pp_def
      show  "fls_subdegree f = 0 ⟹ N ≤ 0 ⟹ ?thesis f N"
      using p_equal_fls_extended_sum_iff[of N f 0]
      by    simp
  qed
  have "f ≃⇩p 0 ⟷ (fls_base_factor f) ≃⇩p 0"
    using p_equal_fls_shift_iff[of f 0] fls_base_factor_def by auto
  also from that pp_def have
    "… = (∀n. pp ^ Suc n dvd (∑k≤n. f $$ ((N + int k)) * pp^k))"
    using fls_base_factor_subdegree[of f] d0_case[of "fls_base_factor f" "N - fls_subdegree f"]
    by    auto
  finally show ?thesis using pp_def by blast
qed

lemma fls_p_equal0_extended_intsum_iff:
  "f ≃⇩p 0 ⟷
    (∀n≥N. (Rep_prime p) ^ Suc (nat (n - N)) dvd
      (∑k=N..n. f$$k * (Rep_prime p) ^ nat (k - N)))"
  if "N ≤ fls_subdegree f"
proof (standard, clarify)
  assume f: "f ≃⇩p 0"
  fix n::int assume n: "n ≥ N"
  define m where "m ≡ nat (n - N)"
  from that f have
    "(Rep_prime p) ^ Suc m dvd (∑k≤m. f$$(N + int k) * (Rep_prime p)^k)"
    using fls_p_equal0_extended_sum_iff by blast
  moreover from n m_def have
    "(∑k=N..n. f$$k * (Rep_prime p) ^ nat (k - N)) =
      (∑k≤m. f$$(N + int k) * (Rep_prime p)^k)"
    by (simp add: sum.atLeastAtMost_int_shift_bounds algebra_simps)
  ultimately show
    "(Rep_prime p) ^ Suc (nat (n - N)) dvd
      (∑k=N..n. f$$k * (Rep_prime p) ^ nat (k - N))"
    using m_def by argo
next
  assume dvd_sum:
    "∀n≥N. (Rep_prime p) ^ Suc (nat (n - N)) dvd
      (∑k=N..n. f$$k * (Rep_prime p) ^ nat (k - N))"
  show "f ≃⇩p 0"
  proof (rule iffD2, rule fls_p_equal0_extended_sum_iff, rule that, safe)
    fix n::nat
    have N_n: "N + int n ≥ N" by fastforce
    moreover have "nat (N + int n - N) = n" by simp
    ultimately have
      "(Rep_prime p) ^ Suc n dvd
        (∑k=N..N + int n. f$$k * (Rep_prime p) ^ nat (k - N))"
      using dvd_sum by fastforce
    moreover from N_n have
      "(∑k≤n. f $$ (N + int k) * Rep_prime p ^ k) =
        (∑k=N..N + int n. f$$k * (Rep_prime p) ^ nat (k - N))"
      by (simp add: sum.atLeastAtMost_int_shift_bounds)
    ultimately show
      "Rep_prime p ^ Suc n dvd (∑k≤n. f $$ (N + int k) * Rep_prime p ^ k)"
      by presburger
  qed
qed

end (* context nontrivial_factorial_comm_ring *)

context
  fixes p :: "'a :: nontrivial_factorial_idom prime"
begin

lemma fls_1_not_p_equal_0: "(1::'a fls) ¬≃⇩p 0"
  using fps_pvanishes_one_iff not_prime_unit Rep_prime[of p] unfolding p_equal_fls_def by auto

lemma p_equal_fls0_nonneg_subdegree:
  "f ≃⇩p 0 ⟷ fps_primevanishes p (fls_regpart f)"
  if "fls_subdegree f ≥ 0"
proof-
  define n where "n ≡ nat (fls_subdegree f)"
  moreover have
    "f ≃⇩p 0 ⟷
      fps_primevanishes p (fls_base_factor_to_fps f * fps_X ^ n)"
    unfolding p_equal_fls_def
    using     Rep_prime[of p] fps_pvanishes_mult_fps_X_power_iff(1)[of "Rep_prime p"]
    by        simp
  ultimately show ?thesis
    using fls_base_factor_subdegree[of f] fls_regpart_times_fps_X_power(1)[of "fls_base_factor f" n]
    by    (auto simp add: that)
qed

lemma p_equal_fls_nonneg_subdegree:
  "f ≃⇩p g ⟷ fps_primevanishes p (fls_regpart (f - g))"
  if "fls_subdegree f ≥ 0" and "fls_subdegree g ≥ 0"
proof-
  from that have "fls_subdegree (f - g) ≥ 0"
    using fls_subdegree_minus[of f g] by (cases "f = g") auto
  thus ?thesis using p_equal_fls_conv_p_equal_0[of p f g] p_equal_fls0_nonneg_subdegree by blast
qed

lemma p_equal_fls_trans_to_0:
  "f ≃⇩p g" if "f ≃⇩p 0" and "g ≃⇩p 0" for f g :: "'a fls"
proof (rule iffD2, rule p_equal_fls_shift_iff, rule iffD2, rule p_equal_fls_nonneg_subdegree)
  define n where "n ≡ min (fls_subdegree f) (fls_subdegree g)"
  from n_def show "fls_subdegree (fls_shift n f) ≥ 0" "fls_subdegree (fls_shift n g) ≥ 0"
    using fls_shift_nonneg_subdegree[of n f] fls_shift_nonneg_subdegree[of n g] by auto
  with that show "fps_primevanishes p (fls_regpart (fls_shift n f - fls_shift n g))"
    using p_equal_fls0_nonneg_subdegree[of "fls_shift n f"] p_equal_fls_shift_iff[of p f 0]
          p_equal_fls0_nonneg_subdegree[of "fls_shift n g"] p_equal_fls_shift_iff[of p g 0]
    by (auto intro: fps_pvanishes_minus)
qed

lemma p_equal_fls_trans:
  "f ≃⇩p g ⟹ g ≃⇩p h ⟹
    f ≃⇩p h"
  for f g h :: "'a fls"
  using p_equal_fls_conv_p_equal_0[of p f g] p_equal_fls_conv_p_equal_0[of p h g]
        p_equal_fls_sym[of p g h] p_equal_fls_trans_to_0[of "f-g" "h-g"]
        p_equal_fls_conv_p_equal_0[of p "f-g" "h-g"] p_equal_fls_conv_p_equal_0[of p f h]
  by    auto

end (* context nontrivial_factorial_idom *)

global_interpretation p_equality_fls:
  p_equality_1
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a fls ⇒ 'a fls ⇒ bool"
proof (unfold_locales, intro equivpI)
  fix p :: "'a prime"
  define E :: "'a fls ⇒ 'a fls ⇒ bool" where "E ≡ p_equal p"
  show "reflp E"
    by (auto intro: reflpI simp add: E_def p_equal_fls_refl)
  show "symp E" using p_equal_fls_sym by (auto intro: sympI simp add: E_def)
  show "transp E"
   using E_def p_equal_fls_trans[of p] by (fastforce intro: transpI)

  fix x y :: "'a fls"
  show "y ≃⇩p 0 ⟹ x * y ≃⇩p 0"
    using     p_equal_flsD fps_pvanishes_mult fls_base_factor_to_fps_mult[of x y]
    unfolding p_equal_fls_def
    by        fastforce

qed (rule p_equal_fls_conv_p_equal_0)

overloading
  globally_p_equal_fls ≡
    "globally_p_equal ::
      'a::nontrivial_factorial_idom fls ⇒ 'a fls ⇒ bool"
begin

definition globally_p_equal_fls ::
  "'a::nontrivial_factorial_idom fls ⇒ 'a fls ⇒ bool"
  where globally_p_equal_fls[simp]:
    "globally_p_equal_fls = p_equality_fls.globally_p_equal"

end  (* overloading *)

context
  fixes p :: "'a :: nontrivial_factorial_idom prime"
begin

lemma p_equal_fls_const_iff:
  "(fls_const c) ≃⇩p (fls_const d) ⟷ c = d" for c d :: 'a
proof
  define pp where "pp ≡ Rep_prime p"
  assume "(fls_const c) ≃⇩p (fls_const d)"
  with pp_def have 1: "∀n::nat. pp ^ Suc n dvd (c - d)"
    using p_equal_flsD unfolding fps_pvanishes_def by (fastforce simp add: fls_minus_const)
  have "infinite {n. pp ^ n dvd (c - d)}"
  proof
    assume "finite {n. pp ^ n dvd (c - d)}"
    moreover have "Suc (Max {n. pp ^ n dvd (c - d)}) ∈ {n. pp ^ n dvd (c - d)}" using 1 by simp
    ultimately have "Suc (Max {n. pp ^ n dvd (c - d)}) ≤ Max {n. pp ^ n dvd (c - d)}" by simp
    thus False by simp
  qed
  with pp_def show "c = d" using Rep_prime_not_unit finite_divisor_powers[of "c - d"] by fastforce
qed simp

lemma p_equal_fls_const_0_iff:
  "(fls_const c) ≃⇩p 0 ⟷ c = 0" for c :: 'a
  using p_equal_fls_const_iff[of c 0] by simp

lemma p_equal_fls_X_intpow_iff:
  "((fls_X_intpow m :: 'a fls) ≃⇩p (fls_X_intpow n)) = (m = n)"
proof (induction m n rule: linorder_less_wlog, standard)
  define pp and X :: "int ⇒ 'a fls"
    where "pp ≡ Rep_prime p" and "X ≡ fls_X_intpow"
  fix m n :: int assume eq: "(X m) ≃⇩p (X n)" and mn: "m < n"
  with pp_def X_def have
    "pp ^ Suc (nat (n - m)) dvd (∑k=m..n. (X m - X n)$$k * pp ^ nat (k - m))"
    using p_equal_fls_extended_intsum_iff[of m "X m" "X n" p]
    by    auto
  moreover have
    "(∑k=m..n. (X m - X n)$$k * pp ^ nat (k - m)) =
      (∑k∈{m,n}. (X m - X n)$$k * pp ^ nat (k - m))"
  proof (rule sum.mono_neutral_right, safe)
    from mn show "m ∈ {m..n}" and "n ∈ {m..n}" by auto
    fix i
    assume  i : "i ∈ {m..n}" "i ≠ m"
      and   Xi: "(X m - X n) $$ i * pp ^ nat (i - m) ≠ 0"
    with X_def have "X m $$ i = 0" by simp
    moreover from X_def have "i < n ⟹ X n $$ i = 0" by force
    ultimately show "i = n" using i(1) Xi by fastforce
  qed
  ultimately have "pp ^ Suc (nat (n - m)) dvd 1 - (pp ^ nat (n - m))"
    using mn X_def by auto
  from this obtain k where "1 - (pp ^ nat (n - m)) = pp ^ Suc (nat (n - m)) * k" by fast
  hence "1 = pp ^ nat (n - m) * (1 + pp * k)" by (simp add: algebra_simps)
  with pp_def mn show "m = n"
    using dvdI[of 1] Rep_prime_not_unit is_unit_power_iff[of pp] by fastforce
qed (auto simp add: p_equal_fls_sym)

lemma fls_X_intpow_nequiv0: "(fls_X_intpow m :: 'a fls) ¬≃⇩p 0"
  using p_equal_fls_shift_iff fls_1_not_p_equal_0 by fastforce

end

subsubsection ‹Depth as maximum subdegree of equivalent series›

text ‹Each nonzero equivalence class will have a maximum subdegree.›

lemma no_greatest_p_equal_subdegree:
  "f ≃⇩p 0"
  if "∀n :: int. (∃g. fls_subdegree g > n ∧ f ≃⇩p g)"
  for p :: "'a::nontrivial_factorial_comm_ring prime" and f :: "'a fls"
proof (cases "f = 0")
  case False show ?thesis
  proof (intro p_equal_flsI fps_pvanishesI)
    fix n :: nat
    define pp where "pp ≡ Rep_prime p"
    from that obtain g where g: "fls_subdegree g > fls_subdegree f + int n" "f ≃⇩p g"
      by blast
    with False pp_def have "fls_base_parteval (f - g) pp n = fls_base_parteval (f - 0) pp n"
      using fps_parteval_fls_base_factor_to_fps_diff by auto
    with False pp_def g(2) show "pp ^ Suc n dvd fls_base_parteval (f - 0) pp n"
      using p_equal_flsD fps_pvanishesD by metis
  qed
qed (simp add: p_equal_fls_refl)

abbreviation
  "p_equal_fls_simplified_set p f ≡
    {g. f ≃⇩p g ∧ fls_subdegree g ≥ fls_subdegree f}"
―‹
We restrict to those equivalent series that represent a simplification of the given series so that
the image of the collection under taking subdegrees is finite.
›

context
  fixes p :: "'a::nontrivial_factorial_comm_ring prime"
  and   f :: "'a fls"
begin

lemma p_equal_fls_simplifed_nempty:
  "fls_subdegree ` (p_equal_fls_simplified_set p f) ≠ {}"
  using p_equal_fls_refl[of p f] by fast

lemma p_equal_fls_simplifed_finite:
  "finite (fls_subdegree ` (p_equal_fls_simplified_set p f))" if "f ¬≃⇩p 0"
proof-
  from that obtain n::int
    where "∀g. f ≃⇩p g ⟶ ¬ fls_subdegree g > n"
    using no_greatest_p_equal_subdegree[of p f]
    by    auto
  hence n: "∀g. f ≃⇩p g ⟶ fls_subdegree g ≤ n" by auto
  define deg_diff where "deg_diff ≡ (λn. n - fls_subdegree f)"
  define D where "D ≡ fls_subdegree ` (p_equal_fls_simplified_set p f)"
  show "finite D"
  proof (rule finite_imageD)
    show "finite (deg_diff ` D)"
    proof (rule finite_imageD)
      have "nat ` deg_diff ` D ⊆ {m::nat. m ≤ nat (deg_diff n)}"
        using n D_def deg_diff_def by auto
      thus "finite (nat ` deg_diff ` D)" using finite_subset by blast
      from D_def deg_diff_def show "inj_on nat (deg_diff ` D)"
        by (auto intro: inj_onI)
    qed
    from deg_diff_def show "inj_on deg_diff D" by (auto intro: inj_onI)
  qed
qed

end  (* context nontrivial_factorial_comm_ring fls *)

overloading
  p_depth_fls ≡
    "p_depth :: 'a::nontrivial_factorial_comm_ring prime ⇒ 'a fls ⇒ int"
  p_depth_const ≡
    "p_depth :: 'a::nontrivial_factorial_comm_ring prime ⇒ 'a ⇒ int"
begin

definition
  p_depth_fls :: "'a::nontrivial_factorial_comm_ring prime ⇒ 'a fls ⇒ int"
  where
  "p_depth_fls p f ≡
    (if f ≃⇩p 0 then 0 else Max (fls_subdegree ` (p_equal_fls_simplified_set p f)))"

definition
  p_depth_const :: "'a::nontrivial_factorial_comm_ring prime ⇒ 'a ⇒ int"
  where
  "p_depth_const p c ≡ p_depth p (fls_const c)"

end  (* overloading *)

context
  fixes p :: "'a::nontrivial_factorial_comm_ring prime"
begin

lemma p_depth_fls_eqI:
  "f°⇧p = fls_subdegree g"
  if  "f ¬≃⇩p 0" and "f ≃⇩p g"
  and "⋀h. f ≃⇩p h ⟹ fls_subdegree h ≤ fls_subdegree g"
  for f g :: "'a fls"
proof-
  define M where "M ≡ Max (fls_subdegree ` (p_equal_fls_simplified_set p f))"
  with that have "M = fls_subdegree g"
    using p_equal_fls_simplifed_finite
    by    (force intro: Max_eqI simp add: p_equal_fls_refl)
  with that(1) M_def show ?thesis by (auto simp add: p_depth_fls_def)
qed

lemma p_depth_fls_p_equal0[simp]:
  "(f°⇧p) = 0" if "f ≃⇩p 0" for f :: "'a fls"
  using that by (simp add: p_depth_fls_def)

lemma p_depth_fls0[simp]: "(0::'a fls)°⇧p = 0"
  by (simp add: p_depth_fls_def p_equal_fls_refl)

lemma p_depth_fls_n0D:
  "f°⇧p = Max (fls_subdegree ` (p_equal_fls_simplified_set p f))"
  if  "f ¬≃⇩p 0"
  for f :: "'a fls"
  using that by (simp add: p_depth_fls_def)

lemma p_depth_flsE:
  fixes   f :: "'a fls"
  assumes "f ¬≃⇩p 0"
  obtains g where "f ≃⇩p g" and "fls_subdegree g = (f°⇧p)"
  and "∀h. f ≃⇩p h ⟶ fls_subdegree h ≤ fls_subdegree g"
proof-
  define M where "M ≡ Max (fls_subdegree ` (p_equal_fls_simplified_set p f))"
  with assms have "M ∈ fls_subdegree ` (p_equal_fls_simplified_set p f)"
    using p_equal_fls_simplifed_finite[of p f] p_equal_fls_simplifed_nempty[of p f] by simp
  from this obtain g where g: "g ∈ p_equal_fls_simplified_set p f" "M = fls_subdegree g" by fast
  from g(1) have "f ≃⇩p g" by blast
  moreover from g(2) M_def assms have 2: "fls_subdegree g = (f°⇧p)"
    by (fastforce simp add: p_depth_fls_def)
  moreover have
    "∀h. f ≃⇩p h ⟶ fls_subdegree h ≤ fls_subdegree g"
  proof clarify
    fix h assume "f ≃⇩p h" show "fls_subdegree h ≤ fls_subdegree g"
    proof (cases "fls_subdegree h ≥ fls_subdegree f")
      case True with assms ‹f ≃⇩p h› M_def g show ?thesis
        using p_equal_fls_simplifed_finite by force
    next
      case False
      moreover from assms M_def g have "fls_subdegree f ≤ fls_subdegree g"
        using p_equal_fls_simplifed_finite by blast
      ultimately show ?thesis by simp
    qed
  qed
  ultimately show thesis using that by simp
qed

lemma p_depth_fls_ge_p_equal_subdegree:
  "(f°⇧p) ≥ fls_subdegree g"
  if  "f ¬≃⇩p 0" and "f ≃⇩p g"
  for f g :: "'a fls"
proof (cases "fls_subdegree g ≥ fls_subdegree f")
  case True with that show ?thesis
    using p_equal_fls_simplifed_finite by (fastforce simp add: p_depth_fls_def)
next
  case False
  moreover from that(1) have "fls_subdegree f ≤ (f°⇧p)"
    using p_equal_fls_simplifed_finite by (fastforce simp add: p_equal_fls_refl p_depth_fls_def)
  ultimately show ?thesis by simp
qed

lemma p_depth_fls_ge_p_equal_subdegree':
  "(f°⇧p) ≥ fls_subdegree f" if  "f ¬≃⇩p 0" for f g :: "'a fls"
  using that p_depth_fls_ge_p_equal_subdegree p_equal_fls_refl by blast

lemma p_equal_fls_simplified_set_shift:
  "p_equal_fls_simplified_set p (fls_shift n f) = fls_shift n ` p_equal_fls_simplified_set p f"
  if  "f ¬≃⇩p 0"
  for f :: "'a fls"
proof-
  have *:
    "⋀f n. (f::'a fls) ¬≃⇩p 0 ⟹
      fls_shift n ` p_equal_fls_simplified_set p f ⊆
        p_equal_fls_simplified_set p (fls_shift n f)"
  proof (intro subsetI, clarify)
    fix n ::int
    and f g :: "'a fls"
    assume f_neq_0: "f ¬≃⇩p 0"
      and  eq     : "f ≃⇩p g"
      and  deg    : "fls_subdegree f ≤ fls_subdegree g"
    from f_neq_0 eq have "f ≠ 0" "g ≠ 0" using p_equal_fls_refl by auto
    with deg have  "fls_subdegree (fls_shift n f) ≤ fls_subdegree (fls_shift n g)" by simp
    moreover from eq have "(fls_shift n f) ≃⇩p (fls_shift n g)"
      using p_equal_fls_shift_iff by fast
    ultimately show
      "(fls_shift n f) ≃⇩p (fls_shift n g) ∧
        fls_subdegree (fls_shift n f) ≤ fls_subdegree (fls_shift n g)"
      by fast
  qed
  have "f ≃⇩p 0 ⟷ (fls_shift n f) ≃⇩p 0"
    using p_equal_fls_shift_iff[of p f 0] by simp
  with that have
    "p_equal_fls_simplified_set p (fls_shift n f) ⊆
        fls_shift n ` p_equal_fls_simplified_set p f"
    using *[of "fls_shift n f" "-n"] by force
  with that show
    "p_equal_fls_simplified_set p (fls_shift n f) = fls_shift n ` p_equal_fls_simplified_set p f"
    using *[of f n] by fast
qed

lemma p_equal_fls_simplified_set_shift_subdegrees:
  "fls_subdegree ` p_equal_fls_simplified_set p (fls_shift n f) =
    (λx. x - n) ` fls_subdegree ` p_equal_fls_simplified_set p f"
  if  "f ¬≃⇩p 0"
  for f :: "'a fls"
proof-
  from that have
    "fls_subdegree ` p_equal_fls_simplified_set p (fls_shift n f) =
      fls_subdegree ` fls_shift n ` p_equal_fls_simplified_set p f"
    using p_equal_fls_simplified_set_shift by fast
  moreover from that have "∀g∈p_equal_fls_simplified_set p f. g ≠ 0" by auto
  ultimately show ?thesis by force
qed

lemma p_depth_fls_shift:
  "(fls_shift n f)°⇧p = (f°⇧p) - n" if "f ¬≃⇩p 0"
  for f :: "'a fls"
proof-
  from that have sf_nequiv_0: "(fls_shift n f) ¬≃⇩p 0"
    using p_equal_fls_shift_iff by fastforce
  with that have
    "(fls_shift n f)°⇧p =
      Max ((λx. x - n) ` fls_subdegree ` p_equal_fls_simplified_set p f)"
    using p_depth_fls_n0D p_equal_fls_simplified_set_shift_subdegrees
    by    fastforce
  thus ?thesis
    using p_equal_fls_simplifed_finite[OF that] p_equal_fls_simplifed_nempty
          p_depth_fls_n0D[OF that]
          Max_add_commute[of
            "fls_subdegree ` p_equal_fls_simplified_set p f"
            "λx. x"
            "-n"
          ]
    by    auto
qed

end (* context factorial_comm_ring_1 *)

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
  and   f g :: "'a fls"
begin

lemma p_depth_fls_p_equal: "(f°⇧p) = (g°⇧p)" if "f ≃⇩p g"
proof (cases "f ≃⇩p 0")
  case True with that show ?thesis using p_equality_fls.trans0_iff by fastforce
next
  case False
  with that have g: "g ¬≃⇩p 0" using p_equality_fls.trans0_iff by blast
  from this obtain h where h:
    "g ≃⇩p h" "fls_subdegree h = (g°⇧p)"
    by (elim p_depth_flsE)
  from that h(1) have "f ≃⇩p h" using p_equality_fls.trans by fast
  moreover from that g h(2) have
    "⋀h'. f ≃⇩p h' ⟹ fls_subdegree h' ≤ fls_subdegree h"
    using p_equality_fls.trans_right p_depth_fls_ge_p_equal_subdegree by metis
  ultimately show ?thesis
    using False h(2) p_depth_fls_eqI by metis
qed

lemma p_depth_fls_can_simplify_iff:
  "p pdvd g $$ (fls_subdegree g) = (fls_subdegree g < (f°⇧p))"
  if  f_nequiv0: "f ¬≃⇩p 0"
  and fg_equiv : "f ≃⇩p g"
proof
  define gdeg where "gdeg ≡ fls_subdegree g"
  define gth where "gth ≡ g $$ gdeg"
  define pp where "pp ≡ Rep_prime p"
  assume p_dvd: "p pdvd gth"
  from this obtain k where k: "gth = pp * k" unfolding pp_def gth_def gdeg_def by (elim dvdE)
  define h where
    "h ≡ g - fls_shift (-gdeg) (fls_const gth) + fls_shift (-(gdeg + 1)) (fls_const k)"
  from f_nequiv0 fg_equiv have "g ≠ 0" by blast
  with gth_def gdeg_def have
    "fls_subdegree (fls_shift (-gdeg) (fls_const gth) - fls_shift (-(gdeg + 1)) (fls_const k)) =
      gdeg"
    by (auto intro: fls_subdegree_eqI)
  with h_def have g_h: "fls_base_factor_to_fps (g - h) = fps_const gth - fps_const k * fps_X"
    by (auto intro: fps_ext)
  have p_g_h: "⋀n. pp ^ Suc n dvd fls_base_parteval (g - h) pp n"
  proof-
    fix n
    from k p_dvd show "pp ^ Suc n dvd fls_base_parteval (g - h) pp n"
      using g_h by (cases n) (auto simp add: fps_parteval_mult_fps_X(1))
  qed
  with pp_def have "g ≃⇩p h" by (fastforce intro: p_equal_flsI fps_pvanishesI)
  moreover have "gdeg < fls_subdegree h"
  proof (intro fls_subdegree_greaterI)
    show "h ≠ 0"
    proof
      assume"h = 0"
      with pp_def have "g ≃⇩p 0"
        using p_g_h by (fastforce intro: p_equal_flsI fps_pvanishesI)
      with f_nequiv0 fg_equiv show False using p_equality_fls.trans0_iff by blast
    qed
  qed (simp add: h_def gdeg_def gth_def)
  ultimately show "gdeg < (f°⇧p)"
    using gdeg_def that p_depth_fls_ge_p_equal_subdegree[of p f h]
          p_equal_fls_trans[of p f g h]
    by    force
next
  define pp where "pp ≡ Rep_prime p"
  assume g: "fls_subdegree g < (f°⇧p)"
  with that obtain h where h: "f ≃⇩p h" "fls_subdegree h = (f°⇧p)"
    by (elim p_depth_flsE)
  from f_nequiv0 fg_equiv have g_n0: "g ≠ 0" by blast
  with g h(2) have "fls_subdegree (g - h) = fls_subdegree g" by (auto intro: fls_subdegree_eqI)
  moreover from fg_equiv h(1) pp_def
    have  "pp ^ Suc 0 dvd (fps_parteval (fls_regpart (fls_base_factor (g - h))) pp 0)"
    using p_equality_fls.trans_right p_equal_flsD fps_pvanishesD
    by    blast
  ultimately show "p pdvd g $$ (fls_subdegree g)" by (simp add: pp_def g h(2))
qed

lemma p_depth_fls_rep_iff:
  "(f°⇧p) = fls_subdegree g ⟷
    ¬ p pdvd g $$ (fls_subdegree g)"
  if "f ¬≃⇩p 0" and "f ≃⇩p g"
  using that p_depth_fls_can_simplify_iff p_depth_fls_ge_p_equal_subdegree by fastforce

end (* context nontrivial_factorial_idom *)

global_interpretation p_depth_fls:
  p_equality_depth_no_zero_divisors_1
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a fls ⇒ 'a fls ⇒ bool"
    "p_depth :: 'a prime ⇒ 'a fls ⇒ int"
proof (unfold_locales, intro notI)
  fix p :: "'a prime" and f g :: "'a fls"
  define pp where "pp ≡ Rep_prime p"
  assume  f_nequiv0: "f ¬≃⇩p 0"
    and   g_nequiv0: "g ¬≃⇩p 0"
    and   fg_equiv0: "(f * g) ≃⇩p 0"
  from f_nequiv0 obtain s_f
    where s_f: "f ≃⇩p s_f" "fls_subdegree s_f = (f°⇧p)"
    using p_depth_flsE
    by    blast
  from g_nequiv0 obtain s_g
    where s_g: "g ≃⇩p s_g" "fls_subdegree s_g = (g°⇧p)"
    using p_depth_flsE
    by    blast
  from s_f(1) s_g(1) fg_equiv0 have "(s_f * s_g) ≃⇩p 0"
    using p_equality_fls.mult p_equality_fls.trans0_iff by blast
  hence "fps_primevanishes p (fls_base_factor_to_fps (s_f * s_g))" using p_equal_flsD by fastforce
  with pp_def have "pp ^ Suc 0 dvd fls_base_parteval (s_f * s_g) pp 0"
    using fps_pvanishesD by fast
  with pp_def have "p pdvd s_f $$ (fls_subdegree s_f) * s_g $$ (fls_subdegree s_g)"
    using fls_base_factor_to_fps_mult[of s_f s_g] by fastforce
  hence
    "p pdvd s_f $$ (fls_subdegree s_f) ∨ p pdvd s_g $$ (fls_subdegree s_g)"
    using Rep_prime prime_dvd_multD by auto
  with pp_def f_nequiv0 s_f g_nequiv0 s_g show False by (metis p_depth_fls_rep_iff)
next
  fix p :: "'a prime"
  show "∃x::'a fls. x ¬≃⇩p 0" using fls_1_not_p_equal_0 by auto
next
  fix p :: "'a :: nontrivial_factorial_idom prime" and f g :: "'a fls"
  assume fg_nequiv0: "(f * g) ¬≃⇩p 0"
  from fg_nequiv0
    have  f_nequiv0: "f ¬≃⇩p 0"
    and   g_nequiv0: "g ¬≃⇩p 0"
    by    (auto simp add: p_equality_fls.mult_0_left p_equality_fls.mult_0_right)
  from f_nequiv0 obtain s_f
    where s_f: "f ≃⇩p s_f" "fls_subdegree s_f = (f°⇧p)"
    using p_depth_flsE
    by    blast
  from g_nequiv0 obtain s_g
    where s_g: "g ≃⇩p s_g" "fls_subdegree s_g = (g°⇧p)"
    using p_depth_flsE
    by    blast
  from s_f(1) s_g(1) have equiv: "(f * g) ≃⇩p (s_f * s_g)"
    using p_equality_fls.mult by fast
  with fg_nequiv0 have "s_f ≠ 0" "s_g ≠ 0" by auto
  hence deg: "fls_subdegree (s_f * s_g) = fls_subdegree s_f + fls_subdegree s_g" by simp
  moreover have "(s_f * s_g)°⇧p = fls_subdegree (s_f * s_g)"
  proof (rule iffD2, rule p_depth_fls_rep_iff)
    from fg_nequiv0 show "(s_f * s_g) ¬≃⇩p 0"
      using equiv p_equality_fls.trans0_iff by fast
    from s_f f_nequiv0 have "¬ p pdvd s_f $$ (fls_subdegree s_f)"
      by (metis p_depth_fls_rep_iff)
    moreover from s_g g_nequiv0 have "¬ p pdvd s_g $$ (fls_subdegree s_g)"
      by (metis p_depth_fls_rep_iff)
    moreover have
      "(s_f * s_g) $$ (fls_subdegree (s_f * s_g)) =
        s_f $$ (fls_subdegree s_f) *
        s_g $$ (fls_subdegree s_g)"
      using deg by simp
    ultimately show "¬ p pdvd (s_f * s_g) $$ (fls_subdegree (s_f * s_g))"
      using Rep_prime prime_dvd_multD by auto
  qed simp
  ultimately show "(f * g)°⇧p = (f°⇧p) + (g°⇧p)"
    using s_f(2) s_g(2) equiv p_depth_fls_p_equal by metis
next
  fix p :: "'a prime" and f :: "'a fls"
  show "(-f°⇧p) = (f°⇧p)"
  proof (cases "f ≃⇩p 0")
    case True thus ?thesis using p_equality_fls.uminus[of p f 0] by simp
  next
    case False
    moreover from this obtain h
      where "f ≃⇩p h"
      and   "fls_subdegree h = (f°⇧p)"
      by    (elim p_depth_flsE)
    ultimately show "(- f)°⇧p = (f°⇧p)"
      using p_depth_fls_rep_iff p_equality_fls.uminus[of p f h] p_equality_fls.uminus[of p "-f" 0]
            p_depth_fls_rep_iff
      by    fastforce
  qed
next
  fix p :: "'a prime" and f g :: "'a fls"
  assume f: "f ¬≃⇩p 0" and d_f_g: "(f°⇧p) < (g°⇧p)"
  show  "((f + g)°⇧p) = (f°⇧p)"
  proof (cases "g ≃⇩p 0")
    case True thus ?thesis using p_equality_fls.add_0_right[of p g f] p_depth_fls_p_equal by auto
  next
    case False
    from f obtain s_f
      where s_f: "f ≃⇩p s_f" "fls_subdegree s_f = (f°⇧p)"
      using p_depth_flsE
      by    blast
    from False obtain s_g
      where s_g: "g ≃⇩p s_g" "fls_subdegree s_g = (g°⇧p)"
      using p_depth_flsE
      by    blast
    from f d_f_g s_f s_g(2) have deg: "fls_subdegree (s_f + s_g) = fls_subdegree s_f"
      using nth_fls_subdegree_zero_iff[of s_f] by (auto intro: fls_subdegree_eqI)
    from s_f s_g have "(f + g) ≃⇩p (s_f + s_g)"
      using p_equality_fls.add by blast
    moreover from s_f s_g(2) f d_f_g
      have  *: "¬ p pdvd (s_f + s_g) $$ (fls_subdegree (s_f + s_g))"
      using deg p_depth_fls_rep_iff
      by    fastforce
    moreover have "(f + g) ¬≃⇩p 0"
    proof
      define pp where "pp ≡ Rep_prime p"
      assume "(f + g) ≃⇩p 0"
      with s_f(1) s_g(1) have f_g: "(s_f + s_g) ≃⇩p 0"
        by (meson p_equality_fls.add p_equality_fls.trans_right)
      with pp_def have "pp ^ Suc 0 dvd fls_base_parteval (s_f + s_g) pp 0"
        using p_equal_flsD[of p _ 0] fps_pvanishesD[of pp _ 0] by fastforce
      with pp_def show False using * by simp
    qed
    ultimately have "(f + g)°⇧p = fls_subdegree (s_f + s_g)"
      using p_depth_fls_rep_iff by blast
    with s_f(2) show ?thesis using deg by auto
  qed
next
  fix p :: "'a prime" and f g :: "'a fls"
  assume  f    : "f ¬≃⇩p 0"
    and   fg   : "f + g ¬≃⇩p 0"
    and   d_f_g: "(f°⇧p) = (g°⇧p)"
  show "(f°⇧p) ≤ ((f + g)°⇧p)"
  proof (cases "g ≃⇩p 0")
    case True thus ?thesis
      using p_equality_fls.add_0_right[of p g f] p_depth_fls_p_equal[of p] by presburger
  next
    case False
    from f obtain s_f
      where s_f: "f ≃⇩p s_f" "fls_subdegree s_f = (f°⇧p)"
      using p_depth_flsE
      by    blast
    from False obtain s_g
      where s_g: "g ≃⇩p s_g" "fls_subdegree s_g = (g°⇧p)"
      using p_depth_flsE
      by    blast
    from s_f s_g have "(f + g) ≃⇩p (s_f + s_g)"
      using p_equality_fls.add by fast
    moreover from this fg d_f_g s_f(2) s_g(2)
      have  "fls_subdegree (s_f + s_g) ≥ fls_subdegree s_f"
      by    (force intro: fls_subdegree_geI)
    ultimately show ?thesis
      using fg s_f(2) p_depth_fls_ge_p_equal_subdegree by fastforce
  qed
qed (simp, rule p_depth_fls_p_equal)

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma p_depth_fls1[simp]: "(1::'a fls)°⇧p = 0"
  by (rule FLS_Prime_Equiv_Depth.p_depth_fls.depth_of_1)

lemma p_depth_fls_X: "(fls_X::'a fls)°⇧p = 1"
  using fls_1_not_p_equal_0 p_equal_fls_shift_iff[of p "fls_X::'a fls" 0 1]
        p_depth_fls_shift[of p _ 1]
  by    fastforce

lemma p_depth_fls_X_inv: "(fls_X_inv::'a fls)°⇧p = -1"
  by (metis fls_1_not_p_equal_0 fls_X_inv_conv_shift_1 p_depth_fls_shift p_depth_fls1 diff_0)

lemma p_depth_fls_X_intpow: "((fls_X_intpow n)::'a fls)°⇧p = n"
    using p_depth_fls_shift[of p] fls_1_not_p_equal_0 by fastforce

lemma p_depth_const:
  "c°⇧p = pmultiplicity p c" for c :: 'a
proof (cases "c = 0")
  define pp where "pp ≡ Rep_prime p"
  case False
  moreover from pp_def have "¬is_unit pp" using Rep_prime_not_unit by simp
  ultimately obtain k where k: "c = pp ^ pmultiplicity p c * k" "¬ p pdvd k"
    unfolding pp_def by (elim multiplicity_decompose')
  from k(2) have k_n0: "fls_const k ≠ 0" using fls_const_nonzero[of k] by blast
  define g and S
    where "g ≡ fls_shift (- pmultiplicity p c) (fls_const k)"
    and   "S ≡ fls_base_parteval (fls_const c - g) pp"
  have "⋀n. pp ^ Suc n dvd S n"
  proof-
    fix n show "pp ^ Suc n dvd S n"
    proof (cases "n < pmultiplicity p c")
      case True
      with False pp_def S_def g_def k show ?thesis
        using k_n0 fps_parteval_fls_base_factor_to_fps_diff[of "fls_const c" n g pp]
              fls_const_nonzero[of c] dvd_power_le[of pp pp "Suc n" "multiplicity pp c"]
        by    force
    next
      case False
      from k(1) g_def have "fls_subdegree (fls_const c - g) = 0"
        by (cases "pmultiplicity p c = 0") (auto intro: fls_subdegree_eqI)
      with g_def False S_def k(1) show ?thesis
        using fls_times_conv_regpart[of "fls_X ^ (pmultiplicity p c)" "fls_const k"]
              fps_parteval_mult_fps_X_power(2)[of "pmultiplicity p c" n "fps_const k"]
        by    (simp add: fls_X_power_times_conv_shift(1) fls_X_pow_conv_fps_X_pow)
    qed
  qed
  with S_def have "fls_const c ≃⇩p g" using pp_def p_equal_flsI fps_pvanishesI by blast
  moreover from g_def pp_def k(2) have "¬ p pdvd g $$ (fls_subdegree g)" using k_n0 by simp
  moreover from False have "fls_const c ¬≃⇩p 0"
    using p_equal_fls_const_0_iff by meson
  ultimately have "c°⇧p = fls_subdegree g"
    by (metis p_depth_const_def  p_depth_fls_rep_iff)
  with g_def pp_def show ?thesis using k_n0 by simp
qed (simp add: p_depth_const_def)

lemma p_depth_prime_const: "(Rep_prime p)°⇧p = 1"
  using Rep_prime[of p] p_depth_const by simp

end (* context factorial_idom *)


subsection ‹Reduction relative to a prime›

subsubsection ‹Of scalars›

class nontrivial_euclidean_ring_cancel = nontrivial_factorial_comm_ring + euclidean_semiring_cancel
begin
subclass nontrivial_factorial_idom ..
subclass euclidean_ring_cancel ..
end

instance int :: nontrivial_euclidean_ring_cancel ..

abbreviation pdiv ::
  "'a ⇒ 'a::nontrivial_euclidean_ring_cancel prime ⇒ 'a" (infix "pdiv" 70)
  where "a pdiv p ≡ a div (Rep_prime p)"

consts p_modulo :: "'a ⇒ 'b prime ⇒ 'a" (infixl "pmod" 70)

overloading p_modulo_scalar ≡ "p_modulo :: 'a ⇒ 'a prime ⇒ 'a"
begin
definition p_modulo_scalar ::
  "'a::nontrivial_euclidean_ring_cancel ⇒ 'a prime ⇒ 'a"
  where p_modulo_scalar_def[simp]: "p_modulo_scalar a p ≡ a mod (Rep_prime p)"
end

class nontrivial_unique_euclidean_ring = nontrivial_factorial_comm_ring + unique_euclidean_semiring
  + assumes division_segment_prime: "prime p ⟹ division_segment p = 1"
begin
subclass nontrivial_euclidean_ring_cancel ..
end

instance int :: nontrivial_unique_euclidean_ring
proof
  fix p::int assume p: "prime p"
  hence "¬ p < 0" using normalize_prime[of p] by force
  thus "division_segment p = 1" using division_segment_int_def by fastforce
qed

lemma division_segment_1: "division_segment (1::'a::unique_euclidean_semiring) = 1"
proof-
  have "is_unit (division_segment (1::'a))" by force
  from this obtain k where "1 = division_segment (1::'a) * k" by blast
  moreover have "division_segment (1::'a) = division_segment 1 * division_segment 1"
    using division_segment_mult[of 1 1] by force
  ultimately show "division_segment (1::'a) = 1"
    using mult.assoc mult_1_right by metis
qed

lemma one_pdiv: "(1::'a) pdiv p = 0"
  and one_pmod: "(1::'a) pmod p = 1"
  for p :: "'a::nontrivial_unique_euclidean_ring prime"
proof-
  define pp where "pp ≡ Rep_prime p"
  have "((1::'a) pdiv p, 1 pmod p) = (0, (1::'a))"
    unfolding p_modulo_scalar_def
  proof (intro euclidean_relationI)
    show "is_unit (Rep_prime p) ⟹ 1 = 0 ∧ 1 = 0 * Rep_prime p"
      using Rep_prime[of p] by auto
    from pp_def have "division_segment (1::'a) = division_segment pp"
      using Rep_prime division_segment_1 division_segment_prime[of pp] by force
    moreover from pp_def have "euclidean_size (1::'a) < euclidean_size (pp * (1::'a))"
      using Rep_prime_n0 Rep_prime_not_unit euclidean_size_times_nonunit[of pp "1::'a"] by auto
    ultimately show
      "division_segment (1::'a) = division_segment (Rep_prime p) ∧
        euclidean_size (1::'a) < euclidean_size (Rep_prime p) ∧
        1 = 0 * Rep_prime p + 1"
      using pp_def by auto
  qed (simp_all add: Rep_prime_n0)
  thus "(1::'a) pdiv p = 0" and "(1::'a) pmod p = 1" by auto
qed

subsubsection ‹Inductive partial reduction of formal Laurent series›

text ‹
  This inductive function reduces one term at a time.
  The @{type nat} argument specifies how far beyond the subdegree to reduce,
  so that all terms to @{emph ‹one less›} than the @{type nat} argument
  beyond the subdegree are reduced,
  and the term at the @{type nat} argument beyond the subdegree is updated
  to include the carry.
›
primrec fls_partially_p_modulo_rep ::
  "'a::nontrivial_euclidean_ring_cancel fls ⇒
    nat ⇒ 'a prime ⇒ (int ⇒ 'a)"
  where "fls_partially_p_modulo_rep f 0 p = ($$) f" |
  "fls_partially_p_modulo_rep f (Suc N) p =
    (fls_partially_p_modulo_rep f N p)(
      fls_subdegree f + int N :=
        (fls_partially_p_modulo_rep f N p (fls_subdegree f + int N)) pmod p,
      fls_subdegree f + int N + 1 :=
        f $$ (fls_subdegree f + int N + 1) +
        (fls_partially_p_modulo_rep f N p (fls_subdegree f + int N)) pdiv p
    )"

lemma fls_partially_p_modulo_rep_zero[simp]:
  "fls_partially_p_modulo_rep 0 N p n = 0"
proof-
  have "∀n. fls_partially_p_modulo_rep 0 N p n = 0" by (induct N) auto
  thus ?thesis by blast
qed

lemma fls_partially_p_modulo_rep_zeros_below:
  "fls_partially_p_modulo_rep f N p n = 0" if "n < fls_subdegree f"
  using that by (induct N) simp_all

lemma fls_partially_p_modulo_rep_func_lower_bound:
  "∀n<fls_subdegree f. fls_partially_p_modulo_rep f (nat (n + 1 - fls_subdegree f)) p n = 0"
  by simp

lemma fls_partially_p_modulo_rep_agrees:
  "fls_partially_p_modulo_rep f N p n = fls_partially_p_modulo_rep f M p n"
  if "n ≤ fls_subdegree f + int N - 1" and "M ≥ N"
proof-
  have *:
    "⋀K. fls_partially_p_modulo_rep f N p n = fls_partially_p_modulo_rep f (N + K) p n"
  proof-
    fix K from that(1) show
      "fls_partially_p_modulo_rep f N p n = fls_partially_p_modulo_rep f (N + K) p n"
      by (induct K) auto
  qed
  from that(2) show ?thesis using *[of "M - N"] by simp
qed

lemma fls_partially_p_modulo_rep_func_partially:
  "n > fls_subdegree f + int N ⟹ fls_partially_p_modulo_rep f N p n = f $$ n"
  by (induct N, simp_all)

lemma fls_partially_p_modulo_rep_cong:
  "fls_partially_p_modulo_rep f N p n = fls_partially_p_modulo_rep g N p n"
  if "fls_subdegree f = fls_subdegree g" and "∀k≤n. f $$ k = g $$ k"
proof-
  have
    "∀k≤n. fls_partially_p_modulo_rep f N p k = fls_partially_p_modulo_rep g N p k"
  proof (induct N, safe)
    case (Suc N)
    fix k assume "k ≤ n"
    moreover consider
      "k = fls_subdegree f + int N" | "k = fls_subdegree f + int N + 1" |
      "k < fls_subdegree f + int N" | "k > fls_subdegree f + int N + 1"
      by fastforce
    ultimately
      show  "fls_partially_p_modulo_rep f (Suc N) p k = fls_partially_p_modulo_rep g (Suc N) p k"
      by    cases (auto simp add: that Suc)
  qed (simp add: that(2))
  thus ?thesis by auto
qed

lemma fls_partially_reduced_nth_vs_rep:
  "N ≤ n + 1 - fls_subdegree f ⟹ fls_partially_p_modulo_rep f N p = ($$) f"
  if "∀k≤n. (f $$ k) pdiv p = 0"
proof (induct N)
  case (Suc N) thus "fls_partially_p_modulo_rep f (Suc N) p = ($$) f"
    using that Suc div_mult_mod_eq[of "f $$ (fls_subdegree f + int N)" "Rep_prime p"] by simp
qed simp

lemma fls_partially_p_modulo_rep_carry:
  "(∑k=fls_subdegree f..N.
    (f$$k - fls_partially_p_modulo_rep f (nat (N - fls_subdegree f)) p k) *
      (Rep_prime p) ^ nat (k - fls_subdegree f)) = 0"
proof (cases "N ≥ fls_subdegree f", induct N rule: int_ge_induct)
  case (step N)
  define pp and d :: "'a fls ⇒ int" and fpmod_rep
    where "pp ≡ Rep_prime p" and "d ≡ fls_subdegree"
    and   "fpmod_rep ≡ (λn. fls_partially_p_modulo_rep f n p)"
  define S where
    "S ≡
      (∑k=d(f)..N+1. (f$$k - fpmod_rep (nat (N + 1 - d(f))) k) * pp ^ nat (k - d(f)))"
  from d_def step(1) have natN: "nat (N + 1 - d(f)) = Suc (nat (N - d(f)))"
    by (simp add: Suc_nat_eq_nat_zadd1)
  from d_def step(1) have "{d(f)..N + 1} = insert (N+1) (insert N {d(f)..N-1})" by auto
  moreover from d_def fpmod_rep_def step(1) have
    "∀k≤N-1. fpmod_rep (nat (N + 1 - d(f))) k = fpmod_rep (nat (N - d(f))) k"
    using fls_partially_p_modulo_rep_agrees[of _ f "nat (N - d(f))" "nat (N + 1 - d(f))"]
    by    simp
  ultimately have
    "S =
      (f$$N - ((fpmod_rep (nat (N - d(f))) N pdiv p) * pp + (fpmod_rep (nat (N - d(f))) N) pmod p))
      * pp ^ nat (N - d(f)) +
      (∑k∈{d(f)..N-1}. (f$$k - fpmod_rep (nat (N - d(f))) k) * pp ^ nat (k - d(f)))"
    using d_def fpmod_rep_def S_def step(1) natN
    by    (simp add: algebra_simps)
  moreover from d_def step(1) have df_to_N: "{d(f)..N} = insert N {d(f)..N-1}" by fastforce
  ultimately have
    "S = (∑k∈{d(f)..N}. (f$$k - fpmod_rep (nat (N - d(f))) k) * pp ^ nat (k - d(f)))"
    using pp_def S_def by (simp add: algebra_simps)
  with pp_def d_def fpmod_rep_def S_def show ?case using step(2) by presburger
qed simp_all

subsubsection ‹Full reduction of formal Laurent series›

text ‹Now we collect the reduced terms into a formal Laurent series.›

overloading p_modulo_fls ≡ "p_modulo :: 'a fls ⇒ 'a prime ⇒ 'a fls"
begin
definition p_modulo_fls ::
  "'a::nontrivial_euclidean_ring_cancel fls ⇒ 'a prime ⇒ 'a fls"
  where
    "p_modulo_fls f p ≡
      Abs_fls (λn. fls_partially_p_modulo_rep f (nat (n + 1 - fls_subdegree f)) p n)"
end

lemma p_modulo_fls_nth:
  "(f pmod p) $$ n = fls_partially_p_modulo_rep f (nat (n + 1 - fls_subdegree f)) p n"
  using     nth_Abs_fls_lower_bound fls_partially_p_modulo_rep_func_lower_bound
  unfolding p_modulo_fls_def
  by        meson

lemma p_modulo_fls_nth':
  "int N ≥ n + 1 - fls_subdegree f ⟹
    (f pmod p) $$ n = fls_partially_p_modulo_rep f N p n"
proof (induct N)
  case (Suc N) thus ?case
    by (cases "int (Suc N) = n + 1 - fls_subdegree f", metis p_modulo_fls_nth nat_int, force)
qed (simp add: p_modulo_fls_nth)

context
  fixes p :: "'a::nontrivial_euclidean_ring_cancel prime"
begin

lemma fls_pmod_reduced[simp]: "((f pmod p) $$ n) pdiv p = 0"
  using fls_partially_p_modulo_rep.simps(2)[of f "nat (n - fls_subdegree f)" p]
  by (
    cases n "fls_subdegree f - 1" rule: linorder_cases,
    simp_all add: p_modulo_fls_nth Suc_nat_eq_nat_zadd1 algebra_simps
  )

lemma fls_pmod_pmod_nth[simp]: "((f pmod p) $$ n) pmod p = (f pmod p) $$ n" for f :: "'a fls"
  using div_mult_mod_eq[of "(f pmod p) $$ n" "Rep_prime p"] by auto

lemma fls_pmod_carry:
  "(∑k=fls_subdegree f..N. (f - (f pmod p)) $$ k * (Rep_prime p) ^ nat (k - fls_subdegree f)) =
    (fls_partially_p_modulo_rep f (nat (N + 1 - fls_subdegree f)) p (N + 1) - f $$ (N + 1)) *
    (Rep_prime p) ^ nat (N + 1 - fls_subdegree f)"
proof (cases "N ≥ fls_subdegree f - 1")
  case True
  define d :: "'a fls ⇒ int" and fpmod_rep
    where "d ≡ fls_subdegree"
    and   "fpmod_rep ≡ (λn. fls_partially_p_modulo_rep f n p)"
  from d_def True have "{d(f)..N + 1} = insert (N+1) {d(f)..N}" by auto
  moreover from d_def fpmod_rep_def True
    have  "∀k≤N. fpmod_rep (nat (N + 1 - d(f))) k = (f pmod p) $$ k"
    using p_modulo_fls_nth'[of _ f "nat (N + 1 - d(f))"]
    by    force
  ultimately show ?thesis
    using d_def fpmod_rep_def fls_partially_p_modulo_rep_carry[of f "N + 1" p]
    by    (simp add: algebra_simps)
qed simp

lemma fls_pmod_carry':
  "(∑k=fls_subdegree f..N. (f - (f pmod p)) $$ k * (Rep_prime p) ^ nat (k - fls_subdegree f)) =
    (fls_partially_p_modulo_rep f (nat (N - fls_subdegree f)) p N pdiv p) *
      (Rep_prime p) ^ Suc (nat (N - fls_subdegree f))"
  if "N ≥ fls_subdegree f"
  using that fls_pmod_carry[of f N]
        fls_partially_p_modulo_rep.simps(2)[of f "nat (N - fls_subdegree f)" p]
  by    (simp add: algebra_simps Suc_nat_eq_nat_zadd1)

lemma fls_p_reduced_is_zero_iff:
  "f = 0 ⟷ f ≃⇩p 0 ∧ (∀n. f$$n pdiv p = 0)"
  for f :: "'a fls"
proof (standard, safe)
  assume f_0: "f ≃⇩p 0" and f_reduced: "∀n. f$$n pdiv p = 0"
  define pp and d :: "'a fls ⇒ int"
    where "pp ≡ Rep_prime p" and "d ≡ fls_subdegree"
  show "f = 0"
  proof (intro fls_eqI)
    fix n have "∀k≤n. f$$k = 0"
    proof (cases "n ≥ d(f) - 1", induct n rule: int_ge_induct, safe)
      case (step n)
      fix k assume k: "k ≤ n + 1"
      define S where "S ≡ (∑k=d(f)..n + 1. f $$ k * pp ^ nat (k - d(f)))"
      with f_0 d_def pp_def step(1) have "pp ^ Suc (nat (n + 1 - d f)) dvd S"
        using fls_p_equal0_extended_intsum_iff[of _ f] by fastforce
      from this obtain T where T: "S = pp ^ Suc (nat (n + 1 - d f)) * T" by (elim dvdE)
      from step(1) have "{d(f)..n + 1} = insert (n + 1) {d(f)..n}" by fastforce
      with S_def pp_def step(2)
        have "S = ((f$$(n+1) pdiv p) * pp + f$$(n+1) pmod p) * pp ^ nat (n + 1 - d(f))"
        by   force
      moreover from f_reduced have "f$$(n+1) pdiv p = 0" by blast
      ultimately have "f$$(n + 1) = 0"
        using pp_def T Rep_prime_n0[of p] dvd_imp_mod_0[of pp] mod_mod_trivial[of "f$$(n + 1)" pp]
        by    force
      with k step(2) show "f $$ k = 0" by (cases "k = n + 1") auto
    qed (simp_all add: d_def)
    thus "f $$ n = 0 $$ n" by auto
  qed
qed simp_all

lemma p_modulo_fls_eq0[simp]:
  "f pmod p = 0" if "f ≃⇩p 0" for f :: "'a fls"
proof-
  define d :: "'a fls ⇒ int" and fpmod_rep
    where "d ≡ fls_subdegree"
    and   "fpmod_rep ≡ (λn. fls_partially_p_modulo_rep f n p)"
  have "∀n. ∀k≤n. (f pmod p) $$ k = 0"
  proof
    fix n show "∀k≤n. (f pmod p) $$ k = 0"
    proof (cases "n ≥ d(f)", induct n rule: int_ge_induct, safe)
      case base fix k assume k: "k ≤ d(f)"
      show "(f pmod p) $$ k = 0"
      proof (cases "k = d(f)")
        case True
        with that d_def show ?thesis
          using fls_p_equal0_extended_intsum_iff[of _ f] p_modulo_fls_nth[of f] by fastforce
      next
        case False with k d_def show ?thesis by (simp add: p_modulo_fls_nth)
      qed
    next
      case (step n)
      fix k assume k: "k ≤ n + 1"
      define pp where "pp ≡ Rep_prime p"
      define S where "S ≡ (∑k=d(f)..n + 1. f $$ k * pp ^ nat (k - d(f)))"
      with that d_def pp_def step(1) have "pp ^ Suc (nat (n + 1 - d f)) dvd S"
        using fls_p_equal0_extended_intsum_iff[of _ f] by fastforce
      from this obtain T where T: "S = pp ^ Suc (nat (n + 1 - d f)) * T" by (elim dvdE)
      moreover from step(1) have "{d(f)..n + 1} = insert (n + 1) {d(f)..n}" by fastforce
      ultimately have
        "(f pmod p) $$ (n+1) * pp ^ nat (n + 1 - d(f)) =
          (T - fpmod_rep (nat (n + 1 - d(f))) (n + 1) pdiv p) * pp * pp ^ nat (n + 1 - d(f))"
        using d_def fpmod_rep_def pp_def S_def step fls_pmod_carry'[of f "n + 1"]
        by (simp add: algebra_simps)
      with pp_def have "(f pmod p) $$ (n+1) = 0"
        using Rep_prime_n0[of p] dvd_mult_cancel_right fls_pmod_reduced[of f "n + 1"] by simp
      with k step(2) show "(f pmod p) $$ k = 0" by (cases "k = n + 1") auto
    qed (simp add: d_def p_modulo_fls_nth)
  qed
  thus "f pmod p = 0" using fls_eqI[of "f pmod p" 0] by auto
qed

lemma fls_pmod_eq0_iff:
  "f pmod p = 0 ⟷ f ≃⇩p 0" for f :: "'a fls"
proof (standard, rule iffD2, rule fls_p_equal0_extended_intsum_iff, safe)
  define pp and d :: "'a fls ⇒ int"
    where "pp ≡ Rep_prime p" and "d ≡ fls_subdegree"
  show "d(f) ≤ d(f)" by blast
  fix n assume "f pmod p = 0" and "n ≥ d(f)"
  with pp_def d_def
    show  "pp ^ Suc (nat (n - d(f))) dvd (∑k=d(f)..n. f $$ k * pp ^ nat (k - d(f)))"
    using fls_pmod_carry'
    by    force
qed simp

lemma fls_pmod_equiv: "f ≃⇩p f pmod p" for f :: "'a fls"
proof (cases "f pmod p = 0")
  case True thus ?thesis using fls_pmod_eq0_iff by simp
next
  case False show ?thesis
  proof (rule iffD2, rule p_equal_fls_extended_intsum_iff, safe)
    define pp and d :: "'a fls ⇒ int"
      where "pp ≡ Rep_prime p" and "d ≡ fls_subdegree"
    from False d_def have "d(f) ≤ d(f pmod p)"
      by (auto intro: fls_subdegree_geI simp add: p_modulo_fls_nth)
    thus "d(f) ≤ min (d(f)) (d(f pmod p))" by fastforce
    fix n assume "n ≥ d(f)"
    with d_def pp_def show
      "pp ^ Suc (nat (n - d(f))) dvd (∑k=d(f)..n. (f - f pmod p) $$ k * pp ^ nat (k - d(f)))"
      using fls_pmod_carry'[of f] by auto
  qed
qed

lemma fls_p_reduced_subdegree_unique:
  "fls_subdegree g = (f°⇧p)"
  if  "f ≃⇩p g" and "∀n. (g $$ n) pdiv p = 0"
  for f g :: "'a fls"
proof (cases "f ≃⇩p 0")
  case True
  with that have "g = 0" using fls_p_reduced_is_zero_iff p_equality_fls.trans_right by blast
  with True show ?thesis by (simp add: p_depth_fls_def)
next
  case False show ?thesis
  proof (intro p_depth_fls_eqI[symmetric], rule False, rule that(1))
    fix h assume h: "f ≃⇩p h"
    from that(1) h
      have  "fls_subdegree h > fls_subdegree g ⟹ p pdvd g $$ (fls_subdegree g)"
      using fls_pmod_equiv p_equality_fls.trans_right[of p f]
            p_equal_fls_extended_intsum_iff[of "fls_subdegree g" g h]
      by    fastforce
    moreover from that(2) have "(g $$ (fls_subdegree g)) pdiv p = 0" by blast
    ultimately show "fls_subdegree h ≤ fls_subdegree g"
      using False that(1) nth_fls_subdegree_nonzero[of g] by fastforce
  qed
qed

lemma fls_pmod_subdegree:
  "fls_subdegree (f pmod p) = (f°⇧p)" for f :: "'a fls"
  using fls_p_reduced_subdegree_unique fls_pmod_reduced fls_pmod_equiv by blast

lemma fls_pmod_depth:
  "(f pmod p)°⇧p = (f°⇧p)" for f :: "'a fls"
  by (metis p_depth_fls.depth_equiv fls_pmod_equiv)

lemma fls_pmod_subdegree_ge:
  "fls_subdegree (f pmod p) ≥ fls_subdegree f" if "f ¬≃⇩p 0"
  for f :: "'a fls"
  using that fls_pmod_subdegree p_depth_fls_ge_p_equal_subdegree' by auto

lemma fls_pmod_nth_below_subdegree:
  "(f pmod p) $$ n = 0" if "n < fls_subdegree f" for f :: "'a fls"
  using that fls_pmod_subdegree_ge[of f] by fastforce

lemma fls_pmod_nth_cong:
  "(f pmod p) $$ n = (g pmod p) $$ n" if "∀k≤n. f $$ k = g $$ k" for f g :: "'a fls"
proof-
  consider
    "f = 0" "g = 0" | (f_n0) "f ≠ 0" "g = 0" | (g_n0) "f = 0" "g ≠ 0" |
    (f_n0_upper) "f ≠ 0" "n ≥ fls_subdegree f" |
    (g_n0_lower) "g ≠ 0" "n < fls_subdegree f"
    by linarith
  thus ?thesis
  proof cases
    case f_n0 with that show ?thesis
      using fls_subdegree_geI[of f "n + 1"] by (simp add: fls_pmod_nth_below_subdegree)
  next
    case g_n0 with that show ?thesis
      using fls_subdegree_geI[of g "n + 1"] by (simp add: fls_pmod_nth_below_subdegree)
  next
    case g_n0_lower with that show ?thesis
      using fls_subdegree_geI[of g "n + 1"] by (simp add: fls_pmod_nth_below_subdegree)
  next
    case f_n0_upper
    from f_n0_upper(2) have "⋀k. k < fls_subdegree f ⟹ k ≤ n" by simp
    with that have "⋀k. k < fls_subdegree f ⟹ g $$ k = 0" by fastforce
    with that f_n0_upper show ?thesis
      using nth_fls_subdegree_nonzero fls_subdegree_eqI p_modulo_fls_nth
            fls_partially_p_modulo_rep_cong
      by    metis
  qed simp
qed

lemma fls_partially_reduced_nth_vs_pmod:
  "(f pmod p) $$ n = f $$ n" if "∀k≤n. (f $$ k) pdiv p = 0"
proof (cases "n ≥ fls_subdegree f")
  case True with that show ?thesis
    by (simp add: p_modulo_fls_nth fls_partially_reduced_nth_vs_rep)
qed (force simp add: fls_pmod_nth_below_subdegree)

lemma fls_pmod_eqI:
  "f pmod p = g" if "f ≃⇩p g" and "∀n. (g $$ n) pdiv p = 0"
proof (intro fls_eq_above_subdegreeI, safe)
  define d :: "'a fls ⇒ int" where "d ≡ fls_subdegree"
  with that have *: "d(f pmod p) ≥ (f°⇧p)" "d(g) ≥ (f°⇧p)"
    using fls_pmod_subdegree fls_p_reduced_subdegree_unique by (simp, presburger)
  thus "d(f pmod p) ≥ (f°⇧p) - 1" "d(g) ≥ (f°⇧p) - 1" by auto
  fix n assume n: "n ≥ (f°⇧p) - 1"
  hence "∀k≤n. (f pmod p) $$ k = g $$ k"
  proof (induct n rule: int_ge_induct)
    case base from that show ?case using fls_pmod_subdegree fls_p_reduced_subdegree_unique by simp
  next
    case (step n) show ?case
    proof clarify
      define pp where "pp ≡ Rep_prime p"
      fix k assume k: "k ≤ n + 1"
      define S where
        "S ≡ (∑k=(f°⇧p)..n + 1.
          (f pmod p - g) $$ k * pp ^ nat (k - (f°⇧p)))"
      define A
        where "A ≡ (if n + 1 = (f°⇧p) then {} else {(f°⇧p)..n})"
      with step(1) have "{(f°⇧p)..n + 1} = insert (n + 1) A" by force
      moreover from A_def step(2) have "∀k∈A. (f pmod p - g) $$ k = 0" by simp
      ultimately have
        "S = (f pmod p - g) $$ (n + 1) * pp ^ nat (n + 1 - (f°⇧p))"
        using S_def A_def by force
      moreover from step(1) that(1) d_def pp_def S_def
        have  "pp ^ Suc (nat (n + 1 - (f°⇧p))) dvd S"
        using * p_equality_fls.trans_right fls_pmod_equiv
              p_equal_fls_extended_intsum_iff[of "(f°⇧p)" "f pmod p" g]
        by    force
      ultimately have "p pdvd ((f pmod p) - g) $$ (n + 1)" using pp_def Rep_prime_n0 by auto
      with pp_def that(2)
        have  "(f pmod p) $$ (n + 1) = ((g$$(n+1)) pdiv p) * pp + (g$$(n+1)) pmod p"
        using mod_eq_dvd_iff fls_pmod_reduced div_mult_mod_eq[of "(f pmod p) $$ (n + 1)" pp]
        by    force
       with pp_def k show "(f pmod p) $$ k = g $$ k"
        using step(2) by (cases "k = n + 1") (auto simp add: div_mult_mod_eq)
    qed
  qed
  thus "(f pmod p) $$ n = g $$ n" by fast
qed

lemma fls_pmod_eq_pmod_iff:
  "f pmod p = g pmod p ⟷ f ≃⇩p g" for f g :: "'a fls"
proof
  show "f pmod p = g pmod p ⟹ f ≃⇩p g"
    by (metis fls_pmod_equiv p_equality_fls.refl p_equality_fls.cong)
  show "f ≃⇩p g ⟹ f pmod p = g pmod p"
    using fls_pmod_equiv p_equality_fls.trans fls_pmod_reduced fls_pmod_eqI by meson
qed

lemma fls_pmod_equiv_pmod_iff:
  "(f pmod p) ≃⇩p (g pmod p) ⟷ f ≃⇩p g"
  for f g :: "'a fls"
  using fls_pmod_equiv p_equality_fls.cong p_equality_fls.sym by meson

lemma fls_p_modulo_iff:
  "f pmod p = g ⟷ f ≃⇩p g ∧ (∀n. (g $$ n) pdiv p = 0)"
  using fls_pmod_equiv fls_pmod_reduced fls_pmod_eqI by blast

lemma fls_pmod_pmod[simp]: "(f pmod p) pmod p = f pmod p" for f :: "'a fls"
  by (metis fls_pmod_equiv p_equal_fls_trans fls_pmod_reduced fls_pmod_eqI)

lemma fls_pmod_cong:
  "f pmod p = g pmod p" if "f ≃⇩p g" for f g :: "'a fls"
  using that fls_pmod_equiv p_equal_fls_trans fls_pmod_reduced fls_pmod_eqI by meson

end (* context nontrivial_euclidean_ring_cancel *)

subsubsection ‹Algebraic properties of reduction›

lemma fls_pmod_1[simp]:
  "(1::'a fls) pmod p = 1" for p :: "'a::nontrivial_unique_euclidean_ring prime"
  by (intro fls_pmod_eqI, simp_all add: one_pdiv)

context
  fixes p :: "'a::nontrivial_euclidean_ring_cancel prime"
begin

lemma fls_pmod_0: "(0::'a fls) pmod p = 0"
  by simp

lemma fls_pmod_uminus_equiv: "(-f) pmod p ≃⇩p -(f pmod p)" for f :: "'a fls"
  using fls_pmod_equiv p_equality_fls.uminus p_equality_fls.trans_right by blast

lemma fls_pmod_equiv_add:
  "(f + g) pmod p = (f' + g') pmod p" if "f ≃⇩p f'" and "g ≃⇩p g'"
  for f f' g g' :: "'a fls"
  using that p_equality_fls.add fls_pmod_equiv p_equal_fls_trans fls_pmod_reduced fls_pmod_eqI
  by    meson

lemma fls_pmod_const_add:
  "(fls_const c + f) pmod p = fls_const c + f pmod p" if "fls_subdegree f > 0" and "c pdiv p = 0"
  for c :: 'a and f :: "'a fls"
proof (intro fls_pmod_eqI, safe)
  fix n from that show "(fls_const c + f pmod p) $$ n pdiv p = 0"
    by (cases n "0::int" rule: linorder_cases, simp_all add: fls_pmod_nth_below_subdegree)
qed (simp add: fls_pmod_equiv p_equality_fls.add)

lemma fls_pmod_add_equiv:
  "(f + g) pmod p ≃⇩p (f pmod p) + (g pmod p)" for f g :: "'a fls"
  by (metis fls_pmod_equiv fls_pmod_equiv_add p_equality_fls.trans_left)

lemma fls_pmod_mismatched_add_nth:
  "n < fls_subdegree g ⟹ ((f + g) pmod p) $$ n = (f pmod p) $$ n"
  "((f + g) pmod p) $$ (fls_subdegree g) =
    ((f pmod p) $$ (fls_subdegree g) + g $$ (fls_subdegree g)) pmod p"
  if "fls_subdegree g > fls_subdegree f"
  for f :: "'a fls"
proof-
  assume n: "n < fls_subdegree g"
  show "((f + g) pmod p) $$ n = (f pmod p) $$ n"
  proof (cases "f = 0")
    case True with n show ?thesis using fls_pmod_nth_below_subdegree by auto
  next
    case False
    with that have "fls_subdegree (f + g) = fls_subdegree f" by (simp add: fls_subdegree_eqI)
    with n show ?thesis
      using fls_partially_p_modulo_rep_cong[of "f + g"] by (simp add: p_modulo_fls_nth)
  qed
next
  define pp and d :: "'a fls ⇒ int" and pmod_rep
    where "pp ≡ Rep_prime p" and "d ≡ fls_subdegree"
    and   "pmod_rep ≡ (λf N. fls_partially_p_modulo_rep f N p)"
  show
    "((f + g) pmod p) $$ (fls_subdegree g) =
      ((f pmod p) $$ (fls_subdegree g) + g $$ (fls_subdegree g)) pmod p"
  proof (cases "f = 0")
    case False
    with that d_def have dfg: "d(f + g) = d(f)" by (simp add: fls_subdegree_eqI)
    with that d_def pmod_rep_def pp_def show ?thesis
      using fls_partially_p_modulo_rep.simps(2)[of "f + g" "nat (d(g) - d(f))"]
            fls_partially_p_modulo_rep.simps(2)[of "f + g" "nat (d(g) - d(f) - 1)"]
            fls_partially_p_modulo_rep.simps(2)[of f "nat (d(g) - d(f) - 1)"]
            fls_partially_p_modulo_rep_cong[of "f + g" f "d(g) - 1" "nat (d(g) - d(f) - 1)"]
            fls_partially_p_modulo_rep.simps(2)[of f "nat (d(g) - d(f))"]
      by    (simp add: p_modulo_fls_nth Suc_nat_eq_nat_zadd1 algebra_simps mod_simps)
  qed (simp add: d_def pmod_rep_def p_modulo_fls_nth)
qed

lemma fls_pmod_equiv_minus:
  "(f - g) pmod p = (f' - g') pmod p" if "f ≃⇩p f'" and "g ≃⇩p g'"
  for f f' g g' :: "'a fls"
  using that p_equality_fls.minus fls_pmod_equiv p_equal_fls_trans fls_pmod_reduced fls_pmod_eqI
  by    meson

lemma fls_pmod_minus_equiv:
  "(f - g) pmod p ≃⇩p ((f pmod p) - (g pmod p))" for f g :: "'a fls"
  by (metis fls_pmod_equiv fls_pmod_equiv_minus p_equality_fls.trans_left)

lemma fls_pmod_equiv_times:
  "(f * g) pmod p = (f' * g') pmod p" if "f ≃⇩p f'" and "g ≃⇩p g'"
  for f f' g g' :: "'a fls"
  using that p_equality_fls.mult fls_pmod_equiv p_equal_fls_trans fls_pmod_reduced fls_pmod_eqI
  by    meson

lemma fls_pmod_times_equiv:
  "(f * g) pmod p ≃⇩p (f pmod p) * (g pmod p)" for f g :: "'a fls"
  by (metis fls_pmod_equiv fls_pmod_equiv_times p_equality_fls.trans_left)

lemma fls_pmod_diff_cancel:
  "(f pmod p) $$ n = (g pmod p) $$ n" if "n < ((f - g)°⇧p)"
  for f g :: "'a fls"
proof-
  consider
    "f ≃⇩p 0" | "g ≃⇩p 0" |
    (nonzero) "f ¬≃⇩p 0" "g ¬≃⇩p 0"
    by fast
  thus ?thesis
    using that
  proof cases
    case nonzero
    hence "n < ((f - g)°⇧p) ⟹ (f pmod p) $$ n = (g pmod p) $$ n"
    proof (induct f g rule: linorder_wlog'[of "λf. f°⇧p"])
      case (le f g)
      have *:
        "⋀n. n < ((f - g)°⇧p) ⟹
          ((f pmod p - g pmod p) pmod p) $$ n = 0"
        using p_depth_fls.depth_diff_equiv fls_pmod_equiv fls_pmod_subdegree fls_eq0_below_subdegree
        by    metis
      from le(2) consider
        (diff_le)   "((f - g)°⇧p) ≤ (f°⇧p)" |
        (diff_gt)   "((f - g)°⇧p) > (g°⇧p)" |
        (diff_betw)
          "(f°⇧p) < ((f - g)°⇧p)"
          "((f - g)°⇧p) ≤ (g°⇧p)"
        by linarith
      thus "(f pmod p) $$ n = (g pmod p) $$ n"
      proof cases
        case diff_le with le(1,2) show ?thesis by (simp add: fls_pmod_subdegree)
      next
        case diff_betw
        from le(2) diff_betw(2) have "∀k≤n. ((f pmod p - g pmod p) $$ k) pdiv p = 0"
          by (auto simp add: fls_pmod_subdegree)
        with le(2) have "(f pmod p - g pmod p) $$ n = 0"
          using * fls_partially_reduced_nth_vs_pmod by metis
        thus ?thesis by auto
      next
        case diff_gt
        have "¬ (f°⇧p) < (g°⇧p)"
        proof
          assume lt: "(f°⇧p) < (g°⇧p)"
          moreover from this
            have  "∀k≤(f°⇧p). ((f pmod p - g pmod p) $$ k) pdiv p = 0"
            by    (auto simp add: fls_pmod_subdegree)
          ultimately have "(f pmod p - g pmod p) $$ (f°⇧p) = 0"
            using diff_gt * fls_partially_reduced_nth_vs_pmod[of _ "f pmod p - g pmod p"]
            by    fastforce
          with le(3) lt show False
            using fls_pmod_subdegree[of _ p] fls_pmod_eq0_iff nth_fls_subdegree_nonzero by force
        qed
        with le(1) have df_dg: "(f°⇧p) = (g°⇧p)" by linarith
        define pp where "pp ≡ Rep_prime p"
        have
          "n < ((f - g)°⇧p) ⟹
            ∀k≤n. (f pmod p) $$ k = (g pmod p) $$ k"
        proof (cases "n ≥ (f°⇧p)")
          case True
          have strong:
            "⋀N. N < ((f - g)°⇧p) ⟹
              ∀k<N. (f pmod p) $$ k = (g pmod p) $$ k ⟹
              ¬ (f pmod p) $$ N ≠ (g pmod p) $$ N"
          proof
            fix N
            assume  N  :  "N < ((f - g)°⇧p)"
                          "∀k<N. (f pmod p) $$ k = (g pmod p) $$ k"
              and   neq:  "(f pmod p) $$ N ≠ (g pmod p) $$ N"
            hence "(f pmod p - g pmod p) $$ N ≠ 0" by simp
            with N(2) have "fls_subdegree (f pmod p - g pmod p) = N"
              using fls_subdegree_eqI[of "f pmod p - g pmod p" N] by auto
            hence "((f pmod p - g pmod p) pmod p) $$ N = ((f pmod p - g pmod p) $$ N) pmod p"
              by (simp add: p_modulo_fls_nth)
            with N(1) have "((f pmod p - g pmod p) $$ N) pmod p = 0"
              using * by metis
            hence "((f pmod p) $$ N) pmod p = ((g pmod p) $$ N) pmod p"
              using mod_eq_dvd_iff by auto
            with neq show False using fls_pmod_pmod_nth[of f] fls_pmod_pmod_nth[of g] by metis
          qed
          from True show
            "n < ((f - g)°⇧p) ⟹
              ∀k≤n. (f pmod p) $$ k = (g pmod p) $$ k"
          proof (induct n rule: int_ge_induct, safe)
            case base
            fix k
            from diff_gt have "(f°⇧p) < (f - g°⇧p)" using df_dg by auto
            moreover have k_lt: "∀k<f°⇧p. (f pmod p) $$ k = (g pmod p) $$ k"
              using df_dg by (auto simp add: fls_pmod_subdegree)
            ultimately have
              "¬ (f pmod p) $$ (f°⇧p) ≠
                (g pmod p) $$ (f°⇧p)"
              "k < (f°⇧p) ⟹ (f pmod p) $$ k = (g pmod p) $$ k"
              using strong by (presburger, blast)
            moreover assume "k ≤ (f°⇧p)"
            ultimately show "(f pmod p) $$ k = (g pmod p) $$ k" by fastforce
          next
            case (step n)
            fix k
            from step(2,3) have "¬ (f pmod p) $$ (n + 1) ≠ (g pmod p) $$ (n + 1)"
              using strong by auto
            hence "k = n + 1 ⟹ (f pmod p) $$ k = (g pmod p) $$ k" by fastforce
            moreover from step(2,3)
              have  "k ≤ n ⟹ (f pmod p) $$ k = (g pmod p) $$ k"
              by    auto
            moreover assume "k ≤ n + 1"
            ultimately show "(f pmod p) $$ k = (g pmod p) $$ k" by fastforce
          qed
        next
          case False thus "∀k≤n. (f pmod p) $$ k = (g pmod p) $$ k"
            using df_dg by (auto simp add: fls_pmod_subdegree)
        qed
        with le(2) show ?thesis by fast
      qed
    qed (simp add: p_depth_fls.depth_diff)
    with that show ?thesis by blast
  qed (
    fastforce simp add: p_depth_fls.depth_diff_equiv0_left fls_pmod_eq0_iff fls_pmod_subdegree,
    fastforce simp add: p_depth_fls.depth_diff_equiv0_right fls_pmod_eq0_iff fls_pmod_subdegree
  )
qed

lemma fls_pmod_diff_cancel_iff:
  "((f - g)°⇧p) > n ⟷
    (∀k≤n. (f pmod p) $$ k = (g pmod p) $$ k)"
  if "f ¬≃⇩p g"
  for f g :: "'a fls"
proof
  assume "∀k≤n. (f pmod p) $$ k = (g pmod p) $$ k"
  moreover from that have "f pmod p ≠ g pmod p" using fls_pmod_eq_pmod_iff by auto
  ultimately have "fls_subdegree (f pmod p - g pmod p) > n"
    using fls_subdegree_greaterI[of "f pmod p - g pmod p"] by auto
  with that have "fls_subdegree ((f pmod p - g pmod p) pmod p) > n"
    using fls_pmod_subdegree_ge[of p "f pmod p - g pmod p"] fls_pmod_equiv_pmod_iff
          p_equality_fls.conv_0
    by    fastforce
  thus "((f - g)°⇧p) > n"
    using fls_pmod_subdegree fls_pmod_equiv p_depth_fls.depth_diff_equiv by metis
qed (simp add: fls_pmod_diff_cancel)

end (* context nontrivial_euclidean_ring_cancel *)


subsection ‹Inversion relative to a prime›

subsubsection ‹Of scalars›

class bezout_semiring = semiring_gcd +
  assumes bezout: "∃u v. u * x + v * y = gcd x y"

class bezout_ring = ring_gcd +
  assumes bezout: "∃u v. u * x + v * y = gcd x y"
begin
subclass bezout_semiring using bezout by unfold_locales
subclass idom ..
end

instance int :: bezout_ring by (standard, rule bezout_int)

class nontrivial_factorial_euclidean_bezout = nontrivial_euclidean_ring_cancel + bezout_semiring
begin
subclass bezout_ring by (standard, rule bezout)
end

class nontrivial_factorial_unique_euclidean_bezout =
  nontrivial_unique_euclidean_ring + bezout_semiring
begin
subclass nontrivial_factorial_euclidean_bezout ..
end

instance int :: nontrivial_factorial_unique_euclidean_bezout ..

lemma prime_residue_inverse_ex1:
  "∃!x. x pdiv p = 0 ∧ (x * a) pmod p = 1" if "¬ p pdvd a"
  for a :: "'a::nontrivial_factorial_unique_euclidean_bezout" and p :: "'a prime"
proof (intro ex_ex1I, safe)
  define pp where "pp ≡ Rep_prime p"
  with that obtain u v where uv: "u * pp + v * a = 1"
    using Rep_prime[of p] prime_imp_coprime bezout[of pp a] coprime_iff_gcd_eq_1[of pp a]
    by    auto
  define y where "y ≡ v pmod p"
  with pp_def have "(y * a) pmod p = 1"
    by (metis
      uv p_modulo_scalar_def mod_add_left_eq mod_mult_self2_is_0 add_0_left mod_mult_left_eq
      one_pmod
    )
  moreover from y_def have "y pdiv p = 0" by auto
  ultimately show "∃x. x pdiv p = 0 ∧ (x * a) pmod p = 1" by fast

  fix x x'
  assume  x : "x  pdiv p = 0" "x  * a pmod p = 1"
    and   x': "x' pdiv p = 0" "x' * a pmod p = 1"
  from pp_def x(1) have "x pmod p = x" using div_mult_mod_eq[of x pp] by auto
  with x'(2) have "x = ((x pmod p) * ((x' * a) pmod p)) pmod p" by auto
  also from pp_def x(2) have "… = (x' * 1) pmod p"
    by (metis p_modulo_scalar_def mult.assoc mult.commute mod_mult_right_eq)
  finally show "x = x'" using pp_def x'(1) div_mult_mod_eq[of x' pp] by simp
qed

consts pinverse :: "'a ⇒ 'b prime ⇒ 'a"
  ("(_¯⇧_)" [51, 51] 50)

overloading pinverse_scalar ≡ "pinverse :: 'a ⇒ 'a prime ⇒ 'a"
begin
definition pinverse_scalar ::
  "'a::nontrivial_factorial_unique_euclidean_bezout ⇒ 'a prime ⇒ 'a"
  where
    "pinverse_scalar a p ≡
      (if p pdvd a then 0 else
        (THE x. x pdiv p = 0 ∧ (x * a) pmod p = 1))"
end

context
  fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
begin

lemma pinverse_scalar: "((a¯⇧p) * a) pmod p = 1" if "¬ p pdvd a" for a :: 'a
  using that theI'[OF prime_residue_inverse_ex1] unfolding pinverse_scalar_def by auto

lemma pinverse_scalar_reduced: "(a¯⇧p) pdiv p = 0" for a :: 'a
  using theI'[OF prime_residue_inverse_ex1] unfolding pinverse_scalar_def by auto

lemma pinverse_scalar_nzero: "(a¯⇧p) ≠ 0" if "¬ p pdvd a" for a :: 'a
  using that pinverse_scalar by fastforce

lemma pinverse_scalar_zero[simp]: "((0::'a)¯⇧p) = 0"
  unfolding pinverse_scalar_def by force

lemma pinverse_scalar_one[simp]: "((1::'a)¯⇧p) = 1"
  using     Rep_prime_not_unit the1_equality[OF prime_residue_inverse_ex1, of p 1] one_pdiv one_pmod
  unfolding pinverse_scalar_def
  by        auto

end (* context *)

subsubsection ‹Inductive partial inversion of formal Laurent series›

text ‹
  Inductively define a depth-zero partial inverse representative function.
  It is effectively a polynomial of degree equal to the @{type nat} argument.
›
primrec fls_partially_pinverse_rep ::
  "'a::nontrivial_factorial_unique_euclidean_bezout fls ⇒ nat ⇒
    'a prime ⇒ (int ⇒ 'a)"
  where
    "fls_partially_pinverse_rep f 0 p n =
      (if n = 0
        then ((f pmod p) $$ (f°⇧p))¯⇧p
        else 0)"
  | "fls_partially_pinverse_rep f (Suc N) p =
      (fls_partially_pinverse_rep f N p)(
        int (Suc N) := -(
          (
            (
              fls_shift (f°⇧p) (Abs_fls (fls_partially_pinverse_rep f N p)) *
              (f pmod p)
            ) pmod p
          ) $$ (int (Suc N)) * (((f pmod p) $$ (f°⇧p))¯⇧p)
        ) pmod p
      )"

lemma fls_partially_pinverse_rep_func_lower_bound:
  "∀n<0. fls_partially_pinverse_rep f (nat n) p n = 0"
  by fastforce

lemma fls_partially_pinverse_rep_at_0:
  "fls_partially_pinverse_rep f N p 0 = (((f pmod p) $$ (f°⇧p))¯⇧p)"
  by (induct N) simp_all

lemma fls_partially_pinverse_rep_func_lower_bound':
  "∀n<0. fls_partially_pinverse_rep f N p n = 0"
  by (induct N) simp_all

lemmas Abs_fls_partially_pinverse_rep_nth =
  nth_Abs_fls_lower_bound[OF fls_partially_pinverse_rep_func_lower_bound']

lemma fls_partially_pinverse_rep_func_truncates:
  "n > int N ⟹ fls_partially_pinverse_rep f N p n = 0"
  by (induct N, simp_all)

context
  fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
begin

lemma pinverse_scalar_fls_pmod_base:
  "(
    (((f pmod p) $$ (f°⇧p))¯⇧p) * (f pmod p) $$ (f°⇧p)
  ) pmod p = 1"
  if  "f ¬≃⇩p 0"
  for f :: "'a fls"
  using that fls_pmod_eq0_iff fls_pmod_subdegree[of f]
        nth_fls_subdegree_nonzero[of "f pmod p"]
        pinverse_scalar[of p "(f pmod p) $$ (f°⇧p)"]
        fls_pmod_reduced[of f p "(f°⇧p)"]
  by    fastforce

lemma fls_partially_pinverse_rep_eq_zero:
  "fls_partially_pinverse_rep f N p = 0" if "f ≃⇩p 0"
  for f :: "'a fls"
proof (induct N)
  case 0 from that show ?case by auto
next
  case (Suc N) show ?case
  proof
    fix n show "fls_partially_pinverse_rep f (Suc N) p n = 0 n"
    proof (cases "n = int (Suc N)")
      case True
      from Suc have
        "fls_shift (f°⇧p) (Abs_fls (fls_partially_pinverse_rep f N p)) = 0"
        using fls_shift_zero unfolding zero_fls_def zero_fun_def by fastforce
      with True show ?thesis using fls_pmod_0 by auto
    qed (simp add: Suc)
  qed
qed

lemma fls_partially_pinverse_rep_nzero_at_0:
  "fls_partially_pinverse_rep f N p 0 ≠ 0" if "f ¬≃⇩p 0"  for f :: "'a fls"
  using that fls_partially_pinverse_rep_at_0[of f] pinverse_scalar_fls_pmod_base by fastforce

lemma fls_partially_pinverse_rep_eq_zero_iff:
  "fls_partially_pinverse_rep f N p = 0 ⟷ f ≃⇩p 0"
  for f :: "'a fls"
  using fls_partially_pinverse_rep_eq_zero[of f N] fls_partially_pinverse_rep_nzero_at_0[of f N]
  by    fastforce

lemma Abs_fls_partially_pinverse_rep_nzero:
  "Abs_fls (fls_partially_pinverse_rep f N p) ≠ 0" if "f ¬≃⇩p 0"
  for f :: "'a fls"
  using that fls_partially_pinverse_rep_nzero_at_0 Abs_fls_partially_pinverse_rep_nth[of f N p]
  by    fastforce

lemma Abs_fls_partially_pinverse_rep_eq_zero_iff:
  "Abs_fls (fls_partially_pinverse_rep f N p) = 0 ⟷ f ≃⇩p 0"
  for f :: "'a fls"
  using fls_eq_iff Abs_fls_partially_pinverse_rep_nth[of f]
        fls_partially_pinverse_rep_eq_zero_iff[of f N]
  by    fastforce

lemma Abs_fls_partially_pinverse_rep_subdegree:
  "fls_subdegree (Abs_fls (fls_partially_pinverse_rep f N p)) = 0" if "f ¬≃⇩p 0"
  for f :: "'a fls"
  using that fls_partially_pinverse_rep_nzero_at_0 fls_partially_pinverse_rep_func_lower_bound'
        Abs_fls_partially_pinverse_rep_nth fls_subdegree_eqI
  by    metis

lemma fls_shift_pinv_rep_subdegree:
  "fls_subdegree (fls_shift m (Abs_fls (fls_partially_pinverse_rep f N p))) = -m"
  if  "f ¬≃⇩p 0"
  for f :: "'a fls"
  using that Abs_fls_partially_pinverse_rep_nzero Abs_fls_partially_pinverse_rep_subdegree
  by    fastforce

lemma fls_partially_pinverse_rep_cong:
  "fls_partially_pinverse_rep f N p (n - K) = fls_partially_pinverse_rep g N p (n - K)"
  if "f°⇧p = K" and "g°⇧p = K" and "∀k≤n. f $$ k = g $$ k"
  for f g :: "'a fls"
proof-
  have equiv0_case:
    "⋀f g :: 'a fls.
      f ≃⇩p 0 ⟹ g°⇧p = 0 ⟹
        ∀k≤n. f $$ k = g $$ k ⟹
        fls_partially_pinverse_rep f N p n = fls_partially_pinverse_rep g N p n"
  proof-
    fix f g :: "'a fls"
    assume  f: "f ≃⇩p 0" and g: "g°⇧p = 0"
      and   fg: "∀k≤n. f $$ k = g $$ k"
    show "fls_partially_pinverse_rep f N p n = fls_partially_pinverse_rep g N p n"
    proof (cases "g ≃⇩p 0", metis f fls_partially_pinverse_rep_eq_zero)
      case False
      have "∀k≤n. fls_partially_pinverse_rep g N p k = 0"
      proof (induct N)
        case 0 with f g fg show ?case using fls_pmod_nth_cong[of 0 g f] by auto
      next
        case (Suc N) show ?case
        proof clarify
          fix k assume k: "k ≤ n" show "fls_partially_pinverse_rep g (Suc N) p k = 0"
          proof (cases "k = int (Suc N)")
            case False with k Suc show ?thesis by force
          next
            case True
            moreover define G where "G ≡ Abs_fls (fls_partially_pinverse_rep g N p)"
            moreover have "((G * (g pmod p)) pmod p) $$ int (Suc N) = (0 pmod p) $$ int (Suc N)"
            proof (rule fls_pmod_nth_cong, clarify)
              fix j assume "j ≤ int (Suc N)"
              with f g fg G_def True False k show "(G * (g pmod p)) $$ j = 0 $$ j"
                using fls_times_nth(1)[of G] fls_pmod_subdegree[of g p]
                      Abs_fls_partially_pinverse_rep_subdegree[of g] fls_pmod_nth_cong[of _ g f]
                      p_modulo_fls_eq0[of p f]
                by    auto
            qed
            ultimately show "fls_partially_pinverse_rep g (Suc N) p k = 0" using g by simp
          qed
        qed
      qed
      with f show ?thesis using fls_partially_pinverse_rep_eq_zero by fastforce
    qed
  qed
  consider
    "f ≃⇩p 0" |
    "g ≃⇩p 0" |
    (nonzero) "f ¬≃⇩p 0" "g ¬≃⇩p 0"
    by blast
  thus ?thesis
    using that equiv0_case
  proof cases
    case nonzero
    from that have base:
      "n ≥ K ⟹
        (((f pmod p) $$ K)¯⇧p) = (((g pmod p) $$ K)¯⇧p)"
      using fls_pmod_nth_cong[of K f g] by simp
    have
      "∀k≤n.
        fls_partially_pinverse_rep f N p (k - K) = fls_partially_pinverse_rep g N p (k - K)"
    proof (induct N, simp add: that(1,2), safe, rule base, simp)
      case (Suc N)
      fix k assume k: "k ≤ n"
      show
        "fls_partially_pinverse_rep f (Suc N) p (k - K) =
          fls_partially_pinverse_rep g (Suc N) p (k - K)"
      proof (cases "k = int (Suc N) + K")
        case False with Suc k show ?thesis by fastforce (* simp works *)
      next
        case True
        with k have K: "n ≥ K" by linarith
        define A :: "'a fls ⇒ 'a fls"
          where "A ≡ (λf. Abs_fls (fls_partially_pinverse_rep f N p))"
        have
          "((fls_shift K (A f) * (f pmod p)) pmod p) $$ (int (Suc N)) =
            ((fls_shift K (A g) * (g pmod p)) pmod p) $$ (int (Suc N))"
        proof (rule fls_pmod_nth_cong, clarify)
          fix j assume j: "j ≤ int (Suc N)"
          with k True have "∀i∈{0..j}. i + K ≤ n" by simp
          with Suc A_def have "∀i∈{0..j}. A f $$ i = A g $$ i"
            using Abs_fls_partially_pinverse_rep_nth[of _ N p] by fastforce
          moreover from that(3) True j k have
            "∀i∈{0..j}. (f pmod p) $$ (K + j - i) = (g pmod p) $$ (K + j - i)"
            using fls_pmod_nth_cong[of "K + j - _" f g p] by simp
          ultimately show
            "(fls_shift K (A f) * (f pmod p)) $$ j = (fls_shift K (A g) * (g pmod p)) $$ j"
            using that(1,2) nonzero A_def fls_shift_pinv_rep_subdegree fls_pmod_subdegree[of _ p]
                  fls_times_nth(1)[of "fls_shift K (A _)"]
            by    auto
        qed
        with that(1,2) True A_def show
          "fls_partially_pinverse_rep f (Suc N) p (k - K) =
            fls_partially_pinverse_rep g (Suc N) p (k - K)"
          using base K by simp
      qed
    qed
    thus ?thesis by auto
  qed (simp_all add: p_depth_fls.depth_equiv_0)
qed

lemma fls_pinv_rep_times_f_subdegree:
  "fls_subdegree (
    fls_shift (f°⇧p) (Abs_fls (fls_partially_pinverse_rep f N p)) *
    (f pmod p)
  ) = 0"
  if  "f ¬≃⇩p 0"
  for f :: "'a fls"
proof-
  from that
    have  "f pmod p ≠ 0" and "Abs_fls (fls_partially_pinverse_rep f N p) ≠ 0"
    using fls_pmod_eq0_iff Abs_fls_partially_pinverse_rep_nzero by (blast, blast)
  with that show ?thesis
    using fls_shift_pinv_rep_subdegree fls_pmod_subdegree
          fls_shift_eq0_iff[of "(f°⇧p)"]
    by    fastforce
qed

lemma Abs_fls_pinv_rep_Suc:
  fixes f :: "'a fls" and N :: nat
  defines
    "c ≡
      -(
          (
            (
              fls_shift (f°⇧p) (Abs_fls (fls_partially_pinverse_rep f N p)) *
              (f pmod p)
            ) pmod p
          ) $$ (int (Suc N)) * (((f pmod p) $$ (f°⇧p))¯⇧p)
      ) pmod p"
  assumes f: "f ¬≃⇩p 0"
  shows
    "Abs_fls (fls_partially_pinverse_rep f (Suc N) p) =
      Abs_fls (fls_partially_pinverse_rep f N p) + fls_shift (- int (Suc N)) (fls_const c)"
proof (intro fls_eqI)
  define Abs_inv_rep and s
    where "Abs_inv_rep ≡ (λN. Abs_fls (fls_partially_pinverse_rep f N p))"
    and   "s ≡ fls_shift (- int (Suc N)) (fls_const c)"
  fix n show "Abs_inv_rep (Suc N) $$ n = (Abs_inv_rep N + s) $$ n"
  proof-
    consider (zero) "n = 0" | (SucN) "n = Suc N" | (neither) "n ≠ 0" "n ≠ Suc N"
      by blast
    thus ?thesis
    proof cases
      case zero
      moreover from this Abs_inv_rep_def have
        "Abs_inv_rep (Suc N) $$ n = (((f pmod p) $$ (f°⇧p))¯⇧p)"
        by (metis Abs_fls_partially_pinverse_rep_nth fls_partially_pinverse_rep_at_0)
      ultimately show ?thesis
        using Abs_inv_rep_def s_def Abs_fls_partially_pinverse_rep_nth[of f N]
              fls_partially_pinverse_rep_at_0[of f N]
        by    force
    next
      case SucN with Abs_inv_rep_def s_def c_def show ?thesis
        using Abs_fls_partially_pinverse_rep_nth[of f N]
              Abs_fls_partially_pinverse_rep_nth[of f "Suc N"]
              fls_partially_pinverse_rep_func_truncates[of N n]
        by    fastforce
    next
      case neither with Abs_inv_rep_def s_def show ?thesis
        using Abs_fls_partially_pinverse_rep_nth[of f N]
              Abs_fls_partially_pinverse_rep_nth[of f "Suc N"]
        by    fastforce
    qed
  qed
qed

lemma fls_pinv_rep_times_f_nth:
  "((
    fls_shift (f°⇧p) (Abs_fls (fls_partially_pinverse_rep f N p)) *
    (f pmod p)
  ) pmod p) $$ n = 0"
  if  f: "f ¬≃⇩p 0" and n: "n ≥ 1" "n ≤ int N"
  for f :: "'a fls" and n :: int
proof-
  define pp where "pp ≡ Rep_prime p"
  define Abs_inv_rep
    where "Abs_inv_rep ≡ (λN. Abs_fls (fls_partially_pinverse_rep f N p))"
  define g where
    "g ≡ (λN. fls_shift (f°⇧p) (Abs_inv_rep N) * (f pmod p))"
  from f g_def Abs_inv_rep_def have dg: "∀N. fls_subdegree (g N) = 0"
    using fls_pinv_rep_times_f_subdegree by presburger
  have "∀k∈{1..int N}. (g N pmod p) $$ k = 0"
  proof (induct N)
    case (Suc N)
    define c where
      "c ≡ -(
        ((g N) pmod p) $$ (int (Suc N)) * (((f pmod p) $$ (f°⇧p))¯⇧p)
      ) pmod p"
    define s where "s ≡ fls_shift ((f°⇧p) - int (Suc N)) (fls_const c)"
    from that s_def c_def g_def Abs_inv_rep_def
      have  g_SucN_decomp: "g (Suc N) = g N + s * (f pmod p)"
      using Abs_fls_pinv_rep_Suc[of f N]
      by    (simp add: algebra_simps)
    from pp_def have fpmod_base:
      "(f pmod p) $$ (f°⇧p) pmod p = (f pmod p) $$ (f°⇧p)"
      using fls_pmod_reduced[of f p "f°⇧p"]
            div_mult_mod_eq[of "(f pmod p) $$ (f°⇧p)" pp]
      by    simp
    show ?case
    proof (cases "c = 0", safe)
      case True fix k assume k: "k ∈ {1..int (Suc N)}"
      from f pp_def True c_def have
        "(((g N) pmod p) $$ (int (Suc N))) pmod p = 0"
        using fpmod_base pinverse_scalar_fls_pmod_base[of f]
              mod_mult_right_eq[of
                "-((g N) pmod p) $$ (int (Suc N))"
                "((((f pmod p) $$ (f°⇧p))¯⇧p) *
                  (f pmod p) $$ (f°⇧p))"
                pp
              ]
        by    (auto simp add: algebra_simps)
      with pp_def have "((g N) pmod p) $$ (int (Suc N)) = 0"
        using fls_pmod_reduced div_mult_mod_eq[of "((g N) pmod p) $$ (int (Suc N))" pp] by simp
      moreover have "{1..int (Suc N)} = insert (int (Suc N)) {1..int N}" by force
      ultimately show "(g (Suc N) pmod p) $$ k = 0" using k Suc s_def True g_SucN_decomp by auto
    next
      case False fix k assume k: "k ∈ {1..int (Suc N)}"
      from False s_def have s_n0: "s ≠ 0" using fls_shift_eq0_iff[of _ "fls_const c"] by auto
      moreover from False s_def
        have  ds: "fls_subdegree s = - ((f°⇧p) - int (Suc N))"
        by    simp
      ultimately have d_s_fpmod: "fls_subdegree (s * (f pmod p)) = int (Suc N)"
        using f fls_pmod_eq0_iff[of f p] fls_pmod_subdegree[of f p]
              fls_subdegree_mult[of s "f pmod p"]
        by    auto
      show "(g (Suc N) pmod p) $$ k = 0"
      proof (cases "k = int (Suc N)")
        case True
        with pp_def s_def c_def have
          "(g (Suc N) pmod p) $$ k =
            (
              (g N pmod p) $$ (int (Suc N)) +
              (
                -(
                  ((g N) pmod p) $$ (int (Suc N)) *
                  (((f pmod p) $$ (f°⇧p))¯⇧p)
                ) pmod p
                * ((f pmod p) $$ (f°⇧p) pmod p)
              ) pmod p
            ) pmod p"
          using g_SucN_decomp dg ds d_s_fpmod fpmod_base
                fls_pmod_mismatched_add_nth(2)[of "g N" "s * (f pmod p)"]
                fls_times_base[of s "f pmod p"]
                fls_pmod_subdegree[of f p]
                mod_add_right_eq[of "(g N pmod p) $$ (int (Suc N))" _ pp]
          by    simp
        with f pp_def show ?thesis
          using pinverse_scalar_fls_pmod_base[of f]
                mod_mult_right_eq[of
                  "- ((g N) pmod p) $$ (int (Suc N))"
                  "(((f pmod p) $$ (f°⇧p))¯⇧p) *
                    ((f pmod p) $$ (f°⇧p))"
                  pp
                ]
                mod_add_right_eq[of
                  "(g N pmod p) $$ (int (Suc N))" "- ((g N) pmod p) $$ (int (Suc N))" pp
                ]
          by    (simp add: mod_mult_eq algebra_simps)
      next
        case False
        with Suc k show ?thesis
          using g_SucN_decomp dg d_s_fpmod by (simp add: fls_pmod_mismatched_add_nth(1))
      qed
    qed
  qed simp
  with n g_def Abs_inv_rep_def show ?thesis by presburger
qed

end (* context *)

subsubsection ‹Full inversion of formal Laurent series›

text ‹
  Now we collect the terms of the infinite sequence of partial inversion polynomials
  into a formal Laurent series,
  shifted to the opposite depth as the original.
›

overloading pinverse_fls ≡ "pinverse :: 'a fls ⇒ 'a prime ⇒ 'a fls"
begin
definition pinverse_fls ::
  "'a::nontrivial_factorial_unique_euclidean_bezout fls ⇒ 'a prime ⇒ 'a fls"
  where
    "pinverse_fls f p ≡
      (if f ≃⇩p 0 then 0 else
        fls_shift (f°⇧p)
          (Abs_fls (λn. fls_partially_pinverse_rep f (nat n) p n)))"
end

context
  fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
begin

lemma pinverse_fls_nth:
  "(f¯⇧p) $$ n =
    fls_partially_pinverse_rep f (nat (n + (f°⇧p))) p (n + (f°⇧p))"
  if "f ¬≃⇩p 0"
  using     that nth_Abs_fls_lower_bound[OF fls_partially_pinverse_rep_func_lower_bound]
  unfolding pinverse_fls_def
  by        auto

lemma pinverse_fls_nth':
  "int N ≥ n + (f°⇧p) ⟹
    (f¯⇧p) $$ n = fls_partially_pinverse_rep f N p (n + (f°⇧p))"
  if "f ¬≃⇩p 0"
proof (induct N)
  case 0 with that show ?case by (simp add: pinverse_fls_nth)
next
  case (Suc N) with that show ?case using nat_int[of "Suc N"]
    by (cases "n + (f°⇧p) = int (Suc N)") (auto simp add: pinverse_fls_nth)
qed

lemma pinverse_fls_eq0[simp]:
  "(f¯⇧p) = 0" if "f ≃⇩p 0" for f :: "'a fls"
  using that unfolding pinverse_fls_def by auto

lemma fls_pinv_eq0_iff:
  "(f¯⇧p) = 0 ⟷ f ≃⇩p 0" for f :: "'a fls"
  using pinverse_scalar_fls_pmod_base pinverse_fls_nth[of f "-(f°⇧p)"] by fastforce

lemma fls_pinv_subdegree:
  "fls_subdegree (f¯⇧p) = -(f°⇧p)" for f :: "'a fls"
  using fls_partially_pinverse_rep_nzero_at_0[of p f 0] fls_partially_pinverse_rep_func_lower_bound
  by    (cases "f ≃⇩p 0")
        (simp, fastforce intro: fls_subdegree_eqI simp add: pinverse_fls_nth)

lemma fls_pinv_reduced[simp]: "((f¯⇧p) $$ n) pdiv p = 0"
proof (cases "f ≃⇩p 0")
  case False show ?thesis
  proof (cases n "fls_subdegree (f¯⇧p)" rule: linorder_cases)
    case greater
    hence "n + (f°⇧p) - 1 ≥ 0" using fls_pinv_subdegree[of f] by force
    hence "nat (n + (f°⇧p)) = Suc (nat (n + (f°⇧p) - 1))" by linarith
    with False show ?thesis by (fastforce simp add: pinverse_fls_nth)
  qed (simp, fastforce simp add: False pinverse_fls_nth fls_pinv_subdegree pinverse_scalar_reduced)
qed simp

lemma pinverse_times_p_modulo_fls:
  "( (f¯⇧p) * (f pmod p) ) pmod p = 1" if "f ¬≃⇩p 0"
  for f :: "'a fls"
proof (intro fls_eq_above_subdegreeI, safe)
  define f_0 where "f_0 ≡ (f pmod p) $$ (f°⇧p)"
  from that have d_prod: "fls_subdegree ((f¯⇧p) * (f pmod p)) = 0"
    using fls_pmod_eq0_iff[of f] fls_pinv_eq0_iff[of f]
    by    (auto simp add: fls_pmod_subdegree fls_pinv_subdegree)
  with that have base: "((f¯⇧p) * (f pmod p) pmod p) $$ 0 = 1"
    using pinverse_scalar_fls_pmod_base fls_times_base[of "f¯⇧p" "f pmod p"]
    by    (auto simp add: p_modulo_fls_nth pinverse_fls_nth fls_pmod_subdegree fls_pinv_subdegree)
  hence "((f¯⇧p) * (f pmod p)) ¬≃⇩p 0" by fastforce
  thus "0 ≤ fls_subdegree ((f¯⇧p) * (f pmod p) pmod p)"
    using d_prod fls_pmod_subdegree_ge by metis
  fix k::int assume k: "k ≥ 0"
  show "((f¯⇧p) * (f pmod p) pmod p) $$ k = 1 $$ k"
  proof (cases "k = 0")
    case False
    define s where
      "s ≡
        fls_shift (f°⇧p) (Abs_fls (fls_partially_pinverse_rep f (nat k) p))"
    from that s_def have "fls_subdegree s = -(f°⇧p)"
      using Abs_fls_partially_pinverse_rep_nzero Abs_fls_partially_pinverse_rep_subdegree
      by    fastforce
    with that s_def
      have  "((f¯⇧p) * (f pmod p) pmod p) $$ k = (s * (f pmod p) pmod p) $$ k"
      using fls_times_nth(1)[of "f¯⇧p"] fls_times_nth(1)[of s]
            pinverse_fls_nth'[of f _ "nat k"] Abs_fls_partially_pinverse_rep_nth[of f]
      by    (auto intro: fls_pmod_nth_cong simp add: fls_pmod_subdegree fls_pinv_subdegree)
    with that k False s_def show ?thesis using fls_pinv_rep_times_f_nth by fastforce
  qed (simp add: base)
qed simp

lemma pinverse_fls:
  "((f¯⇧p) * f) pmod p = 1" if "f ¬≃⇩p 0" for f :: "'a fls"
  using that pinverse_times_p_modulo_fls fls_pmod_equiv[of p f]
        fls_pmod_equiv_times[of p "f¯⇧p" "f¯⇧p"]
  by    fastforce

lemma pinverse_fls_mult_equiv1:
  "((f¯⇧p) * f) ≃⇩p 1" if "f ¬≃⇩p 0" for f :: "'a fls"
  by (metis that pinverse_fls fls_pmod_equiv)

lemma pinverse_fls_mult_equiv1':
  "(f * (f¯⇧p)) ≃⇩p 1" if "f ¬≃⇩p 0" for f :: "'a fls"
  by (metis that pinverse_fls_mult_equiv1 mult.commute)

lemma p_modulo_pinverse_fls[simp]:
  "(f¯⇧p) pmod p = (f¯⇧p)" for f :: "'a fls"
  using fls_pmod_reduced fls_pmod_eqI by force

lemma fls_pinv_equiv0_iff:
  "(f¯⇧p) ≃⇩p 0 ⟷ f ≃⇩p 0"
  for f :: "'a fls"
proof
  assume "((f¯⇧p) ≃⇩p 0)"
  hence "(f¯⇧p) pmod p = 0" by (simp del: p_modulo_pinverse_fls)
  thus "(f ≃⇩p 0)" using fls_pinv_eq0_iff by auto
qed simp

lemma fls_pinv_depth:
  "(f¯⇧p)°⇧p = -(f°⇧p)" for f :: "'a fls"
proof (cases "f ≃⇩p 0")
  case False
  hence "(f¯⇧p)°⇧p = fls_subdegree (f¯⇧p)"
    using fls_pinv_equiv0_iff[of f] fls_pinv_reduced[of f "fls_subdegree (f¯⇧p)"]
          fls_pinv_eq0_iff[of f] nth_fls_subdegree_nonzero[of "f¯⇧p"]
          p_depth_fls_rep_iff[of p _ "f¯⇧p"]
    by    fastforce
  thus ?thesis using fls_pinv_subdegree by presburger
qed simp

lemma fls_pinv_eqI:
  "(f¯⇧p) = g" if "g * f ≃⇩p 1" and "∀n. (g $$ n) pdiv p = 0"
  for f g :: "'a fls"
proof-
  from that(1) have "f ¬≃⇩p 0"
    using p_equality_fls.mult_0_right fls_1_not_p_equal_0 p_equality_fls.trans_right by blast
  moreover from that(1)
    have  "g * ((f¯⇧p) * f) ≃⇩p (f¯⇧p)"
    using p_equality_fls.mult_one_left[of p "g * f" "f¯⇧p"]
    by    (simp add: ac_simps)
  ultimately show ?thesis
    using that(2) fls_pmod_eqI[of p _ g] p_equality_fls.mult_left pinverse_fls_mult_equiv1
          p_equality_fls.trans_right[of p _ _ g]
    by    fastforce
qed

lemma fls_pinv_cong:
  "(f¯⇧p) = (g¯⇧p)" if "f ≃⇩p g" for f :: "'a fls"
proof (cases "g ≃⇩p 0")
  case True with that show ?thesis using p_equal_fls_trans by fastforce
next
  case False
  moreover from that have "(g¯⇧p) * f ≃⇩p (g¯⇧p) * g"
    using p_equality_fls.mult_left by fast
  ultimately show ?thesis
    using pinverse_fls_mult_equiv1 p_equal_fls_trans fls_pinv_eqI fls_pinv_reduced by blast
qed

lemma pinverse_p_modulo_fls:
  "(f pmod p)¯⇧p = (f¯⇧p)" for f :: "'a fls"
  using fls_pinv_cong p_equal_fls_sym fls_pmod_equiv by blast

lemma fls_pinv_X_intpow: "(fls_X_intpow n :: 'a fls)¯⇧p = fls_X_intpow (-n)"
  by (intro fls_pinv_eqI, simp add: fls_times_both_shifted_simp, auto simp add: one_pdiv)

lemma fls_pinv_uminus: "(-f)¯⇧p = (- (f¯⇧p)) pmod p" for f :: "'a fls"
proof (cases "f ≃⇩p 0")
  case True thus ?thesis using p_equality_fls.uminus by fastforce
next
  case False
  hence "( (- (f¯⇧p)) pmod p * - f) ≃⇩p 1"
    using fls_pmod_equiv[of p "(- (f¯⇧p)) pmod p * - f"]
          fls_pmod_equiv[of p "(- (f¯⇧p))"] p_equal_fls_refl[of p "-f"]
          p_equal_fls_sym[of p "(- (f¯⇧p))" "(- (f¯⇧p)) pmod p"]
          fls_pmod_equiv_times[of p _ "(- (f¯⇧p))"] pinverse_fls
    by    fastforce
  thus ?thesis using fls_pinv_eqI fls_pmod_reduced by blast
qed

end (* context nontrivial_factorial_unique_euclidean_bezout *)

subsubsection ‹Algebraic properties of inversion›

context
  fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
begin

lemma fls_pinv0: "(0 :: 'a fls)¯⇧p = 0"
  by simp

lemma fls_pinv1[simp]: "(1 :: 'a fls)¯⇧p = 1"
  by (intro fls_pinv_eqI, simp_all, rule one_pdiv)

lemma fls_pinv_pinv:
  "((f¯⇧p)¯⇧p) = f pmod p" for f :: "'a fls"
proof (cases "f ≃⇩p 0")
  case False thus ?thesis
    using pinverse_times_p_modulo_fls fls_pmod_equiv mult.commute fls_pmod_reduced fls_pinv_eqI
    by    metis
qed simp

lemma fls_pinv_pinv_equiv:
  "((f¯⇧p)¯⇧p) ≃⇩p f" for f :: "'a fls"
  using fls_pinv_pinv[of f] fls_pmod_equiv p_equal_fls_sym by fastforce

lemma fls_pinv_mult:
  "(f * g)¯⇧p = ((f¯⇧p) * (g¯⇧p)) pmod p"
  for f g :: "'a fls"
proof-
  have case0:
    "⋀f g :: 'a fls.
      f ≃⇩p 0 ⟹
        (f * g)¯⇧p = ((f¯⇧p) * (g¯⇧p)) pmod p"
  proof-
    fix f g :: "'a fls" assume "f ≃⇩p 0"
    thus "(f * g)¯⇧p = ((f¯⇧p) * (g¯⇧p)) pmod p"
      using p_equality_fls.mult_0_left by fastforce
  qed
  consider
    "f ≃⇩p 0" | "g ≃⇩p 0" |
    (neither) "f ¬≃⇩p 0" "g ¬≃⇩p 0"
    by blast
  thus ?thesis
  proof (cases, metis case0, metis case0 mult.commute, intro fls_pinv_eqI)
    case neither
    hence "((f¯⇧p) * f * ((g¯⇧p) * g)) ≃⇩p 1"
      using p_equality_fls.mult pinverse_fls_mult_equiv1
      by    fastforce
    moreover have
      "(((f¯⇧p) * (g¯⇧p)) pmod p * (f * g)) ≃⇩p
        ((f¯⇧p) * f * ((g¯⇧p) * g))"
      using fls_pmod_equiv p_equal_fls_sym p_equality_fls.mult_right[of p _ _ "f * g"]
      by    (fastforce simp add: algebra_simps)
    ultimately
      show "((f¯⇧p) * (g¯⇧p) pmod p * (f * g)) ≃⇩p 1"
      using p_equal_fls_trans
      by    blast
    show "∀n. ((f¯⇧p) * (g¯⇧p) pmod p) $$ n pdiv p = 0"
      using fls_pmod_reduced by fast
  qed
qed

lemma fls_pinv_mult_equiv:
  "((f * g)¯⇧p) ≃⇩p (f¯⇧p) * (g¯⇧p)"
  for f g :: "'a fls"
  by (metis fls_pinv_mult fls_pmod_equiv p_equal_fls_sym)

lemma fls_pinv_pow:
  "(f ^ n)¯⇧p = ((f¯⇧p) ^ n) pmod p"
  for f g :: "'a fls"
proof (induct n)
  case (Suc n) thus ?case
    using fls_pinv_mult fls_pmod_equiv[of p "(f¯⇧p) ^ n"]
          fls_pmod_equiv_times[of p "f¯⇧p" "f¯⇧p"]
    by    simp
qed simp

lemma fls_pinv_pow_equiv:
  "((f ^ n)¯⇧p) ≃⇩p (f¯⇧p) ^ n" for f :: "'a fls"
  by (metis fls_pinv_pow fls_pmod_equiv p_equal_fls_sym)

lemma fls_pinv_diff_cancel_lead_coeff:
  "(((f¯⇧p) - (g¯⇧p))°⇧p) > -n"
  if  f : "f ¬≃⇩p 0" "f°⇧p = n"
  and g : "g ¬≃⇩p 0" "g°⇧p = n"
  and fg: "f ¬≃⇩p g" "((f - g)°⇧p) > n"
  for f g :: "'a fls"
proof-
  from fg(1)
    have  inv_diff_n0: "((f¯⇧p) - (g¯⇧p)) ¬≃⇩p 0"
    by    (metis p_equality_fls.conv_0 fls_pinv_cong fls_pinv_pinv fls_pmod_eq_pmod_iff)
  moreover have "fls_subdegree ((f¯⇧p) - (g¯⇧p)) > -n"
  proof (rule fls_subdegree_greaterI)
    show "(f¯⇧p) - (g¯⇧p) ≠ 0" using inv_diff_n0 by fastforce
    fix k :: int
    from fg(2) have fg': "((f pmod p - g pmod p)°⇧p) > n"
      using fls_pmod_depth fls_pmod_equiv fls_pmod_equiv_minus[of p f "f pmod p" g "g pmod p"]
      by    metis
    hence "fls_subdegree ((f pmod p - g pmod p) pmod p) > n" by (metis fls_pmod_subdegree)
    hence "((f pmod p - g pmod p) pmod p) $$ n = 0" by simp
    moreover have
      "((f pmod p - g pmod p) pmod p) $$ n =
        fls_partially_p_modulo_rep
          (f pmod p - g pmod p) (nat (n + 1 - fls_subdegree (f pmod p - g pmod p))) p n"
      using p_modulo_fls_nth[of "f pmod p - g pmod p" p n] by fastforce
    moreover from f(2) g(2) fg' have "fls_subdegree (f pmod p - g pmod p) ≥ n"
      using fls_subdegree_minus[of "f pmod p" "g pmod p"]
            fls_pmod_subdegree[of f p] fls_pmod_subdegree[of g p]
      by    force
    ultimately have "((f pmod p) $$ n) pmod p = ((g pmod p) $$ n) pmod p"
      using mod_eq_dvd_iff by (cases "fls_subdegree (f pmod p - g pmod p) = n", force, simp)
    hence "(f pmod p) $$ n = (g pmod p) $$ n" using fls_pmod_pmod_nth by metis
    moreover from f(2) g(2)
      have  "k < -n ⟹ ((f¯⇧p) - (g¯⇧p)) $$ k = 0"
      by    (simp add: fls_pinv_subdegree)
    ultimately
      show  "k ≤ -n ⟹ ((f¯⇧p) - (g¯⇧p)) $$ k = 0"
      using f g
      by    (cases "k = -n", simp add: pinverse_fls_nth, simp)
  qed
  ultimately show ?thesis using p_depth_fls_ge_p_equal_subdegree' by fastforce
qed

end (* context *)


subsection ‹Topology by place relative to indexed depth for formal Laurent series›

subsubsection ‹General pattern for constructing sequence limits›

definition fls_condition_lim ::
  "'a::nontrivial_euclidean_ring_cancel prime ⇒ (nat ⇒ 'a fls) ⇒
    (nat ⇒ nat ⇒ bool) ⇒ 'a fls"
  where
    "fls_condition_lim p F P =
      Abs_fls (λn. (F (LEAST K. P (nat n) K) pmod p) $$ n)"

lemma fls_condition_lim_fun_ex_lower_bound:
  fixes p :: "'a::nontrivial_euclidean_ring_cancel prime"
    and F :: "nat ⇒ 'a fls"
    and P :: "int ⇒ nat ⇒ bool"
  defines
    "f ≡ (λn. (F (LEAST K. P (nat n) K) pmod p) $$ n)"
  and
    "N ≡ min 0 (fls_subdegree ((F (LEAST K. P 0 K)) pmod p))"
  shows "∀n<N. f n = 0"
  using assms by simp

lemma fls_condition_lim_nth:
  "fls_condition_lim p F P $$ n = ((F (LEAST K. P (nat n) K)) pmod p) $$ n"
  using nth_Abs_fls_lower_bound[OF fls_condition_lim_fun_ex_lower_bound, of F]
        fls_condition_lim_def[of p F]
  by    auto

lemma fls_pmod_condition_lim: "(fls_condition_lim p F P) pmod p = fls_condition_lim p F P"
  by (intro fls_pmod_eqI, simp_all add: fls_condition_lim_nth)


subsubsection ‹Completeness›

abbreviation "fls_p_limseq_condition      ≡ p_depth_fls.p_limseq_condition"
abbreviation "fls_p_limseq                ≡ p_depth_fls.p_limseq"
abbreviation "fls_p_cauchy_condition      ≡ p_depth_fls.p_cauchy_condition"
abbreviation "fls_p_cauchy                ≡ p_depth_fls.p_cauchy"

lemma fls_p_cauchy_condition_pmod_uniformity:
  "((F k) pmod p) $$ m = ((F k') pmod p) $$ m"
  if "fls_p_cauchy_condition p F n K" and "k ≥ K" and "k' ≥ K" and "m ≤ n"
  for p :: "'a::nontrivial_euclidean_ring_cancel prime" and F :: "nat ⇒ 'a fls"
  using that fls_pmod_cong[of p] fls_pmod_diff_cancel[of m p "F k" "F k'"]
        p_depth_fls.p_cauchy_conditionD
  by    fastforce

abbreviation
  "fls_p_cauchy_lim p X ≡
    fls_condition_lim p X (λn. fls_p_cauchy_condition p X (int n))"

lemma fls_p_cauchy_limseq: "fls_p_limseq p F (fls_p_cauchy_lim p F)" if "fls_p_cauchy p F"
proof
  fix n
  define K where "K ≡ (λn. LEAST K. fls_p_cauchy_condition p F (int (nat n)) K)"
  have "fls_p_limseq_condition p F (fls_p_cauchy_lim p F) n (K n)"
  proof
    fix k assume k: "k ≥ K n" "F k ¬≃⇩p (fls_p_cauchy_lim p F)"
    have "fls_subdegree ((F k pmod p) - fls_p_cauchy_lim p F) > n"
    proof (intro fls_subdegree_greaterI)
      from k(2) show "(F k) pmod p - (fls_p_cauchy_lim p F) ≠ 0"
        using fls_p_modulo_iff by auto
      fix j assume j: "j ≤ n"
      have "((F (K j)) pmod p) $$ j = ((F k) pmod p) $$ j"
      proof (intro fls_p_cauchy_condition_pmod_uniformity)
        from that K_def show "fls_p_cauchy_condition p F (int (nat j)) (K j)"
          using p_depth_fls.p_cauchy_condition_LEAST[of p F] by blast
        from j consider "j < 0" "n < 0" | "j < 0" "n ≥ 0" | "j ≥ 0" "n ≥ 0"
          by linarith
        thus "k ≥ K j"
          using that K_def k(1) j p_depth_fls.p_cauchy_condition_LEAST_mono
          by    cases (auto, fastforce, fastforce)
      qed simp_all
      with K_def have "(F k pmod p) $$ j = fls_p_cauchy_lim p F $$ j"
        by (metis fls_condition_lim_nth)
      thus "(F k pmod p - fls_p_cauchy_lim p F) $$ j = 0" by simp
    qed
    moreover from k(2) have
      "((F k - fls_p_cauchy_lim p F)°⇧p) ≥
        fls_subdegree ((F k pmod p) - fls_p_cauchy_lim p F)"
      using p_equality_fls.conv_0[of p] p_equality_fls.minus[of p] fls_pmod_equiv[of p]
      by    (auto intro: p_depth_fls_ge_p_equal_subdegree)
    ultimately show "((F k - fls_p_cauchy_lim p F)°⇧p) > n" by force
  qed
  thus "∃K. fls_p_limseq_condition p F (fls_p_cauchy_lim p F) n K" by blast
qed

lemma fls_p_cauchy_lim_unique:
  "fls_p_cauchy_lim p F = fls_p_cauchy_lim p G"
  if "fls_p_cauchy p G" and "∀n≥N. (F n) ≃⇩p (G n)"
proof-
  have "fls_p_cauchy p F"
  proof
    fix n
    from that(1) obtain M where M: "fls_p_cauchy_condition p G n M" by force
    define K where "K ≡ max M N"
    have "fls_p_cauchy_condition p F n K"
    proof (intro p_depth_fls.p_cauchy_conditionI)
      fix k k' assume kk': "k ≥ K" "k' ≥ K" "(F k) ¬≃⇩p (F k')"
      moreover from that(2) K_def kk'(1,2)
        have  F_kk': "(F k) ≃⇩p (G k)" "(F k') ≃⇩p (G k')"
        by    auto
      ultimately have "k ≥ M" and "k' ≥ M" and "(G k) ¬≃⇩p (G k')"
        using K_def p_equality_fls.sym p_equality_fls.cong by (fastforce, fastforce, metis)
      with M show "((F k - F k')°⇧p) > n"
        using F_kk' p_depth_fls.p_cauchy_conditionD[of p G n M k k'] p_depth_fls.depth_diff_equiv
        by    metis
    qed
    thus "∃K. fls_p_cauchy_condition p F n K" by blast
  qed
  moreover from that have "fls_p_limseq p F (fls_p_cauchy_lim p G)"
    using fls_p_cauchy_limseq[of p G]
          p_depth_fls.p_limseq_p_cong[of N p F G "fls_p_cauchy_lim p G" "fls_p_cauchy_lim p G"]
    by    auto
  ultimately show ?thesis
    by (metis fls_p_cauchy_limseq p_depth_fls.p_limseq_unique fls_pmod_cong fls_pmod_condition_lim)
qed


subsection ‹Transfer to prime-indexed sequences of formal Laurent series›

subsubsection ‹Equivalence and depth›

text ‹
The equivalence is by divisibility of the difference of each pair of corresponding
terms by the index for those terms.
›

type_synonym 'a fls_pseq = "'a prime ⇒ 'a fls"

overloading
  p_equal_fls_pseq ≡
    "p_equal :: 'a::nontrivial_factorial_semiring prime ⇒
      'a fls_pseq ⇒ 'a fls_pseq ⇒ bool"
  p_restrict_fls_pseq ≡
    "p_restrict ::
      'a fls_pseq ⇒ ('a prime ⇒ bool) ⇒ 'a fls_pseq"
  p_depth_fls_pseq ≡
    "p_depth :: 'a prime ⇒ 'a fls_pseq ⇒ int"
  global_unfrmzr_pows_fls_pseq ≡
    "global_unfrmzr_pows :: ('a prime ⇒ int) ⇒ 'a fls_pseq"
begin

definition p_equal_fls_pseq ::
  "'a::nontrivial_factorial_semiring prime ⇒
    'a fls_pseq ⇒ 'a fls_pseq ⇒ bool"
  where p_equal_fls_pseq_def[simp]: "p_equal_fls_pseq p X Y ≡ (X p) ≃⇩p (Y p)"

definition p_restrict_fls_pseq ::
  "'a::nontrivial_factorial_semiring fls_pseq ⇒
    ('a prime ⇒ bool) ⇒ 'a fls_pseq"
  where
    "p_restrict_fls_pseq X P ≡ (λp::'a prime. if P p then X p else 0)"

definition p_depth_fls_pseq ::
  "'a::nontrivial_factorial_semiring prime ⇒ 'a fls_pseq ⇒ int"
  where p_depth_fls_pseq_def[simp]: "p_depth_fls_pseq p X ≡ (X p)°⇧p"

definition global_unfrmzr_pows_fls_pseq ::
  "('a::nontrivial_factorial_semiring prime ⇒ int) ⇒ 'a fls_pseq"
  where "global_unfrmzr_pows_fls_pseq f ≡ (λp::'a prime. fls_X_intpow (f p))"

end  (* overloading *)

global_interpretation p_equality_depth_fls_pseq:
  global_p_equality_depth_no_zero_divisors_1
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a fls_pseq ⇒ 'a fls_pseq ⇒ bool"
    "p_restrict ::
      'a fls_pseq ⇒ ('a prime ⇒ bool) ⇒ 'a fls_pseq"
    "p_depth :: 'a prime ⇒ 'a fls_pseq ⇒ int"
proof
(* 
 (
  unfold_locales,
  simp_all add:
    p_equality_fls.mult_0_right p_depth_fls.no_zero_divisors p_restrict_fls_pseq_def
    p_depth_fls.depth_equiv p_depth_fls.depth_uminus p_depth_fls.depth_pre_nonarch(1)
    p_depth_fls.depth_mult_additive zero_fun_def
)
 *)
  fix p :: "'a prime"
  define
    E :: "'a fls_pseq ⇒ 'a fls_pseq ⇒ bool"
    where "E ≡ p_equal p"
  thus "equivp E"
    using     equivp_transfer p_equality_fls.equivp
    unfolding p_equal_fls_pseq_def
    by        fast

  fix X Y :: "'a fls_pseq"
  show "(X ≃⇩p Y) = ((X - Y) ≃⇩p 0)" using p_equality_fls.conv_0 by auto
  have "(λq::'a prime. (1::'a fls)) ¬≃⇩p 0"
    by (auto simp add: fls_1_not_p_equal_0)
  thus "∃X::'a fls_pseq. X ¬≃⇩p 0" by auto

  show
    "⟦
        X ¬≃⇩p 0; X + Y ¬≃⇩p 0;
        (X°⇧p) = (Y°⇧p)
    ⟧ ⟹ (X°⇧p) ≤ ((X + Y)°⇧p)"
    using p_depth_fls.depth_pre_nonarch(2) by fastforce

qed (
  simp_all add:
    p_equality_fls.mult_0_right p_depth_fls.no_zero_divisors p_restrict_fls_pseq_def
    p_depth_fls.depth_equiv p_depth_fls.depth_uminus p_depth_fls.depth_pre_nonarch(1)
    p_depth_fls.depth_mult_additive
)

overloading
  globally_p_equal_fls_pseq ≡
    "globally_p_equal :: 'a::nontrivial_factorial_idom fls_pseq ⇒
      'a fls_pseq ⇒ bool"
  p_depth_set_fls_pseq ≡
    "p_depth_set ::
      'a::nontrivial_factorial_idom prime ⇒ int ⇒ 'a fls_pseq set"
  global_depth_set_fls_pseq ≡
    "global_depth_set :: int ⇒ 'a fls_pseq set"
begin

definition globally_p_equal_fls_pseq ::
  "'a::nontrivial_factorial_idom fls_pseq ⇒ 'a fls_pseq ⇒ bool"
  where globally_p_equal_fls_pseq_def[simp]:
    "globally_p_equal_fls_pseq = p_equality_depth_fls_pseq.globally_p_equal"

definition p_depth_set_fls_pseq ::
  "'a::nontrivial_factorial_idom prime ⇒ int ⇒ 'a fls_pseq set"
  where p_depth_set_fls_pseq_def[simp]:
    "p_depth_set_fls_pseq = p_equality_depth_fls_pseq.p_depth_set"

definition global_depth_set_fls_pseq ::
  "int ⇒ 'a::nontrivial_factorial_idom fls_pseq set"
  where global_depth_set_fls_pseq_def[simp]:
    "global_depth_set_fls_pseq = p_equality_depth_fls_pseq.global_depth_set"

end

lemma fls_pseq_globally_reduced:
  "X ≃⇩∀⇩p (λp. (X p) pmod p)"
  for X :: "'a::nontrivial_euclidean_ring_cancel fls_pseq"
  unfolding p_equal_fls_pseq_def using fls_pmod_equiv by fastforce

lemma global_unfrmzr_pows0_fls_pseq:
  "(𝔭 (0 :: 'a::nontrivial_factorial_idom prime ⇒ int) :: 'a fls_pseq) = 1"
  unfolding global_unfrmzr_pows_fls_pseq_def by auto

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma global_unfrmzr_pows_fls_pseq_nequiv0:
  "(𝔭 f :: 'a fls_pseq) ¬≃⇩p 0" for f :: "'a prime ⇒ int"
  by (simp add: global_unfrmzr_pows_fls_pseq_def fls_X_intpow_nequiv0)

lemma global_unfrmzr_pows_fls_pseq:
  "(𝔭 f :: 'a fls_pseq)°⇧p = f p" for f :: "'a prime ⇒ int"
  by (simp add: global_unfrmzr_pows_fls_pseq_def p_depth_fls_X_intpow)

lemma global_unfrmzr_pows_fls_pseq_pequiv_iff:
  "(𝔭 f:: 'a fls_pseq) ≃⇩p (𝔭 g) ⟷ f p = g p"
  for f g :: "'a prime ⇒ int"
  using p_equal_fls_X_intpow_iff unfolding global_unfrmzr_pows_fls_pseq_def by auto

end (* context nontrivial_factorial_idom *)

lemma global_unfrmzr_pows_prod_fls_pseq:
  "(𝔭 f :: 'a fls_pseq) * (𝔭 g) = 𝔭 (f + g)"
  for f g :: "'a::nontrivial_factorial_idom prime ⇒ int"
proof (standard)
  fix p :: "'a prime"
  define 𝔭f 𝔭g :: "'a fls_pseq"
    where "𝔭f ≡ 𝔭 f" and "𝔭g ≡ 𝔭 g"
  hence "𝔭f p * 𝔭g p = fls_shift (- f p + - g p) (1 * 1)"
    using fls_times_both_shifted_simp unfolding global_unfrmzr_pows_fls_pseq_def by metis
  thus "(𝔭f * 𝔭g) p = 𝔭 (f + g) p" unfolding global_unfrmzr_pows_fls_pseq_def by simp
qed

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma global_unfrmzr_pows_fls_pseq_nzero:
  "(𝔭 f :: 'a fls_pseq) ¬≃⇩p 0" for f :: "'a prime ⇒ int"
proof-
  define P :: "('a prime ⇒ int) ⇒ 'a fls_pseq" where "P ≡ 𝔭"
  hence *: "⋀f. P f ≃⇩p 0 ⟹ f p = 0"
    using global_unfrmzr_pows_fls_pseq p_equality_depth_fls_pseq.depth_equiv_0 by metis
  from P_def have "¬ P f ≃⇩p 0"
    using *[of f] *[of "f + (λp. 1)"] global_unfrmzr_pows_prod_fls_pseq[of f]
          p_equality_depth_fls_pseq.mult_0_left[of p _ "P (λp. 1)"]
    by    fastforce
  with P_def show ?thesis by blast
qed

lemma prod_w_global_unfrmzr_pows_fls_pseq:
  "(X * 𝔭 f)°⇧p = (X°⇧p) + f p" if "X ¬≃⇩p 0"
  for X :: "'a fls_pseq" and f :: "'a prime ⇒ int"
  using that global_unfrmzr_pows_fls_pseq_nzero p_equality_depth_fls_pseq.no_zero_divisors
        global_unfrmzr_pows_fls_pseq p_equality_depth_fls_pseq.depth_mult_additive
  by    metis

lemma normalize_depth_fls_pseq:
  "(X * 𝔭 (λp::'a prime. -(X°⇧p)))°⇧p = 0"
  for X :: "'a fls_pseq"
  using prod_w_global_unfrmzr_pows_fls_pseq p_equality_depth_fls_pseq.depth_equiv_0
        p_equality_depth_fls_pseq.mult_0_left[of p X]
  by    fastforce

end (* context nontrivial_factorial_idom *)

lemma normalized_depth_fls_pseq_product_additive:
  "(X * 𝔭 (λp::'a prime. -(X°⇧p))) *
    (Y * 𝔭 (λp::'a prime. -(Y°⇧p))) =
      ((X * Y) * 𝔭 (λp::'a prime. -((X°⇧p) + (Y°⇧p))))"
  for X Y :: "'a::nontrivial_factorial_idom fls_pseq"
  by (simp add: algebra_simps global_unfrmzr_pows_prod_fls_pseq plus_fun_def)

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma normalized_depth_fls_pseq_product_equiv:
  "(X * 𝔭 (λp::'a prime. -(X°⇧p))) *
    (Y * 𝔭 (λp::'a prime. -(Y°⇧p))) ≃⇩p
      ((X * Y) * 𝔭 (λp::'a prime. -((X * Y)°⇧p)))"
  for X Y :: "'a fls_pseq"
proof (cases "X * Y ≃⇩p 0")
  case True thus ?thesis
    using normalized_depth_fls_pseq_product_additive[of X Y]
          p_equality_depth_fls_pseq.trans_left[of p _ 0]
          p_equality_depth_fls_pseq.mult_0_left[of p]
    by    presburger
next
  case False thus ?thesis
    using global_unfrmzr_pows_fls_pseq_pequiv_iff[of p]
          p_equality_depth_fls_pseq.depth_mult_additive[of p X Y]
          normalized_depth_fls_pseq_product_additive[of X Y]
          p_equality_depth_fls_pseq.mult_left[of p _ _ "X * Y"]
    by    simp
qed

lemma trivial_global_unfrmzr_pows_fls_pseq:
  "(𝔭 f :: 'a fls_pseq) ≃⇩p 1" if "f p = 0" for f :: "'a prime ⇒ int"
  using that unfolding global_unfrmzr_pows_fls_pseq_def by auto

lemma prod_w_trivial_global_unfrmzr_pows_fls_pseq:
  "X * 𝔭 f ≃⇩p X" if "f p = 0"
  for f :: "'a prime ⇒ int" and X :: "'a fls_pseq"
  using that trivial_global_unfrmzr_pows_fls_pseq p_equality_depth_fls_pseq.mult_left by fastforce

end (* context nontrivial_factorial_idom *)

lemma pow_global_unfrmzr_pows_fls_pseq:
  "(𝔭 f :: 'a fls_pseq) ^ n = (𝔭 (λp::'a prime. int n * f p))"
  for f :: "'a::nontrivial_factorial_idom prime ⇒ int"
  by (
    induct n, simp flip: zero_fun_def one_fun_def, rule global_unfrmzr_pows0_fls_pseq,
    simp add: global_unfrmzr_pows_prod_fls_pseq plus_fun_def algebra_simps
  )

lemma global_unfrmzr_pows_fls_pseq_inv:
  "(𝔭 (-f) :: 'a fls_pseq) * (𝔭 f) = 1"
  for f :: "'a::nontrivial_factorial_idom prime ⇒ int"
  using global_unfrmzr_pows_prod_fls_pseq[of "-f" f] global_unfrmzr_pows0_fls_pseq by fastforce

lemma global_unfrmzr_pows_fls_pseq_decomp:
  "X = (
    (X * 𝔭 (λp::'a prime. -(X°⇧p))) *
    𝔭 (λp::'a prime. X°⇧p)
  )"
  for X :: "'a::nontrivial_factorial_idom fls_pseq"
proof-
  have
    "- (λp::'a prime. X°⇧p) = (λp::'a prime. -(X°⇧p))"
    by force
  thus ?thesis
    using global_unfrmzr_pows_fls_pseq_inv[of "λp::'a prime. (X°⇧p)"]
    by    (simp add: algebra_simps)
qed

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma global_unfrmzr_pth_fls_pseq:
  "(𝔭 (1 :: ('a prime ⇒ int)) p :: 'a fls) ≃⇩p
    (fls_const (Rep_prime p))"
proof (rule iffD2, rule p_equal_fls_extended_intsum_iff, safe)
  define pp where "pp ≡ Rep_prime p"
  define 𝔭1p :: "'a fls" where "𝔭1p ≡ 𝔭 (1 :: 'a prime ⇒ int) p"
  from pp_def 𝔭1p_def
    show      "0 ≤ min (fls_subdegree 𝔭1p) (fls_subdegree (fls_const pp))"
    unfolding global_unfrmzr_pows_fls_pseq_def
    by        simp
  fix n::int assume "n ≥ 0"
  moreover have
    "n ≥ 1 ⟹
      (∑k=0..n. (𝔭1p - fls_const pp) $$ k * pp ^ nat (k - 0)) = 0"
  proof (induct n rule: int_ge_induct)
    case base
    have "{0..1::int} = {0,1}" by fastforce
    thus ?case unfolding 𝔭1p_def  global_unfrmzr_pows_fls_pseq_def by fastforce
  next
    case (step n)
    moreover from step(1) have "{0..n + 1} = insert (n + 1) {0..n}" by fastforce
    ultimately show ?case unfolding 𝔭1p_def global_unfrmzr_pows_fls_pseq_def by fastforce
  qed
  ultimately show
    "pp ^ Suc (nat (n - 0)) dvd (∑k=0..n. (𝔭1p - fls_const pp) $$ k * pp ^ nat (k - 0))"
    by (
      cases "n = 0" "n = 1" rule: case_split[case_product case_split],
      simp_all add: 𝔭1p_def global_unfrmzr_pows_fls_pseq_def
    )
qed

lemma global_unfrmzr_fls_pseq:
  "(𝔭 (1 :: ('a prime ⇒ int)) :: 'a fls_pseq) ≃⇩p
    (λp::'a prime. fls_const (Rep_prime p))"
  using p_equal_fls_pseq_def global_unfrmzr_pth_fls_pseq by fast

end (* context nontrivial_factorial_idom *)

lemma normalize_depth_fls_pseqE:
  fixes   X :: "'a::nontrivial_factorial_idom fls_pseq"
  obtains X_0
  where   "∀p::'a prime. X_0°⇧p = 0"
  and     "X = X_0 * 𝔭 (λp::'a prime. X°⇧p)"
  using   normalize_depth_fls_pseq global_unfrmzr_pows_fls_pseq_decomp
  by      blast


subsubsection ‹Inversion›

abbreviation global_pinverse_fls_pseq ::
  "'a::nontrivial_factorial_comm_ring fls_pseq ⇒ 'a fls_pseq"
  ("(_¯⇧∀⇧p)" [51] 50)
  where "global_pinverse_fls_pseq X ≡ (λp. (X p)¯⇧p)"

context
  fixes X :: "'a::nontrivial_factorial_unique_euclidean_bezout fls_pseq"
begin

lemma global_pinverse_fls_pseq_eq0[simp]:
  "(X¯⇧∀⇧p) = 0" if "X ≃⇩∀⇩p 0"
  using that p_equality_depth_fls_pseq.globally_p_equalD by fastforce

lemma global_pinverse_fls_pseq_eq0_iff:
  "(X¯⇧∀⇧p) = 0 ⟷
    X ≃⇩∀⇩p 0"
proof
  assume X: "(X¯⇧∀⇧p) = 0"
  have "∀p. X p ≃⇩p 0"
  proof
    fix p :: "'a prime"
    have "¬ (X ¬≃⇩p 0)"
    proof
      assume "X ¬≃⇩p 0"
      hence "(X¯⇧∀⇧p) p ≠ 0" using fls_pinv_eq0_iff by auto
      with X show False using zero_fun_def by metis
    qed
    thus "X p ≃⇩p 0" by fastforce
  qed
  thus "X ≃⇩∀⇩p 0" by simp
qed (rule global_pinverse_fls_pseq_eq0)

lemma global_pinverse_fls_pseq_equiv0_iff:
  "(X¯⇧∀⇧p) ≃⇩∀⇩p 0 ⟷
    X ≃⇩∀⇩p 0"
  using     fls_pinv_equiv0_iff
  unfolding globally_p_equal_fls_pseq_def p_equality_depth_fls_pseq.globally_p_equal_def
  by        fastforce

lemma global_left_pinverse_fls_pseq:
  "(X¯⇧∀⇧p) * X  ≃⇩∀⇩p
    (λp. of_bool (X ¬≃⇩p 0))"
  using pinverse_fls_mult_equiv1 by fastforce

lemma global_right_pinverse_fls_pseq:
  "X * (X¯⇧∀⇧p) ≃⇩∀⇩p
    (λp. of_bool (X ¬≃⇩p 0))"
  using global_left_pinverse_fls_pseq mult.commute[of X] by presburger

lemma global_left_pinverse_fls_pseq':
  "(X¯⇧∀⇧p) * X ≃⇩p 1" if "X ¬≃⇩p 0"
  for p :: "'a prime"
  using that global_left_pinverse_fls_pseq p_equality_depth_fls_pseq.globally_p_equalD[of _ _ p]
  by    fastforce

lemma global_right_pinverse_fls_pseq':
  "X * (X¯⇧∀⇧p) ≃⇩p 1" if "X ¬≃⇩p 0"
  for p :: "'a prime"
  using that global_left_pinverse_fls_pseq' by (simp add: mult.commute)

lemma global_pinverse_pinverse_fls_pseq:
  "((X¯⇧∀⇧p)¯⇧∀⇧p)
    ≃⇩∀⇩p X"
  using fls_pinv_pinv_equiv by fastforce

lemma global_pinverse_mult_fls_pseq:
  "((X * Y)¯⇧∀⇧p) ≃⇩∀⇩p
    (X¯⇧∀⇧p) * (Y¯⇧∀⇧p)"
  using fls_pinv_mult_equiv by fastforce

lemma global_pinverse_pow_fls_pseq:
  "((X ^ n)¯⇧∀⇧p) ≃⇩∀⇩p
    (X¯⇧∀⇧p) ^ n"
  by (simp, standard, metis pow_fun_apply fls_pinv_pow_equiv)

lemma global_pinverse_uminus_fls_pseq:
  "((-X)¯⇧∀⇧p) ≃⇩∀⇩p
    - (X¯⇧∀⇧p)"
  by (simp, standard, metis fls_pinv_uminus fls_pmod_equiv p_equal_fls_sym)

end (* context *)

lemma globally_pinverse_pcong:
  "(X¯⇧∀⇧p) ≃⇩p (Y¯⇧∀⇧p)"
  if    "X ≃⇩p Y"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime" and X Y :: "'a fls_pseq"
  using that fls_pinv_cong
  by    fastforce

lemma globally_pinverse_cong:
  "(X¯⇧∀⇧p) ≃⇩∀⇩p
    (Y¯⇧∀⇧p)"
  if  "X ≃⇩∀⇩p Y"
  for X Y :: "'a::nontrivial_factorial_unique_euclidean_bezout fls_pseq"
  using that p_equality_depth_fls_pseq.globally_p_equalD globally_pinverse_pcong by fastforce

lemma globally_pinverse_global_unfrmzr_pows:
  "(𝔭 f :: 'a fls_pseq)¯⇧∀⇧p = 𝔭 (- f)"
  for f :: "'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒ int"
  using fls_pinv_X_intpow unfolding global_unfrmzr_pows_fls_pseq_def by auto

lemma global_pinverse_fls_pseq0:
  "(
    (0::'a::nontrivial_factorial_unique_euclidean_bezout fls_pseq)¯⇧∀⇧p
  ) = 0"
  by fastforce

lemma global_pinverse_fls_pseq1:
  "(
    (1::'a::nontrivial_factorial_unique_euclidean_bezout fls_pseq)¯⇧∀⇧p
  ) = 1"
  by auto

lemma global_pinverse_diff_cancel_lead_coeff:
  "((
    (X¯⇧∀⇧p) -
    (Y¯⇧∀⇧p)
  )°⇧p) > -n"
  if  "X ¬≃⇩p 0" and "X°⇧p = n"
  and "Y ¬≃⇩p 0" and "Y°⇧p = n"
  and "X ¬≃⇩p Y" and "((X - Y)°⇧p) > n"
  for p   :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
  and X Y :: "'a fls_pseq"
  using that fls_pinv_diff_cancel_lead_coeff by auto

subsubsection ‹Topology via global bounded depth›

abbreviation "fls_pseq_bdd_global_depth ≡ p_equality_depth_fls_pseq.bdd_global_depth"
abbreviation "fls_pseq_bdd_global_dist  ≡ p_equality_depth_fls_pseq.bdd_global_dist"
abbreviation "fls_pseq_globally_cauchy  ≡ p_equality_depth_fls_pseq.globally_cauchy"
abbreviation
  "fls_pseq_global_cauchy_condition  ≡ p_equality_depth_fls_pseq.global_cauchy_condition"

lemma fls_pseq_global_cauchy_condition_pmod_uniformity:
  "((X k p) pmod p) $$ m = ((X k' p) pmod p) $$ m"
  if "fls_pseq_global_cauchy_condition X n K" and "k ≥ K" and "k' ≥ K" and "m ≤ int n"
  for p :: "'a::nontrivial_euclidean_ring_cancel prime" and X :: "nat ⇒ 'a fls_pseq"
  using that fls_pmod_cong[of p] fls_pmod_diff_cancel[of m p "X k p" "X k' p"]
        p_equality_depth_fls_pseq.global_cauchy_conditionD
  by    fastforce

abbreviation
  "fls_pseq_cauchy_lim X ≡
    λp. fls_condition_lim p (λn. X n p) (fls_pseq_global_cauchy_condition X)"

lemma fls_pseq_cauchy_condition_lim:
  "∀⇩F k in sequentially. fls_pseq_bdd_global_dist (X k) (fls_pseq_cauchy_lim X) < e"
  if  pos: "e > 0" and cauchy: "fls_pseq_globally_cauchy X"
proof-
  define limval where
    "limval ≡
      λp. fls_condition_lim p (λn. (X n) p) (fls_pseq_global_cauchy_condition X)"
  show "∀⇩F k in sequentially. fls_pseq_bdd_global_dist (X k) limval < e"
  proof (cases "e > 1")
    case True
    hence "⋀n. fls_pseq_bdd_global_dist (X n) limval < e"
      using p_equality_depth_fls_pseq.bdd_global_dist_bdd order_le_less_subst1[of _ id 1 e]
      by    fastforce
    thus ?thesis by simp
  next
    case False show ?thesis
    proof (standard, intro p_equality_depth_fls_pseq.bdd_global_dist_lessI pos)
      fix n :: nat and p :: "'a prime"
      define d where "d ≡ ⌊log 2 (inverse e)⌋"
      define K :: "int ⇒ nat"
        where "K ≡ λn. (LEAST K. fls_pseq_global_cauchy_condition X (nat n) K)"
      assume n: "n ≥ K d" "X n ¬≃⇩p limval"
      have "fls_subdegree (((X n p) pmod p) - limval p) ≥ d"
      proof (intro fls_subdegree_geI)
        from n(2) show "(X n p) pmod p - limval p ≠ 0" using fls_p_modulo_iff by auto
        fix j assume j: "j < d"
        have "((X (K j) p) pmod p) $$ j = ((X n p) pmod p) $$ j"
        proof (intro fls_pseq_global_cauchy_condition_pmod_uniformity)
          from cauchy K_def show "fls_pseq_global_cauchy_condition X (nat j) (K j)"
            using p_equality_depth_fls_pseq.global_cauchy_condition_LEAST[of X "nat j"]
            by    fastforce
          from cauchy n j K_def show "K j ≤ n"
            using p_equality_depth_fls_pseq.global_cauchy_condition_LEAST_mono[of X "nat j" "nat d"]
            by    fastforce
        qed simp_all
        with K_def limval_def have "(X n p pmod p) $$ j = limval p $$ j"
          by (metis fls_condition_lim_nth)
        thus "(X n p pmod p - limval p) $$ j = 0" by auto
      qed
      moreover from n(2) have
        "((X n - limval)°⇧p) ≥
          fls_subdegree ((X n p pmod p) - limval p)"
        using p_equality_fls.conv_0[of p] p_equality_fls.minus[of p] fls_pmod_equiv[of p]
        by    (auto intro: p_depth_fls_ge_p_equal_subdegree)
      ultimately show "((X n - limval)°⇧p) ≥ d" by simp
    qed
  qed
qed

end  (* theory *)