Theory Elementary_Ultrametric_Spaces

(* Author: Benoît Ballenghien, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF
   Author: Benjamin Puyobro, Université Paris-Saclay, IRT SystemX, CNRS, ENS Paris-Saclay, LMF
   Author: Burkhart Wolff, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF *)

(*<*)
theory Elementary_Ultrametric_Spaces
  imports "HOL-Analysis.Elementary_Metric_Spaces"
begin
  (*>*)


section ‹Definition›

setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, NONE)›
  ― ‹To be able to use \<^const>‹dist› out of the \<^class>‹metric_space› class.›

class ultrametric_space = uniformity_dist + open_uniformity +
  assumes dist_eq_0_iff [simp]: ‹dist x y = 0 ⟷ x = y›
    and ultrametric_dist_triangle2: ‹dist x y ≤ max (dist x z) (dist y z)›
begin

subclass metric_space
proof (unfold_locales)
  show ‹dist x y = 0 ⟷ x = y› for x y by simp
next
  show ‹dist x y ≤ dist x z + dist y z› for x y z
    by (rule order_trans[OF ultrametric_dist_triangle2, of _ z], simp)
      (metis local.dist_eq_0_iff ultrametric_dist_triangle2 max.idem)
qed

end

setup ‹Sign.add_const_constraint (\<^const_name>‹dist›, SOME \<^typ>‹'a :: metric_space ⇒ 'a ⇒ real›)›
  ― ‹Back to normal.›


class complete_ultrametric_space = ultrametric_space +
  assumes Cauchy_convergent: ‹Cauchy X ⟹ convergent X›
begin

subclass complete_space by unfold_locales (fact Cauchy_convergent)

end



section ‹Properties on Balls›

text ‹In ultrametric space, balls satisfy very strong properties.›

context ultrametric_space begin

lemma ultrametric_dist_triangle: ‹dist x z ≤ max (dist x y) (dist y z)›
  using ultrametric_dist_triangle2 [of x z y] by (simp add: dist_commute)

lemma ultrametric_dist_triangle3: ‹dist x y ≤ max (dist a x) (dist a y)›
  using ultrametric_dist_triangle2 [of x y a] by (simp add: dist_commute)

end



subsection ‹Balls are centered everywhere›

context fixes x :: ‹'a :: ultrametric_space› begin

text ‹The best way to do this would be to work in the context \<^locale>‹ultrametric_space›.
      Unfortunately, \<^const>‹ball›, \<^const>‹cball›, etc. are not defined inside
      the context \<^locale>‹metric_space› but through a sort constraint.›

lemma ultrametric_every_point_of_ball_is_centre :
  ‹ball y r = ball x r› if ‹y ∈ ball x r› 
proof (unfold set_eq_iff, rule allI)
  from ‹y ∈ ball x r› have * : ‹dist x y < r› by simp
  show ‹z ∈ ball y r ⟷ z ∈ ball x r› for z
    using ultrametric_dist_triangle[of x z y]
      "*" ultrametric_dist_triangle[of y z x]
    by (intro iffI) (simp_all add: dist_commute)
qed


lemma ultrametric_every_point_of_cball_is_centre :
  ‹cball y r = cball x r› if ‹y ∈ cball x r›
proof (unfold set_eq_iff, rule allI)
  from ‹y ∈ cball x r› have * : ‹dist x y ≤ r› by simp
  show ‹z ∈ cball y r ⟷ z ∈ cball x r› for z
    using ultrametric_dist_triangle[of x z y]
      "*" ultrametric_dist_triangle[of y z x]
    by (intro iffI) (simp_all add: dist_commute)
qed

end



subsection ‹Balls are ``clopen''›

text ‹Balls are both open and closed.›

context fixes x :: ‹'a :: ultrametric_space› begin

lemma ultrametric_open_cball [intro, simp] : ‹open (cball x r)› if ‹0 < r›
proof (rule openI) 
  fix y assume ‹y ∈ cball x r›
  hence ‹cball y r = cball x r›
    by (rule ultrametric_every_point_of_cball_is_centre)
  hence ‹ball y (r / 2) ⊆ cball x r›
    by (metis ball_subset_cball cball_divide_subset_numeral subset_trans)
  moreover have ‹0 < r / 2› by (simp add: ‹0 < r›)
  ultimately show ‹∃e>0. ball y e ⊆ cball x r› by blast
qed

lemma ‹closed (cball y r)› by (fact closed_cball)


lemma ultrametric_closed_ball [intro, simp]: ‹closed (ball x r)› if ‹0 ≤ r›
proof (cases ‹r = 0›)
  show ‹r = 0 ⟹ closed (ball x r)› by simp
next
  assume ‹r ≠ 0›
  with ‹0 ≤ r› have ‹0 < r› by simp
  show ‹closed (ball x r)›
  proof (unfold closed_def)
    have ‹- ball x r = (⋃z ∈ - ball x r. ball z r)›
    proof (intro subset_antisym subsetI)
      from ‹0 < r› show ‹z ∈ - ball x r ⟹ z ∈ (⋃z∈- ball x r. ball z r)› for z
        by (meson UN_iff centre_in_ball)
    next
      show ‹z ∈ (⋃z ∈ - ball x r. ball z r) ⟹ z ∈ - ball x r› for z
        by simp (metis ComplD dist_commute mem_ball
            ultrametric_every_point_of_ball_is_centre)
    qed
    show ‹open (- ball x r)› by (subst ‹?this›, rule open_Union, simp)
  qed
qed

lemma ultrametric_open_sphere [intro, simp] : ‹0 < r ⟹ open (sphere x r)›
  by (fold cball_diff_eq_sphere) (simp add: open_Diff order_le_less)

lemma closed_sphere [intro, simp] : ‹closed (sphere y r)›
  by (metis open_ball cball_diff_eq_sphere closed_Diff closed_cball)

end



subsection ‹Balls are disjoint or contained›

context fixes x :: ‹'a :: ultrametric_space› begin

lemma ultrametric_ball_ball_disjoint_or_subset:
  ‹ball x r ∩ ball y s = {} ∨ ball x r ⊆ ball y s ∨
   ball y s ⊆ ball x r›
proof (unfold disj_imp, intro impI)
  assume ‹ball x r ∩ ball y s ≠ {}› ‹¬ ball x r ⊆ ball y s›
  from ‹ball x r ∩ ball y s ≠ {}›
  obtain z where ‹z ∈ ball x r› and ‹z ∈ ball y s› by blast
  with ultrametric_every_point_of_ball_is_centre
  have ‹ball x r = ball z r› and ‹ball y s = ball z s› by auto
  with ‹¬ ball x r ⊆ ball y s› have ‹s < r› by auto
  with ‹ball x r = ball z r› and ‹ball y s = ball z s›
  show ‹ball y s ⊆ ball x r› by auto
qed

lemma ultrametric_ball_cball_disjoint_or_subset:
  ‹ball x r ∩ cball y s = {} ∨ ball x r ⊆ cball y s ∨
   cball y s ⊆ ball x r›
proof (unfold disj_imp, intro impI)
  assume ‹ball x r ∩ cball y s ≠ {}› ‹¬ ball x r ⊆ cball y s›
  from ‹ball x r ∩ cball y s ≠ {}›
  obtain z where ‹z ∈ ball x r› and ‹z ∈ cball y s› by blast
  with ultrametric_every_point_of_ball_is_centre
    ultrametric_every_point_of_cball_is_centre
  have ‹ball x r = ball z r› ‹cball y s = cball z s› by blast+
  with ‹¬ ball x r ⊆ cball y s› have ‹s < r› by auto
  with ‹ball x r = ball z r› and ‹cball y s = cball z s›
  show ‹cball y s ⊆ ball x r› by auto
qed

corollary ultrametric_cball_ball_disjoint_or_subset:
  ‹cball x r ∩ ball y s = {} ∨ cball x r ⊆ ball y s ∨
   ball y s ⊆ cball x r›
  using Elementary_Ultrametric_Spaces.ultrametric_ball_cball_disjoint_or_subset by blast

lemma ultrametric_cball_cball_disjoint_or_subset:
  ‹cball x r ∩ cball y s = {} ∨ cball x r ⊆ cball y s ∨
   cball y s ⊆ cball x r›
proof (unfold disj_imp, intro impI)
  assume ‹cball x r ∩ cball y s ≠ {}› ‹¬ cball x r ⊆ cball y s›
  from ‹cball x r ∩ cball y s ≠ {}›
  obtain z where ‹z ∈ cball x r› and ‹z ∈ cball y s› by blast
  with ultrametric_every_point_of_cball_is_centre
  have ‹cball x r = cball z r› ‹cball y s = cball z s› by auto
  with ‹¬ cball x r ⊆ cball y s› have ‹s < r› by auto
  with ‹cball x r = cball z r› and ‹cball y s = cball z s›
  show ‹cball y s ⊆ cball x r› by auto
qed

end



subsection ‹Distance to a Ball›

context fixes a :: ‹'a :: ultrametric_space› begin

lemma ultrametric_equal_distance_to_ball:
  ‹dist a y = dist a z› if ‹a ∉ ball x r› ‹y ∈ ball x r› ‹z ∈ ball x r›
proof (rule order_antisym)
  show ‹dist a y ≤ dist a z›
    by (rule order_trans[OF ultrametric_dist_triangle[of a y z]], simp)
      (metis dist_commute dual_order.strict_trans2 linorder_linear
        mem_ball that ultrametric_every_point_of_ball_is_centre)
next
  show ‹dist a z ≤ dist a y›
    by (rule order_trans[OF ultrametric_dist_triangle[of a z y]], simp)
      (metis dist_commute dual_order.strict_trans2 linorder_linear
        mem_ball that ultrametric_every_point_of_ball_is_centre)
qed


lemma ultrametric_equal_distance_to_cball:
  ‹dist a y = dist a z› if ‹a ∉ cball x r› ‹y ∈ cball x r› ‹z ∈ cball x r›
proof (rule order_antisym)
  show ‹dist a y ≤ dist a z›
    by (rule order_trans[OF ultrametric_dist_triangle[of a y z]], simp)
      (metis dist_commute dual_order.trans linorder_linear mem_cball
        that ultrametric_every_point_of_cball_is_centre)
next
  show ‹dist a z ≤ dist a y›
    by (rule order_trans[OF ultrametric_dist_triangle[of a z y]], simp)
      (metis dist_commute dual_order.trans linorder_linear mem_cball
        that ultrametric_every_point_of_cball_is_centre)
qed

end


context fixes x :: ‹'a :: ultrametric_space› begin

lemma ultrametric_equal_distance_between_ball_ball:
  ‹ball x r ∩ ball y s = {} ⟹
   ∃d. ∀a ∈ ball x r. ∀b ∈ ball y s. dist a b = d›
  by (metis disjoint_iff dist_commute ultrametric_equal_distance_to_ball)          

lemma ultrametric_equal_distance_between_ball_cball:
  ‹ball x r ∩ cball y s = {} ⟹
   ∃d. ∀a ∈ ball x r. ∀b ∈ cball y s. dist a b = d›
  by (metis disjoint_iff dist_commute ultrametric_equal_distance_to_ball
      ultrametric_equal_distance_to_cball)

lemma ultrametric_equal_distance_between_cball_ball:
  ‹cball x r ∩ ball y s = {} ⟹
   ∃d. ∀a ∈ cball x r. ∀b ∈ ball y s. dist a b = d›
  by (metis disjoint_iff_not_equal dist_commute ultrametric_equal_distance_to_ball
      ultrametric_equal_distance_to_cball)

lemma ultrametric_equal_distance_between_cball_cball:
  ‹cball x r ∩ cball y s = {} ⟹
   ∃d. ∀a ∈ cball x r. ∀b ∈ cball y s. dist a b = d›
  by (metis disjoint_iff dist_commute ultrametric_equal_distance_to_cball)

end



section ‹Additional Properties›

text ‹Here are a few other interesting properties.›

subsection ‹Cauchy Sequences›

lemma (in ultrametric_space) ultrametric_dist_triangle_generalized:
  ‹n < m ⟹ dist (σ n) (σ m) ≤ (MAX l ∈ {n..m - 1}. dist (σ l) (σ (Suc l)))›
proof (induct m)
  show ‹n < 0 ⟹ dist (σ n) (σ 0) ≤ (MAX l∈{n..0 - 1}. dist (σ l) (σ (Suc l)))› by simp
next
  case (Suc m)
  show ‹dist (σ n) (σ (Suc m)) ≤ (MAX l∈{n..Suc m - 1}. dist (σ l) (σ (Suc l)))›
  proof (cases ‹n = m›)
    show ‹n = m ⟹ dist (σ n) (σ (Suc m)) ≤ (MAX l∈{n..Suc m - 1}. dist (σ l) (σ (Suc l)))›
      by simp
  next
    assume ‹n ≠ m›
    with ‹n < Suc m› obtain m' where ‹m = Suc m'› ‹n ≤ m'› 
      by (metis le_add1 less_Suc_eq less_imp_Suc_add)
    have ‹{n..Suc m'} = {n..m-1} ∪ {m}›
      by (simp add: ‹m = Suc m'› ‹n ≤ m'› atLeastAtMostSuc_conv le_Suc_eq)
    have ‹dist (σ n) (σ (Suc m)) ≤ max (dist (σ n) (σ m)) (dist (σ m) (σ (Suc m)))›
      by (simp add: ultrametric_dist_triangle)
    also have ‹… ≤ max ((MAX l∈{n..m - 1}. dist (σ l) (σ (Suc l)))) (dist (σ m) (σ (Suc m)))›
      using Suc.hyps Suc.prems ‹n ≠ m› by linarith
    also have ‹… = (MAX l∈{n..Suc m - 1}. dist (σ l) (σ (Suc l)))›
      by (subst Max_Un[of _ ‹((λl. dist (σ l) (σ (Suc l))) ` {m})›, simplified, symmetric])
        (simp_all add: ‹m = Suc m'› ‹n ≤ m'› ‹{n..Suc m'} = {n..m-1} ∪ {m}›)
    finally show ‹dist (σ n) (σ (Suc m)) ≤ (MAX l∈{n..Suc m - 1}. dist (σ l) (σ (Suc l)))› .
  qed
qed


lemma (in ultrametric_space) ultrametric_Cauchy_iff:
  ‹Cauchy σ ⟷ (λn. dist (σ (Suc n)) (σ n)) ⇢ 0›
proof (rule iffI)
  assume ‹Cauchy σ›
  show ‹(λn. dist (σ (Suc n)) (σ n)) ⇢ 0›
  proof (unfold lim_sequentially, intro allI impI)
    fix ε :: real
    assume ‹0 < ε›
    from ‹Cauchy σ›[unfolded Cauchy_altdef, rule_format, OF ‹0 < ε›]
    show ‹∃N. ∀n≥N. dist (dist (σ (Suc n)) (σ n)) 0 < ε›
      by (auto simp add: dist_commute)
  qed
next
  assume convergent : ‹(λn. dist (σ (Suc n)) (σ n)) ⇢ 0›
  show ‹Cauchy σ›
  proof (unfold Cauchy_altdef2, intro allI impI)
    fix ε :: real
    assume ‹0 < ε›
    from convergent[unfolded lim_sequentially, rule_format, OF ‹0 < ε›]
    obtain N where * : ‹N ≤ n ⟹ dist (σ (Suc n)) (σ n) < ε› for n
      by (simp add: dist_real_def) blast

    have ‹N < n ⟹ dist (σ n) (σ N) < ε› for n
    proof (subst dist_commute, rule le_less_trans)
      show ‹N < n ⟹ dist (σ N) (σ n) ≤ (MAX l∈{N..n - 1}. dist (σ l) (σ (Suc l)))›
        by (fact ultrametric_dist_triangle_generalized)
    next
      show ‹N < n ⟹ (MAX l∈{N..n - 1}. dist (σ l) (σ (Suc l))) < ε›
        by simp (metis "*" atLeastAtMost_iff dist_commute)
    qed
    with ‹0 < ε› have ‹N ≤ n ⟹ dist (σ n) (σ N) < ε› for n
      by (cases ‹N = n›) simp_all 
    thus ‹∃N. ∀n≥N. dist (σ n) (σ N) < ε› by blast
  qed
qed



subsection ‹Isosceles Triangle Principle›

lemma (in ultrametric_space) ultrametric_isosceles_triangle_principle : 
  ‹dist x z = max (dist x y) (dist y z)› if ‹dist x y ≠ dist y z›
proof (rule order_antisym)
  show ‹dist x z ≤ max (dist x y) (dist y z)›
    by (fact ultrametric_dist_triangle)
next
  from ‹dist x y ≠ dist y z› linorder_less_linear
  have ‹dist x y < dist y z ∨ dist y z < dist x y› by blast
  with ultrametric_dist_triangle[of y z x]
    ultrametric_dist_triangle[of x y z]
  show ‹max (dist x y) (dist y z) ≤ dist x z›
    by (elim disjE) (simp_all add: dist_commute)
qed



subsection ‹Distance to a convergent Sequence›

lemma ultrametric_dist_to_convergent_sequence_is_eventually_const :
  fixes σ :: ‹nat ⇒ 'a :: ultrametric_space›
  assumes ‹σ ⇢ Σ› and ‹x ≠ Σ›
  shows ‹∃N. ∀n≥N. dist (σ n) x = dist Σ x›
proof -
  from ‹x ≠ Σ› have ‹0 < dist x Σ› by simp
  then obtain ε where ‹0 < ε› ‹ball x ε ∩ ball Σ ε = {}›
    by (metis centre_in_ball disjoint_iff mem_ball order_less_le
        ultrametric_every_point_of_ball_is_centre)

  from ‹σ ⇢ Σ› ‹0 < ε› obtain N where ‹N ≤ n ⟹ σ n ∈ ball Σ ε› for n
    by (auto simp add: dist_commute lim_sequentially)
  with ‹0 < ε› ‹ball x ε ∩ ball Σ ε = {}› have ‹N ≤ n ⟹ dist (σ n) x = dist Σ x› for n
    by (metis centre_in_ball dist_commute ultrametric_equal_distance_between_ball_ball)
  thus ‹∃N. ∀n≥N. dist (σ n) x = dist Σ x› by blast
qed



subsection ‹Diameter›

lemma ultrametric_diameter : ‹diameter S = (SUP y ∈ S. dist x y)›
  if ‹bounded S› and ‹x ∈ S› for x :: ‹'a :: ultrametric_space›
proof -
  from ‹x ∈ S› have ‹S ≠ {}› by blast
  show ‹diameter S = (SUP y ∈ S. dist x y)›
  proof (rule order_antisym)
    from diameter_bounded_bound[OF ‹bounded S› ‹x ∈ S›]
    have ‹y ∈ S ⟹ dist x y ≤ diameter S› for y .
    thus ‹(SUP y ∈ S. dist x y) ≤ diameter S›
      by (rule cSUP_least[OF ‹S ≠ {}›])
  next
    have ‹bdd_above (dist x ` S)›
      by (meson bdd_above.I2 bounded_any_center ‹bounded S›)
    have ‹y ∈ S ⟹ z ∈ S ⟹ dist y z ≤ max (dist x y) (dist x z)› for y z
      by (metis dist_commute ultrametric_dist_triangle)
    also have ‹y ∈ S ⟹ z ∈ S ⟹
               max (dist x y) (dist x z) ≤ (SUP y ∈ S. dist x y)› for y z
      by (cases ‹dist x y ≤ dist x z›)
        (simp_all add: cSUP_upper2[OF ‹bdd_above (dist x ` S)›])
    finally have * : ‹y ∈ S ⟹ z ∈ S ⟹ dist y z ≤ (SUP y ∈ S. dist x y)› for y z .
    have ‹(SUP (y, z) ∈ S × S. dist y z) ≤ (SUP y ∈ S. dist x y)›
      by (rule cSUP_least) (use "*" in ‹auto simp add: ‹S ≠ {}››)
    thus ‹diameter S ≤ Sup (dist x ` S)›
      by (simp add: diameter_def ‹S ≠ {}›)
  qed
qed



subsection ‹Totally disconnected›

lemma ultrametric_totally_disconnected :
  ‹∃x. S = {x}› if ‹S ≠ {}› ‹connected S›
for S :: ‹'a :: ultrametric_space set›
proof -
  from ‹S ≠ {}› obtain x where ‹x ∈ S› by blast
  have ‹ball x r ∩ S = {} ∨ - ball x r ∩ S = {}› if ‹0 < r› for r
    by (rule ‹connected S›[unfolded connected_def, simplified, rule_format])
      (simp_all, use order_less_imp_le that ultrametric_closed_ball in blast)
  with ‹x ∈ S› have ‹0 < r ⟹ - ball x r ∩ S = {}› for r
    by (metis centre_in_ball disjoint_iff)
  hence ‹0 < r ⟹ y ∈ S ⟹ dist x y < r› for r y
    by (auto simp add: disjoint_iff)
  hence ‹y ∈ S ⟹ dist x y = 0› for y
    by (metis dist_self order_less_irrefl zero_less_dist_iff)
  hence ‹y ∈ S ⟹ y = x› for y by simp
  with ‹x ∈ S› show ‹∃x. S = {x}› by blast
qed



(*<*)
end
  (*>*)