Theory Parametric_Equiv_Depth

(*  Title:       Computational p-Adics: Parametric Equality and Depth
    Author:      Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>, 2025
    Maintainer:  Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>
*)


theory Parametric_Equiv_Depth

imports
  "HOL.Rat"
  "HOL-Computational_Algebra.Fraction_Field"
  "HOL-Computational_Algebra.Primes"
  "HOL-Library.Function_Algebras"
  "HOL-Library.Set_Algebras"
  "HOL.Topological_Spaces"
  Polynomial_Extras

begin


section ‹Common structures for adelic types›


subsection ‹Preliminaries›

lemma ex_least_nat_le':
  fixes P :: "nat ⇒ bool"
  assumes "P n"
  shows "∃k≤n. (∀i<k. ¬ P i) ∧ P k"
  by (metis assms exists_least_iff not_le_imp_less)

lemma ex_ex1_least_nat_le:
  fixes P :: "nat ⇒ bool"
  assumes "∃n. P n"
  shows "∃!k. P k ∧ (∀i. P i ⟶ k ≤ i)"
  by (smt (verit) assms ex_least_nat_le' le_eq_less_or_eq nle_le)

lemma least_le_least:
  "Least Q ≤ Least P"
  if  P : "∃!x. P x ∧ (∀y. P y ⟶ x ≤ y)"
  and Q : "∃!x. Q x ∧ (∀y. Q y ⟶ x ≤ y)"
  and PQ: "∀x. P x ⟶ Q x"
  for P Q :: "'a::order ⇒ bool"
  using PQ Least1_le[OF Q] Least1I[OF P] by blast

lemma linorder_wlog' [case_names le sym]:
  "⟦
    ⋀a b. f a ≤ f b ⟹ P a b;
    ⋀a b. P b a ⟹ P a b
  ⟧ ⟹ P a b"
  for f :: "'a ⇒ 'b::linorder"
  by (cases rule: le_cases[of "f a" "f b"]) blast+

lemma log_powi_cancel [simp]:
  "a > 0 ⟹ a ≠ 1 ⟹ log a (a powi b) = b"
  by (cases "b ≥ 0", simp_all add: power_int_def power_inverse log_inverse)


subsection ‹Existence of primes›

class factorial_comm_ring = factorial_semiring + comm_ring
begin subclass comm_ring_1 .. end

class factorial_idom = factorial_semiring + idom
begin subclass factorial_comm_ring .. end

class nontrivial_factorial_semiring = factorial_semiring +
  assumes nontrivial_elem_exists: "∃x. x ≠ 0 ∧ normalize x ≠ 1"
begin

lemma primeE:
  obtains p where "prime p"
proof-
  from nontrivial_elem_exists obtain x where x: "x ≠ 0" "normalize x ≠ 1" by fast
  from x(1) obtain A
    where "∀x. x ∈# A ⟶ prime x" "normalize (prod_mset A) = normalize x"
    by (auto elim: prime_factorization_exists')
  with x(2) obtain p where "prime p" by fastforce
  with that show thesis by fast
qed

lemma primes_exist: "∃p. prime p"
proof-
  obtain p where "prime p" by (elim primeE)
  thus ?thesis by fast
qed

end (* class nontrivial_factorial_semiring *)

class nontrivial_factorial_comm_ring = nontrivial_factorial_semiring + comm_ring
begin
  subclass factorial_comm_ring ..
end

class nontrivial_factorial_idom = nontrivial_factorial_semiring + idom
begin
  subclass nontrivial_factorial_comm_ring ..
  subclass factorial_idom ..
end

instance int :: nontrivial_factorial_idom
proof
  have "(2::int) ≠ 0" "normalize (2::int) ≠ 1" by auto
  thus "∃x::int. x ≠ 0 ∧ normalize x ≠ 1" by fast
qed

typedef (overloaded) 'a prime =
  "{p::'a::nontrivial_factorial_semiring. prime p}"
  using primes_exist by fast

lemma Rep_prime_n0: "Rep_prime p ≠ 0"
  using Rep_prime[of p] prime_imp_nonzero by simp

lemma Rep_prime_not_unit: "¬ is_unit (Rep_prime p)"
  using Rep_prime[of p] by auto

abbreviation pdvd ::
  "'a::nontrivial_factorial_semiring prime ⇒ 'a ⇒ bool" (infix "pdvd" 50)
  where "p pdvd a ≡ (Rep_prime p) dvd a"
abbreviation "pmultiplicity p ≡ multiplicity (Rep_prime p)"

lemma multiplicity_distinct_primes:
  "p ≠ q ⟹ pmultiplicity p (Rep_prime q) = 0"
  using Rep_prime_inject Rep_prime
        multiplicity_distinct_prime_power[of "Rep_prime p" "Rep_prime q" 1]
  by    auto


subsection ‹Generic algebraic equality›

context
  fixes R
  assumes sympR  : "symp R"
    and   transpR: "transp R"
begin

lemma transp_left: "R x z ⟹ R y z ⟹ R x y"
  by (metis sympR sympD transpR transpD)

lemma transp_right: "R x y ⟹ R x z ⟹ R y z"
  by (metis sympR sympD transpR transpD)

lemma transp_iffs:
  assumes "R x y" shows "R x z ⟷ R y z" and "R z x ⟷ R z y"
  using assms transpD[OF transpR] transp_left transp_right by (blast, blast)

lemma transp_cong: "R w z" if "R x w" and "R y z" and "R x y"
  using that transpD[OF transpR] transp_right by blast

lemma transp_cong_sym: "R x y" if "R x w" and "R y z" and "R w z"
  using that transp_cong sympD[OF sympR] by blast

end (* context symp transp *)

lemma equivp_imp_symp: "equivp R ⟹ symp R"
  by (simp add: equivp_reflp_symp_transp)


locale generic_alg_equality =
  fixes   alg_eq :: "'a ⇒ 'a ⇒ bool"
  assumes equivp: "equivp alg_eq"
begin

lemmas  refl          = equivp_reflp    [OF equivp]
  and   sym [sym]     = equivp_symp     [OF equivp]
  and   trans [trans] = equivp_transp   [OF equivp]
  and   trans_left    = transp_left     [OF equivp_imp_symp equivp_imp_transp, OF equivp equivp]
  and   trans_right   = transp_right    [OF equivp_imp_symp equivp_imp_transp, OF equivp equivp]
  and   trans_iffs    = transp_iffs     [OF equivp_imp_symp equivp_imp_transp, OF equivp equivp]
  and   cong          = transp_cong     [OF equivp_imp_symp equivp_imp_transp, OF equivp equivp]
  and   cong_sym      = transp_cong_sym [OF equivp_imp_symp equivp_imp_transp, OF equivp equivp]

lemma sym_iff: "alg_eq x y = alg_eq y x"
  using sym by blast

end (* locale generic_alg_equality *)


locale ab_group_alg_equality = generic_alg_equality alg_eq
  for alg_eq :: "'a::ab_group_add ⇒ 'a ⇒ bool"
+
  assumes conv_0: "alg_eq x y ⟷ alg_eq (x - y) 0"
begin

lemmas trans0_iff = trans_iffs(1)[of _ _ 0]

lemma add_equiv0_left: "alg_eq (x + y) y" if "alg_eq x 0"
  using that conv_0 by fastforce

lemma add_equiv0_right:  "alg_eq (x + y) x" if "alg_eq y 0"
  using that conv_0 by fastforce

lemma add:
  "alg_eq (x1 + x2) (y1 + y2)" if "alg_eq x1 y1" and "alg_eq x2 y2"
proof (rule iffD2, rule conv_0)
  from that have "alg_eq (x1 - y1) 0" and "alg_eq (x2 - y2) 0"
    using conv_0 by auto
  hence "alg_eq ((x1 - y1) + (x2 - y2)) 0" using add_equiv0_left trans by blast
  moreover have "(x1 - y1) + (x2 - y2) = (x1 + x2) - (y1 + y2)" by simp
  ultimately show "alg_eq ((x1 + x2) - (y1 + y2)) 0" by simp
qed

lemma add_left: "alg_eq (x + y) (x + y')" if "alg_eq y y'"
  using that refl add by simp

lemma add_right: "alg_eq (x + y) (x' + y)" if "alg_eq x x'"
  using that refl add by simp

lemma add_0_left: "alg_eq (x + y) y" if "alg_eq x 0"
  using that add_right[of x 0] by simp

lemma add_0_right: "alg_eq (x + y) x" if "alg_eq y 0"
  using that add_left[of y 0] by simp

lemma sum_zeros:
  "finite A ⟹ ∀a∈A. alg_eq (f a) 0 ⟹ alg_eq (sum f A) 0"
  by (induct A rule: finite_induct, simp add: refl, use add in force)

lemma uminus: "alg_eq x y ⟹ alg_eq (-x) (-y)"
  using conv_0[of x y] conv_0[of "-y" "-x"] sym[of "-y" "-x"] by force

lemma uminus_iff:
  "alg_eq x y ⟷ alg_eq (-x) (-y)"
  using uminus[of x y] uminus[of "-x" "-y"] by fastforce

lemma add_0: "alg_eq (x + y) 0" if "alg_eq x 0" and "alg_eq y 0"
  using that add[of x 0 y 0] by auto

lemma minus:
  "alg_eq x1 y1 ⟹ alg_eq x2 y2 ⟹
    alg_eq (x1 - x2) (y1 - y2)"
  using uminus[of x2 y2] add[of x1 y1 "-x2" "-y2"] by simp

lemma minus_0: "alg_eq (x - y) 0" if "alg_eq x 0" and "alg_eq y 0"
  using that minus[of x 0 y 0] by simp

lemma minus_left: "alg_eq (x - y) (x - y')" if "alg_eq y y'"
  using that refl minus by simp

lemma minus_right: "alg_eq (x - y) (x' - y)" if "alg_eq x x'"
  using that refl minus by simp

lemma minus_0_left: "alg_eq (x - y) (-y)" if "alg_eq x 0"
  using that refl minus_right[of x 0] by simp

lemma minus_0_right: "alg_eq (x - y) x" if "alg_eq y 0"
  using that refl minus_left[of y 0] by simp

end (* locale ab_group_alg_equality *)


locale ring_alg_equality = ab_group_alg_equality alg_eq
  for alg_eq :: "'a::comm_ring ⇒ 'a ⇒ bool"
+
  assumes mult_0_right: "alg_eq y 0 ⟹ alg_eq (x * y) 0"
begin

lemma mult_0_left: "alg_eq x 0 ⟹ alg_eq (x * y) 0"
  using mult_0_right[of x y] by (simp add: mult.commute)

lemma mult:
  "alg_eq x1 y1 ⟹ alg_eq x2 y2 ⟹ alg_eq (x1 * x2) (y1 * y2)"
  using mult_0_right[of "x2 - y2" x1] mult_0_left[of "x1 - y1" y2] conv_0 trans
  by    (force simp add: algebra_simps)

lemma mult_left: "alg_eq y y' ⟹ alg_eq (x * y) (x * y')"
  using refl mult by force

lemma mult_right: "alg_eq x x' ⟹ alg_eq (x * y) (x' * y)"
  using refl mult by force

end (* locale ring_alg_equality *)


locale ring_1_alg_equality = ring_alg_equality alg_eq
  for alg_eq :: "'a::comm_ring_1 ⇒ 'a ⇒ bool"
begin

lemma mult_one_left: "alg_eq x 1 ⟹ alg_eq (x * y) y"
  using mult_right by fastforce

lemma mult_one_right: "alg_eq y 1 ⟹ alg_eq (x * y) x"
  using mult_left by fastforce

lemma prod_ones:
  "finite A ⟹ ∀a∈A. alg_eq (f a) 1 ⟹
    alg_eq (prod f A) 1"
  by (induct A rule: finite_induct, simp add: refl, use mult in force)

lemma prod_with_zero:
  "alg_eq (prod f (insert a A)) 0" if "finite A" and "alg_eq (f a) 0"
  using that prod.insert[of "A - {a}" a f] mult_0_left by fastforce

lemma pow: "alg_eq (x ^ n) (y ^ n)" if "alg_eq x y"
  using that refl mult by (induct n, simp_all)

lemma pow_equiv0: "alg_eq (x ^ n) 0" if "n > 0" and "alg_eq x 0"
  by (metis that zero_power pow)

end (* locale ring_1_alg_equality *)


subsection ‹Indexed equality›

subsubsection ‹General structure›

locale p_equality =
  fixes p_equal :: "'a ⇒ 'b::comm_ring ⇒ 'b ⇒ bool"
  assumes p_alg_equality: "ring_alg_equality (p_equal p)"
begin

lemmas p_group_alg_equality   = ring_alg_equality.axioms(1)[OF p_alg_equality]
lemmas p_generic_alg_equality = ab_group_alg_equality.axioms(1)[OF p_group_alg_equality]

lemmas  equivp        = generic_alg_equality.equivp      [OF p_generic_alg_equality]
  and   refl[simp]    = generic_alg_equality.refl        [OF p_generic_alg_equality]
  and   sym  [sym]    = generic_alg_equality.sym         [OF p_generic_alg_equality]
  and   trans [trans] = generic_alg_equality.trans       [OF p_generic_alg_equality]
  and   sym_iff       = generic_alg_equality.sym_iff     [OF p_generic_alg_equality]
  and   trans_left    = generic_alg_equality.trans_left  [OF p_generic_alg_equality]
  and   trans_right   = generic_alg_equality.trans_right [OF p_generic_alg_equality]
  and   trans_iffs    = generic_alg_equality.trans_iffs  [OF p_generic_alg_equality]
  and   cong          = generic_alg_equality.cong        [OF p_generic_alg_equality]
  and   cong_sym      = generic_alg_equality.cong_sym    [OF p_generic_alg_equality]

lemmas  conv_0           = ab_group_alg_equality.conv_0           [OF p_group_alg_equality]
  and   trans0_iff       = ab_group_alg_equality.trans0_iff       [OF p_group_alg_equality]
  and   add_equiv0_left  = ab_group_alg_equality.add_equiv0_left  [OF p_group_alg_equality]
  and   add_equiv0_right = ab_group_alg_equality.add_equiv0_right [OF p_group_alg_equality]
  and   add              = ab_group_alg_equality.add              [OF p_group_alg_equality]
  and   add_left         = ab_group_alg_equality.add_left         [OF p_group_alg_equality]
  and   add_right        = ab_group_alg_equality.add_right        [OF p_group_alg_equality]
  and   add_0_left       = ab_group_alg_equality.add_0_left       [OF p_group_alg_equality]
  and   add_0_right      = ab_group_alg_equality.add_0_right      [OF p_group_alg_equality]
  and   sum_zeros        = ab_group_alg_equality.sum_zeros        [OF p_group_alg_equality]
  and   uminus           = ab_group_alg_equality.uminus           [OF p_group_alg_equality]
  and   uminus_iff       = ab_group_alg_equality.uminus_iff       [OF p_group_alg_equality]
  and   add_0            = ab_group_alg_equality.add_0            [OF p_group_alg_equality]
  and   minus            = ab_group_alg_equality.minus            [OF p_group_alg_equality]
  and   minus_0          = ab_group_alg_equality.minus_0          [OF p_group_alg_equality]
  and   minus_left       = ab_group_alg_equality.minus_left       [OF p_group_alg_equality]
  and   minus_right      = ab_group_alg_equality.minus_right      [OF p_group_alg_equality]
  and   minus_0_left     = ab_group_alg_equality.minus_0_left     [OF p_group_alg_equality]
  and   minus_0_right    = ab_group_alg_equality.minus_0_right    [OF p_group_alg_equality]

lemmas  mult_0_left  = ring_alg_equality.mult_0_left  [OF p_alg_equality]
  and   mult_0_right = ring_alg_equality.mult_0_right [OF p_alg_equality]
  and   mult         = ring_alg_equality.mult         [OF p_alg_equality]
  and   mult_left    = ring_alg_equality.mult_left    [OF p_alg_equality]
  and   mult_right   = ring_alg_equality.mult_right   [OF p_alg_equality]

definition globally_p_equal :: "'b ⇒ 'b ⇒ bool"
  where globally_p_equal_def[simp]: "globally_p_equal x y = (∀p::'a. p_equal p x y)"

lemma globally_p_equalI[intro]: "globally_p_equal x y" if "⋀p::'a. p_equal p x y"
  using that unfolding globally_p_equal_def by blast

lemma globally_p_equalD: "globally_p_equal x y ⟹ p_equal p x y"
  unfolding globally_p_equal_def by fast

lemma globally_p_nequalE:
  assumes "¬ globally_p_equal x y"
  obtains p where "¬ p_equal p x y"
  using     assms
  unfolding globally_p_equal_def
  by        fast

sublocale globally_p_equality: ring_alg_equality globally_p_equal
proof (standard, intro equivpI)
  show "reflp globally_p_equal"
    using refl unfolding globally_p_equal_def by (fastforce intro: reflpI)
  show "symp globally_p_equal"
    using sym unfolding globally_p_equal_def by (fastforce intro: sympI)
  show "transp globally_p_equal"
    using trans unfolding globally_p_equal_def by (fastforce intro: transpI)
  fix x y :: 'b
  show        "globally_p_equal x y = globally_p_equal (x - y) 0"
  and         "globally_p_equal y 0 ⟹ globally_p_equal (x * y) 0"
    using     conv_0 mult_0_right
    unfolding globally_p_equal_def
    by        auto
qed

lemmas  globally_p_equal_equivp           = globally_p_equality.equivp
  and   globally_p_equal_refl[simp]       = globally_p_equality.refl
  and   globally_p_equal_sym              = globally_p_equality.sym
  and   globally_p_equal_trans            = globally_p_equality.trans
  and   globally_p_equal_trans_left       = globally_p_equality.trans_left
  and   globally_p_equal_trans_right      = globally_p_equality.trans_right
  and   globally_p_equal_trans_iffs       = globally_p_equality.trans_iffs
  and   globally_p_equal_cong             = globally_p_equality.cong
  and   globally_p_equal_conv_0           = globally_p_equality.conv_0
  and   globally_p_equal_trans0_iff       = globally_p_equality.trans0_iff
  and   globally_p_equal_add_equiv0_left  = globally_p_equality.add_equiv0_left
  and   globally_p_equal_add_equiv0_right = globally_p_equality.add_equiv0_right
  and   globally_p_equal_add              = globally_p_equality.add
  and   globally_p_equal_uminus           = globally_p_equality.uminus
  and   globally_p_equal_uminus_iff       = globally_p_equality.uminus_iff
  and   globally_p_equal_add_0            = globally_p_equality.add_0
  and   globally_p_equal_minus            = globally_p_equality.minus
  and   globally_p_equal_mult_0_left      = globally_p_equality.mult_0_left
  and   globally_p_equal_mult_0_right     = globally_p_equality.mult_0_right
  and   globally_p_equal_mult             = globally_p_equality.mult
  and   globally_p_equal_mult_left        = globally_p_equality.mult_left
  and   globally_p_equal_mult_right       = globally_p_equality.mult_right

lemma globally_p_equal_transfer_equals_rsp:
  "p_equal p x1 y1 ⟷ p_equal p x2 y2"
  if "globally_p_equal x1 x2" and "globally_p_equal y1 y2"
  using that trans_iffs globally_p_equalD by blast

end  (* locale p_equality *)


locale p_equality_1 = p_equality p_equal
  for p_equal :: "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
begin

lemma p_alg_equality_1: "ring_1_alg_equality (p_equal p)"
  using ring_1_alg_equality.intro p_alg_equality by blast

lemmas  mult_one_left  = ring_1_alg_equality.mult_one_left  [OF p_alg_equality_1]
  and   mult_one_right = ring_1_alg_equality.mult_one_right [OF p_alg_equality_1]
  and   prod_ones      = ring_1_alg_equality.prod_ones      [OF p_alg_equality_1]
  and   pow            = ring_1_alg_equality.pow            [OF p_alg_equality_1]
  and   pow_equiv0     = ring_1_alg_equality.pow_equiv0     [OF p_alg_equality_1]

end (* locale p_equality_1 *)


locale p_equality_no_zero_divisors = p_equality
+
  assumes no_zero_divisors:
    "¬ p_equal p x 0 ⟹ ¬ p_equal p y 0 ⟹
      ¬ p_equal p (x * y) 0"
begin

lemma mult_equiv_0_iff:
  "p_equal p (x * y) 0 ⟷
    p_equal p x 0 ∨ p_equal p y 0"
  using mult_0_right no_zero_divisors by (fastforce simp add: mult.commute)

end (* locale p_equality_no_zero_divisors *)


locale p_equality_no_zero_divisors_1 = p_equality_no_zero_divisors p_equal
  for p_equal ::
    "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
+
  assumes nontrivial: "∃x. ¬ p_equal p x 0"
begin

sublocale p_equality_1 ..

lemma one_p_nequal_zero: "¬ p_equal p (1::'b) (0::'b)"
  using nontrivial mult_equiv_0_iff[of p "1::'b"] by fastforce

lemma zero_p_nequal_one: "¬ p_equal p (0::'b) (1::'b)"
  using nontrivial one_p_nequal_zero sym by blast

lemma neg_one_p_nequal_zero: "¬ p_equal p (-1::'b) (0::'b)"
  using one_p_nequal_zero uminus by fastforce

lemma pow_equiv_0_iff: "p_equal p (x ^ n) 0 ⟷ p_equal p x 0 ∧ n ≠ 0"
proof (cases n)
  case (Suc k) show ?thesis by (simp only: Suc, induct k, simp_all add: mult_equiv_0_iff)
qed (simp add: one_p_nequal_zero)

lemma pow_equiv_base: "p_equal p (x ^ n) (y ^ n)" if "p_equal p x y"
  using that mult by (induct n) auto

end (* locale p_equality_no_zero_divisors_1 *)


locale p_equality_div_inv = p_equality_no_zero_divisors_1 p_equal
  for p_equal ::
    "'a ⇒ 'b::{comm_ring_1, inverse, divide_trivial} ⇒
      'b ⇒ bool"
+
  assumes divide_inverse    : "⋀x y :: 'b. x / y = x * inverse y"
    and   inverse_inverse   : "⋀x::'b. inverse (inverse x) = x"
    and   inverse_mult      : "⋀x y :: 'b. inverse (x * y) = inverse x * inverse y"
    and   inverse_equiv0_iff: "p_equal p (inverse x) 0 ⟷ p_equal p x 0"
    and   divide_self_equiv : "¬ p_equal p x 0 ⟹ p_equal p (x / x) 1"
begin

text ‹Global algebra facts›

lemma inverse_eq_divide: "inverse x = 1 / x" for x :: 'b
  using divide_inverse by auto

lemma inverse_div_inverse: "inverse x / inverse y = y / x" for x y :: 'b
  by (simp add: divide_inverse inverse_inverse)

lemma inverse_0[simp]: "inverse (0::'b) = 0"
  using inverse_eq_divide by simp

lemma inverse_1[simp]: "inverse (1::'b) = 1"
  using inverse_eq_divide by simp

lemma inverse_pow: "inverse (x ^ n) = inverse x ^ n" for x :: 'b
  by (induct n) (simp_all add: inverse_mult)

lemma power_int_minus: "power_int x (-n) = inverse (power_int x n)" for x :: 'b
  by (cases "n ≥ 0") (simp_all add: power_int_def inverse_pow inverse_inverse)

lemma power_int_minus_divide: "power_int x (-n) = 1 / (power_int x n)" for x :: 'b
  using power_int_minus inverse_eq_divide by presburger

lemma power_int_0_left_if: "power_int (0 :: 'b) m = (if m = 0 then 1 else 0)"
  by (auto simp add: power_int_def zero_power)

lemma power_int_0_left [simp]: "m ≠ 0 ⟹ power_int (0 :: 'b) m = 0"
  by (simp add: power_int_0_left_if)

lemma power_int_1_left [simp]: "power_int (1::'b) n = 1"
  by (auto simp: power_int_def)

lemma inverse_power_int: "inverse (power_int x n) = power_int x (-n)" for x :: 'b
  using inverse_pow inverse_inverse unfolding power_int_def by (cases n) auto

lemma power_int_inverse:
 "power_int (inverse x) n = inverse (power_int x n)" for x :: 'b
proof (cases "n > 0")
  case True thus ?thesis using inverse_pow power_int_def by metis
next
  case False
  moreover define m where "m ≡ - n"
  ultimately have "m ≥ 0" by fastforce
  hence "power_int (inverse x) (-m) = inverse (power_int x (-m))"
  proof (induct m rule: int_ge_induct)
    case (step m)
    from step(1) have "inverse x powi - (m + 1) = x * inverse x powi (- m)"
      using power_Suc[of x "nat m"]
      by    (fastforce simp add: Suc_nat_eq_nat_zadd1 inverse_inverse power_int_def)
    with step show ?case
      by (
        simp  add : inverse_inverse inverse_mult add.commute power_int_def
              flip: Suc_nat_eq_nat_zadd1
      )
  qed simp
  with m_def show ?thesis by force
qed

lemma power_int_mult_distrib:
  "power_int (x * y) m = power_int x m * power_int y m" for x y :: 'b
  by (cases "m ≥ 0") (simp_all add: power_int_def power_mult_distrib inverse_mult)

lemma inverse_divide: "inverse (a / b) = b / a" for a b :: 'b
  by (metis divide_inverse inverse_mult inverse_inverse mult.commute)

lemma minus_divide_left: "- (a / b) = (- a) / b" for a b :: 'b
  by (simp add: divide_inverse algebra_simps)

lemma times_divide_times_eq: "(a / b) * (c / d) = (a * c) / (b * d)" for a b :: 'b
  by (simp add: divide_inverse inverse_mult algebra_simps)

lemma divide_pow: "(x ^ n) / (y ^ n) =  (x / y) ^ n" for x y :: 'b
proof (induct n)
  case (Suc n) thus ?case using times_divide_times_eq[of x y "x ^ n" "y ^ n"] by force
qed simp

lemma power_int_divide_distrib:
  "power_int (x / y) m = power_int x m / power_int y m" for x y :: 'b
  by (cases "m ≥ 0") (simp_all add: power_int_def divide_pow inverse_divide inverse_div_inverse)

lemma power_int_one_over: "power_int (1 / x) n = 1 / power_int x n" for x :: 'b
  by (auto simp add: power_int_inverse simp flip: inverse_eq_divide)

lemma add_divide_distrib: "(a + b) / c = (a / c) + (b / c)" for a b c :: 'b
  by (simp add: divide_inverse algebra_simps)

lemma diff_divide_distrib: "(a - b) / c = (a / c) - (b / c)" for a b c :: 'b
  by (simp add: divide_inverse algebra_simps)

lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" for a b c :: 'b
  using times_divide_times_eq[of a 1] by force

lemma times_divide_eq_left: "(b / c) * a = (b * a) / c" for a b c :: 'b
  using times_divide_eq_right by (simp add: ac_simps)

lemma divide_divide_eq_left: "(a / b) / c = a / (b * c)" for a b c :: 'b
  using divide_inverse mult.assoc inverse_mult[of b c] by metis

lemma swap_numerator: "a * (b / c) = (a / c) * b" for a b c :: 'b
  by (metis times_divide_eq_right mult.commute)

lemma divide_divide_times_eq: "(a / b) / (c / d) = (a * d) / (b * c)" for a b c d :: 'b
  by (metis divide_inverse inverse_divide times_divide_times_eq)

text ‹Algebra facts by place›

lemma right_inverse_equiv: "p_equal p (x * inverse x) 1" if "¬ p_equal p x 0"
  using that divide_self_equiv divide_inverse by force

lemma left_inverse_equiv: "p_equal p (inverse x * x) 1" if "¬ p_equal p x 0"
  using that right_inverse_equiv by (simp add: mult.commute)

lemma inverse_p_unique:
  "p_equal p (inverse x) y" if "p_equal p (x * y) 1"
proof-
  from that have x_n0: "¬ p_equal p x 0"
    using mult_0_left trans_right zero_p_nequal_one by blast
  with that have "p_equal p (inverse x * x * y) (inverse x * x * inverse x)"
    by (metis right_inverse_equiv trans_left mult_left mult.assoc)
  moreover
    have  "p_equal p (inverse x * x * y) y"
    and   "p_equal p (inverse x * x * inverse x) (inverse x)"
    using x_n0 left_inverse_equiv mult_right
    by    (fastforce, fastforce)
  ultimately show "p_equal p (inverse x) y" using cong sym by blast
qed

lemma inverse_equiv_imp_equiv:
  "p_equal p (inverse a) (inverse b) ⟹ p_equal p a b"
proof (cases "p_equal p a 0", metis inverse_equiv0_iff trans_right trans_left)
  case False
  moreover assume ab: "p_equal p (inverse a) (inverse b)"
  ultimately have "¬ p_equal p b 0" using inverse_equiv0_iff trans_right trans_left by meson
  moreover from False ab have
    "p_equal p b (a * (inverse b * b))"
    by (metis mult_left right_inverse_equiv trans_right mult_right mult_1_left mult.assoc)
  ultimately show "p_equal p a b"
    by (metis left_inverse_equiv mult_left trans sym mult_1_right)
qed

lemma inverse_pcong: "p_equal p (inverse x) (inverse y)" if "p_equal p x y"
proof (
  cases "p_equal p x 0", metis that trans_right inverse_equiv0_iff trans_left,
  intro inverse_p_unique
)
  case False with that show "p_equal p (x * inverse y) 1"
    using mult_right right_inverse_equiv cong refl by blast
qed

lemma inverse_equiv_iff_equiv:
  "p_equal p (inverse a) (inverse b) ⟷ p_equal p a b"
  using inverse_equiv_imp_equiv inverse_pcong by blast

lemma power_int_equiv_0_iff:
  "p_equal p (power_int x n) 0 ⟷ p_equal p x 0 ∧ n ≠ 0"
proof (cases "n ≥ 0")
  case False thus ?thesis
    using inverse_pow[of x "nat (-n)"] inverse_equiv0_iff[of p "x ^ nat (- n)"]
          pow_equiv_0_iff[of p x "nat (- n)"]
    by    (force simp add: power_int_def)
qed (simp add: pow_equiv_0_iff power_int_def)

lemma power_diff_conv_inverse_equiv:
  "m ≤ n ⟹ p_equal p (x ^ (n - m)) (x ^ n * inverse x ^ m)"
  if "¬ p_equal p x 0"
proof (induct n)
  case (Suc n) show ?case
  proof (cases "Suc n = m")
    case True show ?thesis
    proof (cases "m = 0")
      case False
      moreover have "p_equal p 1 (x ^ m * inverse x ^ m)"
        using that pow_equiv_0_iff right_inverse_equiv inverse_pow sym by metis
      ultimately show ?thesis using Suc ‹Suc n = m› by simp
    qed simp
  next
    case False
    with Suc(2) have mn: "m ≤ n" by linarith
    with Suc(1) have "p_equal p (x ^ Suc (n - m)) (x ^ Suc n * inverse x ^ m)"
      using mult_left by (simp add: mult.assoc)
    moreover from mn have "Suc (n - m) = Suc n - m" by linarith
    ultimately show ?thesis by argo
  qed
qed simp

lemma power_int_add_1_equiv:
  "p_equal p (power_int x (m + 1)) (power_int x m * x)"
  if "¬ p_equal p x 0 ∨ m ≠ -1"
proof (cases "p_equal p x 0")
  case True
  with that have "p_equal p (power_int x (m + 1)) 0" and "p_equal p (power_int x m * x) 0"
    using power_int_equiv_0_iff mult_0_right by auto
  thus ?thesis using trans_left by blast
next
  case False show ?thesis
  proof (cases "m + 1" rule: int_cases3)
    case zero
    hence "m = -1" by auto
    with False show ?thesis using left_inverse_equiv sym power_int_def by auto
  next
    case (pos n)
    hence "nat (m + 1) = Suc (nat m)" by auto
    moreover from pos have "power_int x (m + 1) = x ^ nat (m + 1)" by auto
    ultimately have "power_int x (m + 1) = power_int x m * x" by (simp add: power_int_def)
    thus ?thesis by fastforce
  next
    case (neg n)
    hence "nat (- m) = Suc n" by fastforce
    hence "power_int x m * x = inverse x ^ n * (inverse x * x)" unfolding power_int_def by auto
    with False neg show ?thesis
      using mult_left left_inverse_equiv mult_1_right sym unfolding power_int_def by fastforce
  qed
qed

lemma power_int_add_equiv:
  "¬ p_equal p x 0 ∨ m + n ≠ 0 ⟹
    p_equal p (power_int x (m + n)) (power_int x m * power_int x n)"
proof (induct m n rule: linorder_wlog)
  fix m n :: int assume mn: "m ≤ n" and x: "¬ p_equal p x 0 ∨ m + n ≠ 0"
  show "p_equal p (power_int x (m + n)) (power_int x m * power_int x n)"
  proof (cases "p_equal p x 0")
    case True
    moreover from this x have "p_equal p (power_int x m) 0 ∨ p_equal p (power_int x n) 0"
      using power_int_equiv_0_iff by presburger
    ultimately show ?thesis
      using x mult_0_left mult_0_right power_int_equiv_0_iff trans_left by meson
  next
    case False
    have
      "m ≤ n ⟹
        p_equal p (power_int x (m + n)) (power_int x m * power_int x n)"
    proof (induct n rule: int_ge_induct)
      case base show ?case
      proof (cases "m ≥ 0")
        case True thus ?thesis
          using nat_add_distrib[of m] power_add[of x] unfolding power_int_def by fastforce
      next
        case False thus ?thesis
          using     nat_add_distrib[of "-m" "-m"] power_add[of "inverse x"]
          unfolding power_int_def
          by        auto
      qed
    next
      case (step n)
      from False have "p_equal p (x powi (m + (n + 1))) (x powi (m + n) * x)"
        using power_int_add_1_equiv[of p x "m + n"] by (simp add: add.assoc)
      with step(2) False have "p_equal p (x powi (m + (n + 1))) (x powi m * (x powi n * x))"
        using mult_right trans by (force simp flip: mult.assoc)
      with False show "p_equal p (x powi (m + (n + 1))) (x powi m * x powi (n + 1))"
        using trans power_int_add_1_equiv sym mult_left by meson
    qed
    with mn show ?thesis by fast
  qed
qed (simp add: ac_simps)

lemma power_int_diff_equiv:
  "p_equal p (power_int x (m - n)) (power_int x m / power_int x n)"
  if "¬ p_equal p x 0 ∨ m ≠ n"
  using that power_int_add_equiv[of p x m "-n"] power_int_minus_divide times_divide_eq_right by auto

lemma power_int_minus_mult_equiv:
  "p_equal p (power_int x (n - 1) * x) (power_int x n)"
  if "¬ p_equal p x 0 ∨ n ≠ 0"
  using that sym power_int_add_1_equiv[of p x "n - 1"] by auto

lemma power_int_not_equiv_zero:
  "¬ p_equal p x 0 ∨ n = 0 ⟹ ¬ p_equal p (power_int x n) 0"
  by (subst power_int_equiv_0_iff) auto

lemma power_int_equiv_base: "p_equal p (power_int x n) (power_int y n)" if "p_equal p x y"
  by (
    cases "n ≥ 0", metis that power_int_def pow_equiv_base,
    metis that inverse_pcong power_int_def pow_equiv_base
  )

lemma divide_equiv_0_iff:
  "p_equal p (x / y) 0 ⟷ p_equal p x 0 ∨ p_equal p y 0"
  using divide_inverse mult_equiv_0_iff inverse_equiv0_iff by metis

lemma divide_pcong: "p_equal p (w / x) (y / z)" if "p_equal p w y" and "p_equal p x z"
  by (metis that divide_inverse inverse_pcong mult)

lemma divide_left_equiv: "p_equal p x y ⟹ p_equal p (x / z) (y / z)"
  by (metis mult_right divide_inverse)

lemma divide_right_equiv: "p_equal p x y ⟹ p_equal p (z / x) (z / y)"
  by (metis inverse_pcong mult_left divide_inverse)

lemma add_frac_equiv:
  "p_equal p ((a / b) + (c / d)) ((a * d + c * b) / (b * d))"
  if "¬ p_equal p b 0" and "¬ p_equal p d 0"
proof-
  from that have
    "(a * d + c * b) / (b * d) =
      a * d * (inverse b * inverse d) + c * b * (inverse b * inverse d)"
    by (metis add_divide_distrib divide_inverse inverse_mult)
  with that show ?thesis
    using mult_left[of p "d * inverse d" 1 "a / b"] mult_right[of p "b * inverse b" 1 "c / d"]
    by    (simp add: ac_simps divide_inverse right_inverse_equiv add sym)
qed

lemma mult_divide_mult_cancel_right:
  "p_equal p ((a * b) / (c * b)) (a / c)" if "¬ p_equal p b 0"
proof-
  have "(a * b) / (c * b) = a * b * (inverse c * inverse b)"
    by (metis divide_inverse inverse_mult)
  with that show ?thesis
    using mult_left[of p "b * inverse b" 1 "a / c"]
    by    (simp add: ac_simps divide_inverse right_inverse_equiv sym)
qed

lemma mult_divide_mult_cancel_right2:
  "p_equal p ((a * c) / (c * b)) (a / b)" if "¬ p_equal p c 0"
  by (metis that mult_divide_mult_cancel_right mult.commute)

lemma mult_divide_mult_cancel_left:
  "p_equal p ((c * a) / (c * b)) (a / b)" if "¬ p_equal p c 0"
  by (metis that mult_divide_mult_cancel_right mult.commute)

lemma mult_divide_mult_cancel_left2:
  "p_equal p ((c * a) / (b * c)) (a / b)" if "¬ p_equal p c 0"
  by (metis that mult_divide_mult_cancel_left mult.commute)

lemma mult_divide_cancel_right: "p_equal p ((a * b) / b) a" if "¬ p_equal p b 0"
  using that mult_divide_mult_cancel_right[of p b a 1] by auto

lemma mult_divide_cancel_left: "p_equal p ((a * b) / a) b" if "¬ p_equal p a 0"
  using that mult_divide_cancel_right mult.commute by metis

lemma divide_equiv_equiv: "(p_equal p (b / c) a) = (p_equal p b (a * c))" if "¬ p_equal p c 0"
proof
  assume "p_equal p (b / c) a"
  hence "p_equal p (b * (inverse c * c)) (a * c)" by (metis divide_inverse mult_right mult.assoc)
  with that show "p_equal p b (a * c)"
    by (metis left_inverse_equiv mult_left mult_1_right trans_right)
next
  assume "p_equal p b (a * c)"
  hence "p_equal p (b / c) (a * (c * inverse c))"
    by (metis mult_right mult.assoc divide_inverse)
  with that show "p_equal p (b / c) a"
    using mult_left right_inverse_equiv trans
    by    fastforce
qed

lemma neg_divide_equiv_equiv:
  "p_equal p (- (b / c)) a ⟷ p_equal p (-b) (a * c)" if "¬ p_equal p c 0"
  using that uminus_iff[of p "- (b / c)" a] divide_equiv_equiv uminus_iff[of p b] by force

lemma equiv_divide_imp:
  "p_equal p (a * c) b ⟹ p_equal p a (b / c)" if "¬ p_equal p c 0"
  using that divide_left_equiv mult_divide_cancel_right trans_right by blast

lemma add_divide_equiv_iff:
  "p_equal p (x + y / z) ((x * z + y) / z)" if "¬ p_equal p z 0"
  using that add sym mult_divide_cancel_right by (fastforce simp add: add_divide_distrib)

lemma divide_add_equiv_iff: "p_equal p (x / z + y) ((x + y * z) / z)" if "¬ p_equal p z 0"
  using that add_divide_equiv_iff[of p z y x] by (simp add: ac_simps)

lemma diff_divide_equiv_iff: "p_equal p (x - y / z) ((x * z - y) / z)" if "¬ p_equal p z 0"
  using that minus sym mult_divide_cancel_right by (fastforce simp add: diff_divide_distrib)

lemma minus_divide_add_equiv_iff:
  "p_equal p (- (x / z) + y) ((- x + y * z) / z)" if "¬ p_equal p z 0"
  by (metis that minus_divide_left divide_add_equiv_iff)

lemma divide_diff_equiv_iff: "p_equal p (x / z - y) ((x - y * z) / z)" if "¬ p_equal p z 0"
  by (metis that diff_conv_add_uminus minus_mult_left divide_add_equiv_iff)

lemma minus_divide_diff_equiv_iff:
  "p_equal p (- (x / z) - y) ((- x - y * z) / z)" if "¬ p_equal p z 0"
  by (metis that divide_diff_equiv_iff minus_divide_left)

lemma divide_mult_cancel_left: "p_equal p (a / (a * b)) (1 / b)" if "¬ p_equal p a 0"
  by (metis that divide_divide_eq_left divide_left_equiv divide_self_equiv)

lemma divide_mult_cancel_right: "p_equal p (b / (a * b)) (1 / a)" if "¬ p_equal p b 0"
  by (metis that divide_mult_cancel_left mult.commute)

lemma diff_frac_equiv:
  "p_equal p (x / y - w / z) ((x * z - w * y) / (y * z))"
  if "¬ p_equal p y 0" and "¬ p_equal p z 0"
proof-
  from that have "p_equal p (x / y - w / z) ((x * z + - (w * y)) / (y * z))"
    using diff_conv_add_uminus minus_divide_left add_frac_equiv minus_mult_left by metis
  thus ?thesis by force
qed

lemma frac_equiv_equiv:
  "p_equal p (x / y) (w / z) ⟷ p_equal p (x * z) (w * y)"
  if "¬ p_equal p y 0" and "¬ p_equal p z 0"
  by (metis that divide_equiv_equiv times_divide_eq_left sym)

lemma inverse_equiv_1_iff:
  "p_equal p (inverse x) 1 ⟷ p_equal p x 1"
  using one_p_nequal_zero trans_right inverse_equiv0_iff mult_left right_inverse_equiv mult_1_right
        mult_right sym mult_1_left
  by    metis

lemma inverse_neg_1_equiv: "p_equal p (inverse (-1)) (-1)"
  using inverse_p_unique by auto

lemma globally_inverse_neg_1: "globally_p_equal (inverse (-1)) (-1)"
  using inverse_neg_1_equiv by blast

lemma inverse_uminus_equiv: "p_equal p (inverse (-x)) (- inverse x)"
  using inverse_mult[of "-1" x] inverse_neg_1_equiv mult_right by fastforce

lemma minus_divide_right_equiv: "p_equal p (a / (- b)) (- (a / b))"
  using divide_inverse inverse_uminus_equiv mult_left trans by fastforce

lemma minus_divide_divide_equiv: "p_equal p ((- a) / (- b)) (a / b)"
  using refl minus_divide_left minus_divide_right_equiv trans by fastforce

lemma divide_minus1_equiv: "p_equal p (x / (-1)) (- x)"
  using minus_divide_right_equiv[of p x 1] by simp

lemma divide_cancel_right:
  "p_equal p (a / c) (b / c) ⟷ p_equal p c 0 ∨ p_equal p a b"
proof
  assume "p_equal p (a / c) (b / c)"
  hence "p_equal p ((c * a) / c) ((c * b) / c)"
    using mult_left times_divide_eq_right by metis
  thus "p_equal p c 0 ∨ p_equal p a b" using mult_divide_cancel_left cong by blast
qed (metis divide_left_equiv divide_equiv_0_iff trans_left)

lemma divide_cancel_left:
  "p_equal p (c / a) (c / b) ⟷ p_equal p c 0 ∨ p_equal p a b"
proof
  assume *: "p_equal p (c / a) (c / b)"
  show "p_equal p c 0 ∨ p_equal p a b"
  proof (cases "p_equal p a 0" "p_equal p c 0" rule: case_split[case_product case_split])
    case False_False
    from * False_False(1) have "p_equal p ((c * a) / c) ((c * b) / c)"
      using divide_equiv_0_iff trans divide_equiv_equiv times_divide_eq_left sym divide_left_equiv
      by    metis
    with False_False(2) show ?thesis using mult_divide_cancel_left cong by blast
  qed (simp, metis * divide_equiv_0_iff trans0_iff trans_left, simp)
qed (metis divide_right_equiv divide_equiv_0_iff trans_left)

lemma divide_equiv_1_iff:
  "p_equal p (a / b) 1 ⟷ ¬ p_equal p b 0 ∧ p_equal p a b"
proof (standard, standard)
  assume "p_equal p (a / b) 1"
  moreover from this show "¬ p_equal p b 0"
    using divide_equiv_0_iff zero_p_nequal_one trans_right by metis
  ultimately show "p_equal p a b"
    using mult_left mult_1_right times_divide_eq_right mult_divide_cancel_left trans_right
    by    metis
qed (metis divide_left_equiv divide_self_equiv trans)

lemma divide_equiv_minus_1_iff:
  "p_equal p (a / b) (- 1) ⟷ ¬ p_equal p b 0 ∧ p_equal p a (- b)"
proof-
  have "p_equal p (a / b) (- 1) ⟷ p_equal p (- (a / b)) 1"
    using uminus_iff by fastforce
  also have "… ⟷ ¬ p_equal p (- b) 0 ∧ p_equal p a (- b)"
    using minus_divide_right_equiv sym trans_right divide_equiv_1_iff by blast
  finally show ?thesis using uminus_iff by fastforce
qed

end (* locale p_equality_div_inv *)


subsection ‹Indexed depth functions›

subsubsection ‹General structure›

locale p_equality_depth = p_equality +
  fixes p_depth :: "'a ⇒ 'b::comm_ring ⇒ int"
  assumes depth_of_0[simp]: "p_depth p 0 = 0"
  and     depth_equiv: "p_equal p x y ⟹ p_depth p x = p_depth p y"
  and     depth_uminus: "p_depth p (-x) = p_depth p x"
  and     depth_pre_nonarch:
    "¬ p_equal p x 0 ⟹ p_depth p x < p_depth p y ⟹
      p_depth p (x + y) = p_depth p x"
    "⟦ ¬ p_equal p x 0; ¬ p_equal p (x + y) 0; p_depth p x = p_depth p y ⟧
      ⟹ p_depth p (x + y) ≥ p_depth p x"
begin

lemma depth_equiv_0: "p_equal p x 0 ⟹ p_depth p x = 0"
  using depth_of_0 depth_equiv by presburger

lemma depth_equiv_uminus: "p_equal p y (-x) ⟹ p_depth p y = p_depth p x"
  using depth_equiv depth_uminus by force

lemma depth_add_equiv0_left: "p_equal p x 0 ⟹ p_depth p (x + y) = p_depth p y"
  using add_equiv0_left depth_equiv by blast

lemma depth_add_equiv0_right: "p_equal p y 0 ⟹ p_depth p (x + y) = p_depth p x"
  using add_equiv0_right depth_equiv by blast

lemma depth_add_equiv:
  "p_depth p (x + y) = p_depth p (w + z)" if "p_equal p x w" and "p_equal p y z"
  using that add depth_equiv by auto

lemma depth_diff: "p_depth p (x - y) = p_depth p (y - x)"
  using depth_uminus[of p "y - x"] by auto

lemma depth_diff_equiv0_left: "p_equal p x 0 ⟹ p_depth p (x - y) = p_depth p y"
  using depth_add_equiv0_right[of p x "-y"] depth_uminus by fastforce

lemma depth_diff_equiv0_right: "p_equal p y 0 ⟹ p_depth p (x - y) = p_depth p x"
  using depth_diff_equiv0_left[of p y x] depth_uminus[of p "x - y"] by simp

lemma depth_diff_equiv:
  "p_depth p (x - y) = p_depth p (w - z)" if "p_equal p x w" and "p_equal p y z"
  using that minus depth_equiv by auto

lemma depth_pre_nonarch_diff_left:
  "p_depth p (x - y) = p_depth p x" if "¬ p_equal p x 0" and "p_depth p x < p_depth p y"
  using that depth_pre_nonarch(1)[of p x "-y"] depth_uminus by simp

lemma depth_pre_nonarch_diff_right:
  "p_depth p (x - y) = p_depth p y" if "¬ p_equal p y 0" and "p_depth p y < p_depth p x"
  using that depth_pre_nonarch_diff_left[of p y x] depth_uminus[of p "x - y"] by simp

lemma depth_nonarch:
  "⟦ ¬ p_equal p x 0; ¬ p_equal p y 0; ¬ p_equal p (x + y) 0 ⟧
    ⟹ p_depth p (x + y) ≥ min (p_depth p x) (p_depth p y)"
  using depth_pre_nonarch[of p x y] depth_pre_nonarch[of p y x]
  by    (cases "p_depth p x" "p_depth p y" rule: linorder_cases, auto simp add: add.commute)

lemma depth_nonarch_diff:
  "⟦ ¬ p_equal p x 0; ¬ p_equal p y 0; ¬ p_equal p (x - y) 0 ⟧
    ⟹ p_depth p (x - y) ≥ min (p_depth p x) (p_depth p y)"
  using depth_nonarch[of p x "-y"] depth_uminus uminus_iff by fastforce

lemma depth_sum_nonarch:
  "finite A ⟹ ¬ p_equal p (sum f A) 0 ⟹
    p_depth p (sum f A) ≥ Min {p_depth p (f a) | a. a ∈ A ∧ ¬ p_equal p (f a) 0 }"
proof (induct A rule: finite_induct)
  case (insert a A)
  define D
    where "D ≡ λA. {p_depth p (f a) |a. a ∈ A ∧ ¬ p_equal p (f a) 0}"
  consider  (fa0)     "p_equal p (f a) 0" |
            (sum0)    "p_equal p (sum f A) 0" |
            (neither) "¬ p_equal p (f a) 0" "¬ p_equal p (sum f A) 0"
    by blast
  thus "p_depth p (sum f (insert a A)) ≥ Min (D (insert a A))"
  proof cases
    case fa0
    with insert D_def have "p_depth p (sum f A) ≥ Min (D A)" using add by fastforce
    moreover from fa0 insert(1,2) have "p_depth p (sum f (insert a A)) = p_depth p (sum f A)"
      using depth_add_equiv0_left by auto
    moreover from fa0 D_def have "D (insert a A) = D A" by blast
    ultimately show ?thesis by argo
  next
    case sum0
    with D_def insert(1,2,4) have "p_depth p (f a) ∈ D (insert a A)" using add by force
    moreover from insert(1,2) sum0 have "p_depth p (sum f (insert a A)) = p_depth p (f a)"
      using depth_add_equiv0_right by fastforce
    ultimately show ?thesis using D_def insert(1) by force
  next
    case neither
    from D_def neither(1) have "D (insert a A) = insert (p_depth p (f a)) (D A)" by blast
    hence "Min (D (insert a A)) = Min (insert (p_depth p (f a)) (D A))" by simp
    also have "… = min (p_depth p (f a)) (Min (D A))"
    proof (rule Min_insert)
      from D_def insert(1) show "finite (D A)" by simp
      from D_def insert(1) neither(2) show "D A ≠ {}" using sum_zeros by fast
    qed
    finally show ?thesis using neither D_def insert depth_nonarch by fastforce
  qed
qed simp

lemma obtains_depth_sum_nonarch_witness:
  assumes "finite A" and "¬ p_equal p (sum f A) 0"
  obtains a
    where "a ∈ A" and "¬ p_equal p (f a) 0" and "p_depth p (sum f A) ≥ p_depth p (f a)"
proof-
  define D where "D ≡ {p_depth p (f a) |a. a ∈ A ∧ ¬ p_equal p (f a) 0}"
  from assms D_def obtain a
    where a: "a ∈ A" "¬ p_equal p (f a) 0" "Min D = p_depth p (f a)"
    using sum_zeros[of A p f] obtains_Min[of D] by auto
  from assms D_def a(3) have "p_depth p (sum f A) ≥ p_depth p (f a)"
    using depth_sum_nonarch by fastforce
  with that a(1,2) show thesis by blast
qed

lemma depth_add_cancel_imp_eq_depth:
  "p_depth p x = p_depth p y" if "¬ p_equal p x 0" and "p_depth p (x + y) > p_depth p x"
  using that depth_pre_nonarch(1)[of p x y] depth_pre_nonarch(1)[of p y x] depth_add_equiv0_right
  by    (fastforce simp add: ac_simps)

lemma depth_diff_cancel_imp_eq_depth_left:
  "p_depth p x = p_depth p y" if  "¬ p_equal p x 0" and "p_depth p (x - y) > p_depth p x"
  using that depth_add_cancel_imp_eq_depth[of p x "-y"] depth_uminus by auto

lemma depth_diff_cancel_imp_eq_depth_right:
  "p_depth p x = p_depth p y" if  "¬ p_equal p y 0" and "p_depth p (x - y) > p_depth p y"
  by (metis that depth_diff_cancel_imp_eq_depth_left depth_diff)

lemma level_closed_add:
  "p_depth p (x + y) ≥ n"
  if "¬ p_equal p (x + y) 0" and "p_depth p x ≥ n" and "p_depth p y ≥ n"
proof-
  consider
    "p_equal p x 0" | "p_equal p y 0" |
    (both_n0) "¬ p_equal p x 0" "¬ p_equal p y 0"
    by blast
  thus ?thesis
  proof cases
    case both_n0 with that show ?thesis using depth_nonarch by fastforce
  qed (simp add: that(3) depth_add_equiv0_left, simp add: that(2) depth_add_equiv0_right)
qed

lemma level_closed_diff:
  "p_depth p (x - y) ≥ n"
  if "¬ p_equal p (x - y) 0" and "p_depth p x ≥ n" and "p_depth p y ≥ n"
  using that level_closed_add[of p x "-y"] depth_uminus by auto

definition p_depth_set :: "'a ⇒ int ⇒ 'b set"
  where "p_depth_set p n = {x. ¬ p_equal p x 0 ⟶ p_depth p x ≥ n}"

definition global_depth_set :: "int ⇒ 'b set"
  where
    "global_depth_set n =
      {x. ∀p. ¬ p_equal p x 0 ⟶ p_depth p x ≥ n}"

lemma global_depth_set: "global_depth_set n = (⋂p. p_depth_set p n)"
  unfolding p_depth_set_def global_depth_set_def by auto

lemma p_depth_setD:
  "¬ p_equal p x 0 ⟹ x ∈ p_depth_set p n ⟹
    p_depth p x ≥ n"
  unfolding p_depth_set_def by blast

lemma nonpos_p_depth_setD:
  "n ≤ 0 ⟹ x ∈ p_depth_set p n ⟹ p_depth p x ≥ n"
  by (cases "p_equal p x 0", simp_all add: depth_equiv_0 p_depth_setD)

lemma global_depth_setD:
  "¬ p_equal p x 0 ⟹ x ∈ global_depth_set n ⟹
    p_depth p x ≥ n"
  unfolding global_depth_set_def by blast

lemma nonpos_global_depth_setD:
  "n ≤ 0 ⟹ x ∈ global_depth_set n ⟹ p_depth p x ≥ n"
  by (cases "p_equal p x 0", simp_all add: depth_equiv_0 global_depth_setD)

lemma p_depth_set_0: "0 ∈ p_depth_set p n"
  unfolding p_depth_set_def by fastforce

lemma global_depth_set_0: "0 ∈ global_depth_set n"
  unfolding global_depth_set_def by fastforce

lemma p_depth_set_equiv0: "p_equal p x 0 ⟹ x ∈ p_depth_set p n"
  unfolding p_depth_set_def by blast

lemma p_depth_setI:
  "x ∈ p_depth_set p n" if "¬ p_equal p x 0 ⟶ p_depth p x ≥ n"
  using that unfolding p_depth_set_def by blast

lemma p_depth_set_by_equivI:
  "x ∈ p_depth_set p n" if "p_equal p x y" and "y ∈ p_depth_set p n"
  by (metis that trans p_depth_setD depth_equiv p_depth_setI)

lemma global_depth_setI:
  "x ∈ global_depth_set n"
  if "⋀p. ¬ p_equal p x 0 ⟹ p_depth p x ≥ n"
  using that unfolding global_depth_set_def by blast

lemma global_depth_setI': "x ∈ global_depth_set n" if "⋀p. p_depth p x ≥ n"
  by (intro global_depth_setI, rule that)

lemma global_depth_setI'': "x ∈ global_depth_set n" if "⋀p. x ∈ p_depth_set p n"
  using that global_depth_set by blast

lemma p_depth_set_antimono:
  "n ≤ m ⟹ p_depth_set p n ⊇ p_depth_set p m"
  unfolding p_depth_set_def by force

lemma global_depth_set_antimono:
  "n ≤ m ⟹ global_depth_set n ⊇ global_depth_set m"
  unfolding global_depth_set_def by force

lemma p_depth_set_add:
  "x + y ∈ p_depth_set p n" if "x ∈ p_depth_set p n" and "y ∈ p_depth_set p n"
proof (intro p_depth_setI, clarify)
  assume nequiv0: "¬ p_equal p (x + y) 0"
  consider "p_equal p x 0" | "p_equal p y 0" | "¬ p_equal p x 0" "¬ p_equal p y 0"
    by blast
  thus "p_depth p (x + y) ≥ n"
    by (
      cases, metis that(2) nequiv0 add_0_left depth_equiv trans p_depth_setD,
      metis that(1) nequiv0 add_0_right depth_equiv trans p_depth_setD,
      metis that nequiv0 level_closed_add p_depth_setD
    )
qed

lemma global_depth_set_add:
  "x + y ∈ global_depth_set n" if "x ∈ global_depth_set n" and "y ∈ global_depth_set n"
  using that p_depth_set_add global_depth_set by simp

lemma p_depth_set_uminus: "-x ∈ p_depth_set p n" if "x ∈ p_depth_set p n"
  using that uminus depth_uminus unfolding p_depth_set_def by fastforce

lemma global_depth_set_uminus: "-x ∈ global_depth_set n" if "x ∈ global_depth_set n"
  using that p_depth_set_uminus global_depth_set by simp

lemma p_depth_set_minus:
  "x - y ∈ p_depth_set p n" if "x ∈ p_depth_set p n" and "y ∈ p_depth_set p n"
  using that p_depth_set_add p_depth_set_uminus by fastforce

lemma global_depth_set_minus:
  "x - y ∈ global_depth_set n" if "x ∈ global_depth_set n" and "y ∈ global_depth_set n"
  using that p_depth_set_minus global_depth_set by simp

lemma p_depth_set_elt_set_plus:
  "x +o p_depth_set p n = p_depth_set p n" if "x ∈ p_depth_set p n"
  unfolding elt_set_plus_def
proof (standard, safe)
  fix y assume y: "y ∈ p_depth_set p n"
  define z where "z ≡ y - x"
  with that y have "z ∈ p_depth_set p n" using p_depth_set_minus by simp
  with z_def show "∃z∈p_depth_set p n. y = x + z" by force
qed (simp add: that p_depth_set_add)

lemma global_depth_set_elt_set_plus:
  "x +o global_depth_set n = global_depth_set n" if "x ∈ global_depth_set n"
  unfolding elt_set_plus_def
proof (standard, safe)
  fix y assume y: "y ∈ global_depth_set n"
  define z where "z ≡ y - x"
  with that y have "z ∈ global_depth_set n" using global_depth_set_minus by simp
  with z_def show "∃z∈global_depth_set n. y = x + z" by force
qed (simp add: that global_depth_set_add)

lemma p_depth_set_elt_set_plus_closed:
  "x +o p_depth_set p m ⊆ p_depth_set p n" if "m ≥ n" and "x ∈ p_depth_set p n"
  using that set_plus_mono p_depth_set_antimono p_depth_set_elt_set_plus by metis

lemma global_depth_set_elt_set_plus_closed:
  "x +o global_depth_set m ⊆ global_depth_set n"
  if "m ≥ n" and "x ∈ global_depth_set n"
  using that set_plus_mono global_depth_set_antimono global_depth_set_elt_set_plus by metis

lemma p_depth_set_plus_coeffs:
  "set xs ⊆ p_depth_set p n ⟹
    set ys ⊆ p_depth_set p n ⟹
    set (plus_coeffs xs ys) ⊆ p_depth_set p n"
proof (induct xs ys rule: list_induct2')
  case (4 x xs y ys) thus ?case
    using cCons_def[of "x + y" "plus_coeffs xs ys"] p_depth_set_add by auto
qed simp_all

lemma global_depth_set_plus_coeffs:
  "set (plus_coeffs xs ys) ⊆ global_depth_set n"
  if "set xs ⊆ global_depth_set n" and "set ys ⊆ global_depth_set n"
  using that p_depth_set_plus_coeffs[of xs _ n ys] global_depth_set[of n] by fastforce

lemma p_depth_set_poly_pCons:
  "set (coeffs (pCons a f)) ⊆ p_depth_set p n"
  if "a ∈ p_depth_set p n" and "set (coeffs f) ⊆ p_depth_set p n"
  by (cases "a = 0 ∧ f = 0") (simp add: p_depth_set_0, use that in auto)

lemma p_depth_set_poly_add:
  "set (coeffs (f + g)) ⊆ p_depth_set p n"
  if "set (coeffs f) ⊆ p_depth_set p n" and "set (coeffs g) ⊆ p_depth_set p n"
  using that coeffs_plus_eq_plus_coeffs p_depth_set_plus_coeffs by metis

lemma global_depth_set_poly_add:
  "set (coeffs (f + g)) ⊆ global_depth_set n"
  if  "set (coeffs f) ⊆ global_depth_set n"
  and "set (coeffs g) ⊆ global_depth_set n"
  using that p_depth_set_poly_add[of f _ n g] global_depth_set by fastforce

end  (* locale p_equality_depth *)


locale p_equality_depth_no_zero_divisors =
  p_equality_no_zero_divisors + p_equality_depth
+ assumes depth_mult_additive:
    "¬ p_equal p (x * y) 0 ⟹ p_depth p (x * y) = p_depth p x + p_depth p y"
begin

lemma depth_mult3_additive:
  "p_depth p (x * y * z) = p_depth p x + p_depth p y + p_depth p z"
  if "¬ p_equal p (x * y * z) 0"
  using that mult_0_left depth_mult_additive by fastforce

lemma p_depth_set_times:
  "x * y ∈ p_depth_set p n"
  if "n ≥ 0" and "x ∈ p_depth_set p n" and "y ∈ p_depth_set p n"
proof (intro p_depth_setI, clarify)
  assume "¬ p_equal p (x * y) 0"
  moreover from this have "¬ p_equal p x 0" and "¬ p_equal p y 0"
    by (metis mult_0_left, metis mult_0_right)
  ultimately show "p_depth p (x * y) ≥ n"
    using that p_depth_setD[of p x] p_depth_setD[of p y] depth_mult_additive by fastforce
qed

lemma global_depth_set_times:
  "x * y ∈ global_depth_set n"
  if "n ≥ 0" and "x ∈ global_depth_set n" and "y ∈ global_depth_set n"
  using that p_depth_set_times global_depth_set by simp

lemma poly_p_depth_set_poly:
  "set (coeffs f) ⊆ p_depth_set p n ⟹ poly f x ∈ p_depth_set p n"
  if "n ≥ 0" and "x ∈ p_depth_set p n"
  by (induct f, simp add: p_depth_set_0, use that p_depth_set_times p_depth_set_add in force)

lemma poly_global_depth_set_poly:
  "poly f x ∈ global_depth_set n"
  if    "n ≥ 0"
  and   "x ∈ global_depth_set n"
  and   "set (coeffs f) ⊆ global_depth_set n"
  using that poly_p_depth_set_poly global_depth_set
  by    fastforce

lemma p_depth_set_ideal:
  "x * y ∈ p_depth_set p n"
  if "x ∈ p_depth_set p 0" and "y ∈ p_depth_set p n"
proof (intro p_depth_setI, clarify)
  assume "¬ p_equal p (x * y) 0"
  moreover from this have "¬ p_equal p x 0" and "¬ p_equal p y 0"
    by (metis mult_0_left, metis mult_0_right)
  ultimately show "p_depth p (x * y) ≥ n"
    using that p_depth_setD[of p x] p_depth_setD[of p y] depth_mult_additive by fastforce
qed

lemma global_depth_set_ideal:
  "x * y ∈ global_depth_set n"
  if "x ∈ global_depth_set 0" and "y ∈ global_depth_set n"
  using that p_depth_set_ideal global_depth_set by simp

lemma poly_p_depth_set_poly_ideal:
  "set (coeffs f) ⊆ p_depth_set p n ⟹ poly f x ∈ p_depth_set p n"
  if "x ∈ p_depth_set p 0"
  using that p_depth_set_0 p_depth_set_ideal p_depth_set_add by (induct f) auto

lemma poly_global_depth_set_poly_ideal:
  "poly f x ∈ global_depth_set n"
  if "x ∈ global_depth_set 0" and "set (coeffs f) ⊆ global_depth_set n"
  using that poly_p_depth_set_poly_ideal global_depth_set by fastforce

lemma p_depth_set_poly_smult:
  "set (coeffs (smult x f)) ⊆ p_depth_set p n"
  if "n ≥ 0" and "x ∈ p_depth_set p n" and "set (coeffs f) ⊆ p_depth_set p n"
proof-
  have "set (coeffs (smult x f)) = (*) x ` set (strip_while (λc. x * c = 0) (coeffs f))"
    using coeffs_smult_eq_smult_coeffs set_map by metis
  also have "… ⊆ set (map ((*) x) (coeffs f))"
    using set_strip_while image_mono set_map by fastforce
  finally show ?thesis using that p_depth_set_times by fastforce
qed

lemma global_depth_set_poly_smult:
  "set (coeffs (smult x f)) ⊆ global_depth_set n"
  if    "n ≥ 0"
  and   "x ∈ global_depth_set n"
  and   "set (coeffs f) ⊆ global_depth_set n"
  using that p_depth_set_poly_smult global_depth_set
  by    fastforce

lemma p_depth_set_poly_smult_ideal:
  "set (coeffs (smult x f)) ⊆ p_depth_set p n"
  if "x ∈ p_depth_set p 0" and "set (coeffs f) ⊆ p_depth_set p n"
proof-
  have "set (coeffs (smult x f)) = (*) x ` set (strip_while (λc. x * c = 0) (coeffs f))"
    using coeffs_smult_eq_smult_coeffs set_map by metis
  also have "… ⊆ set (map ((*) x) (coeffs f))"
    using set_strip_while image_mono set_map by fastforce
  finally show ?thesis using that p_depth_set_ideal by fastforce
qed

lemma global_depth_set_poly_smult_ideal:
  "set (coeffs (smult x f)) ⊆ global_depth_set n"
  if "x ∈ global_depth_set 0" and "set (coeffs f) ⊆ global_depth_set n"
  using that p_depth_set_poly_smult_ideal global_depth_set by fastforce

lemma p_depth_set_poly_times:
  "set (coeffs f) ⊆ p_depth_set p n ⟹
    set (coeffs g) ⊆ p_depth_set p n ⟹
    set (coeffs (f * g)) ⊆ p_depth_set p n"
  if  "n ≥ 0"
proof (induct f)
  case (pCons a f)
  hence "set (coeffs (f * g)) ⊆ p_depth_set p n" by auto
  moreover from pCons(1,3) have "a ∈ p_depth_set p n" by fastforce
  ultimately show ?case
    using that pCons(4) mult_pCons_left p_depth_set_poly_add p_depth_set_poly_smult
          p_depth_set_poly_pCons p_depth_set_0
    by    auto
qed simp

lemma global_depth_set_poly_times:
  "set (coeffs (f * g)) ⊆ global_depth_set n"
  if  "n ≥ 0"
  and "set (coeffs g) ⊆ global_depth_set n"
  and "set (coeffs f) ⊆ global_depth_set n"
  using that p_depth_set_poly_times[of n f _ g] global_depth_set by fastforce

lemma p_depth_set_poly_times_ideal:
  "set (coeffs f) ⊆ p_depth_set p 0 ⟹
    set (coeffs g) ⊆ p_depth_set p n ⟹
    set (coeffs (f * g)) ⊆ p_depth_set p n"
proof (induct f)
  case (pCons a f)
  hence "set (coeffs (f * g)) ⊆ p_depth_set p n" by auto
  moreover from pCons(1,3) have "a ∈ p_depth_set p 0" by fastforce
  ultimately show ?case
    using pCons(4) mult_pCons_left p_depth_set_poly_add p_depth_set_poly_smult_ideal
          p_depth_set_poly_pCons p_depth_set_0
    by    simp
qed simp

lemma global_depth_set_poly_times_ideal:
  "set (coeffs (f * g)) ⊆ global_depth_set n"
  if  "set (coeffs f) ⊆ global_depth_set 0"
  and "set (coeffs g) ⊆ global_depth_set n"
  using that p_depth_set_poly_times_ideal[of f _ g] global_depth_set by fastforce

end


locale p_equality_depth_no_zero_divisors_1 =
  p_equality_no_zero_divisors_1 + p_equality_depth_no_zero_divisors
begin

lemma depth_of_1[simp]: "p_depth p 1 = 0"
  using one_p_nequal_zero depth_mult_additive[of p 1] by auto

lemma depth_of_neg1: "p_depth p (-1) = 0"
  using depth_uminus by auto

lemma depth_pow_additive: "p_depth p (x ^ n) = int n * p_depth p x"
proof (cases "p_equal p x 0")
  case True thus ?thesis using pow_equiv_0_iff depth_equiv_0 by (cases "n = 0") auto
next
  case False show ?thesis
  proof (induct n)
    case (Suc n)
    from False have "p_depth p (x ^ Suc n) = p_depth p x + p_depth p (x ^ n)"
      using pow_equiv_0_iff depth_mult_additive by force
    also from Suc have "… = (int n + 1) * p_depth p x" by algebra
    finally show ?case by auto
  qed simp
qed

lemma depth_prod_summative:
  "finite X ⟹ ¬ p_equal p (∏X) 0 ⟹
    p_depth p (∏X) = sum (p_depth p) X"
  by (induct X rule: finite_induct, simp, use depth_mult_additive mult_0_right in force)

lemma p_depth_set_1: "1 ∈ p_depth_set p 0"
  using p_depth_setI by simp

lemma pos_p_depth_set_1: "n > 0 ⟹ 1 ∉ p_depth_set p n"
  using one_p_nequal_zero p_depth_setD by fastforce

lemma global_depth_set_1: "1 ∈ global_depth_set 0"
  using p_depth_set_1 global_depth_set by blast

lemma pos_global_depth_set_1: "n > 0 ⟹ 1 ∉ global_depth_set n"
  using pos_p_depth_set_1 global_depth_set by blast

lemma p_depth_set_neg1: "-1 ∈ p_depth_set p 0"
  using depth_of_neg1 p_depth_setI by simp

lemma global_depth_set_neg1: "-1 ∈ global_depth_set 0"
  using p_depth_set_neg1 global_depth_set by blast

lemma p_depth_set_pow:
  "x ^ Suc k ∈ p_depth_set p n" if "n ≥ 0" and "x ∈ p_depth_set p n"
  by (induct k, simp_all add: that p_depth_set_times)

lemma global_depth_set_pow:
  "x ^ Suc k ∈ global_depth_set n" if "n ≥ 0" and "x ∈ global_depth_set n"
  using that p_depth_set_pow global_depth_set by simp

lemma p_depth_set_0_pow: "x ^ k ∈ p_depth_set p 0" if "x ∈ p_depth_set p 0"
  by (induct k, simp_all add: that p_depth_set_1 p_depth_set_times)

lemma global_depth_set_0_pow: "x ^ k ∈ global_depth_set 0" if "x ∈ global_depth_set 0"
  using that p_depth_set_0_pow global_depth_set by simp

lemma p_depth_set_of_nat: "of_nat n ∈ p_depth_set p 0"
  using p_depth_set_0 p_depth_set_1 p_depth_set_add by (induct n) simp_all

lemma global_depth_set_of_nat: "of_nat n ∈ global_depth_set 0"
  using p_depth_set_of_nat global_depth_set by blast

lemma p_depth_set_of_int: "of_int n ∈ p_depth_set p 0"
  using p_depth_set_of_nat p_depth_set_neg1 p_depth_set_minus by (induct n) simp_all

lemma global_depth_set_of_int: "of_int n ∈ global_depth_set 0"
  using p_depth_set_of_int global_depth_set by blast

lemma p_depth_set_polyderiv:
  "set (coeffs f) ⊆ p_depth_set p n ⟹
    set (coeffs (polyderiv f)) ⊆ p_depth_set p n"
proof (induct f)
  case (pCons a f)
  from pCons(1) have
    "set (coeffs (polyderiv (pCons a f))) =
      set (plus_coeffs (coeffs f) (coeffs (pCons 0 (polyderiv f))))"
    using polyderiv_pCons coeffs_plus_eq_plus_coeffs by metis
  moreover from pCons(1,3) have "set (coeffs f) ⊆ p_depth_set p n" by fastforce
  ultimately show ?case
    using pCons(2) p_depth_set_poly_pCons p_depth_set_0 p_depth_set_plus_coeffs by presburger
qed simp

lemma global_depth_set_polyderiv:
  "set (coeffs (polyderiv f)) ⊆ global_depth_set n"
  if "set (coeffs f) ⊆ global_depth_set n"
  using that p_depth_set_polyderiv global_depth_set by fastforce

lemma poly_p_depth_set_polyderiv:
  "poly (polyderiv f) x ∈ p_depth_set p n"
  if "n ≥ 0" and "set (coeffs f) ⊆ p_depth_set p n" and "x ∈ p_depth_set p n"
  using that poly_p_depth_set_poly p_depth_set_polyderiv by blast

lemma poly_global_depth_set_polyderiv:
  "poly (polyderiv f) x ∈ global_depth_set n"
  if  "n ≥ 0"
  and "set (coeffs f) ⊆ global_depth_set n"
  and "x ∈ global_depth_set n"
  using that poly_p_depth_set_polyderiv global_depth_set by fastforce

lemma p_set_depth_additive_poly_poly:
  "set (coeffs f) ⊆ p_depth_set p m ⟹
    set (coeffs (coeff (additive_poly_poly f) n)) ⊆ p_depth_set p m"
  if "m ≥ 0"
proof (induct f arbitrary: n rule: pCons_induct')
  case (pCons0 a) thus ?case using additive_poly_poly_pCons0 by (cases n, fastforce, fastforce)
next
  case (pCons a f) show ?case
  proof (cases n)
    case 0 with pCons(1,3) show ?thesis by (simp add: additive_poly_poly_coeff0 cCons_def)
  next
    case (Suc k)
    moreover have
      "set (coeffs (pCons 0 1 * coeff (additive_poly_poly f) n + coeff (additive_poly_poly f) k))
        ⊆ p_depth_set p m"
      by (
        intro p_depth_set_poly_add p_depth_set_poly_times_ideal that pCons(2),
        simp add: p_depth_set_0 p_depth_set_1, use pCons(1,3) in auto
      )
    ultimately show
      "set (coeffs (coeff (additive_poly_poly (pCons a f)) n)) ⊆ p_depth_set p m"
      using pCons(1) additive_poly_poly_pCons coeff_add coeff_smult coeff_pCons_Suc by fastforce
  qed
qed simp

lemma global_depth_set_additive_poly_poly:
  "set (coeffs (coeff (additive_poly_poly f) n)) ⊆ global_depth_set m"
  if "m ≥ 0" and "set (coeffs f) ⊆ global_depth_set m"
  using that p_set_depth_additive_poly_poly global_depth_set by fastforce

lemma poly_p_depth_set_additive_poly_poly:
  "poly (coeff (additive_poly_poly f) n) x ∈ p_depth_set p m"
  if "m ≥ 0" and "set (coeffs f) ⊆ p_depth_set p m" and "x ∈ p_depth_set p m"
  using that poly_p_depth_set_poly p_set_depth_additive_poly_poly by auto

lemma poly_global_depth_set_additive_poly_poly:
  "poly (coeff (additive_poly_poly f) n) x ∈ global_depth_set m"
  if  "m ≥ 0"
  and "set (coeffs f) ⊆ global_depth_set m"
  and "x ∈ global_depth_set m"
  using that poly_p_depth_set_additive_poly_poly global_depth_set by fastforce

lemma sum_poly_additive_poly_poly_depth_bound:
  fixes p :: 'a and f :: "'b poly" and x y :: 'b and a b n :: nat
  defines "g ≡ λi. poly (coeff (additive_poly_poly f) (Suc i)) x * y ^ (Suc i)"
  defines "S ≡ sum g {a..b}"
  assumes coeffs: "set (coeffs f) ⊆ p_depth_set p 0"
    and   arg   : "x ∈ p_depth_set p 0"
    and   sum   : "¬ p_equal p S 0"
  obtains j where "j ∈ {a..b}" and "p_depth p S ≥ int (Suc j) * p_depth p y"
proof-
  from S_def sum obtain j where j:
    "j ∈ {a..b}" "¬ p_equal p (g j) 0" "p_depth p S ≥ p_depth p (g j)"
    using obtains_depth_sum_nonarch_witness by blast
  from g_def j(2)
    have  y_coeff_n0: "¬ p_equal p (poly (coeff (additive_poly_poly f) (Suc j)) x) 0"
    using mult_0_left[of p _ "y ^ Suc j"]
    by    blast
  from g_def j(2,3) have
    "p_depth p (g j) =
      p_depth p (poly (coeff (additive_poly_poly f) (Suc j)) x) +
      int (Suc j) * p_depth p y"
    using depth_mult_additive[of p _ "y ^ Suc j"] depth_pow_additive[of p y "Suc j"] by auto
  also from coeffs arg
    have  "… ≥ int (Suc j) * p_depth p y"
    using y_coeff_n0 poly_p_depth_set_additive_poly_poly[of 0 f p x "Suc j"]
          p_depth_setD[of p "poly (coeff (additive_poly_poly f) (Suc j)) x" 0]
    by    auto
  finally have "p_depth p (g j) ≥ int (Suc j) * p_depth p y" by blast
  with j(3) have "p_depth p S ≥ int (Suc j) * p_depth p y" by simp
  with j(1) that show thesis by blast
qed

end (* locale p_equality_depth_no_zero_divisors_1 *)

subsubsection ‹Depth of inverses and division›

locale p_equality_depth_div_inv =
  p_equality_div_inv + p_equality_depth_no_zero_divisors_1
begin

lemma inverse_depth: "p_depth p (inverse x) = - p_depth p x"
proof (cases "p_equal p x 0")
  case False
  from False have "p_depth p (x * inverse x) = 0"
    using depth_equiv right_inverse_equiv depth_of_1 by metis
  moreover from False have "¬ p_equal p (x * inverse x) 0"
    using right_inverse_equiv trans_right one_p_nequal_zero by blast
  ultimately show ?thesis using depth_mult_additive by simp
qed (simp add: inverse_equiv0_iff depth_equiv_0)

lemma depth_powi_additive: "p_depth p (power_int x n) = n * p_depth p x"
proof (cases "n ≥ 0")
  case True thus ?thesis using depth_pow_additive unfolding power_int_def by auto
next
  case False
  moreover from this have "(- int (nat (-n))) = n" by simp
  ultimately show ?thesis
    using power_int_def inverse_pow inverse_depth depth_pow_additive minus_mult_left by metis
qed

lemma p_depth_set_inverse: "inverse x ∈ p_depth_set p 0" if "p_depth p x = 0"
  using that inverse_depth p_depth_setI by force

lemma divide_depth: "p_depth p (x / y) = p_depth p x - p_depth p y" if "¬ p_equal p (x / y) 0"
  using that by (simp add: divide_inverse depth_mult_additive inverse_depth)

lemma p_depth_set_divide:
  "x / y ∈ p_depth_set p n" if "x ∈ p_depth_set p n" and "p_depth p y = 0"
  by (
    auto  intro   : p_depth_setI
          simp add: that p_depth_set_equiv0 divide_equiv_0_iff p_depth_setD divide_depth
  )

lemma p_depth_poly_deriv_quotient:
  "p_depth p ((poly f a) / (poly (polyderiv f) a)) ≥ n"
  if    "n ≥ 0"
  and   "set (coeffs f) ⊆ p_depth_set p n"
  and   "a ∈ p_depth_set p n"
  and   "¬ p_equal p (poly f a) 0"
  and   "¬ p_equal p (poly (polyderiv f) a) 0"
  and   "p_depth p (poly f a) ≥ 2 * p_depth p (poly (polyderiv f) a)"
  using that divide_equiv_0_iff divide_depth poly_p_depth_set_polyderiv poly_p_depth_set_poly
        p_depth_setD[of p "poly (polyderiv f) a" n]
  by    force

lemma p_depth_set_poly_deriv_quotient:
  "(poly f a) / (poly (polyderiv f) a) ∈ p_depth_set p n"
  if    "n ≥ 0"
  and   "set (coeffs f) ⊆ p_depth_set p n"
  and   "a ∈ p_depth_set p n"
  and   "¬ p_equal p (poly f a) 0"
  and   "¬ p_equal p (poly (polyderiv f) a) 0"
  and   "p_depth p (poly f a) ≥ 2 * p_depth p (poly (polyderiv f) a)"
  using that divide_equiv_0_iff p_depth_poly_deriv_quotient p_depth_setI
  by    presburger

end (* locale p_equality_depth_div_inv *)


subsection ‹Global equality and restriction of places›

subsubsection ‹Locales›

locale global_p_equality = p_equality
+
  fixes   p_restrict :: "'b::comm_ring ⇒ ('a ⇒ bool) ⇒ 'b"
  assumes p_restrict_equiv      : "P p ⟹ p_equal p (p_restrict x P) x"
  and     p_restrict_equiv0     : "¬ P p ⟹ p_equal p (p_restrict x P) 0"
begin

lemma p_restrict_equiv_sym: "P p ⟹ p_equal p x (p_restrict x P)"
  using p_restrict_equiv sym by presburger

lemma p_restrict_equiv0_iff:
  "p_equal p (p_restrict x P) 0 ⟷ p_equal p x 0 ∨ ¬ P p"
  by (metis p_restrict_equiv p_restrict_equiv0 trans trans_right)

lemma p_restrict_restrict_equiv_conj:
  "p_equal p (p_restrict (p_restrict x P) Q) (p_restrict x (λp. P p ∧ Q p))"
proof-
  consider (both) "Q p" "P p" | (Q) "Q p" "¬ P p" | (nQ) "¬ Q p" by blast
  thus ?thesis
  proof cases
    case both thus ?thesis using p_restrict_equiv trans trans_left by metis
  next
    case Q thus ?thesis using p_restrict_equiv p_restrict_equiv0 trans trans_left by metis
  next
    case nQ thus ?thesis using p_restrict_equiv0 trans_left by metis
  qed
qed

lemma p_restrict_restrict_equiv: "p_equal p (p_restrict (p_restrict x P) P) (p_restrict x P)"
  using p_restrict_restrict_equiv_conj[of p x P P] by metis

lemma p_restrict_0_equiv0: "p_equal p (p_restrict 0 P) 0"
  by (metis p_restrict_equiv p_restrict_equiv0)

lemma p_restrict_add_equiv: "p_equal p (p_restrict (x + y) P) (p_restrict x P + p_restrict y P)"
  by (
    cases "P p", metis p_restrict_equiv sym add trans,
    metis p_restrict_equiv0 trans_left add_0_left
  )

lemma p_restrict_add_mixed_equiv:
  "p_equal p (p_restrict x P + p_restrict y Q) (x + y)" if "P p" and "Q p"
  using that p_restrict_equiv add by simp

lemma p_restrict_add_mixed_equiv_drop_right:
  "p_equal p (p_restrict x P + p_restrict y Q) x" if "P p" and "¬ Q p"
  using that p_restrict_equiv[of P p x] p_restrict_equiv0[of Q p y] add by fastforce

lemma p_restrict_add_mixed_equiv_drop_left:
  "p_equal p (p_restrict x P + p_restrict y Q) y" if "¬ P p" and "Q p"
  using that p_restrict_equiv[of Q p y] p_restrict_equiv0[of P p x] add by fastforce

lemma p_restrict_add_mixed_equiv_drop_both:
  "p_equal p (p_restrict x P + p_restrict y Q) 0" if "¬ P p" and "¬ Q p"
  using that p_restrict_equiv0[of P p x] p_restrict_equiv0[of Q p y] add by fastforce

lemma p_restrict_uminus_equiv: "p_equal p (p_restrict (-x) P) (- p_restrict x P)"
  by (
    cases "P p", metis p_restrict_equiv sym uminus trans,
    metis p_restrict_equiv0 uminus trans_left minus_zero
  )

lemma p_restrict_minus_equiv: "p_equal p (p_restrict (x - y) P) (p_restrict x P - p_restrict y P)"
  by (
    cases "P p", metis p_restrict_equiv sym minus trans,
    metis p_restrict_equiv0 minus trans_left diff_zero
  )

lemma p_restrict_minus_mixed_equiv:
  "p_equal p (p_restrict x P - p_restrict y Q) (x - y)" if "P p" and "Q p"
  using that p_restrict_equiv minus by simp

lemma p_restrict_minus_mixed_equiv_drop_right:
  "p_equal p (p_restrict x P - p_restrict y Q) x" if "P p" and "¬ Q p"
  using that p_restrict_equiv[of P p x] p_restrict_equiv0[of Q p y] minus by fastforce

lemma p_restrict_minus_mixed_equiv_drop_left:
  "p_equal p (p_restrict x P - p_restrict y Q) (-y)" if "¬ P p" and "Q p"
  using that p_restrict_equiv[of Q p y] p_restrict_equiv0[of P p x] minus by fastforce

lemma p_restrict_minus_mixed_equiv_drop_both:
  "p_equal p (p_restrict x P - p_restrict y Q) 0" if "¬ P p" and "¬ Q p"
  using that p_restrict_equiv0[of P p x] p_restrict_equiv0[of Q p y] minus by fastforce

lemma p_restrict_times_equiv:
  "p_equal p ((p_restrict x P) * (p_restrict y Q))
    (p_restrict (x * y) (λp. P p ∧ Q p))"
proof-
  consider (both) "P p" "Q p" | (P) "P p" "¬ Q p" | (nP) "¬ P p" by blast
  thus ?thesis
  proof cases
    case both thus ?thesis using p_restrict_equiv sym mult trans by metis
  next
    case P thus ?thesis
      using p_restrict_equiv p_restrict_equiv0 mult trans_left mult_zero_right by metis
  next
    case nP thus ?thesis
      using p_restrict_equiv p_restrict_equiv0 mult trans_left mult_zero_left by metis
  qed
qed

lemma p_restrict_times_equiv':
  "p_equal p ((p_restrict x P) * (p_restrict y P)) (p_restrict (x * y) P)"
  using p_restrict_times_equiv[of p x P y P] by simp

lemma p_restrict_p_equalI:
  "p_equal p (p_restrict x P) y"
  if  "P p ⟶ p_equal p x y"
  and "¬ P p ⟶ p_equal p y 0"
  by  (
    cases "P p", metis that(1) p_restrict_equiv trans, metis that(2) p_restrict_equiv0 trans_left
  )

lemma p_restrict_p_equal_p_restrictI:
  "p_equal p (p_restrict x P) (p_restrict y Q)"
  if  "(P p ∧ Q p)   ⟶ p_equal p x y"
  and "(P p ∧ ¬ Q p) ⟶ p_equal p x 0"
  and "(¬ P p ∧ Q p) ⟶ p_equal p y 0"
proof (cases "P p" "Q p" rule: case_split[case_product case_split])
  case True_True thus ?thesis using that(1) p_restrict_equiv sym cong by metis
next
  case True_False thus ?thesis using that(2) p_restrict_equiv p_restrict_equiv0 sym cong by metis
next
  case False_True thus ?thesis using that(3) p_restrict_equiv p_restrict_equiv0 sym cong by metis
next
  case False_False thus ?thesis using p_restrict_equiv0 refl cong by metis
qed

lemma p_restrict_p_equal_p_restrict_by_sameI:
  "p_equal p (p_restrict x P) (p_restrict y P)" if "P p ⟶ p_equal p x y"
  using that p_restrict_p_equal_p_restrictI by auto

end (* locale global_p_equality *)


locale global_p_equality_div_inv =
  p_equality_div_inv p_equal + global_p_equality p_equal p_restrict
  for p_equal    ::
    "'a ⇒ 'b::{comm_ring_1, inverse, divide_trivial} ⇒
      'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
begin

lemma inverse_p_restrict_equiv: "p_equal p (inverse (p_restrict x P)) (p_restrict (inverse x) P)"
  by (
    cases "p_equal p x 0 ∨ ¬ P p",
    metis p_restrict_equiv0_iff inverse_equiv0_iff trans_left,
    intro inverse_p_unique, metis p_restrict_times_equiv' p_restrict_equiv right_inverse_equiv trans
  )

end (* locale global_p_equality_div_inv *)


locale global_p_equal = global_p_equality
+ assumes global_imp_eq: "globally_p_equal x y ⟹ x = y"
begin

lemma global_eq_iff: "globally_p_equal x y ⟷ x = y"
  using global_imp_eq by fastforce

lemma p_restrict_true[simp] : "p_restrict x (λx. True) = x"
  using p_restrict_equiv[of "λx. True"] global_imp_eq by blast

lemma p_restrict_false[simp]: "p_restrict x (λx. False) = 0"
  using p_restrict_equiv0[of "λx. False"] global_imp_eq by blast

lemma p_restrict_restrict:
  "p_restrict (p_restrict x P) Q = p_restrict x (λp. P p ∧ Q p)"
  using p_restrict_restrict_equiv_conj global_imp_eq by blast

lemma p_restrict_restrict'[simp]: "p_restrict (p_restrict x P) P = p_restrict x P"
  using p_restrict_restrict by fastforce

lemma p_restrict_image_restrict: "p_restrict x P = x" if "x ∈ (λz. p_restrict z P) ` B"
proof-
  from that obtain z where "x = p_restrict z P" by blast
  thus ?thesis using p_restrict_restrict' by auto
qed

lemma p_restrict_zero: "p_restrict 0 P = 0"
  using p_restrict_0_equiv0 global_imp_eq by blast

lemma p_restrict_add: "p_restrict (x + y) P = p_restrict x P + p_restrict y P"
  using p_restrict_add_equiv global_imp_eq by blast

lemma p_restrict_uminus: "p_restrict (-x) P = - p_restrict x P"
  using p_restrict_uminus_equiv global_imp_eq by blast

lemma p_restrict_minus: "p_restrict (x - y) P = p_restrict x P - p_restrict y P"
  using p_restrict_minus_equiv global_imp_eq by blast

lemma p_restrict_times:
  "(p_restrict x P) * (p_restrict y Q) = p_restrict (x * y) (λp. P p ∧ Q p)"
  using p_restrict_times_equiv global_imp_eq by blast

lemma times_p_restrict: "x * (p_restrict y P) = p_restrict (x * y) P"
  using p_restrict_times[of x "λp. True"] by auto

lemmas p_restrict_pre_finite_adele_simps =
  p_restrict_zero p_restrict_add p_restrict_uminus p_restrict_minus p_restrict_times

lemma p_equal_0_iff_p_restrict_eq_0: "p_equal p x 0 ⟷ p_restrict x ((=) p) = 0"
proof (standard, rule global_imp_eq, standard)
  fix q show "p_equal p x 0 ⟹ p_equal q (p_restrict x ((=) p)) 0"
    using p_restrict_equiv[of "(=) p"] trans p_restrict_equiv0[of "(=) p"]
    by    (cases "p = q", blast, blast)
qed (metis (full_types) p_restrict_equiv_sym)

lemma p_equal_iff_p_restrict_eq:
  "p_equal p x y ⟷ p_restrict x ((=) p) = p_restrict y ((=) p)"
  using conv_0 p_equal_0_iff_p_restrict_eq_0 p_restrict_minus by auto

lemma p_restrict_eqI:
  "y = p_restrict x P"
  if      P: "⋀p. P p ⟹ p_equal p y x"
  and not_P: "⋀p. ¬ P p ⟹ p_equal p y 0"
proof (intro global_imp_eq, standard)
  fix p :: 'a show "p_equal p y (p_restrict x P)"
    by (cases "P p", metis P p_restrict_equiv trans_left, metis not_P p_restrict_equiv0 trans_left)
qed

lemma p_restrict_eq_p_restrict_mixedI:
  "p_restrict x P = p_restrict y Q"
  if  both: "⋀p::'a. P p ⟹ Q p ⟹ p_equal p x y"
  and P   : "⋀p::'a. P p ⟹ ¬ Q p ⟹ p_equal p x 0"
  and Q   : "⋀p::'a. ¬ P p ⟹ Q p ⟹ p_equal p y 0"
  by (
    intro p_restrict_eqI, metis both Q p_restrict_equiv trans p_restrict_equiv0 trans_left,
    metis P p_restrict_equiv trans p_restrict_equiv0
  )

lemma p_restrict_eq_p_restrictI:
  "p_restrict x P = p_restrict y P" if "⋀p::'a. P p ⟹ p_equal p x y"
  by (intro p_restrict_eqI, metis that trans p_restrict_equiv, simp add: p_restrict_equiv0)

lemma p_restrict_eq_p_restrict_iff:
  "p_restrict x P = p_restrict y P ⟷
    (∀p::'a. P p ⟶ p_equal p x y)"
  by (standard, safe, metis p_restrict_equiv trans_right, simp add: p_restrict_eq_p_restrictI)

lemma p_restrict_eq_zero_iff:
  "p_restrict x P = 0 ⟷ (∀p. P p ⟶ p_equal p x 0)"
proof-
  have "(p_restrict x P = 0) = (∀p. p_equal p (p_restrict x P) 0)"
    using global_imp_eq by auto
  thus ?thesis by (metis p_restrict_equiv p_restrict_equiv0 trans trans_right)
qed

lemma p_restrict_decomp:
  "x = p_restrict x P + p_restrict x (λp. ¬ P p)"
proof (intro global_imp_eq, standard)
  fix p show "p_equal p x (p_restrict x P + p_restrict x (λp. ¬ P p))"
    using p_restrict_add_mixed_equiv_drop_left p_restrict_add_mixed_equiv_drop_right sym by metis
qed

lemma restrict_complement:
  "range (λx. p_restrict x P) + range (λx. p_restrict x (λp. ¬ P p))
    = UNIV"
  using p_restrict_decomp[of _ P]
        set_plus_intro[of
          "p_restrict _ P" "range (λx. p_restrict x P)"
          "p_restrict _ (λp. ¬ P p)"
          "range (λx. p_restrict x (λp. ¬ P p))"
        ]
  by    fastforce

end (* locale global_p_equal *)


locale global_p_equal_no_zero_divisors =
  global_p_equal p_equal p_restrict + p_equality_no_zero_divisors p_equal
  for p_equal :: "'a ⇒ 'b::comm_ring ⇒ 'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"


locale global_p_equal_no_zero_divisors_1 =
  global_p_equal_no_zero_divisors p_equal p_restrict + p_equality_no_zero_divisors_1 p_equal
  for p_equal :: "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
begin

lemma pow_eq_0_iff: "x ^ n = 0 ⟷ x = 0 ∧ n ≠ 0" for x :: 'b
  using global_eq_iff pow_equiv_0_iff[of _ x n] by force

end (* locale global_p_equal_no_zero_divisors_1 *)


locale global_p_equal_div_inv =
  global_p_equality_div_inv p_equal p_restrict
+ global_p_equal p_equal p_restrict
  for p_equal    ::
    "'a ⇒ 'b::{comm_ring_1, inverse, divide_trivial} ⇒
      'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
begin

lemma power_int_eq_0_iff:
  "power_int x n = 0 ⟷ x = 0 ∧ n ≠ 0" for x :: 'b
  using global_eq_iff power_int_equiv_0_iff[of _ x n] by fastforce

lemma inverse_eq0_iff: "inverse x = 0 ⟷ x = 0" for x :: 'b
  using inverse_equiv0_iff global_eq_iff by fastforce

lemma inverse_neg_1 [simp]: "inverse (-1::'b) = -1"
  using global_imp_eq globally_inverse_neg_1 by force

lemma inverse_uminus: "inverse (-x) = - inverse x" for x :: 'b
  using global_imp_eq inverse_uminus_equiv by blast

lemma global_right_inverse: "x * inverse x = 1" if "∀p. ¬ p_equal p x 0"
  using that global_imp_eq right_inverse_equiv by fast

lemma right_inverse: "x * inverse x = p_restrict 1 (λp. ¬ p_equal p x 0)"
proof (intro global_imp_eq, standard)
  fix p :: 'a show "p_equal p (x * inverse x) (p_restrict 1 (λp. ¬ p_equal p x 0))"
  by (
    cases "p_equal p x 0", metis inverse_equiv0_iff mult_0_right p_restrict_equiv0 trans_left,
    metis right_inverse_equiv p_restrict_equiv trans_left
  )
qed

lemma global_left_inverse: "inverse x * x = 1" if "∀p. ¬ p_equal p x 0"
  using that global_imp_eq left_inverse_equiv by fast

lemma left_inverse: "inverse x * x = p_restrict 1 (λp. ¬ p_equal p x 0)"
  by (metis right_inverse mult.commute)

lemma inverse_unique: "inverse x = y" if "x * y = 1" for x y :: 'b
  using that inverse_p_unique global_imp_eq[of "inverse x" y] by fastforce

lemma inverse_p_restrict: "inverse (p_restrict x P) = p_restrict (inverse x) P"
  using global_imp_eq inverse_p_restrict_equiv by blast

lemma power_diff_conv_inverse:
  "x ^ (n - m) =  x ^ n * inverse x ^ m" if "m < n"
  for x :: 'b
proof (intro global_imp_eq, standard)
  fix p show "p_equal p (x ^ (n - m)) (x ^ n * inverse x ^ m)"
  proof (cases "p_equal p x 0")
    case True
    from that True have "p_equal p (x ^ n * inverse x ^ m) 0"
      using pow_equiv_0_iff inverse_equiv0_iff mult_0_left mult_0_right by force
    moreover from that True have "p_equal p (x ^ (n - m)) 0" using pow_equiv_0_iff by fastforce
    ultimately show ?thesis using trans_left by fast
  next
    case False with that show ?thesis using power_diff_conv_inverse_equiv by simp
  qed
qed

lemma power_int_add_1: "power_int x (m + 1) = power_int x m * x" if "m ≠ -1" for x :: 'b
  using that power_int_add_1_equiv by (auto intro: global_imp_eq)

lemma power_int_add:
  "power_int x (m + n) = power_int x m * power_int x n"
  if "(∀p. ¬ p_equal p x 0) ∨ m + n ≠ 0" for x :: 'b
  using that power_int_add_equiv by (auto intro: global_imp_eq)

lemma power_int_diff:
  "power_int x (m - n) = power_int x m / power_int x n" if "m ≠ n" for x :: 'b
  using that power_int_diff_equiv by (auto intro: global_imp_eq)

lemma power_int_minus_mult: "power_int x (n - 1) * x = power_int x n" if "n ≠ 0" for x :: 'b
  using that power_int_minus_mult_equiv by (auto intro: global_imp_eq)

lemma power_int_not_eq_zero:
  "x ≠ 0 ∨ n = 0 ⟹ power_int x n ≠ 0" for x :: 'b
  by (subst power_int_eq_0_iff) auto

lemma minus_divide_right: "a / (- b) = - (a / b)" for a b :: 'b
  using global_imp_eq minus_divide_right_equiv by blast

lemma minus_divide_divide: "(- a) / (- b) = a / b" for a b :: 'b
  using global_imp_eq minus_divide_divide_equiv by blast

lemma divide_minus1 [simp]: "x / (-1) = - x" for x :: 'b
  using global_imp_eq divide_minus1_equiv by blast

lemma divide_self: "x / x = p_restrict 1 (λp. ¬ p_equal p x 0)"
  by (metis divide_inverse right_inverse)

lemma global_divide_self: "x / x = 1" if "∀p. ¬ p_equal p x 0"
  by (metis that global_right_inverse divide_inverse)

lemma global_mult_divide_mult_cancel_right:
  "(a * b) / (c * b) = a / c" if "∀p. ¬ p_equal p b 0"
  using that global_imp_eq mult_divide_mult_cancel_right[of _ b a c] by fastforce

lemma global_mult_divide_mult_cancel_left:
  "(c * a) / (c * b) = a / b" if "∀p. ¬ p_equal p c 0"
  by (metis that global_mult_divide_mult_cancel_right mult.commute)

lemma divide_p_restrict_left: "(p_restrict x P) / y = p_restrict (x / y) P"
  using p_restrict_eqI[of P "(p_restrict x P) / y"] p_restrict_equiv[of P _ x]
        p_restrict_equiv0[of P _ x] divide_left_equiv
  by    fastforce

lemma divide_p_restrict_right: "x / (p_restrict y P) = p_restrict (x / y) P"
  using p_restrict_eqI[of P "x / (p_restrict y P)"] p_restrict_equiv[of P _ y]
        p_restrict_equiv0[of P _ y] divide_right_equiv
  by    fastforce

lemma inj_divide_right:
  "inj (λb. b / a) ⟷ (∀p. ¬ p_equal p a 0)"
  unfolding inj_def
proof (standard, safe)
  fix p
  assume  inj: "∀x y :: 'b. x / a = y / a ⟶ x = y"
    and   a  : "p_equal p a 0"
  from a have "(p_restrict 1 ((=) p)) / a = (p_restrict 0 ((=) p)) / a"
    by (simp add: p_restrict_eq_p_restrictI divide_equiv_0_iff divide_p_restrict_left)
  with inj show False using p_restrict_eq_p_restrict_iff one_p_nequal_zero by blast
next
  fix x y :: 'b
  assume a: "∀p. ¬ p_equal p a 0 " and xy: "x / a = y / a"
  thus "x = y"
    using times_divide_eq_right[of a x a] times_divide_eq_right[of a y a]
          mult_divide_cancel_left[of _ a x] mult_divide_cancel_left[of _ a y]
          cong global_imp_eq[of x y]
    by    fastforce
qed

end (* locale global_p_equal_div_inv *)


locale global_p_equality_depth = global_p_equality + p_equality_depth
begin

lemma globally_p_equal_p_depth: "globally_p_equal x y ⟹ p_depth p x = p_depth p y"
  using depth_equiv globally_p_equalD by simp

lemma p_restrict_depth:
  "P p ⟹ p_depth p (p_restrict x P) = p_depth p x"
  "¬ P p ⟹ p_depth p (p_restrict x P) = 0"
  by (metis p_restrict_equiv depth_equiv, metis p_restrict_equiv0 depth_equiv_0)

lemma p_restrict_add_mixed_depth_drop_right:
  "p_depth p (p_restrict x P + p_restrict y Q) = p_depth p x" if "P p" and "¬ Q p"
  using that p_restrict_add_mixed_equiv_drop_right depth_equiv by auto

lemma p_restrict_add_mixed_depth_drop_left:
  "p_depth p (p_restrict x P + p_restrict y Q) = p_depth p y" if "¬ P p" and "Q p"
  using that p_restrict_add_mixed_equiv_drop_left depth_equiv by auto

lemma p_depth_set_p_restrict:
  "p_restrict x P ∈ p_depth_set p n" if "P p ⟶ x ∈ p_depth_set p n"
proof (rule p_depth_set_by_equivI)
  show "p_equal p (p_restrict x P) (if P p then x else 0)"
    using p_restrict_equiv p_restrict_equiv0 by simp
  from that show "(if P p then x else 0) ∈ p_depth_set p n"
    using p_depth_set_0 by auto
qed

lemma global_depth_set_p_restrict:
  "p_restrict x P ∈ global_depth_set n" if "x ∈ global_depth_set n"
  using that p_depth_set_p_restrict global_depth_set by auto

lemma p_depth_set_closed_under_p_restrict_image:
  "(λx. p_restrict x P) ` p_depth_set p n ⊆ p_depth_set p n"
  using p_depth_set_p_restrict by blast

lemma global_depth_set_closed_under_p_restrict_image:
  "(λx. p_restrict x P) ` global_depth_set n ⊆ global_depth_set n"
  using global_depth_set_p_restrict by blast

lemma global_depth_set_p_restrictI:
  "p_restrict x P ∈ global_depth_set n"
  if "⋀p. P p ⟹ x ∈ p_depth_set p n"
  by (
    intro global_depth_setI,
    metis that p_restrict_equiv p_restrict_equiv0 trans p_depth_setD p_restrict_depth(1)
  )

lemma p_depth_set_image_under_one_p_restrict_image:
  "(λx. p_restrict x ((=) p)) ` p_depth_set p n ⊆ global_depth_set n"
  using global_depth_set_p_restrictI by force

end (* locale global_p_equality_depth *)


locale global_p_equality_depth_no_zero_divisors_1 =
  p_equality_depth_no_zero_divisors_1 p_equal p_depth
+ global_p_equality_depth p_equal p_restrict p_depth
  for p_equal    ::
    "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and p_depth    :: "'a ⇒ 'b ⇒ int"


locale global_p_equality_depth_div_inv =
  p_equality_depth_div_inv + global_p_equality_depth
begin

sublocale global_p_equality_div_inv ..

lemma global_depth_set_inverse:
  "p_restrict (inverse x) (λp. p_depth p x = 0) ∈ global_depth_set 0"
  using global_depth_set_p_restrictI p_depth_set_inverse by simp

lemma global_depth_set_divide:
  "p_restrict (x / y) (λp. p_depth p y = 0) ∈ global_depth_set n"
  if "x ∈ global_depth_set n"
  using that global_depth_set_p_restrictI global_depth_set p_depth_set_divide by auto

lemma global_depth_set_divideI:
  "p_restrict (x / y) (λp. p_depth p y = 0) ∈ global_depth_set n"
  if "⋀p. p_depth p y = 0 ⟹ x ∈ p_depth_set p n"
  using that global_depth_set_p_restrictI global_depth_set p_depth_set_divide by auto

end


locale global_p_equal_depth = global_p_equal + global_p_equality_depth
begin

lemma p_depth_set_vs_global_depth_set_image_under_one_p_restrict_image:
  "(λx. p_restrict x ((=) p)) ` p_depth_set p n =
    (λx. p_restrict x ((=) p)) `global_depth_set n"
proof (standard, standard, clarify)
  fix x assume "x ∈ p_depth_set p n"
  hence "p_restrict x ((=) p) ∈ global_depth_set n"
    using p_depth_set_image_under_one_p_restrict_image by fast
  thus "p_restrict x ((=) p) ∈ (λx. p_restrict x ((=) p)) `global_depth_set n"
    using p_restrict_restrict'[of x "(=) p", symmetric] by blast
qed (use global_depth_set in fast)

end

locale global_p_equal_depth_no_zero_divisors =
  global_p_equal_no_zero_divisors + p_equality_depth_no_zero_divisors
begin
sublocale global_p_equal_depth ..
end


locale global_p_equal_depth_div_inv =
  global_p_equality_depth_div_inv + global_p_equal_depth_no_zero_divisors
begin

sublocale global_p_equal_div_inv ..

lemma p_depth_set_eq_coset:
  "p_depth_set p n = (w powi n) *o (p_depth_set p 0)"
  if "p_depth p w = 1" and "∀p. ¬ p_equal p w 0"
  unfolding elt_set_times_def
proof safe
  fix x assume "x ∈ p_depth_set p n"
  moreover define y where "y ≡ w powi (-n) * x"
  ultimately have "y ∈ p_depth_set p 0"
    using that(1) mult_0_right p_depth_setD depth_mult_additive depth_powi_additive
    by    (intro p_depth_setI, clarify, fastforce)
  moreover from y_def have "x = w powi n * y"
    using that(2) power_int_equiv_0_iff global_right_inverse power_int_minus
    by    (force simp flip: mult.assoc)
  ultimately show "∃y∈p_depth_set p 0. x = w powi n * y" by metis
next
  fix x assume "x ∈ p_depth_set p 0"
  thus "w powi n * x ∈ p_depth_set p n"
    using that(1) mult_0_right p_depth_setD depth_mult_additive depth_powi_additive
    by    (intro p_depth_setI, clarify, fastforce)
qed

lemma global_depth_set_eq_coset:
  "global_depth_set n = (w powi n) *o (global_depth_set 0)" if "∀p. p_depth p w = 1"
  unfolding elt_set_times_def
proof safe
  fix x assume x: "x ∈ global_depth_set n"
  define y where "y ≡ w powi (-n) * x"
  from that have "∀p. ¬ p_equal p w 0" using depth_equiv_0 by fastforce
  with y_def have "x = w powi n * y"
    using power_int_equiv_0_iff global_right_inverse power_int_minus mult.assoc mult_1_left by metis
  moreover from x y_def have "y ∈ global_depth_set 0"
    using that mult_0_right global_depth_setD depth_mult_additive depth_powi_additive
    by    (intro global_depth_setI, fastforce)
  ultimately show "∃y∈global_depth_set 0. x = w powi n * y" by metis
next
  fix x assume "x ∈ global_depth_set 0"
  thus "w powi n * x ∈ global_depth_set n"
    using that mult_0_right global_depth_setD depth_mult_additive depth_powi_additive
    by    (intro global_depth_setI, fastforce)
qed

lemma p_depth_set_eq_coset':
  "p_depth_set p 0 = (w powi (-n)) *o (p_depth_set p n)"
  if "p_depth p w = 1" and "∀p. ¬ p_equal p w 0"
proof-
  from that(2) have "w powi (-n) * w powi n = 1"
    using power_int_minus power_int_equiv_0_iff global_left_inverse by simp
  with that show ?thesis
    using p_depth_set_eq_coset set_times_rearrange2 power_int_minus set_one_times by metis
qed

lemma global_depth_set_eq_coset':
  "global_depth_set 0 = (w powi (-n)) *o (global_depth_set n)" if "∀p. p_depth p w = 1"
proof-
  from that have "∀p. ¬ p_equal p w 0" using depth_equiv_0 by fastforce
  hence "w powi (-n) * w powi n = 1"
    using power_int_minus power_int_equiv_0_iff global_left_inverse by presburger
  with that show ?thesis
    using global_depth_set_eq_coset set_times_rearrange2 power_int_minus set_one_times by metis
qed

end (* locale global_p_equal_depth_div_inv *)


subsubsection ‹Embedding of base type constants›

locale global_p_equality_w_consts = global_p_equality p_equal p_restrict
  for p_equal    ::
    "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
+
  fixes func_of_consts :: "('a ⇒ 'c::ring_1) ⇒ 'b"
  assumes consts_1    [simp]: "func_of_consts 1 = 1"
    and   consts_diff [simp]: "func_of_consts (f - g) = func_of_consts f - func_of_consts g"
    and   consts_mult [simp]:
      "func_of_consts (f * g) = func_of_consts f * func_of_consts g"
begin

abbreviation "consts ≡ func_of_consts"
abbreviation "const a ≡ consts (λp. a)"

lemma consts_0[simp]: "consts 0 = 0"
  using consts_diff[of 0 0] by force

lemma const_0[simp]: "const 0 = 0"
  using consts_0 unfolding zero_fun_def by simp

lemma const_1[simp]: "const 1 = 1"
  using consts_1 unfolding one_fun_def by simp

lemma consts_uminus [simp]: "consts (- f) = - consts f"
  using consts_diff[of 0 f] by fastforce

lemma const_uminus [simp]: "const (-a) = - const a"
  using consts_uminus unfolding fun_Compl_def by auto

lemma const_diff [simp]: "const (a - b) = const a - const b"
  using consts_diff unfolding fun_diff_def by auto

lemma consts_add [simp]: "consts (f + g) = consts f + consts g"
proof-
  have "consts f + consts g = consts (f - (-g))" by (simp flip: diff_minus_eq_add)
  thus ?thesis by simp
qed

lemma const_add [simp]: "const (a + b) = const a + const b"
  using consts_add unfolding plus_fun_def by auto

lemma const_mult [simp]: "const (a * b) = const a * const b"
  using consts_mult unfolding times_fun_def by auto

lemma const_of_nat: "const (of_nat n) = of_nat n"
  by (induct n) simp_all

lemma const_of_int: "const (of_int z) = of_int z"
  by (cases z rule: int_cases2, simp_all add: const_of_nat)

end (* locale global_p_equality_w_consts *)


locale global_p_equal_w_consts =
  global_p_equal p_equal p_restrict
+ global_p_equality_w_consts p_equal p_restrict func_of_consts
  for p_equal ::
    "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and func_of_consts :: "('a ⇒ 'c::ring_1) ⇒ 'b"


locale global_p_equality_w_inj_consts = global_p_equality_w_consts
+
  assumes p_equal_func_of_consts_0: "p_equal p (consts f) 0 ⟷ f p = 0"
begin

lemmas p_equal_func_of_const_0 = p_equal_func_of_consts_0[of _ "λp. _"]

lemma p_equal_func_of_consts:
  "p_equal p (consts f) (consts g) ⟷ f p = g p"
  by (metis conv_0 consts_diff p_equal_func_of_consts_0 fun_diff_def right_minus_eq)

lemma globally_p_equal_func_of_consts:
  "globally_p_equal (func_of_consts f) (func_of_consts g) ⟷
    (∀p. f p = g p)"
  using p_equal_func_of_consts unfolding globally_p_equal_def by auto

lemma const_p_equal: "p_equal p (const a) (const b) ⟹ a = b"
  using p_equal_func_of_consts by force

end (* locale global_p_equality_w_inj_consts *)


locale global_p_equality_w_inj_consts_char_0 =
  global_p_equality_w_inj_consts p_equal p_restrict func_of_consts
  for p_equal        ::
    "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict     :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and func_of_consts :: "('a ⇒ 'c::ring_char_0) ⇒ 'b"
begin

lemma const_of_nat_p_equal_0_iff: "p_equal p (of_nat n) 0 ⟷ n = 0"
  by (metis const_of_nat p_equal_func_of_const_0 of_nat_eq_0_iff)

lemma const_of_int_p_equal_0_iff: "p_equal p (of_int z) 0 ⟷ z = 0"
  by (metis const_of_int of_int_eq_0_iff p_equal_func_of_const_0)

end (* locale global_p_equality_w_inj_consts_char_0 *)


locale global_p_equality_div_inv_w_inj_consts =
  p_equality_div_inv + global_p_equality_w_inj_consts
begin

lemma consts_divide_self_equiv: "p_equal p ((consts f) / (consts f)) 1" if "f p ≠ 0"
  using that
  by    (simp add: p_equal_func_of_consts divide_self_equiv flip: consts_0)

lemma const_divide_self_equiv: "p_equal p ((const c) / (const c)) 1" if "c ≠ 0"
  using that by (simp add: consts_divide_self_equiv)

end (* locale global_p_equality_div_inv_w_consts *)


locale global_p_equal_w_inj_consts =
  global_p_equal p_equal p_restrict
+ global_p_equality_w_inj_consts p_equal p_restrict
  for p_equal    ::
    "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
begin

lemma consts_eq_iff: "consts f = consts g ⟷ f = g"
  using global_eq_iff globally_p_equal_func_of_consts by blast

lemma consts_eq_0_iff: "consts f = 0 ⟷ f = 0"
  using consts_eq_iff by force

lemma inj_consts: "inj consts"
  using consts_eq_iff injI by meson

lemma const_eq_iff: "const a = const b ⟷ a = b"
  by (metis consts_eq_iff)

lemma const_eq_0_iff: "const a = 0 ⟷ a = 0"
  using consts_eq_0_iff unfolding zero_fun_def by metis

lemma inj_const: "inj const"
  using const_eq_iff injI by meson

end (* locale global_p_equal_w_inj_consts *)


locale global_p_equal_div_inv_w_inj_consts =
  global_p_equal_div_inv + global_p_equal_w_inj_consts
begin

sublocale global_p_equality_div_inv_w_inj_consts ..

lemma consts_divide_self:
  "(consts f) / (consts f) = p_restrict 1 (λp::'a. f p ≠ 0)"
  by (simp add: p_equal_func_of_consts_0 divide_self)

lemma const_right_inverse [simp]: "const a * inverse (const a) = 1" if "a ≠ 0"
  using that global_right_inverse p_equal_func_of_const_0 by blast

lemma const_left_inverse [simp]: "inverse (const a) * const a = 1" if "a ≠ 0"
  by (metis that const_right_inverse mult.commute)

lemma const_divide_self: "(const c) / (const c) = 1" if "c ≠ 0"
  using that by (simp add: divide_inverse)

lemma mult_const_divide_mult_const_cancel_right:
  "(y * const a) / (z * const a) = y / z" if "a ≠ 0"
  using that global_mult_divide_mult_cancel_right p_equal_func_of_const_0 by blast

lemma mult_const_divide_mult_const_cancel_left:
  "(const a * y) / (const a * z) = y / z" if "a ≠ 0"
  by (metis that mult_const_divide_mult_const_cancel_right mult.commute)

lemma mult_const_divide_mult_const_cancel_left_right:
  "(const a * y) / (z * const a) = y / z" if "a ≠ 0"
  by (metis that mult.commute mult_const_divide_mult_const_cancel_left)

lemma mult_const_divide_mult_const_cancel_right_left:
  "(y * const a) / (const a * z) = y / z" if "a ≠ 0"
  by (metis that mult.commute mult_const_divide_mult_const_cancel_left)

end (* locale global_p_equal_div_inv_w_consts *)


locale global_p_equal_div_inv_w_inj_consts_char_0 =
  global_p_equality_w_inj_consts_char_0 p_equal p_restrict func_of_consts
+ global_p_equal_div_inv_w_inj_consts p_equal p_restrict func_of_consts
  for p_equal        ::
    "'a ⇒ 'b::{comm_ring_1, ring_char_0, inverse, divide_trivial} ⇒
      'b ⇒ bool"
  and p_restrict     :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and func_of_consts :: "('a ⇒ 'c::ring_char_0) ⇒ 'b"
begin

context
  fixes n :: nat
  assumes "n ≠ 0"
begin

lemma left_inverse_const_of_nat[simp]: "inverse (of_nat n :: 'b) * of_nat n = 1"
  by (metis ‹n ≠ 0› const_of_nat const_left_inverse of_nat_eq_0_iff)

lemma right_inverse_const_of_nat[simp]: "of_nat n * inverse (of_nat n :: 'b) = 1"
  by (metis left_inverse_const_of_nat mult.commute)

lemma divide_self_const_of_nat[simp]: "(of_nat n :: 'b) / of_nat n = 1"
  by (metis ‹n ≠ 0› of_nat_eq_0_iff const_of_nat const_divide_self)

lemma mult_const_of_nat_divide_const_mult_of_nat_cancel_right:
  "(a * of_nat n) / (b * of_nat n) = a / b" for a b :: 'b
  using ‹n ≠ 0› const_of_nat of_nat_eq_0_iff
        mult_const_divide_mult_const_cancel_right
  by    metis

lemma mult_const_of_nat_divide_const_mult_of_nat_cancel_left:
  "(of_nat n * a) / (of_nat n * b) = a / b" for a b :: 'b
  by (metis mult_const_of_nat_divide_const_mult_of_nat_cancel_right mult.commute)

end (* context nonzero nat *)

context
  fixes z :: int
  assumes "z ≠ 0"
begin

lemma left_inverse_const_of_int[simp]: "inverse (of_int z :: 'b) * of_int z = 1"
  by (metis ‹z ≠ 0› const_of_int const_left_inverse of_int_eq_0_iff)

lemma right_inverse_const_of_int[simp]: "of_int z * inverse (of_int z :: 'b) = 1"
  by (metis left_inverse_const_of_int mult.commute)

lemma divide_self_const_of_int[simp]: "(of_int z :: 'b) / of_int z = 1"
  by (metis ‹z ≠ 0› of_int_eq_0_iff const_of_int const_divide_self)

lemma mult_const_of_int_divide_const_mult_of_int_cancel_right:
  "(a * of_int z) / (b * of_int z) = a / b" for a b :: 'b
  by (
    metis ‹z ≠ 0› const_of_int of_int_eq_0_iff
          mult_const_divide_mult_const_cancel_right
  )

lemma mult_const_of_int_divide_const_mult_of_int_cancel_left:
  "(of_int z * a) / (of_int z * b) = a / b" for a b :: 'b
  by (metis mult_const_of_int_divide_const_mult_of_int_cancel_right mult.commute)

end (* context nonzero int *)

context
  includes rat.lifting
begin

lift_definition const_of_rat :: "rat ⇒ 'b"
  is "λx. of_int (fst x) / of_int (snd x)"
  unfolding ratrel_def
proof (clarify, unfold fst_conv snd_conv)
  fix a b c d :: int
  assume ratrel: "b ≠ 0" "d ≠ 0" "a * d = c * b"
  define oi :: "int ⇒ 'b" where "oi ≡ of_int"
  moreover from this ratrel(1,3) have "(oi a / oi b) * (oi d / oi d) = oi c / oi d"
    by (metis of_int_mult times_divide_eq_right divide_self_const_of_int mult_1_right mult.commute)
  ultimately show "oi a / oi b = oi c / oi d" using ratrel(2) by fastforce
qed

lemma inj_const_of_rat: "inj const_of_rat"
proof
  fix x y show "const_of_rat x = const_of_rat y ⟹ x = y"
  proof (transfer, clarify, unfold ratrel_iff fst_conv snd_conv, clarify)
    fix a b c d :: int
    define oi :: "int ⇒ 'b" where "oi ≡ of_int"
    assume ratrel: "b ≠ 0" "d ≠ 0" "oi a / oi b = oi c / oi d"
    from oi_def ratrel(1,3) have "oi a * oi d = (oi d / oi d) * oi c * oi b"
      by (metis swap_numerator divide_self_const_of_int mult_1_right mult.assoc mult.commute)
    with oi_def ratrel(2) show "a * d = c * b" using of_int_eq_iff by fastforce
  qed
qed

lemma const_of_rat_rat: "const_of_rat (Rat.Fract a b) = (of_int a :: 'b) / of_int b"
  by transfer simp

lemma const_of_rat_0 [simp]: "const_of_rat 0 = 0"
  by transfer simp

lemma const_of_rat_1 [simp]: "const_of_rat 1 = 1"
  by transfer simp

lemma const_of_rat_minus: "const_of_rat (- a) = - const_of_rat a"
  by (transfer, simp add: minus_divide_left)

lemma const_of_rat_add: "const_of_rat (a + b) = const_of_rat a + const_of_rat b"
proof (transfer, clarify, unfold fst_conv snd_conv of_int_add of_int_mult)
  fix a b c d :: int
  assume b: "b ≠ 0" and d: "d ≠ 0"
  define w x y z :: 'b
    where "w ≡ of_int a" and "x ≡ of_int b"
    and   "y ≡ of_int c" and "z ≡ of_int d"
  from d z_def have "(w * z + y * x) / (x * z) = w / x + (y * x) / (x * z)"
    by (
      metis add_divide_distrib mult_const_of_int_divide_const_mult_of_int_cancel_right
    )
  with b x_def show "(w * z + y * x) / (x * z) = w / x + y / z"
    by (metis mult.commute mult_const_of_int_divide_const_mult_of_int_cancel_right)
qed

lemma const_of_rat_mult: "const_of_rat (a * b) = const_of_rat a * const_of_rat b"
  by (transfer, simp, metis times_divide_times_eq)

lemma const_of_rat_p_equal_0_iff: "p_equal p (const_of_rat a) 0 ⟷ a = 0"
  by (transfer fixing: p_equal p, simp, metis divide_equiv_0_iff const_of_int_p_equal_0_iff)

end (* context rat.lifting *)

lemma const_of_rat_eq_0_iff [simp]: "const_of_rat a = 0 ⟷ a = 0"
  using const_of_rat_p_equal_0_iff global_eq_iff by fastforce

lemma const_of_rat_neg_one [simp]: "const_of_rat (- 1) = -1"
  by (simp add: const_of_rat_minus)

lemma const_of_rat_diff: "const_of_rat (a - b) = const_of_rat a - const_of_rat b"
  using const_of_rat_add[of a "-b"] by (simp add: const_of_rat_minus)

lemma const_of_rat_sum: "const_of_rat (∑a∈A. f a) = (∑a∈A. const_of_rat (f a))"
  by (induct rule: infinite_finite_induct) (auto simp: const_of_rat_add)

lemma const_of_rat_prod: "const_of_rat (∏a∈A. f a) = (∏a∈A. const_of_rat (f a))"
  by (induct rule: infinite_finite_induct) (auto simp: const_of_rat_mult)

lemma const_of_rat_inverse: "const_of_rat (inverse a) = inverse (const_of_rat a)"
  by (cases "a = 0", simp, rule inverse_unique[symmetric], simp flip: const_of_rat_mult)

lemma left_inverse_const_of_rat[simp]:
  "inverse (const_of_rat a) * const_of_rat a = 1" if "a ≠ 0"
  by (metis that const_of_rat_inverse const_of_rat_mult Fields.left_inverse const_of_rat_1)

lemma right_inverse_const_of_rat[simp]:
  "const_of_rat a * inverse (const_of_rat a) = 1" if "a ≠ 0"
  by (metis that left_inverse_const_of_rat mult.commute)

lemma const_of_rat_divide: "const_of_rat (a / b) = const_of_rat a / const_of_rat b"
  by (metis Fields.divide_inverse const_of_rat_mult const_of_rat_inverse divide_inverse)

lemma divide_self_const_of_rat[simp]: "(const_of_rat a) / (const_of_rat a) = 1" if "a ≠ 0"
  by (metis that divide_inverse right_inverse_const_of_rat)

lemma const_of_rat_power: "const_of_rat (a ^ n) = (const_of_rat a) ^ n"
  by (induct n) (simp_all add: const_of_rat_mult)

lemma const_of_rat_eq_iff [simp]: "const_of_rat a = const_of_rat b ⟷ a = b"
  by (metis inj_const_of_rat inj_def)

lemma zero_eq_const_of_rat_iff [simp]: "0 = const_of_rat a ⟷ 0 = a"
  by simp

lemma const_of_rat_eq_1_iff [simp]: "const_of_rat a = 1 ⟷ a = 1"
  using const_of_rat_eq_iff [of _ 1] by simp

lemma one_eq_const_of_rat_iff [simp]: "1 = const_of_rat a ⟷ 1 = a"
  by simp

text ‹Collapse nested embeddings.›
lemma const_of_rat_of_nat_eq [simp]: "const_of_rat (of_nat n) = of_nat n"
  by (induct n) (simp_all add: const_of_rat_add)

lemma const_of_rat_of_int_eq [simp]: "const_of_rat (of_int z) = of_int z"
  by (cases z rule: int_diff_cases) (simp add: const_of_rat_diff)

text ‹Product of all p-adic embeddings of the field of rationals.›
definition range_const_of_rat :: "'b set" ("ℚ⇩∀⇩p")
  where "ℚ⇩∀⇩p = range const_of_rat"

lemma range_const_of_rat_cases [cases set: range_const_of_rat]:
  assumes "q ∈ ℚ⇩∀⇩p"
  obtains (const_of_rat) r where "q = const_of_rat r"
proof -
  from assms have "q ∈ range const_of_rat" by (simp only: range_const_of_rat_def)
  then obtain r where "q = const_of_rat r" ..
  then show thesis ..
qed

lemma range_const_of_rat_cases':
  assumes "x ∈ ℚ⇩∀⇩p"
  obtains a b where "b > 0" "coprime a b" "x = of_int a / of_int b"
proof -
  from assms obtain r where "x = const_of_rat r"
    by (auto simp: range_const_of_rat_def)
  obtain a b where quot: "quotient_of r = (a,b)" by force
  have "b > 0" using quotient_of_denom_pos[OF quot] .
  moreover have "coprime a b" using quotient_of_coprime[OF quot] .
  moreover have "x = of_int a / of_int b" unfolding ‹x = const_of_rat r›
      quotient_of_div[OF quot] by (simp add: const_of_rat_divide)
  ultimately show ?thesis using that by blast
qed

lemma range_const_of_rat_of_rat [simp]: "const_of_rat r ∈ ℚ⇩∀⇩p"
  by (simp add: range_const_of_rat_def)

lemma range_const_of_rat_of_int [simp]: "of_int z ∈ ℚ⇩∀⇩p"
  by (subst const_of_rat_of_int_eq [symmetric]) (rule range_const_of_rat_of_rat)

lemma Ints_subset_range_const_of_rat: "ℤ ⊆ ℚ⇩∀⇩p"
  using Ints_cases range_const_of_rat_of_int by blast

lemma range_const_of_rat_of_nat [simp]: "of_nat n ∈ ℚ⇩∀⇩p"
  by (subst const_of_rat_of_nat_eq [symmetric]) (rule range_const_of_rat_of_rat)

lemma Nats_subset_range_const_of_rat: "ℕ ⊆ ℚ⇩∀⇩p"
  using Ints_subset_range_const_of_rat Nats_subset_Ints by blast

lemma range_const_of_rat_0 [simp]: "0 ∈ ℚ⇩∀⇩p"
  unfolding range_const_of_rat_def by (rule range_eqI, rule const_of_rat_0 [symmetric])

lemma range_const_of_rat_1 [simp]: "1 ∈ ℚ⇩∀⇩p"
  unfolding range_const_of_rat_def by (rule range_eqI, rule const_of_rat_1 [symmetric])

lemma range_const_of_rat_add [simp]:
  "a ∈ ℚ⇩∀⇩p ⟹
    b ∈ ℚ⇩∀⇩p ⟹
    a + b ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_cases range_const_of_rat_of_rat const_of_rat_add)

lemma range_const_of_rat_minus_iff [simp]:
  "- a ∈ ℚ⇩∀⇩p ⟷
    a ∈ ℚ⇩∀⇩p"
  by (
    metis range_const_of_rat_cases range_const_of_rat_of_rat add.inverse_inverse
          const_of_rat_minus
  )

lemma range_const_of_rat_diff [simp]:
  "a ∈ ℚ⇩∀⇩p ⟹
    b ∈ ℚ⇩∀⇩p ⟹
    a - b ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_add range_const_of_rat_minus_iff diff_conv_add_uminus)

lemma range_const_of_rat_mult [simp]:
  "a ∈ ℚ⇩∀⇩p ⟹
    b ∈ ℚ⇩∀⇩p ⟹
    a * b ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_cases range_const_of_rat_of_rat const_of_rat_mult)

lemma range_const_of_rat_inverse [simp]:
  "a ∈ ℚ⇩∀⇩p ⟹
    inverse a ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_cases range_const_of_rat_of_rat const_of_rat_inverse)

lemma range_const_of_rat_divide [simp]:
  "a ∈ ℚ⇩∀⇩p ⟹
    b ∈ ℚ⇩∀⇩p ⟹
    a / b ∈ ℚ⇩∀⇩p"
  by (simp add: divide_inverse)

lemma range_const_of_rat_power [simp]:
  "a ∈ ℚ⇩∀⇩p ⟹
    a ^ n ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_cases range_const_of_rat_of_rat const_of_rat_power)

lemma range_const_of_rat_sum [intro]:
  "(⋀x. x ∈ A ⟹ f x ∈ ℚ⇩∀⇩p) ⟹
    sum f A ∈ ℚ⇩∀⇩p"
  by (induction A rule: infinite_finite_induct) auto

lemma range_const_of_rat_prod [intro]:
  "(⋀x. x ∈ A ⟹ f x ∈ ℚ⇩∀⇩p)
    ⟹ prod f A ∈ ℚ⇩∀⇩p"
  by (induction A rule: infinite_finite_induct) auto

lemma range_const_of_rat_induct [case_names const_of_rat, induct set: range_const_of_rat]:
  "q ∈ ℚ⇩∀⇩p ⟹
    (⋀r. P (const_of_rat r)) ⟹ P q"
  by (rule range_const_of_rat_cases) auto

lemma p_adic_Rats_p_equal_0_iff:
  "a ∈ ℚ⇩∀⇩p ⟹
    p_equal p a 0 ⟷ a = 0"
  by (induct a rule: range_const_of_rat_induct, simp, rule const_of_rat_p_equal_0_iff)

lemma range_const_of_rat_infinite: "¬ finite ℚ⇩∀⇩p"
  by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 range_const_of_rat_def)

lemma left_inverse_range_const_of_rat:
  "a ∈ ℚ⇩∀⇩p ⟹ a ≠ 0 ⟹
    inverse a * a = 1"
  by (
    induct a rule: range_const_of_rat_induct, rule left_inverse_const_of_rat,
    simp add: const_of_rat_p_equal_0_iff
  )

lemma right_inverse_range_const_of_rat:
  "a ∈ ℚ⇩∀⇩p ⟹ a ≠ 0 ⟹
    a * inverse a = 1"
  by (metis left_inverse_range_const_of_rat mult.commute)

lemma divide_self_range_const_of_rat:
  "a ∈ ℚ⇩∀⇩p ⟹ a ≠ 0 ⟹
    a / a = 1"
  by (metis divide_inverse right_inverse_range_const_of_rat)

lemma range_const_of_rat_add_iff:
  "a ∈ ℚ⇩∀⇩p ∨
    b ∈ ℚ⇩∀⇩p ⟹
    a + b ∈ ℚ⇩∀⇩p ⟷
      a ∈ ℚ⇩∀⇩p ∧ b ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_add range_const_of_rat_diff add_diff_cancel add_diff_cancel_left')

lemma range_const_of_rat_diff_iff:
  "a ∈ ℚ⇩∀⇩p ∨
    b ∈ ℚ⇩∀⇩p ⟹
      a - b ∈ ℚ⇩∀⇩p ⟷
      a ∈ ℚ⇩∀⇩p ∧ b ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_add_iff diff_add_cancel)

lemma range_const_of_rat_mult_iff:
  "a * b ∈ ℚ⇩∀⇩p ⟷
    a ∈ ℚ⇩∀⇩p ∧ b ∈ ℚ⇩∀⇩p"
  if
    "a ∈ ℚ⇩∀⇩p - {0} ∨
      b ∈ ℚ⇩∀⇩p - {0}"
proof-
  have *:
    "⋀a b :: 'b.
      a ∈ ℚ⇩∀⇩p - {0} ⟹
      a * b ∈ ℚ⇩∀⇩p ⟷
        b ∈ ℚ⇩∀⇩p"
  proof
    fix a b :: 'b
    assume  "a ∈ ℚ⇩∀⇩p - {0}"
      and   "a * b ∈ ℚ⇩∀⇩p"
    thus "b ∈ ℚ⇩∀⇩p"
      using range_const_of_rat_mult[of "inverse a"] left_inverse_range_const_of_rat[of a]
      by    (fastforce simp flip: mult.assoc)
  qed simp
  show ?thesis
  proof (cases "a ∈ ℚ⇩∀⇩p - {0}")
    case True thus ?thesis using *[of a b] by fast
  next
    case False
    with that have "b ∈ ℚ⇩∀⇩p - {0}" by blast
    moreover from this have
      "a * b ∈ ℚ⇩∀⇩p ⟷
        a ∈ ℚ⇩∀⇩p"
      by (metis * mult.commute)
    ultimately show ?thesis by blast
  qed
qed

lemma range_const_of_rat_inverse_iff [simp]:
  "inverse a ∈ ℚ⇩∀⇩p ⟷
    a ∈ ℚ⇩∀⇩p"
  by (metis range_const_of_rat_inverse inverse_inverse)

lemma range_const_of_rat_divide_iff:
  "a / b ∈ ℚ⇩∀⇩p ⟷
      a ∈ ℚ⇩∀⇩p ∧ b ∈ ℚ⇩∀⇩p"
  if
    "a ∈ ℚ⇩∀⇩p - {0} ∨
      b ∈ ℚ⇩∀⇩p - {0}"
  using that range_const_of_rat_inverse inverse_inverse[of b] range_const_of_rat_inverse_iff
        divide_inverse[of a b] range_const_of_rat_mult_iff[of a "inverse b"]
  by    force

end (* locale global_p_equal_div_inv_w_inj_consts_char_0 *)

lemma Fract_eq0_iff: "Fraction_Field.Fract a b = 0 ⟷ a = 0 ∨ b = 0"
  by transfer simp

locale global_p_equal_div_inv_w_inj_idom_consts =
  global_p_equal_div_inv_w_inj_consts p_equal p_restrict func_of_consts
+ global_p_equality_w_inj_consts p_equal p_restrict func_of_consts
  for p_equal        ::
    "'a ⇒ 'b::{comm_ring_1, inverse, divide_trivial} ⇒
      'b ⇒ bool"
  and p_restrict     :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and func_of_consts :: "('a ⇒ 'c::idom) ⇒ 'b"
begin

lift_definition const_of_fract :: "'c fract ⇒ 'b"
  is "λx::'c × 'c. const (fst x) / const (snd x)"
proof (clarify, unfold fractrel_iff fst_conv snd_conv, clarify)
  fix a b c d :: 'c
  assume fractrel: "b ≠ 0" "d ≠ 0" "a * d = c * b"
  from fractrel(1,3) have "(const a / const b) * (const d / const d) = const c / const d"
    by (metis const_mult times_divide_eq_right const_divide_self mult_1_right swap_numerator)
  with fractrel(2) show "const a / const b = const c / const d"
    using const_divide_self by fastforce
qed

lemma inj_const_of_fract: "inj const_of_fract"
proof
  fix x y show "const_of_fract x = const_of_fract y ⟹ x = y"
  proof (transfer, clarify, unfold fractrel_iff fst_conv snd_conv, clarify)
    fix a b c d :: 'c
    assume fractrel: "b ≠ 0" "d ≠ 0" "const a / const b = const c / const d"
    from fractrel(1,3) have "const d * const a = const d * (const c / const d * const b)"
      by (metis swap_numerator const_divide_self mult_1_right)
    with fractrel(2) have "d * a = c * b"
      by (metis mult.assoc swap_numerator const_divide_self mult_1_left const_mult const_eq_iff)
    thus "a * d = c * b" by algebra
  qed
qed

lemma const_of_fract_0 [simp]: "const_of_fract 0 = 0"
  by transfer simp

lemma const_of_fract_1 [simp]: "const_of_fract 1 = 1"
  by transfer simp

lemma const_of_fract_Fract: "const_of_fract (Fraction_Field.Fract a b) = const a / const b"
  by transfer simp

lemma const_of_fract_p_eq_0_iff [simp]: "p_equal p (const_of_fract x) 0 ⟷ x = 0"
  by  (cases x)
      (simp add: const_of_fract_Fract divide_equiv_0_iff p_equal_func_of_const_0 Fract_eq0_iff)

lemma const_of_fract_equal_0_iff [simp]: "const_of_fract x = 0 ⟷ x = 0"
  by (simp flip: global_eq_iff)

lemma const_of_fract_minus: "const_of_fract (- a) = - const_of_fract a"
  by (transfer, simp add: minus_divide_left fun_Compl_def)

lemma const_of_fract_add: "const_of_fract (a + b) = const_of_fract a + const_of_fract b"
  by (
    transfer, clarify,
    simp add: add_divide_distrib mult_const_divide_mult_const_cancel_right
              mult_const_divide_mult_const_cancel_right_left
  )

lemma const_of_fract_mult: "const_of_fract (a * b) = const_of_fract a * const_of_fract b"
  by (transfer, simp add: times_divide_times_eq)

lemma const_of_fract_neg_one [simp]: "const_of_fract (- 1) = -1"
  by (simp add: const_of_fract_minus)

lemma const_of_fract_diff: "const_of_fract (a - b) = const_of_fract a - const_of_fract b"
  using const_of_fract_add[of a "-b"] by (simp add: const_of_fract_minus)

lemma const_of_fract_sum:
  "const_of_fract (∑a∈A. f a) = (∑a∈A. const_of_fract (f a))"
  by (induct rule: infinite_finite_induct) (auto simp: const_of_fract_add)

lemma const_of_fract_prod:
  "const_of_fract (∏a∈A. f a) = (∏a∈A. const_of_fract (f a))"
  by (induct rule: infinite_finite_induct) (auto simp: const_of_fract_mult)

lemma const_of_fract_inverse: "const_of_fract (inverse a) = inverse (const_of_fract a)"
  by (cases "a = 0", simp, rule inverse_unique[symmetric], simp flip: const_of_fract_mult)

lemma left_inverse_const_of_fract[simp]:
  "inverse (const_of_fract a) * const_of_fract a = 1" if "a ≠ 0"
  by (metis that const_of_fract_inverse const_of_fract_mult Fields.left_inverse const_of_fract_1)

lemma right_inverse_const_of_fract[simp]:
  "(const_of_fract a) * inverse (const_of_fract a) = 1" if "a ≠ 0"
  by (metis that left_inverse_const_of_fract mult.commute)

lemma const_of_fract_divide: "const_of_fract (a / b) = const_of_fract a / const_of_fract b"
  by (metis divide_inverse const_of_fract_mult const_of_fract_inverse Fields.divide_inverse)

lemma p_adic_prod_divide_self_of_fract[simp]:
  "(const_of_fract a) / (const_of_fract a) = 1" if "a ≠ 0"
  by (metis that divide_inverse right_inverse_const_of_fract)

lemma const_of_fract_power: "const_of_fract (a ^ n) = (const_of_fract a) ^ n"
  by (induct n) (simp_all add: const_of_fract_mult)

lemma const_of_fract_eq_iff [simp]:
  "const_of_fract a = const_of_fract b ⟷ a = b"
  by (metis inj_const_of_fract inj_def)

lemma zero_eq_const_of_fract_iff [simp]: "0 = const_of_fract a ⟷ 0 = a"
  by simp

lemma const_of_fract_eq_1_iff [simp]: "const_of_fract a = 1 ⟷ a = 1"
  using const_of_fract_eq_iff [of _ 1] by simp

lemma one_eq_const_of_fract_iff [simp]: "1 = const_of_fract a ⟷ 1 = a"
  by simp

text ‹Collapse nested embeddings.›
lemma const_of_fract_numer_eq_const [simp]: "const_of_fract (Fraction_Field.Fract a 1) = const a"
  by (metis const_of_fract_Fract const_1 div_by_1)

lemma const_of_fract_of_nat_eq [simp]: "const_of_fract (of_nat n) = of_nat n"
  by (induct n) (simp_all add: const_of_fract_add)

lemma const_of_fract_of_int_eq [simp]: "const_of_fract (of_int z) = of_int z"
  by (cases z rule: int_diff_cases) (simp add: const_of_fract_diff)

text ‹Product of all p-adic embeddings of the field of fractions of the base ring.›
definition range_const_of_fract :: "'b set" ("𝒬⇩∀⇩p")
  where "𝒬⇩∀⇩p = range const_of_fract"

lemma range_const_of_fract_cases [cases set: range_const_of_fract]:
  assumes "q ∈ 𝒬⇩∀⇩p"
  obtains (const_of_fract) r where "q = const_of_fract r"
proof -
  from assms have "q ∈ range const_of_fract" by (simp only: range_const_of_fract_def)
  then obtain r where "q = const_of_fract r" ..
  then show thesis ..
qed

lemma range_const_of_fract_cases':
  assumes "x ∈ 𝒬⇩∀⇩p"
  obtains a b where "b ≠ 0" "x = const a / const b"
proof -
  from assms obtain r where "x = const_of_fract r" by (auto simp: range_const_of_fract_def)
  moreover obtain a b where Fract: "b ≠ 0" "r = Fraction_Field.Fract a b"
    using Fract_cases by meson
  ultimately have "x = const a / const b" using const_of_fract_Fract by blast
  with that Fract(1) show thesis by fast
qed

lemma range_const_of_fract_of_fract [simp]:
  "const_of_fract r ∈ 𝒬⇩∀⇩p"
  by (simp add: range_const_of_fract_def)

lemma range_const_of_fract_const [simp]: "const a ∈ 𝒬⇩∀⇩p"
  unfolding range_const_of_fract_def
  by        (standard, rule const_of_fract_numer_eq_const[symmetric], simp)

lemma range_const_of_fract_of_int [simp]: "of_int z ∈ 𝒬⇩∀⇩p"
  by (subst const_of_fract_of_int_eq [symmetric]) (rule range_const_of_fract_of_fract)

lemma Ints_subset_range_const_of_fract: "ℤ ⊆ 𝒬⇩∀⇩p"
  using Ints_cases range_const_of_fract_of_int by blast

lemma range_const_of_fract_of_nat [simp]: "of_nat n ∈ 𝒬⇩∀⇩p"
  by (subst const_of_fract_of_nat_eq [symmetric]) (rule range_const_of_fract_of_fract)

lemma Nats_subset_range_const_of_fract: "ℕ ⊆ 𝒬⇩∀⇩p"
  using Ints_subset_range_const_of_fract Nats_subset_Ints by blast

lemma range_const_of_fract_0 [simp]: "0 ∈ 𝒬⇩∀⇩p"
  unfolding range_const_of_fract_def by (rule range_eqI, rule const_of_fract_0 [symmetric])

lemma range_const_of_fract_1 [simp]: "1 ∈ 𝒬⇩∀⇩p"
  unfolding range_const_of_fract_def by (rule range_eqI, rule const_of_fract_1 [symmetric])

lemma range_const_of_fract_add [simp]:
  "a ∈ 𝒬⇩∀⇩p ⟹
    b ∈ 𝒬⇩∀⇩p ⟹
    a + b ∈ 𝒬⇩∀⇩p"
  by (metis range_const_of_fract_cases range_const_of_fract_of_fract const_of_fract_add)

lemma range_const_of_fract_minus_iff [simp]:
  "- a ∈ 𝒬⇩∀⇩p ⟷
    a ∈ 𝒬⇩∀⇩p"
  by (
    metis range_const_of_fract_cases range_const_of_fract_of_fract add.inverse_inverse
          const_of_fract_minus
  )

lemma range_const_of_fract_diff [simp]:
  "a ∈ 𝒬⇩∀⇩p ⟹
    b ∈ 𝒬⇩∀⇩p ⟹
    a - b ∈ 𝒬⇩∀⇩p"
  by (metis range_const_of_fract_add range_const_of_fract_minus_iff diff_conv_add_uminus)

lemma range_const_of_fract_mult [simp]:
  "a ∈ 𝒬⇩∀⇩p ⟹
    b ∈ 𝒬⇩∀⇩p ⟹
    a * b ∈ 𝒬⇩∀⇩p"
  by (metis range_const_of_fract_cases range_const_of_fract_of_fract const_of_fract_mult)

lemma range_const_of_fract_inverse [simp]:
  "a ∈ 𝒬⇩∀⇩p ⟹
    inverse a ∈ 𝒬⇩∀⇩p"
  by (metis range_const_of_fract_cases range_const_of_fract_of_fract const_of_fract_inverse)

lemma range_const_of_fract_divide [simp]:
  "a ∈ 𝒬⇩∀⇩p ⟹
    b ∈ 𝒬⇩∀⇩p ⟹
    a / b ∈ 𝒬⇩∀⇩p"
  by (simp add: divide_inverse)

lemma range_const_of_fract_power [simp]:
  "a ∈ 𝒬⇩∀⇩p ⟹
    a ^ n ∈ 𝒬⇩∀⇩p"
  by (metis range_const_of_fract_cases range_const_of_fract_of_fract const_of_fract_power)

lemma range_const_of_fract_sum [intro]:
  "(⋀x. x ∈ A ⟹
    f x ∈ 𝒬⇩∀⇩p) ⟹
    sum f A ∈ 𝒬⇩∀⇩p"
  by (induction A rule: infinite_finite_induct) auto

lemma range_const_of_fract [intro]:
  "(⋀x. x ∈ A ⟹ f x ∈ 𝒬⇩∀⇩p)
    ⟹ prod f A ∈ 𝒬⇩∀⇩p"
  by (induction A rule: infinite_finite_induct) auto

lemma range_const_of_fract_induct [case_names const_of_fract, induct set: range_const_of_fract]:
  "q ∈ 𝒬⇩∀⇩p ⟹
    (⋀r. P (const_of_fract r)) ⟹ P q"
  by (rule range_const_of_fract_cases) auto

lemma p_adic_Fracts_p_equal_0_iff:
  "a ∈ 𝒬⇩∀⇩p ⟹
    p_equal p a 0 ⟷ a = 0"
  by (induct a rule: range_const_of_fract_induct, simp)

lemma range_const_of_fract_infinite:
  "infinite 𝒬⇩∀⇩p" if "infinite (UNIV :: 'c set)"
  using that finite_imageD[OF _ inj_const] range_const_of_fract_const
        finite_subset[of "range const"]
  by    blast

lemma left_inverse_range_const_of_fract:
  "a ∈ 𝒬⇩∀⇩p ⟹ a ≠ 0 ⟹
    inverse a * a = 1"
  by (induct a rule: range_const_of_fract_induct, rule left_inverse_const_of_fract, simp)

lemma right_inverse_range_const_of_fract:
  "a ∈ 𝒬⇩∀⇩p ⟹ a ≠ 0 ⟹
    a * inverse a = 1"
  by (metis left_inverse_range_const_of_fract mult.commute)

lemma divide_self_range_const_of_fract:
  "a ∈ 𝒬⇩∀⇩p ⟹ a ≠ 0 ⟹
    a / a = 1"
  by (metis divide_inverse right_inverse_range_const_of_fract)

lemma range_const_of_fract_add_iff:
  "a ∈ 𝒬⇩∀⇩p ∨
    b ∈ 𝒬⇩∀⇩p ⟹
    a + b ∈ 𝒬⇩∀⇩p ⟷
      a ∈ 𝒬⇩∀⇩p ∧ b ∈ 𝒬⇩∀⇩p"
  using range_const_of_fract_add range_const_of_fract_diff add_diff_cancel add_diff_cancel_left'
  by    metis

lemma range_const_of_fract_diff_iff:
  "a ∈ 𝒬⇩∀⇩p ∨
    b ∈ 𝒬⇩∀⇩p ⟹
      a - b ∈ 𝒬⇩∀⇩p ⟷
      a ∈ 𝒬⇩∀⇩p ∧ b ∈ 𝒬⇩∀⇩p"
  by (metis range_const_of_fract_add_iff diff_add_cancel)

lemma range_const_of_fract_mult_iff:
  "a * b ∈ 𝒬⇩∀⇩p ⟷
    a ∈ 𝒬⇩∀⇩p ∧ b ∈ 𝒬⇩∀⇩p"
  if
    "a ∈ 𝒬⇩∀⇩p - {0} ∨
      b ∈ 𝒬⇩∀⇩p - {0}"
proof-
  have *:
    "⋀a b :: 'b.
      a ∈ 𝒬⇩∀⇩p - {0} ⟹
      a * b ∈ 𝒬⇩∀⇩p ⟷
        b ∈ 𝒬⇩∀⇩p"
  proof
    fix a b :: 'b
    assume  "a ∈ 𝒬⇩∀⇩p - {0}"
      and   "a * b ∈ 𝒬⇩∀⇩p"
    thus "b ∈ 𝒬⇩∀⇩p"
      using range_const_of_fract_mult[of "inverse a"] left_inverse_range_const_of_fract[of a]
      by    (fastforce simp flip: mult.assoc)
  qed simp
  show ?thesis
  proof (cases "a ∈ 𝒬⇩∀⇩p - {0}")
    case True thus ?thesis using *[of a b] by fast
  next
    case False
    with that have "b ∈ 𝒬⇩∀⇩p - {0}" by blast
    moreover from this have
      "a * b ∈ 𝒬⇩∀⇩p ⟷
        a ∈ 𝒬⇩∀⇩p"
      by (metis * mult.commute)
    ultimately show ?thesis by blast
  qed
qed

lemma range_const_of_fract_inverse_iff [simp]:
  "inverse a ∈ 𝒬⇩∀⇩p ⟷
    a ∈ 𝒬⇩∀⇩p"
  by (metis range_const_of_fract_inverse inverse_inverse)

lemma range_const_of_fract_divide_iff:
  "a / b ∈ 𝒬⇩∀⇩p ⟷
      a ∈ 𝒬⇩∀⇩p ∧ b ∈ 𝒬⇩∀⇩p"
  if
    "a ∈ 𝒬⇩∀⇩p - {0} ∨
      b ∈ 𝒬⇩∀⇩p - {0}"
  using that range_const_of_fract_inverse inverse_inverse[of b]
        range_const_of_fract_inverse_iff divide_inverse[of a b]
        range_const_of_fract_mult_iff[of a "inverse b"]
  by    force

end (* locale global_p_equal_div_inv_w_idom_consts *)

locale global_p_equality_w_inj_index_consts = global_p_equality_w_inj_consts
+
  fixes index_inj :: "'a ⇒ 'c"
  assumes index_inj  : "inj index_inj"
  and index_inj_nzero: "index_inj p ≠ 0"
begin

abbreviation "global_uniformizer ≡ consts index_inj"
abbreviation "index_const p ≡ const (index_inj p)"

lemma global_uniformizer_locally_uniformizes: "p_equal p global_uniformizer (index_const p)"
  using p_equal_func_of_consts by auto

lemma index_const_globally_nequiv_0: "¬ p_equal q (index_const p) 0"
  using p_equal_func_of_consts_0 index_inj_nzero by fast

lemma global_uniformizer_globally_nequiv_0: "¬ p_equal p global_uniformizer 0"
  using p_equal_func_of_consts_0 index_inj_nzero by simp

end (* locale global_p_equality_w_inj_index_consts *)

locale global_p_equality_no_zero_divisors_1_w_inj_index_consts =
  global_p_equality_w_inj_index_consts + p_equality_no_zero_divisors_1
begin

lemma index_const_pow_globally_nequiv_0: "¬ p_equal q (index_const p ^ n) 0"
  using index_const_globally_nequiv_0 pow_equiv_0_iff by fast

lemma global_uniformizer_pow_globally_nequiv_0: "¬ p_equal q (global_uniformizer ^ n) 0"
  using global_uniformizer_globally_nequiv_0 pow_equiv_0_iff by blast

end

locale global_p_equality_depth_w_inj_index_consts =
  p_equality_depth p_equal p_depth
+ global_p_equality_w_inj_index_consts p_equal p_restrict func_of_consts index_inj
  for p_equal        :: "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict     :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and p_depth        :: "'a ⇒ 'b ⇒ int"
  and func_of_consts :: "('a ⇒ 'c::{factorial_semiring,ring_1}) ⇒ 'b"
  and index_inj      :: "'a ⇒ 'c"
+
  assumes p_depth_func_of_consts:
    "p_depth p (func_of_consts f) = int (multiplicity (index_inj p) (f p))"
  and index_inj_nunit  : "¬ is_unit (index_inj p)"
  and index_inj_coprime:
    "p ≠ q ⟹ multiplicity (index_inj p) (index_inj q) = 0"
begin

lemma p_depth_set_consts: "func_of_consts f ∈ p_depth_set p 0"
  using p_depth_func_of_consts p_depth_setI by simp

lemma global_depth_set_consts: "func_of_consts f ∈ global_depth_set 0"
  using p_depth_set_consts global_depth_set by blast

lemma p_depth_1[simp]: "p_depth p (1::'b) = 0"
  using p_depth_func_of_consts[of p 1] by simp

lemma p_depth_index_const: "p_depth p (index_const p) = 1"
  using p_depth_func_of_consts index_inj_nzero index_inj_nunit multiplicity_self by fastforce

lemma p_depth_index_const': "p_depth q (index_const p) = of_bool (q = p)"
  by (cases "q = p", simp_all add: p_depth_index_const p_depth_func_of_consts index_inj_coprime)

lemma p_depth_global_uniformizer: "p_depth p (global_uniformizer::'b) = 1"
  using p_depth_func_of_consts index_inj_nzero index_inj_nunit multiplicity_self by fastforce

lemma p_depth_consts_func_ge0: "p_depth p (consts f) ≥ 0"
  using p_depth_func_of_consts by fastforce

end (* locale global_p_equality_depth_w_inj_index_consts *)


locale global_p_equal_depth_no_zero_divisors_w_inj_index_consts =
  global_p_equal p_equal p_restrict
+ global_p_equality_depth_no_zero_divisors_1 p_equal p_restrict p_depth
+ global_p_equality_depth_w_inj_index_consts p_equal p_restrict p_depth func_of_consts index_inj
  for p_equal        :: "'a ⇒ 'b::comm_ring_1 ⇒ 'b ⇒ bool"
  and p_restrict     :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and p_depth        :: "'a ⇒ 'b ⇒ int"
  and func_of_consts :: "('a ⇒ 'c::{factorial_semiring,ring_1}) ⇒ 'b"
  and index_inj      :: "'a ⇒ 'c"
begin

sublocale global_p_equal_w_inj_consts ..
sublocale global_p_equal_depth_no_zero_divisors ..

lemma p_depth_index_const_pow: "p_depth p ((index_const p) ^ n) = int n"
  using p_depth_index_const depth_pow_additive by auto

lemma p_depth_index_const_pow': "p_depth q ((index_const p) ^ n) = int n * of_bool (q = p)"
  using p_depth_index_const' depth_pow_additive by fastforce

lemma p_depth_global_uniformizer_pow: "p_depth p (global_uniformizer ^ n) = int n"
  using p_depth_global_uniformizer depth_pow_additive by auto

end

locale global_p_equal_depth_div_inv_w_inj_index_consts =
  global_p_equal_depth_div_inv p_equal p_depth p_restrict
+ global_p_equal_depth_no_zero_divisors_w_inj_index_consts
    p_equal p_restrict p_depth func_of_consts index_inj
  for p_equal        ::
    "'a ⇒ 'b::{comm_ring_1, inverse, divide_trivial} ⇒
      'b ⇒ bool"
  and p_depth        :: "'a ⇒ 'b ⇒ int"
  and p_restrict     :: "'b ⇒ ('a ⇒ bool) ⇒ 'b"
  and func_of_consts :: "('a ⇒ 'c::{factorial_semiring,ring_1}) ⇒ 'b"
  and index_inj      :: "'a ⇒ 'c"
begin

lemma index_const_powi_globally_nequiv_0: "¬ p_equal q (index_const p powi n) 0"
  using index_const_globally_nequiv_0 power_int_equiv_0_iff by simp

lemma global_uniformizer_powi_globally_nequiv_0: "¬ p_equal q (global_uniformizer powi n) 0"
  using global_uniformizer_globally_nequiv_0 power_int_equiv_0_iff by blast

lemma index_const_powi_add:
  "(index_const p) powi (m + n) = (index_const p) powi m * (index_const p) powi n"
  using power_int_add index_const_globally_nequiv_0 by blast

lemma global_uniformizer_powi_add:
  "global_uniformizer powi (m + n) = global_uniformizer powi m * global_uniformizer powi n"
  using power_int_add global_uniformizer_globally_nequiv_0 by blast

lemma p_depth_index_const_powi: "p_depth p (index_const p powi n) = n"
  by  (cases "n ≥ 0")
      (simp_all add: power_int_def p_depth_index_const_pow inverse_depth flip: inverse_pow)

lemma p_depth_index_const_powi': "p_depth q (index_const p powi n) = n * of_bool (q = p)"
  by (
    cases "q = p", simp add: p_depth_index_const_powi, cases "n ≥ 0",
    simp_all add: power_int_def p_depth_index_const_pow' inverse_depth flip: inverse_pow
  )

lemma p_depth_global_uniformizer_powi: "p_depth p (global_uniformizer powi n) = n"
  by (
    cases "n ≥ 0",
    simp_all add: power_int_def p_depth_global_uniformizer_pow inverse_depth flip: inverse_pow
  )

lemma local_uniformizer_locally_uniformizes:
  "p_depth p ((index_const p) powi (-n) * x) = 0" if "p_depth p x = n"
  using that depth_equiv_0 mult_0_right index_const_powi_globally_nequiv_0 no_zero_divisors
        depth_mult_additive p_depth_index_const_powi
  by    (cases "p_equal p x 0") auto

lemma global_uniformizer_locally_uniformizes:
  "p_depth p (global_uniformizer powi (-n) * x) = 0" if "p_depth p x = n"
  using that depth_equiv_0 mult_0_right global_uniformizer_powi_globally_nequiv_0 no_zero_divisors
        depth_mult_additive p_depth_global_uniformizer_powi
  by    (cases "p_equal p x 0") auto

lemma p_depth_set_eq_index_const_coset:
  "p_depth_set p n = ((index_const p) powi n) *o (p_depth_set p 0)"
  using p_depth_set_eq_coset p_depth_index_const index_const_globally_nequiv_0 by blast

lemma p_depth_set_eq_index_const_coset':
  "p_depth_set p 0 = ((index_const p) powi (-n)) *o (p_depth_set p n)"
  using p_depth_set_eq_coset' p_depth_index_const index_const_globally_nequiv_0 by blast

lemma p_depth_set_eq_global_uniformizer_coset:
  "p_depth_set p n = (global_uniformizer powi n) *o (p_depth_set p 0)"
  using p_depth_set_eq_coset p_depth_global_uniformizer global_uniformizer_globally_nequiv_0
  by    blast

lemma p_depth_set_eq_global_uniformizer_coset':
  "p_depth_set p 0 = (global_uniformizer powi (-n)) *o (p_depth_set p n)"
  using p_depth_set_eq_coset' p_depth_global_uniformizer global_uniformizer_globally_nequiv_0
  by    blast

lemma global_depth_set_eq_global_uniformizer_coset:
  "global_depth_set n = (global_uniformizer powi n) *o (global_depth_set 0)"
  using global_depth_set_eq_coset p_depth_global_uniformizer by simp

lemma global_depth_set_eq_global_uniformizer_coset':
  "global_depth_set 0 = (global_uniformizer powi (-n)) *o (global_depth_set n)"
  using global_depth_set_eq_coset' p_depth_global_uniformizer by simp

definition shift_p_depth :: "'a ⇒ int ⇒ 'b ⇒ 'b"
  where "shift_p_depth p n x = x * (consts (λq. if q = p then index_inj p else 1)) powi n"

lemma shift_p_depth_0[simp]: "shift_p_depth p n 0 = 0"
  by (simp add: shift_p_depth_def)

lemma shift_p_depth_by_0[simp]: "shift_p_depth p 0 x = x"
  unfolding shift_p_depth_def by fastforce

lemma shift_p_depth_add[simp]:
  "shift_p_depth p n (x + y) = shift_p_depth p n x + shift_p_depth p n y"
  using shift_p_depth_def distrib_right[of x y] by presburger

lemma shift_p_depth_uminus[simp]:
  "shift_p_depth p n (- x) = - shift_p_depth p n x"
  using shift_p_depth_def mult_minus_left[of x] by presburger

lemma shift_p_depth_minus[simp]:
  "shift_p_depth p n (x - y) = shift_p_depth p n x - shift_p_depth p n y"
  using shift_p_depth_add[of p n x "-y"] by auto

lemma shift_p_depth_equiv_at_place: "p_equal p (shift_p_depth p n x) (x * (index_const p powi n))"
  using shift_p_depth_def p_equal_func_of_consts power_int_equiv_base mult_left by simp

lemma shift_p_depth_equiv_at_other_places:
  "p_equal q (shift_p_depth p n x) x" if "q ≠ p"
  using that p_equal_func_of_consts[of q _ 1] power_int_equiv_base power_int_1_left
        shift_p_depth_def mult_left
  by    fastforce

lemma shift_p_depth_equiv0_iff:
  "p_equal q (shift_p_depth p n x) 0 ⟷ p_equal q x 0"
  using shift_p_depth_equiv_at_place trans0_iff mult_equiv_0_iff power_int_equiv_0_iff
        index_const_globally_nequiv_0 shift_p_depth_equiv_at_other_places
  by (metis (full_types))

lemma shift_p_depth_equiv_iff:
  "p_equal q (shift_p_depth p n x) (shift_p_depth p n y) = p_equal q x y"
  using conv_0 shift_p_depth_minus shift_p_depth_equiv0_iff by metis

lemma shift_p_depth_trivial_iff:
  "shift_p_depth p n x = x ⟷ n = 0 ∨ p_equal p x 0"
proof
  assume "shift_p_depth p n x = x"
  hence "p_equal p (x * (1 - index_const p powi n)) 0"
    using shift_p_depth_equiv_at_place conv_0 mult_1_right right_diff_distrib by metis
  thus "n = 0 ∨ p_equal p x 0"
    using mult_equiv_0_iff conv_0 sym depth_equiv p_depth_1 p_depth_index_const_powi by metis
next
  assume "n = 0 ∨ p_equal p x 0"
  moreover have "n = 0 ⟹ shift_p_depth p n x = x" by simp
  moreover have "p_equal p x 0 ⟹ p_equal p (shift_p_depth p n x) x"
    using shift_p_depth_equiv_at_place mult_0_left trans trans_left by blast
  ultimately have "p_equal p (shift_p_depth p n x) x" by fastforce
  thus "shift_p_depth p n x = x" using global_imp_eq shift_p_depth_equiv_at_other_places by force
qed

lemma shift_p_depth_times_right: "shift_p_depth p n (x * y) = x * shift_p_depth p n y"
proof (intro global_imp_eq, standard)
  fix q show "p_equal q (shift_p_depth p n (x * y)) (x * shift_p_depth p n y)"
  proof (cases "q = p")
    case True thus "p_equal q (shift_p_depth p n (x * y)) (x * shift_p_depth p n y)"
      using shift_p_depth_equiv_at_place[of p n "x * y"] mult.assoc[of x y]
            shift_p_depth_equiv_at_place mult_left sym trans
      by    presburger
  qed (use shift_p_depth_equiv_at_other_places mult_left sym trans in fast)
qed

lemma shift_p_depth_times_left: "shift_p_depth p n (x * y) = shift_p_depth p n x * y"
  using shift_p_depth_times_right mult.commute by metis

lemma shift_shift_p_depth: "shift_p_depth p n (shift_p_depth p m x) = shift_p_depth p (m + n) x"
proof (intro global_imp_eq, standard)
  fix q show "p_equal q (shift_p_depth p n (shift_p_depth p m x)) (shift_p_depth p (m + n) x)"
  proof (cases "q = p")
    case True
    thus ?thesis
      using shift_p_depth_equiv_at_place[of p n "shift_p_depth p m x"]
            shift_p_depth_equiv_at_place[of p m x]
            mult_right trans mult.assoc[of x, symmetric]
            index_const_globally_nequiv_0
            power_int_add[of "index_const p" m n]
            shift_p_depth_equiv_at_place[of p "m + n" x]
            trans_left[of
              p "shift_p_depth p n (shift_p_depth p m x)" "x * index_const p powi (m + n)"
              "shift_p_depth p (m + n) x"
            ]
      by    presburger
  next
    case False
    hence   "p_equal q (shift_p_depth p n (shift_p_depth p m x)) x"
      and   "p_equal q ((shift_p_depth p (m + n) x)) x"
      using shift_p_depth_equiv_at_other_places trans
      by    (blast, blast)
    thus ?thesis using trans_left by blast
  qed
qed

lemma shift_shift_p_depth_image:
  "shift_p_depth p n ` shift_p_depth p m ` A = shift_p_depth p (m + n) ` A"
proof safe
  fix a assume a: "a ∈ A"
  have *: "shift_p_depth p n (shift_p_depth p m a) = shift_p_depth p (m + n) a"
    using shift_shift_p_depth by auto
  from a show "shift_p_depth p n (shift_p_depth p m a) ∈ shift_p_depth p (m + n) ` A"
    using * by fast
  from a show "shift_p_depth p (m + n) a ∈ shift_p_depth p n ` shift_p_depth p m ` A"
    using *[symmetric] by fast
qed

lemma shift_p_depth_at_place:
  "p_depth p (shift_p_depth p n x) = p_depth p x + n" if "n = 0 ∨ ¬ p_equal p x 0"
proof (cases "n = 0")
  case True
  moreover from this have "p_equal p (shift_p_depth p n x) x"
    using shift_p_depth_equiv_at_place power_int_0_right mult_1_right by metis
  ultimately show ?thesis using depth_equiv by fastforce
next
  case False
  with that have "¬ p_equal p (x * (index_const p powi n)) 0"
    using no_zero_divisors power_int_equiv_0_iff index_const_globally_nequiv_0 by auto
  hence "p_depth p (shift_p_depth p n x) = p_depth p x + p_depth p (index_const p powi n)"
    using depth_equiv shift_p_depth_equiv_at_place depth_mult_additive by metis
  thus ?thesis using p_depth_index_const_powi by simp
qed

lemma shift_p_depth_at_other_places:
  "p_depth q (shift_p_depth p n x) = p_depth q x" if "q ≠ p"
  using that depth_equiv shift_p_depth_equiv_at_other_places by blast

lemma p_depth_set_shift_p_depth_closed:
  "shift_p_depth p n x ∈ p_depth_set p m" if "p_depth p x ≥ m - n"
  using that shift_p_depth_equiv0_iff shift_p_depth_at_place p_depth_setI by auto

lemma global_depth_set_shift_p_depth_closed:
  "shift_p_depth p n x ∈ global_depth_set m"
  if  "x ∈ global_depth_set m"
  and "¬ p_equal p x 0 ⟶ p_depth p x ≥ m - n"
  using that p_depth_set_shift_p_depth_closed p_depth_setD shift_p_depth_at_other_places
        shift_p_depth_equiv0_iff global_depth_setD global_depth_setI
  by    metis

lemma shift_p_depth_mem_p_depth_set:
  "p_depth p x ≥ m - n"
  if "¬ p_equal p x 0" and "shift_p_depth p n x ∈ p_depth_set p m"
  using that shift_p_depth_equiv0_iff shift_p_depth_at_place
        p_depth_setD[of p "shift_p_depth p n x"]
  by    fastforce

lemma shift_p_depth_mem_global_depth_set:
  "p_depth p x ≥ m - n"
  if "¬ p_equal p x 0" and "shift_p_depth p n x ∈ global_depth_set m"
  using that shift_p_depth_equiv0_iff shift_p_depth_at_place
        global_depth_setD[of p "shift_p_depth p n x"]
  by    fastforce

lemma shift_p_depth_p_depth_set: "shift_p_depth p n ` p_depth_set p m = p_depth_set p (m + n)"
proof safe
  fix x assume "x ∈ p_depth_set p m"
  thus "shift_p_depth p n x ∈ p_depth_set p (m + n)"
    using     shift_p_depth_at_place shift_p_depth_equiv0_iff
    unfolding p_depth_set_def
    by        simp
next
  fix x assume "x ∈ p_depth_set p (m + n)"
  hence "¬ p_equal p x 0 ⟶ p_depth p x ≥ m + n"
    using p_depth_setD by blast
  hence
    "¬ p_equal p (shift_p_depth p (-n) x) 0 ⟶
      p_depth p (shift_p_depth p (-n) x) ≥ m"
    using shift_p_depth_at_place shift_p_depth_equiv0_iff by force
  hence "shift_p_depth p (-n) x ∈ p_depth_set p m" using p_depth_setI by simp
  moreover have "x = shift_p_depth p n (shift_p_depth p (-n) x)"
    using shift_shift_p_depth by force
  ultimately show "x ∈ shift_p_depth p n ` p_depth_set p m" by blast
qed

lemma shift_p_depth_cong:
  "p_equal q (shift_p_depth p n x) (shift_p_depth p n y)" if "p_equal q x y"
  using that cong_sym shift_p_depth_equiv_at_place mult_right
        shift_p_depth_equiv_at_other_places
  by    (cases "q = p", blast, blast)

lemma shift_p_depth_p_restrict:
  "shift_p_depth p n (p_restrict x P) = p_restrict (shift_p_depth p n x) P"
proof (intro global_imp_eq, standard)
  fix q
  show "p_equal q (shift_p_depth p n (p_restrict x P)) (p_restrict (shift_p_depth p n x) P)"
    by (
      cases "P q",
      metis p_restrict_equiv shift_p_depth_cong trans_right,
      metis p_restrict_equiv0 shift_p_depth_cong shift_p_depth_0 trans_left
    )
qed

lemma shift_p_depth_p_restrict_global_depth_set_memI:
  "shift_p_depth p n (p_restrict x ((=) p)) ∈ global_depth_set m"
  if "¬ p_equal p x 0 ⟶ p_depth p x ≥ m - n"
  using that shift_p_depth_p_restrict shift_p_depth_equiv0_iff shift_p_depth_at_place
        global_depth_set_p_restrictI p_depth_setI
  by    fastforce

lemma shift_p_depth_p_restrict_global_depth_set_memI':
  "shift_p_depth p n (p_restrict x ((=) p)) ∈ global_depth_set (m + n)"
  if "x ∈ p_depth_set p m"
proof-
 from that have "p_restrict x ((=) p) ∈ p_depth_set p m"
  using p_depth_set_p_restrict by simp
  hence "p_restrict (shift_p_depth p n x) ((=) p) ∈ p_depth_set p (m + n)"
    using shift_p_depth_p_depth_set shift_p_depth_p_restrict[of p n x "(=) p"] by force
  hence "p_restrict (shift_p_depth p n x) ((=) p) ∈ global_depth_set (m + n)"
    using global_depth_set_p_restrictI[of "(=) p"] by force
  thus ?thesis using shift_p_depth_p_restrict[of p n x "(=) p"] by auto
qed

lemma shift_p_depth_p_restrict_global_depth_set_image:
  "shift_p_depth p n ` (λx. p_restrict x ((=) p)) ` global_depth_set m
    = (λx. p_restrict x ((=) p)) ` global_depth_set (m + n)"
proof safe
  fix x assume "x ∈ global_depth_set m"
  hence
    "shift_p_depth p n (p_restrict x ((=) p)) ∈ global_depth_set (m + n)"
    using shift_p_depth_p_restrict_global_depth_set_memI' global_depth_set by blast
  moreover have
    "shift_p_depth p n (p_restrict x ((=) p)) =
      p_restrict (shift_p_depth p n (p_restrict x ((=) p))) ((=) p)"
    using shift_p_depth_p_restrict p_restrict_restrict' by presburger
  ultimately show
    "shift_p_depth p n (p_restrict x ((=) p)) ∈
      (λx. p_restrict x ((=) p)) ` global_depth_set (m + n)"
      by fast
next
  fix x assume "x ∈ global_depth_set (m + n)"
  moreover define y where "y ≡ shift_p_depth p (-n) (p_restrict x ((=) p))"
  ultimately have "y ∈ global_depth_set m"
    using shift_p_depth_p_restrict_global_depth_set_memI'[of x p "m + n" "-n"]
          global_depth_set[of "m + n"]
    by    simp
  moreover from y_def have
    "p_restrict x ((=) p) = shift_p_depth p n (p_restrict y ((=) p))"
    using shift_p_depth_p_restrict[of p n y "(=) p"] p_restrict_restrict'[of x "(=) p"]
          shift_shift_p_depth[of p n "-n" "p_restrict x ((=) p)"]
    by    force
  ultimately show
    "p_restrict x ((=) p) ∈
      shift_p_depth p n ` (λx. p_restrict x ((=) p)) ` global_depth_set m"
    using y_def by fast
qed

end (* locale global_p_equal_depth_div_inv_w_inj_index_consts *)


subsection ‹Topological patterns›

subsubsection ‹By place›

text ‹Convergence of sequences as measured by depth›

context p_equality_depth
begin

definition p_limseq_condition ::
  "'a ⇒ (nat ⇒ 'b) ⇒ 'b ⇒ int ⇒
    nat ⇒ bool"
  where
    "p_limseq_condition p X x n K =
      (∀k≥K. ¬ p_equal p (X k) x ⟶ p_depth p (X k - x) > n)"

lemma p_limseq_conditionI [intro]:
  "p_limseq_condition p X x n K"
  if
    "⋀k. k ≥ K ⟹ ¬ p_equal p (X k) x ⟹
      p_depth p (X k - x) > n"
  using that unfolding p_limseq_condition_def by blast

lemma p_limseq_conditionD:
  "p_depth p (X k - x) > n"
  if "p_limseq_condition p X x n K" and "k ≥ K" and "¬ p_equal p (X k) x"
  using that unfolding p_limseq_condition_def by blast

abbreviation p_limseq ::
  "'a ⇒ (nat ⇒ 'b) ⇒ 'b ⇒ bool"
  where "p_limseq p X x ≡ (∀n. ∃K. p_limseq_condition p X x n K)"

lemma p_limseq_p_cong:
  "p_limseq p X x"
  if "∀n≥N. p_equal p (X n) (Y n)" and "p_equal p x y" and "p_limseq p Y y"
proof
  fix n
  from that(3) obtain M where M: "p_limseq_condition p Y y n M" by fastforce
  define K where "K ≡ max M N"
  with M that(1,2) have "p_limseq_condition p X x n K"
    using trans[of p "X _" "Y _" y] trans_left[of p "X _" y x] p_limseq_conditionD[of p Y y n M]
          depth_diff_equiv
    by    fastforce
  thus "∃K. p_limseq_condition p X x n K" by auto
qed

lemma p_limseq_p_constant: "p_limseq p X x" if "∀n. p_equal p (X n) x"
  using that by fast

lemma p_limseq_constant: "p_limseq p (λn. x) x"
  using p_limseq_p_constant by auto

lemma p_limseq_p_eventually_constant:
  "p_limseq p X x" if "∀⇩F k in sequentially. p_equal p (X k) x"
proof
  fix n
  from that obtain K where K: "∀k≥K. p_equal p (X k) x"
    using eventually_sequentially by auto
  hence "p_limseq_condition p X x n K" by blast
  thus "∃K. p_limseq_condition p X x n K" by blast
qed

lemma p_limseq_0 [simp]: "p_limseq p 0 0"
  using p_limseq_p_constant by simp

lemma p_limseq_0_iff: "p_limseq p 0 x ⟷ p_equal p x 0"
proof
  have "¬ p_equal p x 0 ⟹ ¬ p_limseq p 0 x"
  proof
    assume x: "¬ p_equal p x 0" "p_limseq p 0 x"
    have "∀n. p_depth p x > n"
    proof
      fix n
      from x obtain K :: nat where "∀k≥K. p_depth p x > n"
        using p_limseq_conditionD zero_fun_apply diff_0 depth_uminus sym by metis
      thus "p_depth p x > n" by fast
    qed
    thus False by fast
  qed
  thus "p_limseq p 0 x ⟹ p_equal p x 0" by blast
qed (use sym in force)

lemma p_limseq_add: "p_limseq p (X + Y) (x + y)" if "p_limseq p X x" and "p_limseq p Y y"
proof
  fix n
  from that obtain K_x K_y
    where K_x: "p_limseq_condition p X x n K_x"
    and   K_y: "p_limseq_condition p Y y n K_y"
    by    blast
  define K where "K ≡ max K_x K_y"
  have "p_limseq_condition p (X + Y) (x + y) n K"
  proof (standard, unfold plus_fun_apply)
    fix k assume k: "k ≥ K" "¬ p_equal p (X k + Y k) (x + y)"
    from K_def k(1) have k_K_x_y: "k ≥ K_x" "k ≥ K_y" by auto
    have *:
      "⋀X Y x y.
        p_equal p (X k) x ⟹ p_depth p (Y k - y) > n ⟹
          p_depth p (X k + Y k - (x + y)) > n"
    proof-
      fix X Y x y
      assume X: "p_equal p (X k) x" and Y: "p_depth p (Y k - y) > n"
      have "p_depth p (X k + Y k - (x + y)) = p_depth p (X k + (Y k - (x + y)))"
        by (simp add: algebra_simps)
      also from X have "… = p_depth p (x + (Y k - (x + y)))"
        using add_right depth_equiv by blast
      also have "… = p_depth p (Y k - y)" by fastforce
      finally show "p_depth p (X k + Y k - (x + y)) > n" using Y by metis
    qed
    from k(2) consider
      (x_not_y) "  p_equal p (X k) x" "¬ p_equal p (Y k) y" |
      (y_not_x) "¬ p_equal p (X k) x" "  p_equal p (Y k) y" |
      (neither) "¬ p_equal p (X k) x" "¬ p_equal p (Y k) y"
      using add by blast
    thus "p_depth p (X k + Y k - (x + y)) > n"
    proof cases
      case x_not_y
      from K_y k_K_x_y(2) x_not_y(2) have "p_depth p (Y k - y) > n"
        using p_limseq_conditionD by auto
      with x_not_y(1) show ?thesis using * by blast
    next
      case y_not_x
      from K_x k_K_x_y(1) y_not_x(1) have "p_depth p (X k - x) > n"
        using p_limseq_conditionD by auto
      with y_not_x(2) have "p_depth p (Y k + X k - (y + x)) > n" using * by force
      thus ?thesis by (simp add: algebra_simps)
    next
      case neither
      moreover from K_x K_y k_K_x_y this have "min (p_depth p (X k - x)) (p_depth p (Y k - y)) > n"
        using p_limseq_conditionD by simp
      moreover from k(2) have "¬ p_equal p (X k - x + (Y k - y)) 0"
        using conv_0 by (simp add: algebra_simps)
      ultimately have "p_depth p (X k - x + (Y k - y)) > n"
        using conv_0 depth_nonarch[of p "X k - x" "Y k - y"] by auto
      thus ?thesis by (simp add: algebra_simps)
    qed
  qed
  thus "∃K. p_limseq_condition p (X + Y) (x + y) n K" by blast
qed

lemma p_limseq_uminus: "p_limseq p (-X) (-x)" if "p_limseq p X x"
proof
  fix n from that obtain K where "p_limseq_condition p X x n K" by metis
  hence "p_limseq_condition p (-X) (-x) n K"
    using uminus depth_diff unfolding p_limseq_condition_def by auto
  thus "∃K. p_limseq_condition p (-X) (-x) n K" by blast
qed

lemma p_limseq_diff: "p_limseq p (X - Y) (x - y)" if "p_limseq p X x" and "p_limseq p Y y"
  using that p_limseq_uminus[of p Y y] p_limseq_add[of p X x "-Y" "-y"] by force

lemma p_limseq_conv_0: "p_limseq p X x ⟷ p_limseq p (λn. X n - x) 0"
proof
  assume "p_limseq p X x"
  moreover have "X - (λn. x) = (λn. X n - x)" by fastforce
  ultimately show "p_limseq p (λn. X n - x) 0"
    using p_limseq_diff[of p X x "λn. x"] p_limseq_constant by force
next
  assume "p_limseq p (λn. X n - x) 0"
  moreover have "(λn. X n - x) + (λn. x) = X" by force
  ultimately show "p_limseq p X x"
    using p_limseq_add[of p "λn. X n - x" 0 "λn. x"] p_limseq_constant by simp
qed

lemma p_limseq_unique: "p_equal p x y" if "p_limseq p X x" and "p_limseq p X y"
  using that p_limseq_diff[of p X x X y] p_limseq_0_iff[of p "x - y"] conv_0[of p] by auto

lemma p_limseq_eventually_nequiv_0:
  "∀⇩F k in sequentially. ¬ p_equal p (X k) 0"
  if "¬ p_equal p x 0" and "p_limseq p X x"
proof-
  have "¬ (∀K. ∃k≥K. p_equal p (X k) 0)"
  proof
    assume "∀K. ∃k≥K. p_equal p (X k) 0"
    with that have "∀n. p_depth p x > n"
      by (metis p_limseq_conditionD trans_right depth_diff_equiv0_left)
    thus False by blast
  qed
  thus ?thesis using eventually_sequentially by force
qed

lemma p_limseq_bdd_depth:
  assumes "¬ p_equal p x 0" and "p_limseq p X x"
  obtains d where "∀k. ¬ p_equal p (X k) 0 ⟶ p_depth p (X k) ≤ d"
proof-
  from assms(2) obtain K where K: "p_limseq_condition p X x (p_depth p x) K" by auto
  define D where "D ≡ {p_depth p x} ∪ {p_depth p (X k) | k. k < K}"
  define d where "d ≡ Max D"
  have "∀k. ¬ p_equal p (X k) 0 ⟶ p_depth p (X k) ≤ d"
  proof clarify
    fix k show "p_depth p (X k) ≤ d"
    proof (cases "k ≥ K")
      case True
      with assms(1) K have "p_depth p (X k) ≤ p_depth p x"
        using depth_equiv depth_pre_nonarch_diff_right[of p x "X k"] p_limseq_conditionD
        by    fastforce
      also from D_def d_def have "… ≤ d" using Max_ge[of D "p_depth p x"] by simp
      finally show ?thesis by blast
    next
      case False with D_def d_def show ?thesis using Max_ge[of D "p_depth p (X k)"] by fastforce
    qed
  qed
  with that show thesis by blast
qed

lemma p_limseq_eventually_bdd_depth:
  "∀⇩F k in sequentially. p_depth p (X k) ≤ p_depth p x"
  if "¬ p_equal p x 0" and "p_limseq p X x"
proof-
  from that(2) obtain K where K: "p_limseq_condition p X x (p_depth p x) K" by auto
  have "∀k≥K. p_depth p (X k) ≤ p_depth p x"
  proof clarify
    fix k assume "k ≥ K"
    with that(1) K show "p_depth p (X k) ≤ p_depth p x"
      using depth_equiv depth_pre_nonarch_diff_right[of p x "X k"] p_limseq_conditionD by fastforce
  qed
  thus ?thesis using eventually_sequentially by blast
qed

lemma p_limseq_delayed_iff:
  "p_limseq p X x ⟷ p_limseq p (λn. X (N + n)) x"
proof (standard, safe)
  fix n
  assume "p_limseq p X x"
  from this obtain K where "p_limseq_condition p X x n K" by fastforce
  hence "p_limseq_condition p (λn. X (N + n)) x n K"
    unfolding p_limseq_condition_def by simp
  thus "∃K. p_limseq_condition p (λn. X (N + n)) x n K" by blast
next
  fix n
  assume "p_limseq p (λn. X (N + n)) x"
  from this obtain M where M: "p_limseq_condition p (λn. X (N + n)) x n M" by auto
  define K where "K ≡ M + N"
  have "p_limseq_condition p X x n K"
  proof
    fix k assume k: "k ≥ K" and X: "¬ p_equal p (X k) x"
    from k K_def have "N + (k - N) = k" by simp
    moreover from k K_def have "k - N ≥ M" by auto
    moreover from k K_def X have "¬ p_equal p (X (N + (k - N))) x"
      by (simp add: algebra_simps)
    ultimately show "p_depth p (X k - x) > n" using M p_limseq_conditionD by metis
  qed
  thus "∃K. p_limseq_condition p X x n K" by blast
qed

lemma p_depth_set_p_limseq_closed:
  "x ∈ p_depth_set p n"
  if "p_limseq p X x" and "∀⇩F k in sequentially. X k ∈ p_depth_set p n"
proof (intro p_depth_setI, clarify)
  assume x_n0: "¬ p_equal p x 0"
  from that(1) obtain K where K: "p_limseq_condition p X x n K" by blast
  from that(2) obtain N where N: "∀k≥N. X k ∈ p_depth_set p n"
    using eventually_sequentially by fastforce
  define k where "k ≡ max N K"
  show "p_depth p x ≥ n"
  proof (cases "p_equal p (X k) x")
    case True with N x_n0 k_def show ?thesis
      using trans_right[of p _ x] p_depth_setD[of p "X k"] depth_equiv by fastforce
  next
    case False
    with K k_def have X_x: "p_depth p (X k - x) > n"
      using p_limseq_conditionD by force
    show ?thesis
    proof (cases "p_equal p (X k) 0")
      case True thus ?thesis using X_x depth_diff_equiv0_left by simp
    next
      case False
      with N x_n0 k_def show "p_depth p x ≥ n"
        using X_x depth_pre_nonarch_diff_right[of p x "X k"] p_depth_setD[of p _ n] by fastforce
    qed
  qed
qed

text ‹Cauchy sequences by place›

definition p_cauchy_condition ::
  "'a ⇒ (nat ⇒ 'b) ⇒ int ⇒ nat ⇒ bool"
  where
    "p_cauchy_condition p X n K =
      (∀k1≥K. ∀k2≥K.
        ¬ p_equal p (X k1) (X k2) ⟶ p_depth p (X k1 - X k2) > n
      )"

lemma p_cauchy_conditionI:
  "p_cauchy_condition p X n K"
  if
    "⋀k k'. k ≥ K ⟹ k' ≥ K ⟹
      ¬ p_equal p (X k) (X k') ⟹ p_depth p (X k - X k') > n"
  using that unfolding p_cauchy_condition_def by blast

lemma p_cauchy_conditionD:
  "p_depth p (X k - X k') > n"
  if  "p_cauchy_condition p X n K" and "k ≥ K" and "k' ≥ K"
  and "¬ p_equal p (X k) (X k')"
  using that unfolding p_cauchy_condition_def by blast

lemma p_cauchy_condition_mono_seq_tail:
  "p_cauchy_condition p X n K ⟹ p_cauchy_condition p X n K'"
  if "K' ≥ K"
  using that unfolding p_cauchy_condition_def by auto

lemma p_cauchy_condition_mono_depth:
  "p_cauchy_condition p X n K ⟹ p_cauchy_condition p X m K"
  if "m ≤ n"
  using that unfolding p_cauchy_condition_def by fastforce

abbreviation "p_cauchy p X ≡ (∀n. ∃K. p_cauchy_condition p X n K)"

lemma p_cauchy_condition_LEAST:
  "p_cauchy_condition p X n (LEAST K. p_cauchy_condition p X n K)"
  if "p_cauchy p X"
  using that Least1I[OF ex_ex1_least_nat_le] by blast

lemma p_cauchy_condition_LEAST_mono:
  "(LEAST K. p_cauchy_condition p X m K) ≤ (LEAST K. p_cauchy_condition p X n K)"
  if "p_cauchy p X" and "m ≤ n"
  using that least_le_least[OF ex_ex1_least_nat_le ex_ex1_least_nat_le]
        p_cauchy_condition_mono_depth
  by    force

definition p_consec_cauchy_condition ::
  "'a ⇒ (nat ⇒ 'b) ⇒ int ⇒ nat ⇒ bool"
  where
    "p_consec_cauchy_condition p X n K =
      (∀k≥K.
        ¬ p_equal p (X (Suc k)) (X k) ⟶ p_depth p (X (Suc k) - X k) > n
      )"

lemma p_consec_cauchy_conditionI:
  "p_consec_cauchy_condition p X n K"
  if
    "⋀k. k ≥ K ⟹ ¬ p_equal p (X (Suc k)) (X k) ⟹
      p_depth p (X (Suc k) - X k) > n"
  using that unfolding p_consec_cauchy_condition_def by blast

lemma p_consec_cauchy:
  "p_cauchy p X = (∀n. ∃K. p_consec_cauchy_condition p X n K)"
proof (standard, safe)
  fix n
  assume "p_cauchy p X"
  from this obtain K where K: "p_cauchy_condition p X n K" by auto
  hence "p_consec_cauchy_condition p X n K"
    using p_cauchy_conditionD by (force intro: p_consec_cauchy_conditionI)
  thus "∃K. p_consec_cauchy_condition p X n K" by blast
next
  fix n
  assume "∀n. ∃K. p_consec_cauchy_condition p X n K"
  from this obtain K where K: "p_consec_cauchy_condition p X n K" by blast
  have "p_cauchy_condition p X n K"
  proof (intro p_cauchy_conditionI)
    fix k k' show
      "k ≥ K ⟹ k' ≥ K ⟹
        ¬ p_equal p (X k) (X k') ⟹ p_depth p (X k - X k') > n"
    proof (induct k' k rule: linorder_wlog)
      case (le a b)
      define c where "c ≡ b - a"
      have
        "a ≥ K ⟹ ¬ p_equal p (X (a + c)) (X a) ⟹
          p_depth p (X (a + c) - X a) > n"
      proof (induct c)
        case (Suc c)
        have decomp: "X (a + Suc c) - X a = (X (a + Suc c) - X (a + c)) + (X (a + c) - X a)"
          by fastforce
        consider  "p_equal p (X (a + Suc c)) (X (a + c))"   |
                  "p_equal p (X (a + c)) (X a)"             |
                  "¬ p_equal p (X (a + Suc c)) (X (a + c))"
                  "¬ p_equal p (X (a + c)) (X a)"
          by blast
        thus ?case
        proof (cases, metis Suc trans decomp conv_0 depth_add_equiv0_left)
          case 2
          with Suc(3) have "¬ p_equal p (X (a + Suc c)) (X (a + c))" using trans by blast
          with K Suc(2) have "p_depth p (X (a + Suc c) - X (a + c)) > n"
            using p_consec_cauchy_condition_def[of p X n K] by force
          with 2 show ?thesis using decomp conv_0 depth_add_equiv0_right by presburger
        next
          case 3
          moreover from K Suc(2) 3(1) have "p_depth p (X (a + Suc c) - X (a + c)) > n"
            using p_consec_cauchy_condition_def[of p X n K] by force
          moreover from 3(2) Suc(1,2) have "p_depth p (X (a + c) - X a) > n" by fast
          ultimately show ?thesis using Suc(3) decomp conv_0 depth_nonarch[of p] by fastforce
        qed
      qed simp
      with le c_def show ?case by force
    qed (metis sym depth_diff)
  qed
  thus "∃K. p_cauchy_condition p X n K" by blast
qed

end (* context p_equality_depth *)

context p_equality_depth_no_zero_divisors
begin

lemma p_limseq_mult_both_0: "p_limseq p (X * Y) 0" if "p_limseq p X 0" and "p_limseq p Y 0"
proof
  fix n
  from that obtain K_X K_Y
    where "p_limseq_condition p X 0 ¦n¦ K_X"
    and   "p_limseq_condition p Y 0 ¦n¦ K_Y"
    by    metis
  moreover define K where "K ≡ max K_X K_Y"
  ultimately have "p_limseq_condition p (X * Y) 0 n K"
    using     K_def mult_0_left mult_0_right depth_mult_additive
    unfolding p_limseq_condition_def
    by        fastforce
  thus "∃K. p_limseq_condition p (X * Y) 0 n K" by blast
qed

lemma p_limseq_constant_mult_0: "p_limseq p (λn. x * Y n) 0" if "p_limseq p Y 0"
proof
  fix n
  from that obtain K where "p_limseq_condition p Y 0 (n - p_depth p x) K" by auto
  hence "p_limseq_condition p (λn. x * Y n) 0 n K"
    using mult_0_right depth_mult_additive unfolding p_limseq_condition_def by auto
  thus "∃K. p_limseq_condition p (λn. x * Y n) 0 n K" by auto
qed

lemma p_limseq_mult_0_right: "p_limseq p (X * Y) 0" if "p_limseq p X x" and "p_limseq p Y 0"
proof-
  from that(1) have "p_limseq p (λn. X n - x) 0" using p_limseq_conv_0 by blast
  with that(2) have "p_limseq p ((λn. X n - x) * Y) 0" using p_limseq_mult_both_0 by blast
  moreover have "(λn. X n - x) * Y = X * Y - (λn. x * Y n)"
    unfolding times_fun_def fun_diff_def by (auto simp add: algebra_simps)
  ultimately have "p_limseq p (X * Y - (λn. x * Y n)) 0" by auto
  with that(2) have "p_limseq p (X * Y - (λn. x * Y n) + (λn. x * Y n)) 0"
    using p_limseq_constant_mult_0[of p Y x]
          p_limseq_add[of p "X * Y - (λn. x * Y n)" 0 "λn. x * Y n"]
    by    simp
  thus ?thesis by (simp add: algebra_simps)
qed

lemma p_limseq_mult: "p_limseq p (X * Y) (x * y)" if "p_limseq p X x" and "p_limseq p Y y"
proof-
  from that have "p_limseq p (X * (λn. Y n - y)) 0"
    using p_limseq_conv_0 p_limseq_mult_0_right by simp
  moreover from that have "p_limseq p (λn. y * (X n - x)) 0"
    using p_limseq_conv_0 p_limseq_constant_mult_0 by blast
  ultimately have "p_limseq p (X * (λn. Y n - y) + (λn. y * (X n - x))) 0"
    using p_limseq_add[of p "X * (λn. Y n - y)" 0] by force
  moreover have
    "X * (λn. Y n - y) + (λn. y * (X n - x)) = (λn. (X * Y) n - x * y)"
    by (auto simp add: algebra_simps)
  ultimately show "p_limseq p (X * Y) (x * y)" using p_limseq_conv_0 by metis
qed

lemma poly_continuous_p_open_nbhds:
  "p_limseq p (λn. poly f (X n)) (poly f x)" if "p_limseq p X x"
proof (induct f)
  case (pCons a f)
  have "(λn. poly (pCons a f) (X n)) = (λn. a) + X * (λn. poly f (X n))"
    by auto
  with that pCons(2) show ?case using p_limseq_constant p_limseq_add p_limseq_mult by simp
qed (simp flip: zero_fun_def)

end (* context p_equality_depth_no_zero_divisors *)

context p_equality_depth_no_zero_divisors_1
begin

lemma p_limseq_pow: "p_limseq p (λk. (X k)^n) (x ^ n)" if "p_limseq p X x"
proof (induct n)
  case (Suc n)
  moreover have "(λk. X k ^ Suc n) = X * (λk. X k ^ n)" by auto
  ultimately show ?case using that p_limseq_mult by simp
qed (simp add: p_limseq_constant)

lemma p_limseq_poly: "p_limseq p (λn. poly f (X n)) (poly f x)" if "p_limseq p X x"
proof (induct f)
  case (pCons a f)
  have "(λn. poly (pCons a f) (X n)) = (λn. a) + X * (λn. poly f (X n))"
    by auto
  with that pCons(2) show ?case using p_limseq_mult p_limseq_add p_limseq_constant by auto
qed (simp flip: zero_fun_def)

end (* context p_equality_depth_no_zero_divisors_1 *)

context p_equality_depth_div_inv
begin

lemma p_limseq_inverse:
  "p_limseq p (λn. inverse (X n)) (inverse x)"
  if "¬ p_equal p x 0" and "p_limseq p X x"
proof
  fix n
  from that obtain K1 where K1: "∀k≥K1. p_depth p (X k) ≤ p_depth p x"
    using p_limseq_eventually_bdd_depth eventually_sequentially by fastforce
  from that obtain K2 where K2: "∀k≥K2. ¬ p_equal p (X k) 0"
    using p_limseq_eventually_nequiv_0 eventually_sequentially by force
  from that(2) obtain K3
    where K3: "p_limseq_condition p X x (¦n¦ + 2 * p_depth p x) K3"
    by    fast
  define K where "K ≡ Max {K1, K2, K3}"
  have "p_limseq_condition p (λn. inverse (X n)) (inverse x) n K"
  proof
    fix k assume k: "k ≥ K" and X_k: "¬ p_equal p (inverse (X k)) (inverse x)"
    from k(1) K_def K2 have "p_equal p (inverse (X k) * X k) 1" using left_inverse_equiv by simp
    moreover from that(1) have "p_equal p (x * inverse x) 1" using right_inverse_equiv by simp
    ultimately have "p_equal p (inverse (X k) * (x - X k) * inverse x) (inverse (X k) - inverse x)"
      using minus mult_left[of p "x * inverse x" 1 "inverse (X k)"]
            mult_right[of p "inverse (X k) * X k" 1 "inverse x"]
      by    (simp add: algebra_simps)
    with X_k have
      "p_depth p (inverse (X k) - inverse x) =
        p_depth p (inverse (X k)) + p_depth p (X k - x) + p_depth p (inverse x)"
      using depth_equiv trans_right conv_0 depth_mult3_additive depth_diff by metis
    also from k X_k K_def K1 K2 K3 have "… > n"
      using inverse_depth inverse_equiv_iff_equiv p_limseq_conditionD
      by    (fastforce simp add: algebra_simps)
    finally show "p_depth p (inverse (X k) - inverse x) > n" by force
  qed
  thus "∃K. p_limseq_condition p (λn. inverse (X n)) (inverse x) n K" by blast
qed

lemma p_limseq_divide:
  "p_limseq p (λn. X n / Y n) (x / y)"
  if "¬ p_equal p y 0" and "p_limseq p X x" and "p_limseq p Y y"
proof-
  have "(λn. X n / Y n) = X * (λn. inverse (Y n))" using divide_inverse by force
  with that show ?thesis using p_limseq_mult p_limseq_inverse divide_inverse by simp
qed

end (* context p_equality_depth_div_inv *)

context global_p_equality_depth
begin

lemma p_limseq_p_restrict_iff:
  "p_limseq p (λn. p_restrict (X n) P) x ⟷ p_limseq p X x" if "P p"
  using that sym p_restrict_equiv p_limseq_p_cong[of 0 p "λn. p_restrict (X n) P" X x x]
        p_limseq_p_cong[of 0 p X "λn. p_restrict (X n) P" x x]
  by    auto

lemma p_limseq_p_restricted: "p_limseq p (λn. p_restrict (X n) P) 0" if "¬ P p"
  using that p_restrict_equiv0 p_limseq_p_cong by blast

end (* context global_p_equality_depth *)

text ‹Base of open sets at local places›

context global_p_equal_depth
begin

abbreviation p_open_nbhd :: "'a ⇒ int ⇒ 'b ⇒ 'b set"
  where "p_open_nbhd p n x ≡ x +o p_depth_set p n"

abbreviation "local_p_open_nbhds p ≡ { p_open_nbhd p n x | n x. True }"
abbreviation "p_open_nbhds         ≡ (⋃p. local_p_open_nbhds p)"

lemma p_open_nbhd: "x ∈ p_open_nbhd p n x"
  unfolding elt_set_plus_def using p_depth_set_0 by force

lemma local_p_open_nbhd_is_open: "generate_topology (local_p_open_nbhds p) (p_open_nbhd p n x)"
  using generate_topology.intros(4)[of _ "local_p_open_nbhds p"] by blast

lemma p_open_nbhd_is_open: "generate_topology p_open_nbhds (p_open_nbhd p n x)"
  using generate_topology.intros(4)[of _ p_open_nbhds] by blast

lemma local_p_open_nbhds_are_coarser:
  "generate_topology (local_p_open_nbhds p) S ⟹ generate_topology p_open_nbhds S"
proof (
  induct S rule: generate_topology.induct, rule generate_topology.UNIV,
  use generate_topology.Int in blast, use generate_topology.UN in blast
)
  case (Basis S)
  hence "S ∈ p_open_nbhds" by blast
  thus ?case using generate_topology.Basis by meson
qed

lemma p_open_nbhd_diff_depth:
  "p_depth p (y - x) ≥ n" if "¬ p_equal p y x" and "y ∈ p_open_nbhd p n x"
proof-
  from that(2) have "y - x ∈ p_depth_set p n"
    unfolding elt_set_plus_def by fastforce
  with that(1) show ?thesis using conv_0 p_depth_setD by blast
qed

lemma p_open_nbhd_eq_circle:
  "p_open_nbhd p n x = {y. ¬ p_equal p y x ⟶ p_depth p (y - x) ≥ n}"
proof safe
(* simp add: p_open_nbhd_diff_depth *)
  fix y assume "y ∉ p_open_nbhd p n x" "p_equal p y x"
  thus False using conv_0 p_depth_set_equiv0 unfolding elt_set_plus_def by force
next
  fix y assume "n ≤ p_depth p (y - x)"
  thus "y ∈ p_open_nbhd p n x"
    unfolding elt_set_plus_def using p_depth_setI by force
qed (simp add: p_open_nbhd_diff_depth)

lemma p_open_nbhd_circle_multicentre:
  "p_open_nbhd p n y = p_open_nbhd p n x" if "y ∈ p_open_nbhd p n x"
proof-
  have *:
    "⋀x y. y ∈ p_open_nbhd p n x ⟹
      p_open_nbhd p n y ⊆ p_open_nbhd p n x"
  proof clarify
    fix x y z assume yx: "y ∈ p_open_nbhd p n x" and zy: "z ∈ p_open_nbhd p n y"
    have "¬ p_equal p z x ⟶ p_depth p (z - x) ≥ n"
    proof
      assume zx: "¬ p_equal p z x"
      have zyx: "z - x = (z - y) + (y - x)" by auto
      consider
        "p_equal p z y" | "p_equal p y x" | (neq) "¬ p_equal p z y" "¬ p_equal p y x"
        by fast
      thus "p_depth p (z - x) ≥ n"
      proof (
        cases,
        metis zyx yx zx yx trans conv_0 depth_add_equiv0_left p_open_nbhd_diff_depth,
        metis zyx zy zx trans conv_0 depth_add_equiv0_right p_open_nbhd_diff_depth
      )
        case neq
        with yx zy have "p_depth p (z - y) ≥ n" and "p_depth p (y - x) ≥ n"
          using p_open_nbhd_diff_depth by simp_all
        hence "min (p_depth p (z - y)) (p_depth p (y - x)) ≥ n" by presburger
        moreover from neq zyx zx
          have  "p_depth p (z - x) ≥ min (p_depth p (z - y)) (p_depth p (y - x))"
          by    (metis conv_0 depth_nonarch)
        ultimately show ?thesis by linarith
      qed
    qed
    thus "z ∈ p_open_nbhd p n x" using p_open_nbhd_eq_circle by auto
  qed
  moreover from that have "x ∈ p_open_nbhd p n y"
    using p_open_nbhd_eq_circle sym depth_diff by force
  ultimately show ?thesis using that by auto
qed

lemma p_open_nbhd_circle_multicentre':
  "x ∈ p_open_nbhd p n y ⟷ y ∈ p_open_nbhd p n x"
  using p_open_nbhd p_open_nbhd_circle_multicentre by blast

lemma p_open_nbhd_p_restrict:
  "p_open_nbhd p n (p_restrict x P) = p_open_nbhd p n x" if "P p"
proof (intro set_eqI)
  fix y from that show
    "y ∈ p_open_nbhd p n (p_restrict x P) ⟷
      y ∈ p_open_nbhd p n x"
    using p_open_nbhd_eq_circle[of "p_restrict x P" p n]
          p_open_nbhd_eq_circle[of x p n] p_restrict_equiv[of P p x]
          depth_diff_equiv[of p y y "p_restrict x P" x]
          trans[of p y "p_restrict x P" x] trans_left[of p y x "p_restrict x P"]
    by    force
qed

lemma p_restrict_p_open_nbhd_mem_iff:
  "y ∈ p_open_nbhd p n x ⟷ p_restrict y P ∈ p_open_nbhd p n x" if "P p"
  using that p_open_nbhd_circle_multicentre' p_open_nbhd_p_restrict by auto

lemma p_open_nbhd_p_restrict_add_mixed_drop_right:
  "p_open_nbhd p n (p_restrict x P + p_restrict y Q) = p_open_nbhd p n x"
  if "P p" and "¬ Q p"
proof (intro set_eqI)
  fix z
  from that have *: "p_equal p (p_restrict x P + p_restrict y Q) x"
    using p_restrict_add_mixed_equiv_drop_right by simp
  hence
    "z ∈ p_open_nbhd p n (p_restrict x P + p_restrict y Q) ⟷
      ¬ p_equal p z x ⟶
        p_depth p (z - (p_restrict x P + p_restrict y Q)) ≥ n"
    using p_open_nbhd_eq_circle trans trans_left by blast
  moreover have "p_depth p (z - (p_restrict x P + p_restrict y Q)) = p_depth p (z - x)"
    using * depth_diff_equiv by auto
  ultimately show
    "z ∈ p_open_nbhd p n (p_restrict x P + p_restrict y Q) ⟷
      z ∈ p_open_nbhd p n x"
    using p_open_nbhd_eq_circle by auto
qed

lemma p_open_nbhd_p_restrict_add_mixed_drop_left:
  "p_open_nbhd p n (p_restrict x P + p_restrict y Q) = p_open_nbhd p n y"
  if "¬ P p" and "Q p"
  using that p_open_nbhd_p_restrict_add_mixed_drop_right[of Q p P y x] by (simp add: add.commute)

lemma p_open_nbhd_antimono:
  "p_open_nbhd p n x ⊆ p_open_nbhd p m x" if "m ≤ n"
  using that p_open_nbhd_eq_circle by auto

lemma p_open_nbhds_open_subopen:
  "generate_topology (local_p_open_nbhds p) A =
    (∀a∈A. ∃n. p_open_nbhd p n a ⊆ A)"
proof
  show
    "generate_topology (local_p_open_nbhds p) A ⟹
      ∀a∈A. ∃n. p_open_nbhd p n a ⊆ A"
  proof (induct A rule: generate_topology.induct)
    case (Int A B) show ?case
    proof
      fix x assume x: "x ∈ A ∩ B"
      from x Int(2) obtain n_A where "p_open_nbhd p n_A x ⊆ A" by blast
      moreover from x Int(4) obtain n_B where "p_open_nbhd p n_B x ⊆ B" by blast
      moreover define n where "n = max n_A n_B"
      ultimately have "p_open_nbhd p n x ⊆ A ∩ B"
        using p_open_nbhd_antimono[of n_A n x p] p_open_nbhd_antimono[of n_B n x p] by auto
      thus "∃n. p_open_nbhd p n x ⊆ A ∩ B" by blast
    qed
  qed (simp, fast, use p_open_nbhd_circle_multicentre in blast)
next
  assume *: "∀a∈A. ∃n. p_open_nbhd p n a ⊆ A"
  define f where "f ≡ λa. (SOME n. p_open_nbhd p n a ⊆ A)"
  have "A = (⋃a∈A. p_open_nbhd p (f a) a)"
  proof safe
    fix a show "a ∈ A ⟹ a ∈ (⋃a∈A. p_open_nbhd p (f a) a)"
      using p_open_nbhd by blast
  next
    fix x a assume a: "a ∈ A" and x: "x ∈ p_open_nbhd p (f a) a"
    from a * have ex_n: "∃n. p_open_nbhd p n a ⊆ A" by fastforce
    from x f_def show "x ∈ A" using someI_ex[OF ex_n] by blast
  qed
  moreover have "∀a∈A. generate_topology (local_p_open_nbhds p) (p_open_nbhd p (f a) a)"
    using generate_topology.Basis[of _ "local_p_open_nbhds p"] by blast
  ultimately show "generate_topology (local_p_open_nbhds p) A"
    using generate_topology.UN[of "(λa. p_open_nbhd p (f a) a) ` A" "local_p_open_nbhds p"]
    by    fastforce
qed

lemma p_restrict_p_open_set_mem_iff:
  "a ∈ A ⟷ p_restrict a P ∈ A"
  if "generate_topology (local_p_open_nbhds p) A" and "P p"
  using that p_open_nbhds_open_subopen p_open_nbhd p_restrict_p_open_nbhd_mem_iff by fast

lemma hausdorff:
  "∃p n. (p_open_nbhd p n x) ∩ (p_open_nbhd p n y) = {}" if "x ≠ y"
proof-
  from that obtain p :: 'a where p: "¬ p_equal p x y" using global_imp_eq by blast
  define n where "n ≡ p_depth p (x - y) + 1"
  have "(p_open_nbhd p n x) ∩ (p_open_nbhd p n y) = {}"
    unfolding elt_set_plus_def
  proof (intro equals0I, clarify)
    fix a b
    assume  a : "a ∈ p_depth_set p n"
      and   b : "b ∈ p_depth_set p n"
      and   ab: "x + a = y + b"
    from ab have "x - y = b - a" by (simp add: algebra_simps)
    with p a b have "p_depth p (x - y) ≥ n"
      using p_depth_set_minus conv_0 p_depth_setD by metis
    with n_def show False by linarith
  qed
  thus ?thesis by blast
qed

sublocale t2_p_open_nbhds: t2_space "generate_topology p_open_nbhds"
proof (intro class.t2_space.intro, rule topological_space_generate_topology, unfold_locales)
  fix x y :: 'b assume "x ≠ y"
  from this obtain p and n where pn: "(p_open_nbhd p n x) ∩ (p_open_nbhd p n y) = {}"
    using hausdorff by presburger
  thus
    "∃V V'. generate_topology p_open_nbhds V ∧ generate_topology p_open_nbhds V' ∧
      x ∈ V ∧ y ∈ V' ∧ V ∩ V' = {}"
    using p_open_nbhd_is_open p_open_nbhd by meson
qed

abbreviation "p_open_nbhds_tendsto    ≡ t2_p_open_nbhds.tendsto"
abbreviation "p_open_nbhds_convergent ≡ t2_p_open_nbhds.convergent"
abbreviation "p_open_nbhds_LIMSEQ     ≡ t2_p_open_nbhds.LIMSEQ"

lemma locally_limD: "∃K. p_limseq_condition p X x n K" if "p_open_nbhds_LIMSEQ X x"
proof-
  from that have "∃K. ∀k≥K. X k ∈ p_open_nbhd p (n + 1) x"
    using     p_open_nbhd_is_open p_open_nbhd
    unfolding t2_p_open_nbhds.tendsto_def eventually_sequentially
    by        presburger
  thus "∃K. p_limseq_condition p X x n K" using p_open_nbhd_eq_circle by force
qed

lemma globally_limseq_imp_locally_limseq:
  "p_limseq p X x" if "p_open_nbhds_LIMSEQ X x"
  using that locally_limD by blast

lemma globally_limseq_iff_locally_limseq: "p_open_nbhds_LIMSEQ X x = (∀p. p_limseq p X x)"
proof (standard, standard, use globally_limseq_imp_locally_limseq in fast)
  assume X: "∀p. p_limseq p X x"
  show "p_open_nbhds_LIMSEQ X x"
    unfolding t2_p_open_nbhds.tendsto_def eventually_sequentially
  proof clarify
    fix S :: "'b set"
    have
      "generate_topology p_open_nbhds S ⟹ x ∈ S ⟹
        (∀p. p_limseq p X x) ⟹ ∃K. ∀k≥K. X k ∈ S"
    proof (induct S rule: generate_topology.induct)
      case (Int A B)
      from Int(2,4-6) obtain Ka and Kb
        where "∀k≥Ka. X k ∈ A"
        and   "∀k≥Kb. X k ∈ B"
        by    blast
      from this have "∀k≥max Ka Kb. X k ∈ A ∩ B" by fastforce
      thus ?case by blast
    next
      case (Basis S)
      from Basis(1,2) obtain p n where "S = p_open_nbhd p n x"
        using p_open_nbhd_circle_multicentre by blast
      moreover from Basis(3) have "∃K. p_limseq_condition p X x (n - 1) K" by blast
      ultimately show ?case using p_limseq_conditionD p_open_nbhd_eq_circle by fastforce
    qed (simp, blast)
    with X show
      "generate_topology p_open_nbhds S ⟹
        x ∈ S ⟹ ∃K. ∀k≥K. X k ∈ S"
      by fast
  qed
qed

lemma p_open_nbhds_LIMSEQ_eventually_p_constant:
  "p_equal p x c"
  if "p_open_nbhds_LIMSEQ X x" and "∀⇩F k in sequentially. p_equal p (X k) c"
proof-
  have "¬ (¬ p_equal p x c)"
  proof
    assume contra: "¬ p_equal p x c"
    define d where "d ≡ max 1 (p_depth p (x - c))"
    from that(1) obtain K1 where K1: "p_limseq_condition p X x d K1"
      using locally_limD by blast
    from that(2) obtain K2 where K2: "∀k≥K2. p_equal p (X k) c"
      using eventually_sequentially by auto
    define K where "K ≡ max K1 K2"
    show False
    proof (cases "p_equal p (X K) x")
      case True with contra K2 K_def show False using trans_right[of p "X K"] by simp
    next
      case False
      with K1 K_def have "p_depth p (X K - x) > d" using p_limseq_conditionD by simp
      with d_def K2 K_def show False using depth_diff_equiv[of p "X K" c x x] depth_diff by simp
    qed
  qed
  thus ?thesis by blast
qed

lemma p_open_nbhds_LIMSEQ_p_restrict:
  "p_equal p x 0" if "p_open_nbhds_LIMSEQ (λn. p_restrict (X n) P) x" and "¬ P p"
    using that globally_limseq_iff_locally_limseq sym p_restrict_equiv0 p_limseq_0_iff
          p_limseq_p_cong[of 0 p 0 "λn. p_restrict (X n) P" x x]
   by     auto

lemma global_depth_set_p_open_nbhds_LIMSEQ_closed:
  "x ∈ global_depth_set n"
  if  "p_open_nbhds_LIMSEQ X x"
  and "∀⇩F k in sequentially. X k ∈ global_depth_set n"
proof (intro global_depth_setI'')
  fix p
  from that(2) have "∀⇩F k in sequentially. X k ∈ p_depth_set p n"
    using eventually_sequentially global_depth_set by force
  with that(1) show "x ∈ p_depth_set p n"
    using globally_limseq_imp_locally_limseq p_depth_set_p_limseq_closed by blast
qed

end (* context global_p_equal_depth *)

context global_p_equal_depth_div_inv_w_inj_index_consts
begin

lemma shift_p_depth_p_open_nbhd:
  "shift_p_depth p n ` p_open_nbhd p m x = p_open_nbhd p (m + n) (shift_p_depth p n x)"
proof safe
  fix y assume y: "y ∈ p_open_nbhd p m x"
  show "shift_p_depth p n y ∈ p_open_nbhd p (m + n) (shift_p_depth p n x)"
    unfolding p_open_nbhd_eq_circle
  proof clarify
    assume *: "¬ p_equal p (shift_p_depth p n y) (shift_p_depth p n x)"
    hence "¬ p_equal p y x" using shift_p_depth_equiv_iff by force
    moreover from this y have "p_depth p (y - x) + n ≥ m + n"
      using p_open_nbhd_eq_circle by auto
    ultimately show "p_depth p (shift_p_depth p n y - shift_p_depth p n x) ≥ m + n"
      using conv_0 shift_p_depth_at_place shift_p_depth_minus by metis
  qed
next
  fix y assume y: "y ∈ p_open_nbhd p (m + n) (shift_p_depth p n x)"
  have "shift_p_depth p (-n) y ∈ p_open_nbhd p m x"
  proof (cases "n = 0", use y in auto)
    case n: False show ?thesis
    proof (cases "p_equal p y (shift_p_depth p n x)")
      case True
      hence "p_equal p (shift_p_depth p (-n) y) x"
        using shift_p_depth_equiv_iff[of p p "-n" y] shift_shift_p_depth[of p "-n" n x] by force
      thus "shift_p_depth p (-n) y ∈ p_open_nbhd p m x" using p_open_nbhd_eq_circle by simp
    next
      case False
      moreover from this y have "p_depth p (y - shift_p_depth p n x) + (-n) ≥ m"
        using p_open_nbhd_diff_depth by fastforce
      moreover have "shift_p_depth p (-n) (shift_p_depth p n x) = x"
        using shift_shift_p_depth by simp
      ultimately have "p_depth p (shift_p_depth p (-n) y - x) ≥ m"
        using n conv_0 shift_p_depth_at_place shift_p_depth_minus by metis
      with False show "shift_p_depth p (-n) y ∈ p_open_nbhd p m x"
        using p_open_nbhd_eq_circle shift_p_depth_equiv_iff[of p p "-n" y "shift_p_depth p n x"]
              shift_shift_p_depth
        by    blast
    qed
  qed
  moreover have "y = shift_p_depth p n (shift_p_depth p (-n) y)"
    using shift_shift_p_depth by auto
  ultimately show "y ∈ shift_p_depth p n ` p_open_nbhd p m x" by blast
qed

lemma shift_p_depth_p_open_set:
  "generate_topology (local_p_open_nbhds p) (shift_p_depth p n ` A)"
  if "generate_topology (local_p_open_nbhds p) A"
proof (rule iffD2, rule p_open_nbhds_open_subopen, clarify)
  fix a assume "a ∈ A"
  with that obtain m where "p_open_nbhd p m a ⊆ A"
    using p_open_nbhds_open_subopen by fastforce
  hence "shift_p_depth p n ` p_open_nbhd p m a ⊆ shift_p_depth p n ` A" by fast
  moreover have
    "shift_p_depth p n ` p_open_nbhd p m a = p_open_nbhd p (m + n) (shift_p_depth p n a)"
    using shift_p_depth_p_open_nbhd by blast
  ultimately
    show  "∃m. p_open_nbhd p m (shift_p_depth p n a) ⊆ shift_p_depth p n ` A"
    by    fast
qed

end (* context global_p_equal_depth_div_inv_w_inj_index_consts *)

locale p_complete_global_p_equal_depth = global_p_equal_depth +
  assumes complete:
    "p_cauchy p X ⟹ p_open_nbhds_convergent (λn. p_restrict (X n) ((=) p))"
begin

lemma p_cauchyE:
  assumes "p_cauchy p X"
  obtains x where "p_open_nbhds_LIMSEQ (λn. p_restrict (X n) ((=) p)) x"
  using   assms complete t2_p_open_nbhds.convergent_def
  by      blast

end (* locale p_complete_global_p_equal_depth *)

text ‹Hensel's Lemma.›

context p_equality_div_inv
begin

― ‹A sequence to approach a root from within the ring of integers.›
primrec hensel_seq :: "'a ⇒ 'b poly ⇒ 'b ⇒ nat ⇒ 'b"
  where "hensel_seq p f x 0 = x" |
  "hensel_seq p f x (Suc n) = (
    if p_equal p (poly f (hensel_seq p f x n)) 0 then hensel_seq p f x n
    else
      hensel_seq p f x n - (poly f (hensel_seq p f x n)) / (poly (polyderiv f) (hensel_seq p f x n))
  )"

lemma constant_hensel_seq_case:
  "k ≥ n ⟹ hensel_seq p f x k = hensel_seq p f x n"
  if "p_equal p (poly f (hensel_seq p f x n)) 0"
proof (induct k)
  case (Suc k) thus ?case by (cases "n = Suc k", simp, use that in force)
qed simp

end (* context p_equality_div_inv *)

context p_equality_depth_div_inv
begin

― ‹Context for inductive steps leading to Hensel's Lemma.›
context
  fixes p :: 'a and f :: "'b poly" and x :: 'b and n :: nat
  assumes f_deg   : "degree f > 0"
    and   f_depth : "set (coeffs f) ⊆ p_depth_set p 0"
    and   d_hensel: "hensel_seq p f x n ∈ p_depth_set p 0"
    and   f       : "¬ p_equal p (poly f (hensel_seq p f x n)) 0"
    and   deriv_f : "¬ p_equal p (poly (polyderiv f) (hensel_seq p f x n)) 0"
    and   df      :
      "p_depth p (poly f (hensel_seq p f x n)) >
        2 * p_depth p (poly (polyderiv f) (hensel_seq p f x n))"
begin

lemma hensel_seq_step_1:
  "p_depth p (poly f (hensel_seq p f x (Suc n))) >
    p_depth p (poly f ((hensel_seq p f x n)))"
  if  next_f: "¬ p_equal p (poly f (hensel_seq p f x (Suc n))) 0"
proof (cases f)
  case (pCons c q)
  define a a' where "a ≡ hensel_seq p f x n" and "a' ≡ hensel_seq p f x (Suc n)"
  define b where "b ≡ - ((poly f a) / (poly (polyderiv f) a))"
  define c_add_poly :: "nat ⇒ 'b poly"
    where "c_add_poly ≡ coeff (additive_poly_poly f)"
  define  sum_fun Suc_sum_fun :: "nat ⇒ 'b"
    where "sum_fun     ≡ λi. poly (c_add_poly i) a * b ^ i"
    and   "Suc_sum_fun ≡ λi. poly (c_add_poly (Suc i)) a * b ^ (Suc i)"
  define S :: "'b" where "S ≡ sum Suc_sum_fun {1..degree q}"
  moreover from sum_fun_def Suc_sum_fun_def have Suc_sum_fun: "Suc_sum_fun = sum_fun ∘ Suc"
    by auto
  moreover have "{0..degree q} = {..degree q}" by auto
  moreover from f_deg pCons have "degree f = Suc (degree q)" by auto
  ultimately have "poly f a' = poly f a + poly (polyderiv f) a * b + S"
    using f a_def a'_def b_def c_add_poly_def sum_fun_def additive_poly_poly_decomp[of f a b]
          sum_up_index_split[of sum_fun 0] sum.atLeast_Suc_atMost_Suc_shift[of sum_fun 0]
          sum_up_index_split[of "sum_fun ∘ Suc" 0] additive_poly_poly_coeff0[of f]
          additive_poly_poly_coeff1[of f]
    by    (simp add: ac_simps)
  with deriv_f a_def b_def have equiv_sum: "p_equal p (poly f a') S"
    using minus_divide_left times_divide_eq_right mult_divide_cancel_left add_left
          add.right_inverse add_equiv0_left
    by    metis
  with next_f a'_def have "¬ p_equal p S 0" using trans by fast
  from this f_depth d_hensel a_def c_add_poly_def Suc_sum_fun_def S_def obtain j where j:
    "j ∈ {1..degree q}" "p_depth p S ≥ int (Suc j) * p_depth p b"
    using sum_poly_additive_poly_poly_depth_bound[of f p] by force
  from f_depth f deriv_f d_hensel df a_def b_def have "p_depth p b ≥ 0"
    using p_depth_poly_deriv_quotient depth_uminus[of p b] by fastforce
  moreover from j(1) have "2 ≤ int (Suc j)" by force
  ultimately have "int (Suc j) * p_depth p b ≥ 2 * p_depth p b" using mult_right_mono by blast
  moreover from f deriv_f a_def b_def
    have  "p_depth p b = p_depth p (poly f a) - p_depth p (poly (polyderiv f) a)"
    using divide_equiv_0_iff depth_uminus divide_depth by metis
  ultimately show "p_depth p (poly f a') > p_depth p (poly f a)"
    using j(2) df a_def equiv_sum depth_equiv by force
qed

lemma hensel_seq_step_2:
  "¬ p_equal p (poly (polyderiv f) (hensel_seq p f x (Suc n))) 0"
  "p_depth p (poly (polyderiv f) (hensel_seq p f x (Suc n))) =
    p_depth p (poly (polyderiv f) (hensel_seq p f x n))"
proof-

  define a a' where "a ≡ hensel_seq p f x n" and "a' ≡ hensel_seq p f x (Suc n)"
  define b where "b ≡ - ((poly f a) / (poly (polyderiv f) a))"
  from f deriv_f a_def b_def
    have  db: "p_depth p b = p_depth p (poly f a) - p_depth p (poly (polyderiv f) a)"
    using divide_equiv_0_iff depth_uminus divide_depth by metis

  have
    "p_depth p (poly (polyderiv f) (a')) = p_depth p (poly (polyderiv f) a) ∧
      ¬ p_equal p (poly (polyderiv f) a') 0"
  proof (cases "degree (polyderiv f)")
    case (Suc m)
    define  c_add_poly :: "nat ⇒ 'b poly"
      where "c_add_poly ≡ coeff (additive_poly_poly (polyderiv f))"
    define sum_fun :: "nat ⇒ 'b"
      where "sum_fun ≡ λi. poly (c_add_poly i) a * b ^ i"
    define S :: "'b" where "S ≡ sum (sum_fun ∘ Suc) {0..m}"
    from f a_def a'_def b_def Suc c_add_poly_def sum_fun_def S_def have diff_eq_sum:
      "poly (polyderiv f) a' - poly (polyderiv f) a = S"
      using additive_poly_poly_decomp[of "polyderiv f" a b] sum_up_index_split[of sum_fun 0]
            sum.atLeast_Suc_atMost_Suc_shift[of sum_fun 0]
      by    (simp add: algebra_simps additive_poly_poly_coeff0)
    show ?thesis
    proof (cases "p_equal p S 0", safe)
      case True
      from True show
        "p_depth p (poly (polyderiv f) a') = p_depth p (poly (polyderiv f) a)"
        using diff_eq_sum conv_0 depth_equiv by metis
      from deriv_f a_def True show "p_equal p (poly (polyderiv f) a') 0 ⟹ False"
        using diff_eq_sum conv_0 trans_right by blast
    next
      case False
      from this f_depth d_hensel a_def S_def sum_fun_def c_add_poly_def obtain j
        where j: "p_depth p S ≥ int (Suc j) * p_depth p b"
        using p_depth_set_polyderiv[of f p 0]
              sum_poly_additive_poly_poly_depth_bound[of "polyderiv f" p a b 0 m]
        by    force
      from f_depth d_hensel deriv_f a_def have "p_depth p (poly (polyderiv f) a) ≥ 0"
        using poly_p_depth_set_polyderiv[of 0 f p a] p_depth_setD[of p "poly (polyderiv f) a" 0]
        by    simp
      hence
        "p_depth p (poly (polyderiv f) a) ≤
          int (Suc j) * (2 * p_depth p (poly (polyderiv f) a) - p_depth p (poly (polyderiv f) a))"
        using mult_right_mono[of 1 "int (Suc j)"] by auto
      also from df a_def have "… < int (Suc j) * p_depth p b" using db by simp
      finally have *:
        "p_depth p (poly (polyderiv f) a) <
          p_depth p (poly (polyderiv f) a' - poly (polyderiv f) a)"
        using j diff_eq_sum by fastforce
      with deriv_f a_def
        show  "p_depth p (poly (polyderiv f) a') = p_depth p (poly (polyderiv f) a)"
        using depth_diff_cancel_imp_eq_depth_right by blast
      show "p_equal p (poly (polyderiv f) a') 0 ⟹ False"
        using * depth_diff_equiv0_left by fastforce
    qed
  qed (elim degree_eq_zeroE, simp, use deriv_f in fastforce)

  thus  "p_depth p (poly (polyderiv f) (a')) = p_depth p (poly (polyderiv f) a)"
    and "¬ p_equal p (poly (polyderiv f) a') 0"
    by  auto

qed

end (* Hensel's step context *)

― ‹Context for Hensel's Lemma.›
context
  fixes p :: 'a and f :: "'b poly" and x :: 'b
  assumes f_deg       : "degree f > 0"
    and   f_depth     : "set (coeffs f) ⊆ p_depth_set p 0"
    and   d_init      : "x ∈ p_depth_set p 0"
    and   init_deriv  :
      "¬ p_equal p (poly f x) 0 ⟶ ¬ p_equal p (poly (polyderiv f) x) 0"
    and   d_init_deriv:
      "¬ p_equal p (poly f x) 0 ⟶
        p_depth p (poly f x) > 2 * p_depth p (poly (polyderiv f) x)"
begin

lemma
      hensel_seq_adelic_int : "hensel_seq p f x n ∈ p_depth_set p 0" (is "?A")
  and hensel_seq_poly_depth :
    "¬ p_equal p (poly f (hensel_seq p f x n)) 0 ⟶
      p_depth p (poly f (hensel_seq p f x n)) ≥ p_depth p (poly f x) + int n"
      (is "?B")
  and hensel_seq_deriv      :
    "¬ p_equal p (poly f (hensel_seq p f x n)) 0 ⟶
      ¬ p_equal p (poly (polyderiv f) (hensel_seq p f x n)) 0"
      (is "?C")
  and hensel_seq_deriv_depth:
    "¬ p_equal p (poly f (hensel_seq p f x n)) 0 ⟶
      p_depth p (poly (polyderiv f) (hensel_seq p f x n)) = p_depth p (poly (polyderiv f) x)"
      (is "?D")
  and hensel_seq_depth_ineq:
    "¬ p_equal p (poly f (hensel_seq p f x n)) 0 ⟶
      p_depth p (poly f (hensel_seq p f x n)) >
      2 * p_depth p (poly (polyderiv f) (hensel_seq p f x n))"
      (is "?E")
proof-

  have "?A ∧ ?B ∧ ?C ∧ ?D ∧ ?E"
  proof (induct n, use d_init init_deriv d_init_deriv in force)
    case (Suc n)
    define a a' where "a ≡ hensel_seq p f x n" and "a' ≡ hensel_seq p f x (Suc n)"
    show ?case
    proof (cases "p_equal p (poly f a) 0")
      case False show ?thesis
      proof (fold a_def a'_def, safe)

        from False Suc a_def a'_def
          have  prev_int        : "a ∈ p_depth_set p 0"
          and   prev_poly_depth : "p_depth p (poly f a) ≥ p_depth p (poly f x) + int n"
          and   prev_deriv      : "¬ p_equal p (poly (polyderiv f) a) 0"
          and   prev_deriv_depth:
            "p_depth p (poly (polyderiv f) a) = p_depth p (poly (polyderiv f) x)"
          and   prev_depth_ineq : "p_depth p (poly f a) > 2 * p_depth p (poly (polyderiv f) a)"
          by    auto

        define b where "b ≡ (poly f a) / (poly (polyderiv f) a)"
        with f_depth False a_def a'_def b_def show "a' ∈ p_depth_set p 0"
          using prev_int prev_deriv prev_depth_ineq p_depth_set_minus
                p_depth_set_poly_deriv_quotient[of 0 f p]
          by    force

        from f_deg f_depth a_def a'_def False
          show  next_deriv: "p_equal p (poly (polyderiv f) a') 0 ⟹ False"
          using hensel_seq_step_2(1) prev_int prev_deriv prev_depth_ineq by blast

        from f_deg f_depth a_def a'_def False show next_deriv_depth:
          "p_depth p (poly (polyderiv f) a') = p_depth p (poly (polyderiv f) x)"
          by (metis hensel_seq_step_2(2) prev_int prev_deriv prev_depth_ineq prev_deriv_depth)

        moreover assume *: "¬ p_equal p (poly f a') 0"

        ultimately
          show  "p_depth p (poly f a') > 2 * p_depth p (poly (polyderiv f) a')"
          using f_deg f_depth a_def a'_def False hensel_seq_step_1 prev_int prev_deriv
                prev_depth_ineq next_deriv prev_depth_ineq prev_deriv_depth next_deriv_depth
          by    force

        from f_deg f_depth a_def a'_def False
          show  "p_depth p (poly f a') ≥ p_depth p (poly f x) + int (Suc n)"
          using * hensel_seq_step_1 prev_int prev_deriv prev_depth_ineq next_deriv prev_poly_depth
          by    force

      qed
    qed (simp add: a_def Suc)
  qed

  thus ?A ?B ?C ?D ?E by auto

qed

lemma hensel_seq_cauchy: "p_cauchy p (hensel_seq p f x)"
proof (rule iffD2, rule p_consec_cauchy, clarify)
  fix n
  show "∃K. p_consec_cauchy_condition p (hensel_seq p f x) n K"
  proof (cases "∃N. p_equal p (poly f (hensel_seq p f x N)) 0")
    case True
    from this obtain N where N: "p_equal p (poly f (hensel_seq p f x N)) 0" by fast
    have "p_consec_cauchy_condition p (hensel_seq p f x) n N"
    proof (intro p_consec_cauchy_conditionI)
      fix k
      assume  "k ≥ N"
        and   "¬ p_equal p (hensel_seq p f x (Suc k)) (hensel_seq p f x k)"
      with N show "p_depth p (hensel_seq p f x (Suc k) - hensel_seq p f x k) > n"
        using constant_hensel_seq_case[of p f x N k] by auto
    qed
    thus ?thesis by blast
  next
    case False
    hence *: "∀n. ¬ p_equal p (poly f (hensel_seq p f x n)) 0" by fast
    define d where "d ≡ p_depth p (poly f x) - p_depth p (poly (polyderiv f) x)"
    define K where "K ≡ nat (n - d + 1)"
    have "p_consec_cauchy_condition p (hensel_seq p f x) n K"
    proof (intro p_consec_cauchy_conditionI)
      fix k assume "k ≥ K"
      moreover define a a'
        where "a ≡ hensel_seq p f x k" and "a' ≡ hensel_seq p f x (Suc k)"
      moreover define b where "b ≡ - ((poly f a) / (poly (polyderiv f) a))"
      moreover from this a_def
        have  "p_depth p b = p_depth p (poly f a) - p_depth p (poly (polyderiv f) a)"
        using * hensel_seq_deriv divide_equiv_0_iff depth_uminus divide_depth by metis
      ultimately show "p_depth p (a' - a) > n"
        using d_def K_def * hensel_seq_deriv_depth hensel_seq_poly_depth by fastforce
    qed
    thus ?thesis by blast
  qed
qed

lemma p_limseq_poly_hensel_seq: "p_limseq p (λn. poly f (hensel_seq p f x n)) 0"
proof
  fix n
  define K where "K ≡ nat (n - p_depth p (poly f x) + 1)"
  have "p_limseq_condition p (λn. poly f (hensel_seq p f x n)) 0 n K"
  proof (intro p_limseq_conditionI)
    fix k assume "k ≥ K" and "¬ p_equal p (poly f (hensel_seq p f x k)) 0"
    with K_def show "p_depth p (poly f (hensel_seq p f x k) - 0) > n"
      using hensel_seq_poly_depth by fastforce
  qed
  thus "∃K. p_limseq_condition p (λn. poly f (hensel_seq p f x n)) 0 n K" by fast
qed

end (* Hensel's lemma context *)

end (* context p_equality_depth_div_inv *)


locale p_complete_global_p_equal_depth_div_inv =
  global_p_equal_depth_div_inv + p_complete_global_p_equal_depth
begin

lemma hensel:
  fixes p :: 'a and f :: "'b poly" and x :: 'b
  assumes "degree f > 0"
    and   "set (coeffs f) ⊆ p_depth_set p 0"
    and   "x ∈ p_depth_set p 0"
    and
      "¬ p_equal p (poly f x) 0 ⟶ ¬ p_equal p (poly (polyderiv f) x) 0"
    and
      "¬ p_equal p (poly f x) 0 ⟶
        p_depth p (poly f x) > 2 * p_depth p (poly (polyderiv f) x)"
  obtains z where "z ∈ p_depth_set p 0" and "p_equal p (poly f z) 0"
proof-
  define X where "X ≡ hensel_seq p f x"
  define res_X where "res_X ≡ λn. p_restrict (X n) ((=) p)"
  from assms X_def res_X_def obtain z where "p_open_nbhds_LIMSEQ res_X z"
    using hensel_seq_cauchy p_cauchyE by blast
  hence "p_limseq p res_X z" using globally_limseq_iff_locally_limseq by blast
  with res_X_def have X_to_z: "p_limseq p X z" using p_limseq_p_restrict_iff by blast
  with assms X_def have "p_equal p (poly f z) 0"
    using poly_continuous_p_open_nbhds p_limseq_poly_hensel_seq p_limseq_unique by metis
  moreover from assms X_def have "z ∈ p_depth_set p 0"
    using X_to_z hensel_seq_adelic_int p_depth_set_p_limseq_closed by fastforce
  ultimately show thesis using that by blast
qed

end (* locale p_complete_global_p_equal_depth_div_inv *)


subsubsection ‹Globally›

text ‹We use bounded depth to create a global metric.›

context p_equality_depth
begin

definition bdd_global_depth :: "'b ⇒ nat"
  where
    "bdd_global_depth x =
      (if globally_p_equal x 0 then 0 else Inf {nat (p_depth p x + 1) | p. ¬ p_equal p x 0})"
― ‹The plus-one is to distinguish depth-0 from negative depth.›

lemma bdd_global_depth_0[simp]: "globally_p_equal x 0 ⟹ bdd_global_depth x = 0"
  unfolding bdd_global_depth_def by simp

lemma bdd_global_depthD:
  "bdd_global_depth x = Inf {nat (p_depth p x + 1) | p. ¬ p_equal p x 0}"
  if "¬ globally_p_equal x 0"
  using that unfolding bdd_global_depth_def by argo

lemma bdd_global_depthD_as_image:
  "bdd_global_depth x = (INF p∈{p. ¬ p_equal p x 0}. nat (p_depth p x + 1))"
  if "¬ globally_p_equal x 0"
  using that image_Collect unfolding bdd_global_depth_def by metis

lemma bdd_global_depth_cong:
  "bdd_global_depth x = bdd_global_depth y" if "globally_p_equal x y"
proof (cases "globally_p_equal x 0")
  case True with that show ?thesis using globally_p_equal_trans_right[of x y 0] by fastforce
next
  case False
  moreover from that have "{p. ¬ p_equal p x 0} = {p. ¬ p_equal p y 0}"
    using trans[of _ x y 0] trans_right[of _ x y 0] by auto
  moreover from that
    have  "(λp. nat (p_depth p x + 1)) = (λp. nat (p_depth p y + 1))"
    using depth_equiv[of _ x y]
    by    simp
  ultimately show ?thesis using that globally_p_equal_trans bdd_global_depthD_as_image by metis
qed

lemma bdd_global_depth_le:
  "bdd_global_depth x ≤ nat (p_depth p x + 1)" if "¬ p_equal p x 0"
  using that bdd_global_depthD_as_image cINF_lower[of "λp. nat (p_depth p x + 1)"]
  by    fastforce

lemma bdd_global_depth_greatest:
  "bdd_global_depth x ≥ B"
  if  "¬ p_equal p x 0"
  and "∀q. ¬ p_equal q x 0 ⟶ nat (p_depth q x + 1) ≥ B"
  using that bdd_global_depthD_as_image
        cINF_greatest[of
          "{p. ¬ p_equal p x 0}" B "λp. nat (p_depth p x + 1)"
        ]
  by    fastforce

lemma bdd_global_depth_witness:
  assumes "¬ globally_p_equal x 0"
  obtains p where "¬ p_equal p x 0" and "bdd_global_depth x = nat (p_depth p x + 1)"
proof-
  define D where "D ≡ {nat (p_depth p x + 1) | p. ¬ p_equal p x 0}"
  from assms obtain q where "¬ p_equal q x 0" by blast
  with D_def have "nat (p_depth q x + 1) ∈ D" by force
  with assms D_def obtain p
    where "¬ p_equal p x 0"
    and   "bdd_global_depth x = nat (p_depth p x + 1)"
    using wellorder_InfI[of _ D] bdd_global_depthD
    by    auto
  with that show thesis by meson
qed

lemma bdd_global_depth_eq_0:
  "bdd_global_depth x = 0" if "p_depth p x < 0"
  using that depth_equiv_0 bdd_global_depth_le[of p x] by fastforce

lemma bdd_global_depth_eq_0_iff:
  "bdd_global_depth x = 0 ⟷
    (∃p. p_depth p x < 0) ∨ (globally_p_equal x 0)"
  (is "?L = ?R")
proof
  assume L: ?L show ?R
  proof clarify
    assume "¬ globally_p_equal x 0"
    from this obtain p where "¬ p_equal p x 0" and "bdd_global_depth x = nat (p_depth p x + 1)"
      using bdd_global_depth_witness[of x] by auto
    with L have "p_depth p x < 0" by force
    thus "∃p. p_depth p x < 0" by blast
  qed
next
  assume ?R thus ?L by (cases "globally_p_equal x 0", use bdd_global_depth_eq_0 in auto)
qed

lemma bdd_global_depth_diff: "bdd_global_depth (x - y) = bdd_global_depth (y - x)"
  using depth_diff conv_0 sym_iff[of _ x y] unfolding bdd_global_depth_def by simp

lemma bdd_global_depth_uminus: "bdd_global_depth (- x) = bdd_global_depth x"
  using depth_uminus uminus_iff[of _ x 0] unfolding bdd_global_depth_def by auto

lemma bdd_global_depth_nonarch:
  "bdd_global_depth (x + y) ≥ min (bdd_global_depth x) (bdd_global_depth y)"
  if "¬ globally_p_equal (x + y) 0"
proof-
  consider  "globally_p_equal x 0" | "globally_p_equal y 0" |
            (n0) "¬ globally_p_equal x 0" "¬ globally_p_equal y 0"
    by      blast
  thus ?thesis
  proof cases
    case n0
    define N :: "'b ⇒ 'a set" where "N ≡ λx. {p. ¬ p_equal p x 0}"
    define dp1 where "dp1 ≡ λx p. p_depth p x + 1"
    define trunc_dp1 where "trunc_dp1 ≡ λx p. nat (dp1 x p)"
    define inf_trunc_dp1 :: "'b ⇒ nat"
      where "inf_trunc_dp1 ≡ λx. (INF p∈N x. trunc_dp1 x p)"
    from inf_trunc_dp1_def have inf_trunc_dp1:
      "⋀p x. p ∈ N x ⟹ inf_trunc_dp1 x ≤ trunc_dp1 x p"
      using cINF_lower by fast
    define choose_dpth :: "'a ⇒ int" where
      "choose_dpth ≡ λp.
        if p_equal p x 0 then dp1 y p
        else if p_equal p y 0 then dp1 x p
        else min (dp1 x p) (dp1 y p)"
    from that n0 N_def
      have  nempty: "N x ≠ {}" "N y ≠ {}" "N (x + y) ≠ {}"
      using globally_p_equalI
      by    (blast, blast, blast)
    have
      "Inf ((nat ∘ choose_dpth) ` (N x ∪ N y)) =
        min (inf_trunc_dp1 x) (inf_trunc_dp1 y)"
    proof (intro cInf_eq_non_empty)
      fix n assume "n ∈ (nat ∘ choose_dpth) ` (N x ∪ N y)"
      from this obtain p where "p ∈ N x ∪ N y" "n = nat (choose_dpth p)" by auto
      thus "min (inf_trunc_dp1 x) (inf_trunc_dp1 y) ≤ n"
        using N_def trunc_dp1_def choose_dpth_def inf_trunc_dp1[of p x] inf_trunc_dp1[of p y]
        by    auto
    next
      fix n
      assume *:
        "⋀m. m ∈ (nat ∘ choose_dpth) ` (N x ∪ N y) ⟹
          n ≤ m"
      have "n ≤ inf_trunc_dp1 x"
        unfolding inf_trunc_dp1_def
      proof (intro cInf_greatest)
        fix m assume "m ∈ trunc_dp1 x ` N x"
        from this obtain p where "p ∈ N x" "m = trunc_dp1 x p" by blast
        with N_def trunc_dp1_def choose_dpth_def * show "n ≤ m"
          by (cases "p ∈ N y", fastforce, fastforce)
      qed (simp add: nempty(1))
      moreover have "n ≤ inf_trunc_dp1 y"
        unfolding inf_trunc_dp1_def
      proof (intro cInf_greatest)
        fix m assume "m ∈ trunc_dp1 y ` N y"
        from this obtain p where "p ∈ N y" "m = trunc_dp1 y p" by blast
        with N_def trunc_dp1_def choose_dpth_def * show "n ≤ m"
          by (cases "p ∈ N x", fastforce, fastforce)
      qed (simp add: nempty(2))
      ultimately
        show  "n ≤ min (inf_trunc_dp1 x) (inf_trunc_dp1 y)"
        by    auto
    qed (simp add: nempty(1))
    moreover from n0(1) have "inf_trunc_dp1 x = bdd_global_depth x"
      using     bdd_global_depthD_as_image
      unfolding N_def inf_trunc_dp1_def trunc_dp1_def dp1_def
      by        auto
    moreover from n0(2) have "inf_trunc_dp1 y = bdd_global_depth y"
      using     bdd_global_depthD_as_image
      unfolding N_def inf_trunc_dp1_def trunc_dp1_def dp1_def
      by        auto
    ultimately have
      "min (bdd_global_depth x) (bdd_global_depth y) =
        Inf ((nat ∘ choose_dpth) ` (N x ∪ N y))"
      by presburger
    also have "… ≤ inf_trunc_dp1 (x + y)"
      unfolding inf_trunc_dp1_def
    proof (intro cINF_mono nempty(3))
      fix p assume p: "p ∈ N (x + y)"
      with N_def have nequiv0:
        "¬ p_equal p (x + y) 0" "¬ p_equal p x 0 ∨ ¬ p_equal p y 0"
        using add[of p x 0 y 0] by auto
      from nequiv0(2) consider
        "p_equal p x 0" | "p_equal p y 0" "¬ p_equal p x 0" |
        (neither) "¬ p_equal p x 0" "¬ p_equal p y 0"
        by blast
      hence "(nat ∘ choose_dpth) p ≤ trunc_dp1 (x + y) p"
      proof cases
        case neither with nequiv0(1) show "(nat ∘ choose_dpth) p ≤ trunc_dp1 (x + y) p"
          using depth_nonarch
          by    (fastforce simp add: choose_dpth_def trunc_dp1_def dp1_def)
      qed (
        simp_all add: choose_dpth_def trunc_dp1_def dp1_def depth_add_equiv0_left
                      depth_add_equiv0_right
      )
      moreover from N_def nequiv0(2) have "p ∈ N x ∪ N y" by force
      ultimately show
        "∃q∈N x ∪ N y. (nat ∘ choose_dpth) q ≤ trunc_dp1 (x + y) p"
        by blast
    qed simp
    finally show ?thesis
      using that N_def inf_trunc_dp1_def trunc_dp1_def dp1_def bdd_global_depthD_as_image by simp
  qed simp_all
qed

definition bdd_global_dist :: "'b ⇒ 'b ⇒ real" where
  "bdd_global_dist x y =
    (if globally_p_equal x y then 0 else inverse (2 ^ bdd_global_depth (x - y)))"

lemma bdd_global_dist_eqD [simp]: "bdd_global_dist x y = 0" if "globally_p_equal x y"
  using that unfolding bdd_global_dist_def by simp

lemma bdd_global_distD:
  "bdd_global_dist x y = inverse (2 ^ bdd_global_depth (x - y))" if "¬ globally_p_equal x y"
  using that unfolding bdd_global_dist_def by fastforce

lemma bdd_global_dist_cong:
  "bdd_global_dist w x = bdd_global_dist y z"
  if "globally_p_equal w y" and "globally_p_equal x z"
proof (cases "globally_p_equal w x")
  case True with that show ?thesis using globally_p_equal_cong using bdd_global_dist_eqD by metis
next
  case False with that show ?thesis
    using globally_p_equal_sym globally_p_equal_cong bdd_global_distD globally_p_equal_minus
          bdd_global_depth_cong[of "w - x" "y - z"]
    by    metis
qed

lemma bdd_global_dist_nonneg: "bdd_global_dist x y ≥ 0"
  unfolding bdd_global_dist_def by auto

lemma bdd_global_dist_bdd: "bdd_global_dist x y ≤ 1"
  using     le_imp_inverse_le[of 1 "2 ^ bdd_global_depth (x - y)"]
  unfolding bdd_global_dist_def
  by        auto

lemma bdd_global_dist_lessI:
  "bdd_global_dist x y < e"
  if pos: "e > 0"
  and depth:
    "⋀p. ¬ p_equal p x y ⟹
      p_depth p (x - y) ≥ ⌊log 2 (inverse e)⌋"
proof (cases "e > 1")
  case True
  moreover have "bdd_global_dist x y ≤ 1" by (rule bdd_global_dist_bdd)
  ultimately show ?thesis by linarith
next
  case False
  hence small: "e ≤ 1" by linarith
  show ?thesis
  proof (cases "globally_p_equal x y")
    case False
    define d where "d ≡ ⌊log 2 (inverse e)⌋"
    have
      "∀p. ¬ p_equal p x y ⟶
        nat (p_depth p (x - y) + 1) ≥ nat (d + 1)"
    proof clarify
      fix p assume "¬ p_equal p x y"
      with depth d_def have *: "p_depth p (x - y) ≥ d" by simp
      moreover from pos d_def have "d ≥ 0"
        using small le_imp_inverse_le zero_le_log_cancel_iff[of 2 "inverse e"] by force
      ultimately have "p_depth p (x - y) + 1 > 0" by linarith
      with * show "nat (p_depth p (x - y) + 1) ≥ nat (d + 1)"
        using le_nat_iff[of "p_depth p (x - y) + 1" "nat d"] by simp
    qed
    with False have "bdd_global_depth (x - y) ≥ nat (d + 1)"
      using conv_0 bdd_global_depth_greatest by auto
    with d_def have "bdd_global_depth (x - y) ≥ d + 1" by auto
    with pos d_def have "e > inverse (2 ^ bdd_global_depth (x - y))"
      using real_of_int_floor_add_one_gt[of "log 2 (inverse e)"]
            log_pow_cancel[of 2 "bdd_global_depth (x - y)"]
            log_less_cancel_iff[of 2 "inverse e" "2 ^ bdd_global_depth (x - y)"]
            less_imp_inverse_less
      by    fastforce
    moreover from False have "bdd_global_dist x y = inverse (2 ^ bdd_global_depth (x - y))"
      using bdd_global_distD by force
    ultimately show ?thesis by simp
  qed (simp add: pos)
qed

lemma bdd_global_dist_less_imp:
  "p_depth p (x - y) ≥ ⌊log 2 (inverse e)⌋"
  if "e > 0" and "e ≤ 1" and "¬ p_equal p x y" and "bdd_global_dist x y < e"
proof-
  from that have "log 2 (inverse e) < bdd_global_depth (x - y)"
    using bdd_global_distD inverse_less_imp_less[of _ "inverse e"] log_less[of 2 "inverse e"]
    by    fastforce
  hence "⌊log 2 (inverse e)⌋ < bdd_global_depth (x - y)" by linarith
  with that(3) have "⌊log 2 (inverse e)⌋ < int (nat (p_depth p (x - y) + 1))"
    using conv_0 bdd_global_depth_le by fastforce
  moreover from that(1,2) have "⌊log 2 (inverse e)⌋ ≥ 0"
    using le_imp_inverse_le zero_le_log_cancel_iff[of 2 "inverse e"] by force
  ultimately show ?thesis by linarith
qed

lemma bdd_global_dist_less_pow2_iff:
  "bdd_global_dist x y < inverse (2 ^ n) ⟷
    (∀p. ¬ p_equal p x y ⟶ p_depth p (x - y) ≥ int n)"
proof (cases "globally_p_equal x y")
  case False show ?thesis
  proof (standard, standard, clarify)
    fix p assume "¬ p_equal p x y"
    moreover assume "bdd_global_dist x y < inverse (2 ^ n)"
    ultimately show "p_depth p (x - y) ≥ int n"
      using le_imp_inverse_le[of 1 "2 ^ n"] bdd_global_dist_less_imp[of "inverse (2 ^ n)" p x y]
      by    force
  next
    assume "∀p. ¬ p_equal p x y ⟶ p_depth p (x - y) ≥ int n"
    thus "bdd_global_dist x y < inverse (2 ^ n)" by (auto intro: bdd_global_dist_lessI)
  qed
qed simp

lemma bdd_global_dist_sym: "bdd_global_dist x y = bdd_global_dist y x"
  using globally_p_equal_sym bdd_global_depth_diff unfolding bdd_global_dist_def by force

lemma bdd_global_dist_conv0: "bdd_global_dist x y = bdd_global_dist (x - y) 0"
  using globally_p_equal_conv_0 unfolding bdd_global_dist_def by simp

lemma bdd_global_dist_conv0': "bdd_global_dist x y = bdd_global_dist 0 (x - y)"
  using bdd_global_dist_conv0 bdd_global_dist_sym by simp

lemma bdd_global_dist_nonarch:
  "bdd_global_dist x y ≤ max (bdd_global_dist x z) (bdd_global_dist y z)"
proof (cases "globally_p_equal x y")
  case True thus ?thesis
    using bdd_global_dist_nonneg[of x z] bdd_global_dist_nonneg[of y z] by simp
next
  case xy: False show ?thesis
  proof (cases "globally_p_equal x z")
    case True thus ?thesis
      using bdd_global_dist_cong[of x z y y] bdd_global_dist_sym by auto
  next
    case xz: False show ?thesis
    proof (cases "globally_p_equal y z")
      case True thus ?thesis
        using bdd_global_dist_cong[of y z x x] bdd_global_dist_sym by auto
    next
      case False with xy xz show ?thesis
      proof (induct x y rule: linorder_wlog'[of "λx. bdd_global_dist x z"])
        case (le x y)
        from le(2) have "¬ globally_p_equal ((x - z) + (z - y)) 0"
          using globally_p_equal_conv_0[of x y] by fastforce
        moreover from le(1,3,4) have "bdd_global_depth (x - z) ≥ bdd_global_depth (y - z)"
          using bdd_global_distD inverse_le_imp_le by auto
        ultimately have "bdd_global_depth (x - y) ≥ bdd_global_depth (y - z)"
          using bdd_global_depth_nonarch[of "x - z" "z - y"] bdd_global_depth_diff[of y z] by auto
        with le(1,2,4)
          show  "bdd_global_dist x y ≤ max (bdd_global_dist x z) (bdd_global_dist y z)"
          using le_imp_inverse_le bdd_global_distD
          by    auto
      next
        case (sym x y)
        hence "bdd_global_dist y x ≤ max (bdd_global_dist y z) (bdd_global_dist x z)"
          using globally_p_equal_sym[of y x] by blast
        thus ?case using bdd_global_dist_sym max.commute by metis
      qed
    qed
  qed
qed

lemma bdd_global_dist_ball_multicentre:
  "{z. bdd_global_dist y z < e} = {z. bdd_global_dist x z < e}"
  if "bdd_global_dist x y < e"
proof-
  define B where "B ≡ λx. {z. bdd_global_dist x z < e}"
  moreover have "⋀x y. bdd_global_dist x y < e ⟹ B y ⊆ B x"
    unfolding B_def
  proof clarify
    fix x y z
    assume "bdd_global_dist x y < e" and "bdd_global_dist y z < e"
    thus "bdd_global_dist x z < e"
      using bdd_global_dist_nonarch[of x z y] bdd_global_dist_sym by simp
  qed
  ultimately show ?thesis using that bdd_global_dist_sym by fastforce
qed

lemma bdd_global_dist_ball_at_0:
  "{z. bdd_global_dist 0 z < inverse (2 ^ n)} = global_depth_set (int n)"
  using bdd_global_dist_less_pow2_iff bdd_global_dist_sym unfolding global_depth_set_def by auto

lemma bdd_global_dist_ball_UNIV:
  "{z. bdd_global_dist x z < e} = UNIV" if "e > 1"
  using that bdd_global_dist_bdd order_le_less_subst1[of _ id 1 e] by fastforce

lemma bdd_global_dist_ball_at_0_normalize:
  "{z. bdd_global_dist 0 z < e} = global_depth_set (⌊log 2 (inverse e)⌋)"
  if "e > 0" and "e ≤ 1"
  using     that bdd_global_dist_less_imp bdd_global_dist_sym bdd_global_dist_lessI
  unfolding global_depth_set_def
  by        fastforce

lemma bdd_global_dist_ball_translate:
  "{z. bdd_global_dist x z < e} = x +o {z. bdd_global_dist 0 z < e}"
  unfolding elt_set_plus_def
proof safe
  fix y assume "bdd_global_dist x y < e"
  hence "bdd_global_dist 0 (y - x) < e"
    using bdd_global_dist_sym bdd_global_dist_conv0' by presburger
  moreover have "y = x + (y - x)" by auto
  ultimately show "∃b∈{z. bdd_global_dist 0 z < e}. y = x + b" by fast
next
  fix y assume "bdd_global_dist 0 y < e"
  thus "bdd_global_dist x (x + y) < e"
    using bdd_global_dist_conv0'[of "x + y" x] bdd_global_dist_sym by auto
qed

lemma bdd_global_dist_left_translate_continuous:
  "bdd_global_dist (x + y) (x + z) < e" if "bdd_global_dist y z < e"
  using that bdd_global_dist_conv0[of y z] bdd_global_dist_conv0[of "x + y" "x + z"] by simp

lemma bdd_global_dist_right_translate_continuous:
  "bdd_global_dist (y + x) (z + x) < e" if "bdd_global_dist y z < e"
  using that bdd_global_dist_conv0[of y z] bdd_global_dist_conv0[of "y + x" "z + x"] by simp

definition global_cauchy_condition ::
  "(nat ⇒ 'b) ⇒ nat ⇒ nat ⇒ bool"
  where
    "global_cauchy_condition X n K =
      (∀k1≥K. ∀k2≥K. ∀p.
        ¬ p_equal p (X k1) (X k2) ⟶ nat (p_depth p (X k1 - X k2)) > n
      )"

lemma global_cauchy_conditionI:
  "global_cauchy_condition X n K"
  if
    "⋀p k k'. k ≥ K ⟹ k' ≥ K ⟹
      ¬ p_equal p (X k) (X k') ⟹ nat (p_depth p (X k - X k')) > n"
  using that unfolding global_cauchy_condition_def by blast

lemma global_cauchy_conditionD:
  "nat (p_depth p (X k - X k')) > n"
  if  "global_cauchy_condition X n K" and "k ≥ K" and "k' ≥ K"
  and "¬ p_equal p (X k) (X k')"
  using that unfolding global_cauchy_condition_def by blast

lemma global_cauchy_condition_mono_seq_tail:
  "global_cauchy_condition X n K ⟹ global_cauchy_condition X n K'"
  if "K' ≥ K"
  using that unfolding global_cauchy_condition_def by auto

lemma global_cauchy_condition_mono_depth:
  "global_cauchy_condition X n K ⟹ global_cauchy_condition X m K"
  if "m ≤ n"
  using that unfolding global_cauchy_condition_def by fastforce

abbreviation "globally_cauchy X ≡ (∀n. ∃K. global_cauchy_condition X n K)"

lemma global_cauchy_condition_LEAST:
  "global_cauchy_condition X n (LEAST K. global_cauchy_condition X n K)" if "globally_cauchy X"
  using that Least1I[OF ex_ex1_least_nat_le] by blast

lemma global_cauchy_condition_LEAST_mono:
  "(LEAST K. global_cauchy_condition X m K) ≤ (LEAST K. global_cauchy_condition X n K)"
  if "globally_cauchy X" and "m ≤ n"
  using that least_le_least[OF ex_ex1_least_nat_le ex_ex1_least_nat_le]
        global_cauchy_condition_mono_depth
  by    force

definition bdd_global_uniformity :: "('b × 'b) filter"
  where "bdd_global_uniformity = (INF e∈{0 <..}. principal {(x, y). bdd_global_dist x y < e})"

end (* context p_equality_depth *)

context global_p_equal_depth
begin

sublocale metric_space_by_bdd_depth:
  metric_space bdd_global_dist bdd_global_uniformity
    "λU. ∀x∈U.
      eventually (λ(x', y). x' = x ⟶ y ∈ U) bdd_global_uniformity"
proof
  fix x y z
  define dxy dxz dyz
    where "dxy ≡ bdd_global_dist x y"
    and   "dxz ≡ bdd_global_dist x z"
    and   "dyz ≡ bdd_global_dist y z"
  hence "dxy ≤ max dxz dyz" using bdd_global_dist_nonarch by metis
  also from dxz_def dyz_def have "… ≤ max dxz dyz + min dxz dyz"
    using bdd_global_dist_def by auto
  finally show "dxy ≤ dxz + dyz" by auto
  from dxy_def show "(dxy = 0) = (x = y)" using global_eq_iff unfolding bdd_global_dist_def by simp
qed (simp only: bdd_global_uniformity_def, simp)

lemma nonneg_global_depth_set_LIMSEQ_closed:
  "x ∈ global_depth_set (int n)"
  if  lim: "metric_space_by_bdd_depth.LIMSEQ X x"
  and seq: "∀⇩F k in sequentially. X k ∈ global_depth_set (int n)"
proof (intro global_depth_setI)
  fix p assume p: "¬ p_equal p x 0"
  from seq obtain K where K: "∀k≥K. X k ∈ global_depth_set (int n)"
    using eventually_sequentially by fastforce
  from lim have "∀⇩F k in sequentially. bdd_global_dist (X k) x < inverse (2 ^ n)"
    using metric_space_by_bdd_depth.tendstoD[of X x sequentially "inverse (2 ^ n)"] by fastforce
  from this obtain K' :: nat
    where K': "∀k≥K'. bdd_global_dist (X k) x < inverse (2 ^ n)"
    using eventually_sequentially
    by    meson
  define m where "m ≡ max K K'"
  consider
    (eq) "p_equal p (X m) x" |
    (0)  "¬ p_equal p (X m) x"   "p_equal p (X m) 0" |
    (n0) "¬ p_equal p (X m) x" "¬ p_equal p (X m) 0"
    by blast
  thus "p_depth p x ≥ int n"
  proof cases
    case eq
    moreover from this K m_def have "X m ∈ global_depth_set (int n)" by auto
    ultimately show ?thesis using p trans_right global_depth_setD depth_equiv by metis
  next
    case 0 with K' m_def show ?thesis
      using bdd_global_dist_less_pow2_iff[of "X m" x n] depth_diff_equiv0_left by auto
  next
    case n0
    with p K K' m_def show ?thesis
      using bdd_global_dist_less_pow2_iff[of "X m" x n] global_depth_setD[of p "X m" "int n"]
            depth_pre_nonarch_diff_right[of p x "X m"]
      by    force
  qed
qed

lemma globally_cauchy_vs_bdd_metric_Cauchy:
  "globally_cauchy X = metric_space_by_bdd_depth.Cauchy X" for X :: "nat ⇒ 'b"
proof
  assume X: "globally_cauchy X" show "metric_space_by_bdd_depth.Cauchy X"
  proof (intro metric_space_by_bdd_depth.metric_CauchyI)
    fix e :: real assume pos: "e > 0"
    show "∃M. ∀m≥M. ∀n≥M. bdd_global_dist (X m) (X n) < e"
    proof (cases "e > 1")
      case True
      hence "∀m≥0. ∀n≥0. bdd_global_dist (X m) (X n) < e"
        using bdd_global_dist_bdd order_le_less_subst1[of _ id 1 e] by fastforce
      thus ?thesis by blast
    next
      case False
      hence small: "e ≤ 1" by simp
      define d where "d ≡ ⌊log 2 (inverse e)⌋"
      from X obtain M where M: "global_cauchy_condition X (nat d) M" by fast
      have "∀m≥M. ∀n≥M. bdd_global_dist (X m) (X n) < e"
      proof (clarify, intro bdd_global_dist_lessI pos)
        fix m n :: nat and p :: 'a
        assume "m ≥ M" and "n ≥ M" and "¬ p_equal p (X m) (X n)"
        with M have "nat (p_depth p (X m - X n)) > nat d" using global_cauchy_conditionD by blast
        moreover from d_def pos small have "d ≥ 0"
          using le_imp_inverse_le zero_le_log_cancel_iff[of 2 "inverse e"] by force
        ultimately show "p_depth p (X m - X n) ≥ ⌊log 2 (inverse e)⌋"
          using d_def by simp
      qed
      thus ?thesis by blast
    qed
  qed
next
  assume X: "metric_space_by_bdd_depth.Cauchy X" show "globally_cauchy X"
  proof
    fix n
    from X obtain M
      where M:
        "∀m≥M. ∀m'≥M. bdd_global_dist (X m) (X m') < inverse (2 ^ Suc n)"
      using metric_space_by_bdd_depth.metric_CauchyD[of X "inverse (2 ^ Suc n)"]
      by    auto
    hence "global_cauchy_condition X n M"
      using bdd_global_dist_less_pow2_iff[of _ _ "Suc n"]
      by    (fastforce intro: global_cauchy_conditionI)
    thus "∃M. global_cauchy_condition X n M" by fast
  qed
qed

end (* context global_p_equal_depth *)

context global_p_equal_depth_no_zero_divisors
begin

lemma bdd_global_dist_bdd_mult_continuous:
  "bdd_global_dist (w * x) (w * y) < e"
  if  pos  : "e > 0"
  and bdd  : "∀p. ¬ p_equal p w 0 ⟶ p_depth p w ≥ n"
  and input: "bdd_global_dist x y < min (e * 2 powi (n - 1)) 1"
proof (cases "e > 1", use bdd_global_dist_ball_UNIV in blast, intro bdd_global_dist_lessI pos)
  case False
  fix p assume p: "¬ p_equal p (w * x) (w * y)"
  from p have w: "¬ p_equal p w 0"
    using mult_0_left cong[of p 0 "w * x" 0 "w * y"] sym by force
  from p have xy: "¬ p_equal p x y" using mult_left by force
  from p have wxy: "¬ p_equal p (w * (x - y)) 0"
    using conv_0 right_diff_distrib[of w x y] by auto
  define d' where "d' ≡ e * 2 powi (n - 1)"
  define d  where "d  ≡ min d' 1"
  define m  where "m  ≡ ⌊log 2 (inverse d)⌋"
  from pos d_def d'_def have "d > 0" "d ≤ 1" by auto
  with input m_def d_def d'_def have "m ≤ p_depth p (x - y)"
    using xy bdd_global_dist_less_imp[of d p x y] by fast
  with bdd have *: "n + m ≤ p_depth p (w * x - w * y)"
    using w wxy right_diff_distrib[of w x y] depth_mult_additive[of p w "x - y"]
          bdd_global_depth_le[of p w]
    by    force
  moreover have "n + m ≥ log 2 (inverse e)"
  proof (cases "e * 2 powi (n - 1) < 1")
    case True
    moreover from m_def have "real_of_int (n + m) ≥ real_of_int n + (- log 2 d - 1)"
      using real_of_int_floor_ge_diff_one log_inverse by fastforce
    ultimately show ?thesis using d_def d'_def pos by (simp add: log_mult log_inverse algebra_simps)
  next
    case False
    moreover from this pos have "log 2 (e * 2 powi (n - 1)) ≥ 0"
      by (simp add: le_imp_inverse_le log_mono log_inverse)
    ultimately show ?thesis using pos m_def d_def d'_def
    by (fastforce simp add: log_mult log_inverse)
  qed
  ultimately show  "p_depth p (w * x - w * y) ≥ ⌊log 2 (inverse e)⌋" by linarith
qed

lemma bdd_global_dist_limseq_bdd_mult:
  "metric_space_by_bdd_depth.LIMSEQ (λk. w * X k) (w * x)"
  if  bdd: "∀p. ¬ p_equal p w 0 ⟶ p_depth p w ≥ n"
  and seq: "metric_space_by_bdd_depth.LIMSEQ X x"
proof
  fix e :: real assume e: "e > 0"
  define d where "d ≡ min (e * 2 powi (n - 1)) 1"
  with e have d: "d > 0" by auto
  with seq obtain K :: nat where "∀k≥K. bdd_global_dist (X k) x < d"
    using metric_space_by_bdd_depth.tendstoD[of X x] eventually_sequentially by meson
  with bdd e d_def have "∀k≥K. bdd_global_dist (w * X k) (w * x) < e"
    using bdd_global_dist_bdd_mult_continuous by blast
  thus "∀⇩F k in sequentially. bdd_global_dist (w * X k) (w * x) < e"
    using eventually_sequentially by blast
qed

end (* context global_p_equal_depth_no_zero_divisors *)

context global_p_equal_depth_div_inv_w_inj_index_consts
begin

lemma bdd_global_dist_limseq_global_uniformizer_powi_mult:
  "metric_space_by_bdd_depth.LIMSEQ
    (λk. global_uniformizer powi n * X k) (global_uniformizer powi n * x)"
  if "metric_space_by_bdd_depth.LIMSEQ X x"
  using that bdd_global_dist_limseq_bdd_mult[of _ n] p_depth_global_uniformizer_powi by auto

lemma global_depth_set_LIMSEQ_closed:
  "x ∈ global_depth_set n"
  if  lim  : "metric_space_by_bdd_depth.LIMSEQ X x"
  and depth: "∀⇩F k in sequentially. X k ∈ global_depth_set n"
proof-
  define Y and y
    where "Y ≡ λk. global_uniformizer powi (-n) * X k"
    and   "y ≡ global_uniformizer powi (-n) * x"
  from depth Y_def have "∀⇩F k in sequentially. Y k ∈ global_depth_set 0"
    using global_depth_set_eq_global_uniformizer_coset'[of n] eventually_sequentially by auto
  with Y_def y_def lim have "y ∈ global_depth_set 0"
    using bdd_global_dist_limseq_global_uniformizer_powi_mult
          nonneg_global_depth_set_LIMSEQ_closed[of Y y 0]
    by    simp
  moreover from y_def have "global_uniformizer powi n * y = x"
    using global_uniformizer_powi_add[of n "-n"] by (simp add: ac_simps)
  ultimately show ?thesis
    using global_depth_set_eq_global_uniformizer_coset[of n] by blast
qed

end (* context global_p_equality_w_inj_index_consts *)


subsection ‹Notation›

consts
  p_equal :: "'a ⇒ 'b ⇒ 'b ⇒ bool"
  globally_p_equal ::
    "'b ⇒ 'b ⇒ bool"
    ("(_/ ≃⇩∀⇩p/ _)" [51, 51] 50)
  p_restrict :: "'b ⇒ ('a ⇒ bool) ⇒ 'b" (infixl "prestrict" 70)
  p_depth :: "'a ⇒ 'b ⇒ int"
  p_depth_set :: "'a ⇒ int ⇒ 'b set" ("𝒫⇩@⇩_⇧_")
  global_depth_set :: "int ⇒ 'b set" ("𝒫⇩∀⇩p⇧_")
  global_unfrmzr_pows :: "('a ⇒ 'c) ⇒ 'b"

abbreviation p_equal_notation :: "'b ⇒ 'a ⇒ 'b ⇒ bool"
  ("(_/ ≃⇩_/ _)" [51, 51, 51] 50)
  where "p_equal_notation x p y ≡ p_equal p x y"

abbreviation p_nequal_notation :: "'b ⇒ 'a ⇒ 'b ⇒ bool"
  ("(_/ ¬≃⇩_/ _)" [51, 51, 51] 50)
  where "p_nequal_notation x p y ≡ ¬ p_equal p x y"

abbreviation p_depth_notation :: "'b ⇒ 'a ⇒ int"
  ("(_°⇧_)" [51, 51] 50)
  where "p_depth_notation x p ≡ p_depth p x"

abbreviation p_depth_set_0_notation :: "'a ⇒ 'b set" ("𝒪⇩@⇩_")
  where "p_depth_set_0_notation p ≡ p_depth_set p 0"

abbreviation p_depth_set_1_notation :: "'a ⇒ 'b set" ("𝒫⇩@⇩_")
  where "p_depth_set_1_notation p ≡ p_depth_set p 1"

abbreviation global_depth_set_0_notation :: "'b set" ("𝒪⇩∀⇩p")
  where "global_depth_set_0_notation ≡ global_depth_set 0"

abbreviation global_depth_set_1_notation :: "'b set" ("𝒫⇩∀⇩p")
  where "global_depth_set_1_notation ≡ global_depth_set 1"

abbreviation "𝔭 ≡ global_unfrmzr_pows"

end (* theory *)